Изменения
→Коммутативность сложения
Переход. Пусть <tex> b' + a = b + a'</tex>. Докажем, что <tex> b' + a' = b + a'' </tex>.
<tex> b' + a' = (b' + a)' = (b + a')' = b' + a'' </tex>.
}}
<tex>\vdash a = a </tex>
|proof =
<!tex>(Ai)</tex> {{-- \to тоже самое-}} аксиома арифметики, что \rightarrow <tex>(i)</tex> {{--->}} аксиома ИВ или ИП, <tex>(1MP) a = b \to a = c \to b = c ~</tex> {{---}} Modus Ponens, <tex> (A2) \\(2forall) 0 = 1 \to 0 = 1 \to 0 = 1 ~(1) \\(3) (a = b \to a = c \to b = c) \to (0 = 1 \to 0 = 1 \to 0 = 1) \to (a = b \to a = c \to b = c) ~(1) \\(4) (0 = 1 \to 0 = 1 \to 0 = 1) \to {,}(a = b \to a = c \to b = c) ~(MPexists)</tex> Применяем {{---}} правила введения вывода для кванторов три раза.
<tex>
(k1)~ 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) \\(l10) ~ \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>
}}
