Теории первого порядка — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
м
м (rollbackEdits.php mass rollback)
 
(не показано 14 промежуточных версий 6 участников)
Строка 24: Строка 24:
 
# <tex> a + 0 = a </tex>
 
# <tex> a + 0 = a </tex>
 
# <tex> a + b' = (a + b)'</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>.
 +
 +
}}
 +
 +
=== Коммутативность сложения ===
  
 
{{Лемма
 
{{Лемма
Строка 35: Строка 49:
 
Переход. Пусть <tex> a + 0 = 0 + a</tex>. Докажем, что <tex> a' + 0 = 0 + a' </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>.
 
По первому свойству <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>.
 
}}
 
}}
  
Строка 40: Строка 66:
 
|about = коммутативность сложения
 
|about = коммутативность сложения
 
|statement = Так определенное сложение коммутативно.
 
|statement = Так определенное сложение коммутативно.
|proof = Упражнение {{TODO | t = ща будет}}
+
|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>.
 
}}
 
}}
 +
 +
== Больше формальности! ==
  
 
Но данная аксиоматика сформулирована неформально, поэтому мы не сможем доказать никаких содержательных утверждений про нее, пользуясь формальными средствами. Поэтому нам нужно эту конструкцию как-то объединить с исчислением предикатов, чем мы сейчас и займемся.
 
Но данная аксиоматика сформулирована неформально, поэтому мы не сможем доказать никаких содержательных утверждений про нее, пользуясь формальными средствами. Поэтому нам нужно эту конструкцию как-то объединить с исчислением предикатов, чем мы сейчас и займемся.
Строка 51: Строка 86:
 
* Маленькими латинскими буквами a,b,... (возможно, с индексами) будем обозначать индивидные переменные.
 
* Маленькими латинскими буквами a,b,... (возможно, с индексами) будем обозначать индивидные переменные.
 
