1632
правки
Изменения
м
rollbackEdits.php mass rollback
[[Лекция 5 | <<]][[Лекция 7 | >>]]
[[Категория: Математическая логика]]
= Теории первого порядка =
Мы занимались до этого момента только логическими рассуждениями самими по себе. Это интересно, но не очень практически полезно: мы все-таки используем логические рассуждения для доказательства утверждений о каких-то объектах. Было бы разумно каким-то образом включить эти объекты в рамки формальной теории.
Рассмотрим некоторое множество <tex>N</tex>. Будем говорить, что оно удовлетворяет аксиомам Пеано, если выполнено следующее:
* В нем существует некоторый выделенный элемент 0.
* Для каждого элемента множества определена операция <tex>'</tex>.
Кроме того, эти элемент и операция должны удовлетворять следующим требованиям:
* Не существует такого <tex>x</tex>, что <tex>x'=0</tex>.
* Если <tex>x'=y'</tex>, то <tex>x=y</tex>.
* Если некоторое предположение верно для <tex>0</tex>, и если из допущения его для <tex>n</tex> можно вывести его истинность для <tex>n+1</tex>, то предположение верно для любого элемента множества.
Данная аксиоматика позволяет определить натуральные числа (множество натуральных чисел — это множество, удовлетворяющее аксиомам Пеано; заметим, что тут натуральные числа содержат 0, так оказывается удобнее) и операции над ними. Например, сложение можно задать следующими уравнениями (будем называть их свойствами сложения):
=== Свойства сложения ===
# <tex> a + 0 = a </tex>
# <tex> a + b' = (a + b)'</tex>
{{Утверждение
|about = "существование результата сложения"
|statement =<tex>\forall a, b \in N \exists x : x = a + b, x \in N</tex>
|proof =
По индукции.
База. <tex>b = 0</tex>, <tex>a + 0 = a</tex> (по свойству 1).
Переход. Пусть <tex>a + b = c \in N </tex>. Тогда <tex>a + b' = </tex> (по свойству 2) <tex> = (a + b)' = c' \in N </tex> по свойству операции <tex>(')</tex>.
}}
=== Коммутативность сложения ===
{{Лемма
|about = 1
|statement = <tex> a + 0 = 0 + a</tex>
|proof =
Доказательство по индукции:
База. <tex> 0 + 0 = 0 + 0</tex>.
Переход. Пусть <tex> a + 0 = 0 + a</tex>. Докажем, что <tex> a' + 0 = 0 + a' </tex>.
По первому свойству <tex> a' + 0 = a' </tex>. Тогда <tex> a' = (a + 0)' = (0 + a)' = 0 + a'</tex>.
}}
{{Лемма
|about = 2
|statement = <tex> b + a' = b' + a</tex>
|proof =
Индукция по <tex> a </tex>:
База. <tex> b + 0' = (b + 0)' </tex>, <tex>b' = b' + 0</tex>
Переход. Пусть <tex> b' + a = b + a'</tex>. Докажем, что <tex> b' + a' = b + a'' </tex>.
<tex> b' + a' = (b' + a)' = (b + a')' = b + a'' </tex>.
}}
{{Теорема
|about = коммутативность сложения
|statement = Так определенное сложение коммутативно.
|proof =
Доказательство по индукции:
База. <tex> a + 0 = 0 + a</tex> по лемме 1.
Переход. Пусть <tex> a + b = b + a</tex>. Докажем, что <tex> a + b' = b' + a </tex>.
<tex> a + b' = (a + b)' = (b + a)' = b + a' = </tex> (по лемме 2) <tex> = b' + a</tex>.
}}
== Больше формальности! ==
Но данная аксиоматика сформулирована неформально, поэтому мы не сможем доказать никаких содержательных утверждений про нее, пользуясь формальными средствами. Поэтому нам нужно эту конструкцию как-то объединить с исчислением предикатов, чем мы сейчас и займемся.
Рассмотрим следующее исчисление. Мы уже не будем приводить грамматику, ожидая, что это является простым упражнением, приведем только общее описание.
Возьмем язык исчисления предикатов со следующими изменениями и особенностями:
* Маленькими латинскими буквами a,b,... (возможно, с индексами) будем обозначать индивидные переменные.
* К логическим связкам добавляются такие: (<tex>=</tex>) — двуместный предикат, (<tex>+</tex>) и (<tex>\cdot</tex>) — двуместные функции, и (<tex>'</tex>) — одноместная функция. Все левоассоциативное, приоритеты в порядке убывания: (<tex>'</tex>), потом (<tex>\cdot</tex>), потом (<tex>+</tex>). Все логические связки имеют приоритет ниже. (Например, <tex>a= b'+b'+c \cdot c \& b = c</tex> надо интерпретировать как <tex>(a = (((b') + (b')) + (c \cdot c))) \& (b = c)</tex>)
* Вводится 0-местный предикат <tex>0</tex>. (иногда бывает удобно сделать его 1-местным или даже <tex>n</tex>-местным)
Ранее мы для простоты не рассматривали функции в исчислении предикатов, но здесь без них уже не обойтись. Функции, в отличие от предикатов, имеют своей областью значений предметное множество, то есть в качестве аргумента предикатов в таком исчислении можно писать не только переменные, но и произвольные выражения из переменных и применения функций. Функции нетрудно формализовать, добавив дополнительные правила к грамматике и расширив логические схемы аксиом (11) и (12), разрешив в них заменять индивидную переменную не только на другую переменную, но и на произвольное выражение из функций и переменных.
К стандартным аксиомам исчисления предикатов добавим следующие 8 ''нелогических'' аксиом и одну нелогическую схему аксиом.
<tex>
\begin{cases}
(A1) & a = b \rightarrow a' = b' \\
(A2) & a = b \rightarrow a = c \rightarrow b = c \\
(A3) & a' = b' \rightarrow a = b \\
(A4) & \neg a' = 0 \\
(A5) & a + b' = (a+b)' \\
(A6) & a + 0 = a \\
(A7) & a \cdot 0 = 0 \\
(A8) & a \cdot b' = a \cdot b + a \\
(A9) & (\psi [x := 0]) \& \forall{x}((\psi) \rightarrow (\psi) [x := x']) \rightarrow (\psi)\\
\end{cases}
</tex>
В схеме аксиом (A9) <tex>\psi</tex> – некоторая формула исчисления предикатов и <tex>x</tex> — некоторая переменная, входящая свободно в <tex>\psi</tex>.
A1, A2 {{---}} про предикат равенства. A5, A6 {{---}} про сложение. A7, A8 {{---}} про умножение. A9 {{---}} схема аксиом индукции.
{{Теорема
|statement =
<tex>\vdash a = a </tex>
|proof =
Взято из: Клини, "Введение в метаматематику", Гл. <tex>19</tex>, пример <tex> 1 </tex> (стр. <tex> 78 </tex>)
<tex>(Ai)</tex> {{---}} аксиома арифметики, <tex>(i)</tex> {{---}} аксиома ИВ или ИП, <tex>(MP)</tex> {{---}} Modus Ponens, <tex> (\forall){,}(\exists) </tex> {{---}} правила вывода для кванторов
<tex>
(1)~ a = b \to a = c \to b = c ~(A2) \\
(2)~ 0 = 0 \to (0 = 0 \to 0 = 0) ~(1) \\
(3)~ (a = b \to a = c \to b = c) \to ((0 = 0 \to (0 = 0 \to 0 = 0))\to (a = b \to a = c \to b = c)) ~(1) \\
(4)~ (0 = 0 \to (0 = 0 \to 0 = 0)) \to (a = b \to a = c \to b = c) ~(MP~ 1{,}3) \\
(5)~ (0 = 0 \to (0 = 0 \to 0 = 0)) \to \forall c(a = b \to a = c \to b = c) ~(\forall) \\
(6)~ (0 = 0 \to (0 = 0 \to 0 = 0)) \to \forall b\forall c(a = b \to a = c \to b = c) ~(\forall) \\
(7)~ (0 = 0 \to (0 = 0 \to 0 = 0)) \to \forall a\forall b\forall c(a = b \to a = c \to b = c) ~(\forall) \\
(8)~ \forall a\forall b\forall c(a = b \to a = c \to b = c) ~(MP~ 2{,}7) \\
(9)~ \forall a\forall b\forall c(a = b \to a = c \to b = c) \to \forall b\forall c(a + 0 = b \to a + 0 = c \to b = c) ~(11) \\
(10)~ \forall b\forall c(a + 0 = b \to a + 0 = c \to b = c) ~(MP~ 8{,}9) \\
(11)~ \forall b\forall c(a + 0 = b \to a + 0 = c \to b = c) \to \forall c(a + 0 = a \to a + 0 = c \to a = c) ~(11) \\
(12)~ \forall c(a + 0 = a \to a + 0 = c \to a = c) ~(MP~ 10{,}11) \\
(13)~ \forall c(a + 0 = b \to a + 0 = c \to b = c) \to (a + 0 = a \to a + 0 = a \to a = a) ~(11) \\
(14)~ a + 0 = a \to a + 0 = a \to a = a ~(MP~ 12{,}13) \\
(15)~ a + 0 = a ~(A6) \\
(16)~ a + 0 = a \to a = a (MP~ 15{,}14) \\
(17)~ a = a (MP~ 15{,}16) \\
</tex>
}}
Комментарии:
Для большей четкости изложения у функций и предикатов при общей записи мы будем указывать дополнительный
(верхний) индекс --- количество аргументов. Таким образом, мы будем говорить о языке первого
порядка, в котором в дополнение к символам исчисления высказываний есть некоторое множество
функциональных символов <tex>f_n^k</tex> для <tex>k</tex>-местных функций, и предикатных символов <tex>P_n^k</tex> ---
для <tex>k</tex>-местных предикатов.
{{Определение
|definition=
Структурой теории первого порядка мы назовем упорядоченную тройку <tex>\langle{}D, F, P\rangle</tex>, где <tex>F = \langle{}F_0, F_1, ... \rangle</tex> --- списки оценок для 0-местных, 1-местных и т.д. функций, и <tex>P = \langle{}P_0, P_1, ... \rangle</tex> --- списки оценок для 0-местных, 1-местных и т.д. предикатов, <tex>D </tex> --- предметное множество.
(Например, функции <tex>f_n^k</tex> соответствует <tex>k</tex>-й элемент списка <tex>F</tex>)
}}
Понятие структуры — развитие понятия оценки из исчисления предикатов. Но оно касается только нелогических составляющих теории; истинностные значения и оценки для связок по-прежнему определяются исчислением предикатов, лежащим в основе теории. Для получения оценки формулы нам нужно задать структуру, значения всех свободных индивидных переменных, и (естественным образом) вычислить результат.
{{Определение
|definition= Назовем структуру корректной, если любая доказуемая формула истинна в данной структуре.
}}
{{Определение
|definition= Моделью теории мы назовем любую корректную структуру.
}}
Еще одним примером теории первого порядка может являться теория групп. К исчислению предикатов добавим двуместный предикат (<tex>=</tex>), двуместную функцию (<tex>\cdot</tex>), одноместную функцию (<tex>x^{-1}</tex>), константу (т.е. 0-местную функцию) <tex>1</tex> и следующие аксиомы:
<table>
<tr class="odd">
<td align="left">(E1)</td>
<td align="left"><tex>a = b \rightarrow (a = c \rightarrow b = c)</tex></td>
</tr>
<tr class="even">
<td align="left">(E2)</td>
<td align="left"><tex>a = b \rightarrow (a \cdot c = b \cdot c)</tex></td>
</tr>
<tr class="odd">
<td align="left">(E3)</td>
<td align="left"><tex>a = b \rightarrow (c \cdot a = c \cdot b)</tex></td>
</tr>
<tr class="even">
<td align="left">(G1)</td>
<td align="left"><tex>a \cdot (b \cdot c) = (a \cdot b) \cdot c</tex></td>
</tr>
<tr class="odd">
<td align="left">(G2)</td>
<td align="left"><tex>a \cdot 1 = a</tex></td>
</tr>
<tr class="even">
<td align="left">(G3)</td>
<td align="left"><tex>a \cdot a ^ {-1} = 1</tex></td>
</tr>
</table>
{{Теорема
|statement=
Доказуемо, что <tex>a=b \rightarrow b=a</tex> и что <tex>a^{-1} \cdot a = 1 </tex>
|proof=
Упражнение.
}}
{{Определение
|definition=
Назовем модели некоторой теории первого порядка с предметными множествами <tex>D_1</tex> и <tex>D_2</tex> изоморфными, если существует биективная функция <tex>I: D_1 \rightarrow D_2</tex>, при этом для любой функции <tex>f</tex> данной теории, имеющей оценки <tex>f_1</tex> и <tex>f_2</tex> (в первой и второй модели соответственно) и любых <tex>x_1,... x_n</tex> из <tex>D_1</tex> справедливо <tex>f_2 (I(x_1), ... I(x_n)) = I (f_1(x_1, ... x_n))</tex> и для любого предиката <tex>P</tex> (<tex>P_1</tex> и <tex>P_2</tex> определены аналогично) <tex>P_2 (I(x_1), ... I(x_n))</tex> тогда и только тогда, когда <tex>P_1(x_1, ... x_n)</tex>.
}}
{{Теорема
|statement=
Существуют неизоморфные модели для теории групп, имеющие конечные предметные множества равной мощности.
|proof=
Упражнение.
}}
