Утверждение А неопровержимо, когда у нас есть терм-доказательство --А, т.е. док-во ложности отрицания А. Док-ва самого А у нас может не быть. Если оно есть, т.е. А одновременно истинно и неопровержимо, такое утверждение называется stable. Далеко не все увтерждения stable, например А | -A не stable. Зато все отрицательные утверждения stable: ---P == -P, ----P == --P.
Возвращаясь к посту: если бы у нас было доказательство forall A. A | -A, то это получилась бы программа, которая для любого А за конечное число шагов определяет, останавливается вычисление А или виснет (-А), выдавая из ничего конструктивное док-во или А, или -А. Т.е. это было бы решением halting problem, и даже круче - кроме ответа да или нет еще и обоснование давалось бы.
no subject
Утверждение А неопровержимо, когда у нас есть терм-доказательство --А, т.е. док-во ложности отрицания А. Док-ва самого А у нас может не быть. Если оно есть, т.е. А одновременно истинно и неопровержимо, такое утверждение называется stable. Далеко не все увтерждения stable, например А | -A не stable. Зато все отрицательные утверждения stable: ---P == -P, ----P == --P.
Возвращаясь к посту: если бы у нас было доказательство forall A. A | -A, то это получилась бы программа, которая для любого А за конечное число шагов определяет, останавливается вычисление А или виснет (-А), выдавая из ничего конструктивное док-во или А, или -А. Т.е. это было бы решением halting problem, и даже круче - кроме ответа да или нет еще и обоснование давалось бы.