Как известно, теорема Гёделя о неполноте утверждает, что если мы ограничимся некоторым набором аксиом и правил вывода, то мы не сможем доказать или опровергнуть любое утверждение данного языка. Интересно, однако, пробовал ли кто-нибудь рассматривать множество доказуемых (и опровержимых) утверждений при фиксированных аксиомах и правилах вывода? Может быть, оно обладает некоторой простой, но нетривиальной структурой, или "алгеброй"? Может быть, можно указать критерий принадлежности утверждения данному множеству? То есть, придумать алгоритм, у которого на входе - формулировка утверждения, а на выходе - ответ "да" или "нет", причём ответ "да" означает, что поданное на вход утверждение может быть доказано или опровергнуто с помощью принятых аксиом и правил вывода. Теперь, подав на вход, скажем, теорему Ферма или вторую проблему Гольдбаха, мы получим один из трёх ответов:
1) Теорема доказана;
2) Теорема опровергнута;
3) Принятых аксиом и правил вывода недостаточно, чтобы доказать или опровергнуть её.
(Если на выходе алгоритма получим "нет", то выбираем ответ 3; если "да", то начинаем перебирать одно за другим все возможные пути доказательства и опровержения, а так как они образуют счётное множество, то через конечное число шагов непременно наткнёмся либо на доказательство, либо на опровержение, и таким образом выберем ответ 1 или 2.)
Теперь, если мы хотим иметь возможность доказать либо опровергнуть любую теорему, то конечного числа аксиом и правил вывода недостаточно (по теореме Гёделя), так что необходима бесконечная последовательность правил вывода, или же бесконечная последовательность аксиом. Каждый элемент этой бесконечной последовательности не вытекает из предыдущих в том смысле, что нельзя придумать алгоритм, который бы выводил его из предыдущих. Однако, может оказаться, что с привлечением интуиции (т. е. с привлечением живого человека) такой вывод возможен. То есть, просмотрев все предыдущие аксиомы (или правила вывода) и почесав затылок, живой человек, искушённый в математике, сразу сформулирует следующую аксиому (или правило вывода), которая не вытекает из предыдущих, но интуитивно ясна. Может также случиться, что при надлежащем построении ряда аксиом (или правил вывода) вся существующая к настоящему моменту математика укладывается в небольшое число (скажем, в десять) первых аксиом и правил вывода. Тогда следующие аксиомы или правила вывода откроют новые пути доказательства теорем, возможно, "безумные" с точки зрения современного математика.
Или, например, так. Предположим, что существует алгоритм распознавания доказуемости (или опровержимости) утверждений языка. Тогда, приняв некий затравочный набор аксиом, машина перебирает все возможные утверждения в порядке возрастания сложности и находит простейшее утверждение, не доказуемое и не опровержимое в рамках этого набора аксиом. Математик доказывает его (или опровергает) на основе интуитивных соображений, и если оно доказано, то оно добавляется к набору аксиом, а если опровергнуто - то его отрицание добавляется к набору аксиом. После чего машина продолжает перебор утверждений, уже с учётом добавленной аксиомы. И так далее. Получается цепочка аксиом всё возрастающей сложности, такая, что для любого произвольно взятого утверждения сразу можно сказать, сколько аксиом из этой цепочки потребуется, чтобы доказать либо опровергнуть данное утверждение: для этого нужно идти от начала цепочки, сравнивая аксиомы с данным утверждением по сложности, и первая из аксиом цепочки, которая окажется сложнее данного утверждения, вместе со всеми предыдущими ей аксиомами образует набор, достаточный для доказательства или опровержения данного утверждения.
Конечно, составить такую цепочку аксиом невозможно без понимания структуры множества утверждений, доказуемых и опровержимых при фиксированном наборе аксиом, потому что тупо перебирать все утверждения подряд не под силу никакому компьютеру, и даже квантовому. Необходимо какое-то "решето", которое сразу отсеивает не перебирая все тривиальные случаи и оставляет для рассмотрения (т. е. подаёт на вход алгоритма распознавания доказуемости) только сравнительно небольшое (т. е. не экспоненциально большое) действительно нетривиальных (и не вытекающих из уже рассмотренных) утверждений.