Здравствуйте, ·, Вы писали:

KV>>Если isFermaTheoremCorrect частично рекурсивна -- это не "несколько сложнее", а невозможно доказать в принципе.
·>Доказать возможно (и теорема Ферма была доказана!)

Я вообще не про доказательство теоремы, это не имеет никакого значения Моё замечание про доказательство того, по какой именно ветке пойдёт предложенный тобой алгоритм с if'ом, т.е. того, реализует ли данный алгоритм первоначальную функцию. Это теорема Райса в чистом виде.

·>Алгебра используется для построения доказательства функции.

В результате которого мы получаем уже другую (эквивалентную исходной) функцию. В данном конкретном примере принципиальной разницы между "эквивалентна" и "является" нет, если допустить, что x принадлежит счётному множеству, на котором всюду определены используемые в функции арифметические операции (что в общем случае совершенно необязательно).

·>Ок. Верно. Давай рассмотрим алгоритм "print 42". Он по обоим твоим пунктам удовлетворяет для функции f(x) = 42 + x — x. Так? Значит он корректно работает. Так?

Пока ты не определил, какому множеству принадлежит x и какие отношения определены на этом множестве -- нет, не "так", а "хз как". Но он удовлетворяет функции f(x) = 42 без этой оговорки.