Теорема Гёделя о неполноте и нестандартная логика/основополагающие системы

Я любитель в области математической логики, поэтому извините за любые запутанные части этого вопроса.

Хорошо известно, что теорема Гёделя о неполноте показывает, что существуют большие пределы возможностей логики первого порядка. Можно ли основывать наши формальные рассуждения на какой-то другой системе (другой вид логики, теории типов (?), чем-то, основанном на теории категорий) таким образом, чтобы теорема Гёделя о неполноте не применялась?

Кто-нибудь пытался изобрести совершенно новую систему в качестве основы математики, чтобы предотвратить это? Может быть, не на формулах и доказательствах, а на чем-то совсем другом?

Начальная логика свободна от теорем Гёделя. На самом деле это потому, что бесконечная логика не рекурсивна.
Вам понадобятся более жесткие ограничения, чем «рассуждения в какой-либо другой системе таким образом, чтобы теорема Гёделя о неполноте не применялась», чтобы сделать вопрос интересным. Это явно применимо к теориям первого порядка, включая арифметику Пеано, рекурсивно аксиоматизируемым и непротиворечивым, любое из вышеперечисленного может быть и было отброшено, но не без затрат. Например, существует полная паранепротиворечивая арифметика , полна элементарная геометрия Тарского и т. д.
Если вас также интересуют доказательства непротиворечивости, вам может быть интересно узнать, что можно доказать непротиворечивость арифметики с помощью логики релевантности. Чтобы быть более точным, если вы создаете релевантную арифметику, добавляя аксиомы Пеано к логике релевантности, эта арифметика доказуемо абсолютно непротиворечива с использованием финитных методов. Релевантная логика слабее классической, поэтому релевантная арифметика не содержит всех теорем классической арифметики. См. Мейер и Фридман, 1992, «Куда относится арифметика?», Журнал символической логики, 57: 824–831.
Очевидно, вы неправильно поняли теоремы Гёделя о неполноте, почти наверняка потому, что популярное сообщение, которое вы читали, неверно или вводит в заблуждение. Первоначальный результат Гёделя относился к классической теории арифметики первого порядка, но обобщенные теоремы о неполноте справедливы для любой разумной фундаментальной системы математики, даже для тех, которые еще не созданы. Как указано в связанном сообщении, неверно , что это применимо только к FOL или только к дедуктивным системам, включающим обычные формулы.
В частности, какой бы экзотической фундаментальной системы вы ни обладали, если она имеет программу проверки доказательств и может рассуждать о программах, то она непоследовательна (доказывает противоречивые утверждения о программах) или неполна (не может доказать, что P останавливается на X, для некоторой программы P, которая действительно останавливается на входе X). Этим условиям удовлетворяет любая разумная базовая система S, потому что для того, чтобы S можно было использовать в первую очередь, она должна иметь программу проверки доказательств, и если S не может даже рассуждать о конечном выполнении программы, то она слишком слаба, чтобы быть фундаментальной.
Самопроверяющаяся теория Дэна Уилларда не может рассуждать о программах. Таким образом, это неадекватно для основы математики. Подходит ли он для повседневных рассуждений или нет — это отдельный (и потенциально интересный) вопрос.

Ответы (2)

Существует множество способов обойти доказательство Гёделя. Вопрос в том, имеют ли эти системы достаточную практическую ценность для математики, чтобы их можно было использовать для каких-либо других целей, кроме обхода его доказательства.

Лично мне больше всего нравится работа Дэна Уилларда: Самопроверка систем аксиом, теорема о неполноте и связанные с ней принципы отражения. . В нем он создал систему, которая могла доказать все свои собственные истинные утверждения и содержала все истины арифметики (т.е. арифметики Пеано), но он не определял умножение как полное. Этого было достаточно (достаточно слабо?), чтобы отказаться от диагонализации, необходимой для доказательства Гёделя.

По-видимому, у него была интересная особенность: в системе можно построить исчисляемую бесконечность, а затем сконструировать внутри нее такую ​​самореферентную систему, чтобы эта конкретная бесконечность была доказуемо несчетной в самореферентном «мире Уилларда», но доказуемо счетной. внутри большей системы. Мне было весело играть с философскими последствиями, которые можно извлечь из этого.

"все свои заявления"??? Не будет ли отрицание утверждения также утверждением? Вы имеете в виду, что в ней нет неразрешимых утверждений, потому что она слишком слаба, чтобы содержать всю арифметику Пеано, или нарушает некоторые другие предположения Гёделя (какие именно?).
@Conifold Хороший улов. Я пропустил слово "правда". Отредактировано, чтобы сказать, что это доказывает все его истинные утверждения. Он содержит всю арифметику Пеано , за исключением того, что не гарантирует, что умножение является суммарной функцией.

Очень, очень упрощенно Гёдель показал, как можно выразить утверждение S «для утверждения S нет доказательства» в арифметике, и либо S истинно, тогда у вас есть истинное утверждение без доказательства, либо S ложно, тогда у вас есть ложное утверждение с доказательством. Неполнота или противоречие.

Вы получите точно такой же результат в любой системе, где вы можете выразить одно и то же утверждение S в системе. Теперь можно обоснованно утверждать, что системы, в которых можно выразить S, сильнее, а те, в которых нельзя выразить S, слабее, и отсюда следует, что более сильные системы неполны или противоречивы, тогда как более слабые системы могут быть как полными, так и не имеющими противоречий.

Что, если мы введем какое-то альтернативное понятие доказательства? Кто-нибудь изучал такие системы?
Теорема Гёделя о неполноте и нестандартная логика/основополагающие системы
СпросиСетьПолитика конфиденциальности1y, 0v