* К логическим связкам добавляются такие: (<tex>=</tex>) &mdash; двуместный предикат, (<tex>+</tex>) и (<tex>\cdot</tex>) &mdash; двуместные функции, и (<tex>'</tex>) &mdash; одноместная функция. Все левоассоциативное, приоритеты в порядке убывания: (<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>)
 
* К логическим связкам добавляются такие: (<tex>=</tex>) &mdash; двуместный предикат, (<tex>+</tex>) и (<tex>\cdot</tex>) &mdash; двуместные функции, и (<tex>'</tex>) &mdash; одноместная функция. Все левоассоциативное, приоритеты в порядке убывания: (<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>.
+
* Вводится 0-местный предикат <tex>0</tex>. (иногда бывает удобно сделать его 1-местным или даже <tex>n</tex>-местным)
  
  
Строка 58: Строка 93:
 
К стандартным аксиомам исчисления предикатов добавим следующие 8 ''нелогических'' аксиом и одну нелогическую схему аксиом.
 
К стандартным аксиомам исчисления предикатов добавим следующие 8 ''нелогических'' аксиом и одну нелогическую схему аксиом.
  
<table>
+
<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>
  
<tr class="odd">
+
В схеме аксиом (A9) <tex>\psi</tex> &ndash; некоторая формула исчисления предикатов и <tex>x</tex> &mdash; некоторая переменная, входящая свободно в <tex>\psi</tex>.
<td align="left">(A1)</td>
 
<td align="left"><tex>a = b \rightarrow a' = b'</tex></td>
 
</tr>
 
<tr class="even">
 
<td align="left">(A2)</td>
 
<td align="left"><tex>a = b \rightarrow a = c \rightarrow b = c</tex></td>
 
</tr>
 
<tr class="odd">
 
<td align="left">(A3)</td>
 
<td align="left"><tex>a' = b' \rightarrow a = b</tex></td>
 
</tr>
 
<tr class="even">
 
<td align="left">(A4)</td>
 
<td align="left"><tex>\neg a' = 0</tex></td>
 
</tr>
 
<tr class="odd">
 
<td align="left">(A5)</td>
 
<td align="left"><tex>a + b' = (a+b)'</tex></td>
 
</tr>
 
<tr class="even">
 
<td align="left">(A6)</td>
 
<td align="left"><tex>a + 0 = a</tex></td>
 
</tr>
 
<tr class="odd">
 
<td align="left">(A7)</td>
 
<td align="left"><tex>a \cdot 0 = a</tex></td>
 
</tr>
 
<tr class="even">
 
<td align="left">(A8)</td>
 
<td align="left"><tex>a \cdot b' = a \cdot b + a</tex></td>
 
</tr>
 
<tr class="odd">
 
<td align="left">(A9)</td>
 
<td align="left"><tex>(\psi [x := 0]) \& \forall{x}((\psi) \rightarrow (\psi) [x := x']) \rightarrow (\psi)</tex></td>
 
</tr>
 
  
</table>
+
A1, A2 {{---}} про предикат равенства. A5, A6 {{---}} про сложение. A7, A8 {{---}} про умножение. A9 {{---}} схема аксиом индукции.
  
В схеме аксиом (A9) <tex>\psi</tex> &ndash; некоторая формула исчисления предикатов и <tex>x</tex> &mdash; некоторая переменная, входящая свободно в <tex>\psi</tex>.
 
  
 
{{Теорема
 
{{Теорема
|statement=  
+
|statement =
 
<tex>\vdash a = a </tex>
 
<tex>\vdash a = a </tex>
|proof=
+
|proof =
Упражнение. Клини, стр. 254.
+
Взято из: Клини, "Введение в метаматематику", Гл. <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>
 +
 
 
}}
 
}}
  

Текущая версия на 19:15, 4 сентября 2022

<< >>

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

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

Рассмотрим некоторое множество [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]
Утверждение ("существование результата сложения"):
[math]\forall a, b \in N \exists x : x = a + b, x \in N[/math]
[math]\triangleright[/math]

По индукции.

База. [math]b = 0[/math], [math]a + 0 = a[/math] (по свойству 1).

Переход. Пусть [math]a + b = c \in N [/math]. Тогда [math]a + b' = [/math] (по свойству 2) [math] = (a + b)' = c' \in N [/math] по свойству операции [math](')[/math].
[math]\triangleleft[/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]
Лемма (2):
[math] b + a' = b' + a[/math]
Доказательство:
[math]\triangleright[/math]

Индукция по [math] a [/math]:

База. [math] b + 0' = (b + 0)' [/math], [math]b' = b' + 0[/math]

Переход. Пусть [math] b' + a = b + a'[/math]. Докажем, что [math] b' + a' = b + a'' [/math].

[math] b' + a' = (b' + a)' = (b + a')' = b + a'' [/math].
[math]\triangleleft[/math]
Теорема (коммутативность сложения):
Так определенное сложение коммутативно.
Доказательство:
[math]\triangleright[/math]

Доказательство по индукции:

База. [math] a + 0 = 0 + a[/math] по лемме 1.

Переход. Пусть [math] a + b = b + a[/math]. Докажем, что [math] a + b' = b' + a [/math].

[math] a + b' = (a + b)' = (b + a)' = b + a' = [/math] (по лемме 2) [math] = b' + a[/math].
[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 нелогических аксиом и одну нелогическую схему аксиом.

[math] \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} [/math]

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

A1, A2 — про предикат равенства. A5, A6 — про сложение. A7, A8 — про умножение. A9 — схема аксиом индукции.


Теорема:
[math]\vdash a = a [/math]
Доказательство:
[math]\triangleright[/math]

Взято из: Клини, "Введение в метаматематику", Гл. [math]19[/math], пример [math] 1 [/math] (стр. [math] 78 [/math])

[math](Ai)[/math] — аксиома арифметики, [math](i)[/math] — аксиома ИВ или ИП, [math](MP)[/math] — Modus Ponens, [math] (\forall){,}(\exists) [/math] — правила вывода для кванторов

[math] (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) \\ [/math]
[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]