В

-исчислении существует стандартный способ доказательства противоречия, через вторую теорему о неподвижной точке:

, так же верно

, где

означает геделев номер терма

.
Я попробовал его применить здесь.
Пусть А - множество термов с бесконечным графом. Допустим существует алгоритм определения, тогда существует и вычислимая характерестическая функция разрешающее множество геделевых номеров термов с бесконечным графом. Она определена в

-исчислении термом F. Получаем:

Положим теперь

, то

, иначе

, где

Тогда

Тут возникает проблема, что с помошью этой конструкции можно доказать противоречие для данной задачи только в случае

, где мы показываем, что

, чего не может быть, потому что в результате

-редукции у терма не мог возникнуть бесконечный граф.
В противоположном случае для

противоречия не получается, потому что в результате теоремы мы только знаем, что

можно редуцировать до терма с конечным графом, а это вполне нормально.
Можно ли тут что-то придумать или это доказывается вообще другим образом?
https://math.stackexchange.com/question ... dr-d-theta