Изменения
→Больше формальности!
[[Лекция 5 | <<]][[Лекция 7 | >>]]
[[Категория: Математическая логика]]
= Теории первого порядка =
* Если некоторое предположение верно для <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>ab +0 ' = a(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>-местным)
К стандартным аксиомам исчисления предикатов добавим следующие 8 ''нелогических'' аксиом и одну нелогическую схему аксиом.
<tabletex>\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>
{{Теорема
|statement=
<tex>\vdash a = a </tex>
|proof=УпражнениеВзято из: Клини, "Введение в метаматематику", Гл. Клини<tex>19</tex>, пример <tex> 1 </tex> (стр. 254.<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>
}}
