Теории первого порядка
Содержание
Теории первого порядка
Мы занимались до этого момента только логическими рассуждениями самими по себе. Это интересно, но не очень практически полезно: мы все-таки используем логические рассуждения для доказательства утверждений о каких-то объектах. Было бы разумно каким-то образом включить эти объекты в рамки формальной теории.
Рассмотрим некоторое множество . Будем говорить, что оно удовлетворяет аксиомам Пеано, если выполнено следующее:
- В нем существует некоторый выделенный элемент 0.
- Для каждого элемента множества определена операция .
Кроме того, эти элемент и операция должны удовлетворять следующим требованиям:
- Не существует такого , что .
- Если , то .
- Если некоторое предположение верно для , и если из допущения его для можно вывести его истинность для , то предположение верно для любого элемента множества.
Данная аксиоматика позволяет определить натуральные числа (множество натуральных чисел — это множество, удовлетворяющее аксиомам Пеано; заметим, что тут натуральные числа содержат 0, так оказывается удобнее) и операции над ними. Например, сложение можно задать следующими уравнениями (будем называть их свойствами сложения):
Свойства сложения
| Утверждение ("существование результата сложения"): |
|
По индукции. База. , (по свойству 1). Переход. Пусть . Тогда (по свойству 2) по свойству операции . |
Коммутативность сложения
| Лемма (1): |
| Доказательство: |
|
Доказательство по индукции: База. . Переход. Пусть . Докажем, что . По первому свойству . Тогда . |
| Лемма (2): |
| Доказательство: |
|
Индукция по : База. , Переход. Пусть . Докажем, что . . |
| Теорема (коммутативность сложения): |
Так определенное сложение коммутативно. |
| Доказательство: |
|
Доказательство по индукции: База. по лемме 1. Переход. Пусть . Докажем, что . (по лемме 2) . |
Больше формальности!
Но данная аксиоматика сформулирована неформально, поэтому мы не сможем доказать никаких содержательных утверждений про нее, пользуясь формальными средствами. Поэтому нам нужно эту конструкцию как-то объединить с исчислением предикатов, чем мы сейчас и займемся.
Рассмотрим следующее исчисление. Мы уже не будем приводить грамматику, ожидая, что это является простым упражнением, приведем только общее описание.
Возьмем язык исчисления предикатов со следующими изменениями и особенностями:
- Маленькими латинскими буквами a,b,... (возможно, с индексами) будем обозначать индивидные переменные.
- К логическим связкам добавляются такие: () — двуместный предикат, () и () — двуместные функции, и () — одноместная функция. Все левоассоциативное, приоритеты в порядке убывания: (), потом (), потом (). Все логические связки имеют приоритет ниже. (Например, надо интерпретировать как )
- Вводится 0-местный предикат . (иногда бывает удобно сделать его 1-местным или даже -местным)
Ранее мы для простоты не рассматривали функции в исчислении предикатов, но здесь без них уже не обойтись. Функции, в отличие от предикатов, имеют своей областью значений предметное множество, то есть в качестве аргумента предикатов в таком исчислении можно писать не только переменные, но и произвольные выражения из переменных и применения функций. Функции нетрудно формализовать, добавив дополнительные правила к грамматике и расширив логические схемы аксиом (11) и (12), разрешив в них заменять индивидную переменную не только на другую переменную, но и на произвольное выражение из функций и переменных.
К стандартным аксиомам исчисления предикатов добавим следующие 8 нелогических аксиом и одну нелогическую схему аксиом.
В схеме аксиом (A9) – некоторая формула исчисления предикатов и — некоторая переменная, входящая свободно в .
A1, A2 — про предикат равенства. A5, A6 — про сложение. A7, A8 — про умножение. A9 — схема аксиом индукции.
| Теорема: |
| Доказательство: |
|
Взято из: Клини, "Введение в метаматематику", Гл. , пример (стр. ) — аксиома арифметики, — аксиома ИВ или ИП, — Modus Ponens, — правила вывода для кванторов |
Комментарии:
Для большей четкости изложения у функций и предикатов при общей записи мы будем указывать дополнительный (верхний) индекс --- количество аргументов. Таким образом, мы будем говорить о языке первого порядка, в котором в дополнение к символам исчисления высказываний есть некоторое множество функциональных символов для -местных функций, и предикатных символов --- для -местных предикатов.
| Определение: |
| Структурой теории первого порядка мы назовем упорядоченную тройку , где --- списки оценок для 0-местных, 1-местных и т.д. функций, и --- списки оценок для 0-местных, 1-местных и т.д. предикатов, --- предметное множество. (Например, функции соответствует -й элемент списка ) |
Понятие структуры — развитие понятия оценки из исчисления предикатов. Но оно касается только нелогических составляющих теории; истинностные значения и оценки для связок по-прежнему определяются исчислением предикатов, лежащим в основе теории. Для получения оценки формулы нам нужно задать структуру, значения всех свободных индивидных переменных, и (естественным образом) вычислить результат.
| Определение: |
| Назовем структуру корректной, если любая доказуемая формула истинна в данной структуре. |
| Определение: |
| Моделью теории мы назовем любую корректную структуру. |
Еще одним примером теории первого порядка может являться теория групп. К исчислению предикатов добавим двуместный предикат (), двуместную функцию (), одноместную функцию (), константу (т.е. 0-местную функцию) и следующие аксиомы:
| (E1) | |
| (E2) | |
| (E3) | |
| (G1) | |
| (G2) | |
| (G3) |
| Теорема: |
Доказуемо, что и что |
| Доказательство: |
| Упражнение. |
| Определение: |
| Назовем модели некоторой теории первого порядка с предметными множествами и изоморфными, если существует биективная функция , при этом для любой функции данной теории, имеющей оценки и (в первой и второй модели соответственно) и любых из справедливо и для любого предиката ( и определены аналогично) тогда и только тогда, когда . |
| Теорема: |
Существуют неизоморфные модели для теории групп, имеющие конечные предметные множества равной мощности. |
| Доказательство: |
| Упражнение. |
