Здравствуйте, thesz, Вы писали: MC>>Ты сечас про конструктивную логику? T>Их много. Ты про какую?
Не суть. Просто убеждаюсь, что под "логикой " ты имеешь в виду некоторую систему, в которой можно формулировать утверждения и приводить их конструктивные доказательства в виде программ.
T>Bottom — это и не завершимость тоже. Циклический вызов функциями друг друга в бесконечном цикле — тоже bottom. А порождения throw some_value не даёт.
Изначально мы говорили о противоречии. А незавершающиеся вычисления противоречием не являются. Противоречие — это когда мы доказали что-то чего доказать не должны были.