Что произойдет, если мы отбросим условие, согласно которому доказательства представляют собой конечные цепочки выводов в теореме Гёделя о неполноте?

Теорема Гёделя о неполноте показывает, что есть предложения, которые неразрешимы, то есть ни они, ни их отрицание не могут быть доказаны.

Эта теорема действует чисто синтаксически или формально, то есть не использует модель. Никакая семантика не задействована.

Теперь формальное доказательство представляет собой конечную цепочку выводов. Что произойдет, если отбросить это условие, то есть использовать бесконечное количество выводов? Чтобы понять это, нужно использовать теорию бесконечного, поскольку выводы упорядочены, следует использовать порядковую теорию, а не кардинальную.

Существует ли бесконечный ординал, для которого все предложения становятся разрешимыми?

Действительно ли так работает доказательство непротиворечивости PA Генцена , которое может означать только то, что все предложения разрешимы?

Что это может означать , когда доказательства на самом деле являются конечными выводами?

Ответы (1)

  1. Если вы допускаете бесконечные правила, такие как омега-правило, становится доказуемым больше, поэтому PA плюс омега-правило доказывает предложение Гёделя для PA. Но PA плюс омега-правило все еще не завершены — результат, который восходит к статье Россера JSL 1937 года о теоремах Гёделя для неконструктивной логики. Здесь может быть полезна статья Дэна Исааксона о правиле омеги: «Некоторые соображения об арифметической истинности и ω-правиле», в книге Майкла Детлефсена (редактор), Доказательство, логика и формализация, Рутледж, Лондон, 1991, стр. 94–138. .

  2. Генценовское доказательство непротиворечивости PA выполняется в рамках, предполагающих определенную степень трансфинитной индукции (больше трансфинитной индукции, доступной посредством кодирования внутри самой PA). Но доказательства с помощью трансфинитной индукции по-прежнему являются конечными цепочками предложений (рассмотрите, например, такие доказательства в ZF!).

Доказательства по трансбесконечной индукции, я согласен, могут быть конечными. Но если Генцен проделывал это на протяжении всех доказательств в PA — а я предполагаю, что так оно и было, поскольку я не вижу ничего другого, на чем можно было бы провести индукцию, — то что это значит? Не мета-доказательство, а индуцированное доказательство.
Нет, индукция проводится по порядку конечных доказательств, где порядок имеет эпсилон-ноль порядка.
хорошо, все конечные доказательства находятся в биекции с набором конечных корневых деревьев, который имеет эпсилон-ноль порядкового типа.
@PeterSmith Что не так с этим доказательством того, что PA плюс правило омеги завершено? m-phi.blogspot.com/2011/03/…
Что произойдет, если мы отбросим условие, согласно которому доказательства представляют собой конечные цепочки выводов в теореме Гёделя о неполноте?
СпросиСетьПолитика конфиденциальности1y, 0v