Теорема Гёделя о неполноте является полностью формальной (в моем понимании) и опирается на систему доказательств, которую я считаю первопорядковой. Имеет ли какое-либо значение для теоремы использование логики более высокого порядка?
Правильно ли я думаю, что это не так, потому что логика первого порядка включается в логику высшего порядка?
Предположительно также, Гёдель использовал систему вывода в стиле Гильберта , и не имеет никакого значения, если вместо нее используются системы вывода типа естественной дедукции.
На самом деле в логике высшего порядка теорема Гёделя обобщается вполне естественным образом. Суть в том, что, хотя теорема о неполноте верна в отношении логики высшего порядка, ваше интуитивное предположение, что она не должна отражать следующее: HOL может быть систематизирован на различные подъязыки, каждый из которых способен формализовать незавершенность некоторых подъязыков самого себя.
Пусть L будет нашим заданным языком, тогда мы можем разделить L на бесконечную последовательность языков L 0 , L 1 , ..., L n . Каждый L n определяется как язык, который получается в результате дополнения L n-1 кванторами типа n, а тип 0 является типом индивидуумов. В каждом L n для n > 0 мы можем сформулировать предикат Pr n (n), который истинен для n тогда и только тогда, когда n является числом Гёделя выражения E, которое доказуемо в L n . Мы также можем сформулировать функцию d n (x), которая отображает каждое гёделевское число p n предиката P n (имеется в виду открытое предложение с одной свободной переменной "x n-1" типа n-1) в гёделевское число выражения P[p/x]. Взяв гёделевское число d n ("~Pr n (x)"), мы получили выражение, истинное в L n тогда и только тогда, когда оно недоказуемо в L n . Однако мы можем найти гёделевское число доказательства в L n+1 выражения, соответствующего ~Pr n+1 (d n ("~Pr n (x)").
Когда мы арифметизируем выражение Pr(x), которое истинно тогда и только тогда, когда x есть число Гёделя выражения, которое доказуемо в L, мы снова оказываемся в известном затруднительном положении. d("~Pr(x)") семантически верно, но не доказуемо.
На этот раз ваши предположения неверны. Гёдель использовал теорию типов Рассела из Principia Mathematica . Таким образом, Гёдель использует теорию более высокого порядка в исходном доказательстве (хотя я не уверен, не вдаваясь в подробности, насколько используется аппарат более высокого порядка). На самом деле, название оригинальной статьи (в переводе) звучит так : «О формально неразрешимых предложениях Principia Mathematica и родственных систем» .
Полная логика второго порядка также неполна.
Я считаю, что единственными требованиями к системе для получения неполноты являются следующие (я могу что-то упустить):
Как только эти два значения выполняются (по модулю моего опасения, что я могу что-то забыть), к этой системе применяется неполнота.
РЕДАКТИРОВАТЬ:
Я считаю, что мое утверждение о том, что это единственные два требования, на самом деле правильно (поэтому мои опасения были неуместны), Гёдель формулирует условия следующим образом:
пользователь 21820