Во, прекрасно (за исключением того, что логические аксиомы тоже входят в теорию, а приведённое — лишь её
собственные аксиомы; ладно, примем классическую логику). Теперь, во-первых, заметим, что раз у нас теория первого порядка, 2 — это не одна аксиома, а
схема аксиом — по одной аксиоме для всех возможных формул
(вообще там ещё должно быть написано, что
в этой формуле не свободна). В том числе аксиомой этой схемы будет
. Теперь, пользуясь аксиомой 1, можно показать [тут пропущен формальный вывод], что
(не только существует, но и единственно). Теперь можно ввести новую константу*
и определение
И мы сразу же имеем
, что получается по правилу
, где
— любой терм и
— подстановка
вместо всех свободных вхождений
в
.
Итак, у нас на руках
, и как отсюда выводятся одновременно и
, и
, я уж писать не буду (с законом исключенного третьего это раз плюнуть, а если взять интуиционистскую логику, я не в курсе). Тогда они оба выводятся из
, так что аналогичные формулы без
** выводятся в нерасширенной этим определением теории без каких-либо гипотез. Теория противоречива.
* Можно, конечно, оставаться в нерасширенной теории без
, но это уж без меня.
** Например, перевод формулы
:
. Правила перевода всегда есть там, где вводится расширение теории определением.
*** Надеюсь, комментарии не нужны и все умолчания покрываются предложенной литературой. (А что таить, там много где и предыдущее должно быть, и даже в большей строгости).
-- Пн июл 11, 2016 21:43:14 --Надеюсь, комментарии не нужны
Ибо перехожу в read-only.