Теории первого порядка

<< >>

Теории первого порядка

Мы занимались до этого момента только логическими рассуждениями самими по себе. Это интересно, но не очень практически полезно: мы все-таки используем логические рассуждения для доказательства утверждений о каких-то объектах. Было бы разумно каким-то образом включить эти объекты в рамки формальной теории.

Рассмотрим некоторое множество [math]N[/math]. Будем говорить, что оно удовлетворяет аксиомам Пеано, если выполнено следующее:

• В нем существует некоторый выделенный элемент 0.
• Для каждого элемента множества определена операция [math]'[/math].

Кроме того, эти элемент и операция должны удовлетворять следующим требованиям:

• Не существует такого [math]x[/math], что [math]x'=0[/math].
• Если [math]x'=y'[/math], то [math]x=y[/math].
• Если некоторое предположение верно для [math]0[/math], и если из допущения его для [math]n[/math] можно вывести его истинность для [math]n+1[/math], то предположение верно для любого элемента множества.

Данная аксиоматика позволяет определить натуральные числа (множество натуральных чисел — это множество, удовлетворяющее аксиомам Пеано; заметим, что тут натуральные числа содержат 0, так оказывается удобнее) и операции над ними. Например, сложение можно задать следующими уравнениями (будем называть их свойствами сложения):

Свойства сложения

1. [math] a + 0 = a [/math]
2. [math] a + b' = (a + b)'[/math]

Коммутативность сложения

Лемма (1):

[math] a + 0 = 0 + a[/math]

Доказательство:

[math]\triangleright[/math]

Доказательство по индукции: База. [math] 0 + 0 = 0 + 0[/math]. Переход. Пусть [math] a + 0 = 0 + a[/math]. Докажем, что [math] a' + 0 = 0 + a' [/math]. По первому свойству [math] a' + 0 = a' [/math]. Тогда [math] a' = (a + 0)' = (0 + a)' = 0 + a'[/math].

[math]\triangleleft[/math]

Теорема (коммутативность сложения):

Так определенное сложение коммутативно.

Доказательство:

[math]\triangleright[/math]

Упражнение TODO: ща будет

[math]\triangleleft[/math]

Больше формальности!

Но данная аксиоматика сформулирована неформально, поэтому мы не сможем доказать никаких содержательных утверждений про нее, пользуясь формальными средствами. Поэтому нам нужно эту конструкцию как-то объединить с исчислением предикатов, чем мы сейчас и займемся.

Рассмотрим следующее исчисление. Мы уже не будем приводить грамматику, ожидая, что это является простым упражнением, приведем только общее описание.

Возьмем язык исчисления предикатов со следующими изменениями и особенностями:

• Маленькими латинскими буквами a,b,... (возможно, с индексами) будем обозначать индивидные переменные.
• К логическим связкам добавляются такие: ([math]=[/math]) — двуместный предикат, ([math]+[/math]) и ([math]\cdot[/math]) — двуместные функции, и ([math]'[/math]) — одноместная функция. Все левоассоциативное, приоритеты в порядке убывания: ([math]'[/math]), потом ([math]\cdot[/math]), потом ([math]+[/math]). Все логические связки имеют приоритет ниже. (Например, [math]a= b'+b'+c \cdot c \& b = c[/math] надо интерпретировать как [math](a = (((b') + (b')) + (c \cdot c))) \& (b = c)[/math])
• Вводится 0-местный предикат [math]0[/math]. (иногда бывает удобно сделать его 1-местным или даже [math]n[/math]-местным)

Ранее мы для простоты не рассматривали функции в исчислении предикатов, но здесь без них уже не обойтись. Функции, в отличие от предикатов, имеют своей областью значений предметное множество, то есть в качестве аргумента предикатов в таком исчислении можно писать не только переменные, но и произвольные выражения из переменных и применения функций. Функции нетрудно формализовать, добавив дополнительные правила к грамматике и расширив логические схемы аксиом (11) и (12), разрешив в них заменять индивидную переменную не только на другую переменную, но и на произвольное выражение из функций и переменных.

К стандартным аксиомам исчисления предикатов добавим следующие 8 нелогических аксиом и одну нелогическую схему аксиом.

