Предположим, что у нас алгоритм вычисления того, существует ли предел натурального ряда. Он будет соответствовать индуктивному определению нат ряда Nnext=N+1. Запускаем его, допустим, на МТ. Надо сказать, что интуитивно понятно, что данное вычисление бесконечно. Но это не доказано. На самом деле, этот алгоритм и есть попытка доказательства этого, поскольку, если бы он когда нибудь остановился, мы могли бы сделать вывод, что данное вычисление конечно. То есть, мы получили бы доказательство от противного.
Тут существенно и другое. Мы не можем доказать, что это вычисление бесконечно. Это всего лишь, наше интуитивное априорное допущение. Компьютер не обладает интуицией человека, следовательно он не может этого сделать.
Из этого следует, что не существует никакой возможности ни доказать, ни опровергнуть утверждение о конечности или бесконечности данного алгоритма.
Ясно, что это лишь частный случай, и существует тьма подобных случаев. Количество которых недетерминированно.
В таком случае, как компилятор может доказать невычисляемость того или иного выражения?
