Любая непротиворечивая формальная система F, в рамках которой может быть выполнена определенная часть элементарной арифметики, неполна; т. е. существуют утверждения языка F, которые нельзя ни доказать, ни опровергнуть в F.
Так почему же нельзя иметь конечное количество Формальных систем F2...FN, которые доказывают все утверждения (или, иначе, значительное количество), которые не могут быть доказаны внутри самих себя?
Если нет, то не доказывает ли это, что некоторые утверждения вообще нельзя доказать ни в каких формальных системах?
Первоначально я думал, что это может быть связано с тем, что F2 и F, предполагающие согласованность, могут рассматриваться как одна система и, следовательно, вместе являются неполными.
Я рассудил, что, с другой стороны, это будет означать, что существует совершенная формальная система, которая доказывает все, что возможно.
Однако затем это заставило меня задуматься о возможности сделать это с более слабой формальной системой и более сильной формальной системой (W1 и F), доказывая или иным образом упрощая утверждения, которые F не может доказать сама по себе. Почему это невыполнимо? Чтобы быть точным, я задался вопросом, почему вы не можете комбинировать формальные системы, не используя их в качестве новой формальной системы в этом контексте? Например, используя W1 или F2 для доказательства утверждений в F (которые F не может доказать), не обращаясь непосредственно к F.
Укороченная версия:
Во-первых, обратите внимание, что вы не правильно сформулировали теорему Геделя - скорее, это так:
Всякая непротиворечивая вычислимо аксиоматизируемая теория, «содержащая достаточно арифметики», неполна.
«Вычислимо аксиоматизируемая» здесь в основном означает, что теория не настолько сложна, чтобы ее невозможно было описать; например, принимая платонистскую позицию для простоты, набор всех истинных предложений о натуральных числах непротиворечив, полон и тривиально «содержит достаточно арифметики».
Это не станет актуальным до конца моего ответа, но важно указать.
Каждое предложение может быть решено в некоторой теории. В качестве глупого примера: если p логически неверно, то оно опровергается пустым набором аксиом, а если p логически не неверно, то { p } является непротиворечивым набором аксиом, доказывающим p . Менее глупо, предполагая (скажем) ZFC непротиворечивым, тогда одно из ZFC+ p и ZFC+~ p непротиворечиво, или оба , и в зависимости от того, что является непротиворечивым, ясно решает p .
(Обратите внимание, что именно этот случай, выделенный жирным шрифтом, здесь имеет решающее значение: если непротиворечиво только одно из ZFC+ p и ZFC+~ p , то только ZFC определяет p уже.)
Итак, это отвечает на один из ваших вопросов: «Если нет, то не доказывает ли это, что некоторые утверждения вообще не могут быть доказаны ни в каких формальных системах?»
Теперь давайте посмотрим, что происходит, когда мы пытаемся использовать несколько теорий, чтобы обойти неполноту.
Если у нас есть теории T1 ,..., Tn , ни в чем не противоречащие друг другу , то их объединение T также является теорией, к которой применима теорема Гёделя; полученное гёделевское предложение g(T) заведомо неразрешимо в каждом из T1 ,..., Tn .
(На самом деле, с технической точки зрения здесь мы должны вместо этого использовать предложение Россера, но не так.)
Что, если мы допустим разногласия? Ну, начнем с того, что это бросает всю идею в хаос - если есть расхождение между Ti (скажем, T1 доказывает p , а T2 опровергает p ), то трудно сказать, как совокупность теорий T1,...,Tn могла справедливо сказать, чтобы решить что-либо - но оказывается, что даже допущение разногласий не помогает:
Если каждая из теорий T1 ,..., Tn является теорией, к которой применима теорема Гёделя о неполноте (= непротиворечивой, вычислимо аксиоматизируемой и содержащей достаточно арифметики) , то в каждой из T1 ,..., Tn есть неразрешимое предложение .
(Я выделил это гигантским шрифтом, так как считаю, что это действительно самый важный результат, упомянутый в этом ответе.)
Это удивительно сложно доказать; пара моих старых ответов ( 1 , 2 ) обрабатывают случай двух теорий (вторая обходится без ненужного предположения, используемого в первой), а общий случай более запутанный, но в основном такой же. В частности, дело в том, что у нас не может быть «петли непротиворечивости», когда одна теория доказывает непротиворечивость другой теории, которая доказывает непротиворечивость еще одной теории, которая... доказывает непротиворечивость исходной теории, но если каждое предложение разрешима в одной из наших теорий, то избежать такой «петли непротиворечивости» невозможно.
Наконец, ваше заявление
Я рассудил, что, с другой стороны, это означало бы, что существует совершенная формальная система, доказывающая, насколько это возможно,
противоречит требованию вычислимой аксиоматизируемости в теореме Гёделя. Даже игнорируя проблему поиска механизма для выбора «правильной» теории, решающей данное предложение, которое мы до сих пор не решили, мы не можем обойти проблему, заключающуюся в том, что объединение бесконечного множества вычислимо аксиоматизируемых теорий не обязательно должно быть вычислимо аксиоматизируемым . .
Именно в этот момент теория вычислимости становится очень актуальной: оказывается, мы можем количественно определить , насколько сложной должна быть непротиворечивая полная теория, содержащая достаточно арифметических операций. Ответ технический , но дело в том, что это то, что мы можем тщательно атаковать и развить хорошее понимание.
Джей Ди
Конифолд