(A1)	[math]a = b \rightarrow a' = b'[/math]
(A2)	[math]a = b \rightarrow a = c \rightarrow b = c[/math]
(A3)	[math]a' = b' \rightarrow a = b[/math]
(A4)	[math]\neg a' = 0[/math]
(A5)	[math]a + b' = (a+b)'[/math]
(A6)	[math]a + 0 = a[/math]
(A7)	[math]a \cdot 0 = a[/math]
(A8)	[math]a \cdot b' = a \cdot b + a[/math]
(A9)	[math](\psi [x := 0]) \& \forall{x}((\psi) \rightarrow (\psi) [x := x']) \rightarrow (\psi)[/math]

В схеме аксиом (A9) [math]\psi[/math] – некоторая формула исчисления предикатов и [math]x[/math] — некоторая переменная, входящая свободно в [math]\psi[/math].

Теорема:

[math]\vdash a = a [/math]

Доказательство:

[math]\triangleright[/math]

Упражнение. Клини, стр. 254.

[math]\triangleleft[/math]

Комментарии:

Для большей четкости изложения у функций и предикатов при общей записи мы будем указывать дополнительный (верхний) индекс --- количество аргументов. Таким образом, мы будем говорить о языке первого порядка, в котором в дополнение к символам исчисления высказываний есть некоторое множество функциональных символов [math]f_n^k[/math] для [math]k[/math]-местных функций, и предикатных символов [math]P_n^k[/math] --- для [math]k[/math]-местных предикатов.

Определение:

Структурой теории первого порядка мы назовем упорядоченную тройку [math]\langle{}D, F, P\rangle[/math], где [math]F = \langle{}F_0, F_1, ... \rangle[/math] --- списки оценок для 0-местных, 1-местных и т.д. функций, и [math]P = \langle{}P_0, P_1, ... \rangle[/math] --- списки оценок для 0-местных, 1-местных и т.д. предикатов, [math]D [/math] --- предметное множество. (Например, функции [math]f_n^k[/math] соответствует [math]k[/math]-й элемент списка [math]F[/math])

Понятие структуры — развитие понятия оценки из исчисления предикатов. Но оно касается только нелогических составляющих теории; истинностные значения и оценки для связок по-прежнему определяются исчислением предикатов, лежащим в основе теории. Для получения оценки формулы нам нужно задать структуру, значения всех свободных индивидных переменных, и (естественным образом) вычислить результат.

Определение:

Назовем структуру корректной, если любая доказуемая формула истинна в данной структуре.

Определение:

Моделью теории мы назовем любую корректную структуру.

Еще одним примером теории первого порядка может являться теория групп. К исчислению предикатов добавим двуместный предикат ([math]=[/math]), двуместную функцию ([math]\cdot[/math]), одноместную функцию ([math]x^{-1}[/math]), константу (т.е. 0-местную функцию) [math]1[/math] и следующие аксиомы:

(E1)	[math]a = b \rightarrow (a = c \rightarrow b = c)[/math]
(E2)	[math]a = b \rightarrow (a \cdot c = b \cdot c)[/math]
(E3)	[math]a = b \rightarrow (c \cdot a = c \cdot b)[/math]
(G1)	[math]a \cdot (b \cdot c) = (a \cdot b) \cdot c[/math]
(G2)	[math]a \cdot 1 = a[/math]
(G3)	[math]a \cdot a ^ {-1} = 1[/math]

Теорема:

Доказуемо, что [math]a=b \rightarrow b=a[/math] и что [math]a^{-1} \cdot a = 1 [/math]

Доказательство:

[math]\triangleright[/math]

Упражнение.

[math]\triangleleft[/math]

Определение:

Назовем модели некоторой теории первого порядка с предметными множествами [math]D_1[/math] и [math]D_2[/math] изоморфными, если существует биективная функция [math]I: D_1 \rightarrow D_2[/math], при этом для любой функции [math]f[/math] данной теории, имеющей оценки [math]f_1[/math] и [math]f_2[/math] (в первой и второй модели соответственно) и любых [math]x_1,... x_n[/math] из [math]D_1[/math] справедливо [math]f_2 (I(x_1), ... I(x_n)) = I (f_1(x_1, ... x_n))[/math] и для любого предиката [math]P[/math] ([math]P_1[/math] и [math]P_2[/math] определены аналогично) [math]P_2 (I(x_1), ... I(x_n))[/math] тогда и только тогда, когда [math]P_1(x_1, ... x_n)[/math].

Теорема:

Существуют неизоморфные модели для теории групп, имеющие конечные предметные множества равной мощности.

Доказательство:

[math]\triangleright[/math]

Упражнение.

[math]\triangleleft[/math]