Во, прекрасно (за исключением того, что логические аксиомы тоже входят в теорию, а приведённое — лишь её
собственные аксиомы; ладно, примем классическую логику). Теперь, во-первых, заметим, что раз у нас теория первого порядка, 2 — это не одна аксиома, а
схема аксиом — по одной аксиоме для всех возможных формул

(вообще там ещё должно быть написано, что

в этой формуле не свободна). В том числе аксиомой этой схемы будет

. Теперь, пользуясь аксиомой 1, можно показать [тут пропущен формальный вывод], что

(не только существует, но и единственно). Теперь можно ввести новую константу*

и определение

И мы сразу же имеем

, что получается по правилу
![$\forall x\varphi\vdash\varphi[t/x]$ $\forall x\varphi\vdash\varphi[t/x]$](https://dxdy-03.korotkov.co.uk/f/2/e/7/2e76d4c4039bd5b421947e05acf9582a82.png)
, где

— любой терм и
![$\varphi[t/x]$ $\varphi[t/x]$](https://dxdy-02.korotkov.co.uk/f/5/d/4/5d41da9c65fbcc0c731fc1c54713358482.png)
— подстановка

вместо всех свободных вхождений

в

.
Итак, у нас на руках

, и как отсюда выводятся одновременно и

, и

, я уж писать не буду (с законом исключенного третьего это раз плюнуть, а если взять интуиционистскую логику, я не в курсе). Тогда они оба выводятся из

, так что аналогичные формулы без

** выводятся в нерасширенной этим определением теории без каких-либо гипотез. Теория противоречива.
* Можно, конечно, оставаться в нерасширенной теории без

, но это уж без меня.
** Например, перевод формулы

:

. Правила перевода всегда есть там, где вводится расширение теории определением.
*** Надеюсь, комментарии не нужны и все умолчания покрываются предложенной литературой. (А что таить, там много где и предыдущее должно быть, и даже в большей строгости).
-- Пн июл 11, 2016 21:43:14 --Надеюсь, комментарии не нужны
Ибо перехожу в read-only.