В теории алгоритмов есть теорема гласящая что не существует алгоритма опредляющего для любой пары (alg, state), где alg — запись некоторого алгоритма, state — его входные параметры, завершится ли выполнение alg или нет.

Доказательство теоремы ароводят от противного. Полагают что такой алгоритм A существует и подают ему на вход другой алгоритм B. При этом B конструируют с использованием A.

Можно ли провести это доказательство не передавая некоему алгоритму на вход самого себя?

Или в более общей постоновке. Можно ли доказать эту теорему в Конструктивистской логике?