1302
правки
Изменения
→Больше формальности!: ололол
{{Теорема
|statement=
<tex>\vdash a = a </tex>
|proof=
Упражнение. Клини, стр. 254.
(Ai) - аксиома арифметики. (i) - аксиома ИВ или ИП, (MP) - Modus Ponens.
<!-- \to тоже самое, что \rightarrow -->
<tex>
(1) a = b \to a = c \to b = c ~(A2) \\
(2) 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) ~(MP)
</tex>
Применяем правила введения кванторов три раза.
<tex>
(k) (0 = 1 \to 0 = 1 \to 0 = 1) \to \forall c \forall b \forall a (a = b \to a = c \to b = c) \\
(l) \forall c \forall b \forall a (a = b \to a = c \to b = c) ~(MP)
</tex>
Применяем схему аксиом для квантора <tex>\forall</tex> и получаем требуемое.
}}
