Оригинальное доказательство теоремы Гёделя о полноте

Курт Гёдель (1925)

Доказательство теоремы Гёделя о полноте, данное Куртом Гёделем в его докторской диссертации 1929 года (и более короткая версия доказательства, опубликованная в 1930 году в виде статьи под названием «Полнота аксиом функционального логического исчисления» (на немецком языке) ) сегодня нелегко читать; он использует концепции и формализмы, которые больше не используются, а также терминологию, которая часто неясна. В приведенной ниже версии делается попытка достоверно отобразить все этапы доказательства и все важные идеи, переформулировав доказательство на современном языке математической логики . Этот план не следует рассматривать как строгое доказательство теоремы.

Предположения

Мы работаем с исчислением предикатов первого порядка . Наши языки допускают символы констант, функций и отношений. Структуры состоят из (непустых) областей и интерпретаций соответствующих символов как постоянных членов, функций или отношений в этой области.

Мы предполагаем классическую логику (в отличие, например, от интуиционистской логики).

Мы фиксируем некоторую аксиоматизацию (т. е. основанную на синтаксисе, управляемую машиной систему доказательства) исчисления предикатов: логические аксиомы и правила вывода. Подойдет любая из нескольких хорошо известных эквивалентных аксиоматизаций. Первоначальное доказательство Гёделя предполагало систему доказательств Гильберта-Акермана .

Мы предполагаем без доказательства все основные известные результаты о нашем формализме, которые нам нужны, такие как теорема о нормальной форме или теорема о корректности .

Мы аксиоматизируем исчисление предикатов без равенства (иногда его ошибочно называют без тождества ), т. е. не существует специальных аксиом, выражающих свойства (объектного) равенства в виде специального символа отношения. После того как основная форма теоремы будет доказана, ее нетрудно распространить на случай исчисления предикатов с равенством .

Формулировка теоремы и ее доказательство

Ниже мы сформулируем две эквивалентные формы теоремы и покажем их эквивалентность.

Позже мы докажем теорему. Это делается следующими шагами:

1. Сведение теоремы к предложениям (формулам без свободных переменных) в пренексной форме , т.е. со всеми кванторами ( ∀ и ∃ ) в начале. Более того, мы сводим его к формулам, первый квантор которых равен ∀ . Это возможно, потому что для каждого предложения существует эквивалентное в пренексной форме, первый квантор которого равен ∀ .
2. Сведение теоремы к предложениям вида ∀ x ₁ ∀ x ₂ ... ∀ x _k ∃ y ₁ ∃ y ₂ ... ∃ y _m φ ( x ₁ ... x _k , y ₁ ... y _m ) . Хотя мы не можем сделать это, просто переставляя кванторы, мы показываем, что этого еще достаточно, чтобы доказать теорему для предложений такой формы.
3. Наконец, мы докажем теорему для предложений такой формы.
   • Для этого сначала отметим, что такое предложение, как B = ∀ x ₁ ∀ x ₂ ...∀ x _k ∃ y ₁ ∃ y ₂ ...∃ y _m φ( x ₁ ... x _k , y ₁ . .. y _m ) либо опровержимо (его отрицание всегда истинно), либо выполнимо, т. е. существует некоторая модель, в которой оно выполняется (оно может даже быть всегда истинным, т.е. тавтология); эта модель просто присваивает истинностные значения подпредложениям, из которых построено B. Причиной этого является полнота пропозициональной логики , в которой кванторы существования не играют никакой роли.
   • Мы распространим этот результат на все более и более сложные и длинные предложения D _n ( n = 1,2...), построенные из B , так что либо любое из них опровержимо, а значит, и φ , либо все они опровержимы. не является опровержимым и, следовательно, каждое из них справедливо в некоторой модели.
   • Наконец, мы используем модели, в которых выполняются D _n (в случае, если все они неопровержимы), чтобы построить модель, в которой выполняется φ .

Теорема 1. Любая допустимая формула (истинная во всех структурах) доказуема.

Это самая основная форма теоремы о полноте. Сразу переформулируем это в более удобной для наших целей форме: Когда мы говорим «все структуры», важно указать, что рассматриваемые структуры представляют собой классические (тарские) интерпретации I, где I = <U,F> (U — непустое (возможно, бесконечное) множество объектов, тогда как F представляет собой набор функций из выражений интерпретируемой символики в U). [Напротив, так называемые «свободные логики» допускают, возможно, пустые множества для U. Дополнительную информацию о свободной логике см. в работе Карела Ламберта.]

Теорема 2. Любая формула φ либо опровержима, либо выполнима в некоторой структуре.

« φ опровержимо» означает по определению « ¬φ доказуемо».

Эквивалентность обеих теорем

Если теорема 1 верна и φ не выполнима ни в одной структуре, то ¬φ действительна во всех структурах и, следовательно, доказуема, таким образом, φ опровержима и теорема 2 верна. Если, с другой стороны, теорема 2 верна и φ справедлива во всех структурах, то ¬φ невыполнима ни в одной структуре и, следовательно, опровержима; тогда ¬¬φ доказуемо, а затем и φ, поэтому теорема 1 верна.

Доказательство теоремы 2: первый шаг

Мы подходим к доказательству теоремы 2, последовательно ограничивая класс всех формул φ, для которых нам нужно доказать, что «φ либо опровержима, либо выполнима». Вначале нам нужно доказать это для всех возможных формул φ в нашем языке. Однако предположим, что для каждой формулы φ существует некоторая формула ψ, взятая из более ограниченного класса формул C , такая, что «ψ либо опровержимо, либо выполнимо» → «φ либо опровержимо, либо выполнимо». Тогда, как только это утверждение (выраженное в предыдущем предложении) будет доказано, будет достаточно доказать, что «φ либо опровержима, либо выполнима» только для принадлежности φ классу C . Если φ доказуемо эквивалентно ψ ( т. е . ( φ ≡ ψ ) доказуемо), то это действительно тот случай, когда «ψ либо опровержимо, либо выполнимо» → « φ либо опровержимо, либо выполнимо» ( теорема о корректности необходима для того, чтобы покажи это).

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

Далее мы рассматриваем общую формулу φ (которая больше не использует функциональные или постоянные символы) и применяем теорему о предварительной форме , чтобы найти формулу ψ в нормальной форме такую, что φ ≡ ψ ( ψ нахождение в нормальной форме означает, что все кванторы в ψ , если они есть, то находятся в самом начале ψ ). Отсюда следует, что нам осталось доказать теорему 2 только для формул φ в нормальной форме.

Далее мы исключаем все свободные переменные из φ, определяя их экзистенциально: если, скажем, x ₁ ... x _n свободны в φ , мы образуем $\psi =\exists x_{1}\cdots \exists x_{n}\varphi$. Если ψ выполнима в структуре M , то, конечно, так же выполнима и ψ , и если ψ опровержима, то $\neg \psi =\forall x_{1}\cdots \forall x_{n}\neg \varphi$ доказуемо, а значит, и ¬ φ , следовательно, φ опровержимо. что мы можем ограничить φ предложением Мы видим , , то есть формулой без свободных переменных.

Наконец, нам хотелось бы, по соображениям технического удобства, чтобы префикс φ φ (то есть строка кванторов в начале , которая находится в нормальной форме) начинался с квантора всеобщности и заканчивался квантором существования. Чтобы добиться этого для общего φ (с учетом ограничений, которые мы уже доказали), мы берем некоторый одноместный символ отношения F, не используемый в φ , и две новые переменные y и z . Если φ = (P)Φ , где (P ) обозначает префикс φ и Φ для матрицы (оставшаяся, свободная от кванторов часть φ ), которую мы формируем $\psi =\forall y(P)\exists z(\Phi \wedge [F(y)\vee \neg F(z)])$. С $\forall y\exists z(F(y)\vee \neg F(z))$ ясно доказуемо, легко видеть, что $\varphi =\psi$ доказуемо.

Сведение теоремы к формулам степени 1

Наша общая формула φ теперь представляет собой предложение в нормальной форме, и ее префикс начинается с квантора универсальности и заканчивается квантором существования. Назовем класс всех таких формул R . Нам предстоит доказать, что каждая формула из R либо опровержима, либо выполнима. Учитывая нашу формулу φ, мы группируем строки кванторов одного вида в блоки:

$\varphi =(\forall x_{1}\cdots \forall x_{k_{1}})(\exists x_{k_{1}+1}\cdots \exists x_{k_{2}})\cdots (\forall x_{k_{n-2}+1}\cdots \forall x_{k_{n-1}})(\exists x_{k_{n-1}+1}\cdots \exists x_{k_{n}})(\Phi )$

Мы степень определяем $\varphi$ быть количеством блоков кванторов универсальности, разделенных блоками кванторов существования, как показано выше, в префиксе $\varphi$. Следующая лемма, которую Гёдель адаптировал из доказательства Скулема теоремы Левенгейма–Скулема , позволяет резко снизить сложность общей формулы $\varphi$ нам нужно доказать теорему для:

Лемма . Пусть k ≥ 1. Если каждая формула из R степени k либо опровержима, либо выполнима, то то же самое можно сказать и о любой формуле из R степени k + 1.

Комментарий : Возьмем формулу φ степени k + 1 вида $\varphi =(\forall x)(\exists y)(\forall u)(\exists v)(P)\psi$, где $(P)\psi$ это остаток $\varphi$ (таким образом, он имеет степень k − 1). φ утверждает, что для каждого x существует такой, что... (что-то). Было бы неплохо иметь предикат Q', чтобы для каждого x Q '( x , y ) был истинным тогда и только тогда, когда y является необходимым для того, чтобы сделать (что-то) истинным. Тогда мы могли бы написать формулу степени k , эквивалентную φ, а именно $(\forall x')(\forall x)(\forall y)(\forall u)(\exists v)(\exists y')(P)Q'(x',y')\wedge (Q'(x,y)\rightarrow \psi )$. Эта формула действительно эквивалентна φ, поскольку она утверждает, что для каждого x, если существует y, удовлетворяющее Q'(x,y), то (что-то) имеет место, и, более того, мы знаем, что существует такое y, потому что для каждого x ', существует y', который удовлетворяет условию Q'(x',y'). Поэтому φ следует из этой формулы. Также легко показать, что если формула неверна, то ложна и φ. К сожалению , такого предиката Q' вообще не существует. Однако эту идею можно понять как основу для следующего доказательства леммы.

Доказательство. Пусть φ — формула степени k + 1; тогда мы можем написать это как

$\varphi =(\forall x)(\exists y)(\forall u)(\exists v)(P)\psi$

где (P) — остаток префикса $\varphi$ (таким образом, он имеет степень k – 1) и $\psi$ представляет собой бескванторную матрицу $\varphi$. x , y , u и v обозначают здесь кортежи переменных, а не отдельные переменные; например $(\forall x)$ действительно означает $\forall x_{1}\forall x_{2}\cdots \forall x_{n}$ где $x_{1}\ldots x_{n}$ являются некоторыми отдельными переменными.

Пусть теперь x' и y' будут кортежами ранее неиспользованных переменных той же длины, что и x и y соответственно, и пусть Q будет ранее неиспользованным символом отношения, который принимает столько аргументов, сколько сумма длин x и y ; мы рассматриваем формулу

$\Phi =(\forall x')(\exists y')Q(x',y')\wedge (\forall x)(\forall y)(Q(x,y)\rightarrow (\forall u)(\exists v)(P)\psi )$

Четко, $\Phi \rightarrow \varphi$ доказуемо.

Теперь, поскольку строка кванторов $(\forall u)(\exists v)(P)$ не содержит переменных из x или y , следующая эквивалентность легко доказывается с помощью любого используемого нами формализма:

$(Q(x,y)\rightarrow (\forall u)(\exists v)(P)\psi )\equiv (\forall u)(\exists v)(P)(Q(x,y)\rightarrow \psi )$

А так как эти две формулы эквивалентны, то если заменить первую на вторую внутри Φ, мы получим формулу Φ' такую, что Φ≡Φ':

$\Phi '=(\forall x')(\exists y')Q(x',y')\wedge (\forall x)(\forall y)(\forall u)(\exists v)(P)(Q(x,y)\rightarrow \psi )$

Теперь Ф' имеет вид $(S)\rho \wedge (S')\rho '$, где (S) и (S') — некоторые строки-кванторы, ρ и ρ' не содержат кванторов, и, кроме того , ни одна переменная из (S) не встречается в ρ' и ни одна переменная из (S') не встречается в ρ. В таких условиях каждая формула вида $(T)(\rho \wedge \rho ')$, где (T) — строка кванторов, содержащая все кванторы в (S) и (S'), перемежающиеся между собой любым способом, но сохраняющие относительный порядок внутри (S) и (S'), будет эквивалентен исходному формула Ф' (это еще один основной результат исчисления предикатов первого порядка, на который мы опираемся). А именно, сформируем Ψ следующим образом:

$\Psi =(\forall x')(\forall x)(\forall y)(\forall u)(\exists y')(\exists v)(P)Q(x',y')\wedge (Q(x,y)\rightarrow \psi )$

и у нас есть $\Phi '\equiv \Psi$.

Сейчас $\Psi$ является формулой степени k и, следовательно, по предположению либо опровержима, либо выполнима. Если $\Psi$ выполнима в структуре M , то, учитывая $\Psi \equiv \Phi '\equiv \Phi \wedge \Phi \rightarrow \varphi$, мы видим это $\varphi$ также является удовлетворительным. Если $\Psi$ опровержимо, то и так $\Phi$, что эквивалентно ему; таким образом $\neg \Phi$ доказуемо. Теперь мы можем заменить все вхождения Q в доказуемую формулу $\neg \Phi$ по какой-то другой формуле, зависящей от тех же переменных, и мы все равно получим доказуемую формулу. ( Это еще один основной результат исчисления предикатов первого порядка. В зависимости от конкретного формализма, принятого для исчисления, его можно рассматривать как простое применение правила вывода «функциональной замены», как в статье Гёделя, или как быть доказана путем рассмотрения формального доказательства $\neg \Phi$, заменив в нем все вхождения Q какой-либо другой формулой с теми же свободными переменными и отметив, что все логические аксиомы в формальном доказательстве остаются логическими аксиомами после замены, и все правила вывода по-прежнему применяются таким же образом. )

В данном конкретном случае мы заменяем Q(x',y') в $\neg \Phi$ с формулой $(\forall u)(\exists v)(P)\psi (x,y\mid x',y')$. Здесь (x,y | x',y') означает, что вместо ψ мы пишем другую формулу, в которой x и y заменены на x' и y'. Q(x,y) просто заменяется на $(\forall u)(\exists v)(P)\psi$.

$\neg \Phi$ затем становится

$\neg ((\forall x')(\exists y')(\forall u)(\exists v)(P)\psi (x,y\mid x',y')\wedge (\forall x)(\forall y)((\forall u)(\exists v)(P)\psi \rightarrow (\forall u)(\exists v)(P)\psi ))$

и эта формула доказуема; поскольку отрицаемая часть и после $\wedge$ знака очевидно доказуема, а отрицаемая часть и перед $\wedge$ знак, очевидно, φ, просто заменив x и y на x' и y' , мы видим, что $\neg \varphi$ доказуемо, а φ опровержимо. Мы доказали, что ф либо выполнима, либо опровержима, и этим завершается доказательство леммы .

Обратите внимание, что мы не могли использовать $(\forall u)(\exists v)(P)\psi (x,y\mid x',y')$ вместо Q(x',y') с самого начала, потому что $\Psi$ В этом случае формула не была бы корректной . Вот почему мы не можем наивно использовать аргумент, приведенный в комментарии, предшествующем доказательству.

Доказательство теоремы для формул степени 1

Как показывает лемма выше , нам нужно доказать нашу теорему только для формул φ из R степени 1. φ не может иметь степень 0, поскольку формулы в R не имеют свободных переменных и не используют константные символы. Таким образом, формула φ имеет общий вид:

$(\forall x_{1}\ldots x_{k})(\exists y_{1}\ldots y_{m})\varphi (x_{1}\ldots x_{k},y_{1}\ldots y_{m}).$

Теперь мы определим порядок k - наборов натуральных чисел следующим образом: $(x_{1}\ldots x_{k})<(y_{1}\ldots y_{k})$ должно сохраняться, если либо $\Sigma _{k}(x_{1}\ldots x_{k})<\Sigma _{k}(y_{1}\ldots y_{k})$, или $\Sigma _{k}(x_{1}\ldots x_{k})=\Sigma _{k}(y_{1}\ldots y_{k})$, и $(x_{1}\ldots x_{k})$ предшествует $(y_{1}...y_{k})$ в лексикографическом порядке . [Здесь $\Sigma _{k}(x_{1}\ldots x_{k})$ обозначает сумму членов кортежа.] Обозначим n-й кортеж в этом порядке через $(a_{1}^{n}\ldots a_{k}^{n})$.

Установите формулу $B_{n}$ как $\varphi (z_{a_{1}^{n}}\ldots z_{a_{k}^{n}},z_{(n-1)m+2},z_{(n-1)m+3}\ldots z_{nm+1})$. Затем положите $D_{n}$ как

$(\exists z_{1}\ldots z_{nm+1})(B_{1}\wedge B_{2}\wedge \cdots \wedge B_{n}).$

Лемма : Для n каждого $\varphi \rightarrow D_{n}$.

Доказательство : индукцией по n ; у нас есть $D_{n}\Leftarrow D_{n-1}\wedge (\forall z_{1}\ldots z_{(n-1)m+1})(\exists z_{(n-1)m+2}\ldots z_{nm+1})B_{n}\Leftarrow D_{n-1}\wedge (\forall z_{a_{1}^{n}}\ldots z_{a_{k}^{n}})(\exists y_{1}\ldots y_{m})\varphi (z_{a_{1}^{n}}\ldots z_{a_{k}^{n}},y_{1}\ldots y_{m})$, где последнее импликация выполняется путем замены переменных, поскольку порядок кортежей таков, что $(\forall k)(a_{1}^{n}\ldots a_{k}^{n})<(n-1)m+2$. Но последняя формула эквивалентна $D_{n-1}\wedge$ф.

Для базового случая $D_{1}\equiv (\exists z_{1}\ldots z_{m+1})\varphi (z_{a_{1}^{1}}\ldots z_{a_{k}^{1}},z_{2},z_{3}\ldots z_{m+1})\equiv (\exists z_{1}\ldots z_{m+1})\varphi (z_{1}\ldots z_{1},z_{2},z_{3}\ldots z_{m+1})$ очевидно, также является следствием φ. Итак, лемма доказана.

Теперь, если $D_{n}$ опровержимо для некоторого n , то из этого следует, что φ опровержима. С другой стороны, предположим, что $D_{n}$ неопровержимо ни для какого n . Тогда для каждого n существует некоторый способ присвоить истинностные значения различным подпредложениям. $E_{h}$ (упорядочены по их первому появлению в $D_{n}$; «различный» здесь означает либо отдельные предикаты, либо отдельные связанные переменные) в $B_{k}$, такой, что $D_{n}$ будет истинным, если каждое предложение оценивать таким образом. Это следует из полноты лежащей в основе пропозициональной логики .

Теперь мы покажем, что существует такое присвоение истинностных значений $E_{h}$, так что все $D_{n}$ будет правдой: $E_{h}$ появляются в одном и том же порядке во всех $D_{n}$; мы индуктивно определим общее присвоение им своего рода «большинством голосов»: поскольку существует бесконечно много присвоений (по одному на каждое $D_{n}$) влияет $E_{1}$, либо бесконечно много делают $E_{1}$ истинным, или бесконечно многие делают его ложным, и только конечное число делают его истинным. В первом случае мы выбираем $E_{1}$ быть правдой в целом; в последнем случае мы считаем его вообще ложным. Тогда из бесконечного числа n, для которых $E_{1}$ через $E_{h-1}$ присваиваются то же истинностное значение, что и в общем присваивании, мы выбираем общее присвоение для $E_{h}$ таким же образом.

Это общее задание должно привести к каждому из $B_{k}$ и $D_{k}$ верно, поскольку если один из $B_{k}$ были ложными по общему заданию, $D_{n}$ также будет ложным для каждого n > k . Но это противоречит тому, что для конечного набора общих $E_{h}$ задания появляются в $D_{k}$, существует бесконечно много n , где выполнение присваивания $D_{n}$ true соответствует общему назначению.

Из этого общего задания, которое делает все $D_{k}$ true, мы создаем интерпретацию предикатов языка, которая делает φ истинным. Вселенная модели будет состоять из натуральных чисел . Каждый i-арный предикат $\Psi$ должно быть правдой для натуральных людей $(u_{1}\ldots u_{i})$ именно тогда, когда предложение $\Psi (z_{u_{1}}\ldots z_{u_{i}})$ либо истинно в общем присваивании, либо не задано им (поскольку оно никогда не появляется ни в одном из $D_{k}$).

В этой модели каждая из формул $(\exists y_{1}\ldots y_{m})\varphi (a_{1}^{n}\ldots a_{k}^{n},y_{1}...y_{m})$ верно по построению. Но это означает, что φ сама по себе верна в модели, поскольку $a^{n}$ диапазон по всем возможным k-кортежам натуральных чисел. Итак, φ выполнимо, и мы закончили.

Интуитивное объяснение

Мы можем записать каждый B _i как Φ( x ₁ ... x _k , y ₁ ... y _m ) для некоторых x s, которые мы можем назвать «первыми аргументами», и y s, которые мы можем назвать «последними аргументами».

Возьмем Б ₁ , к примеру, . Его «последними аргументами» являются z ₂ , z ₃ ... z _{m +1} , и для каждой возможной комбинации k этих переменных существует некоторый j, так что они появляются как «первые аргументы» в B _j . при достаточно большом n ₁ Таким образом , D _{n 1} обладает свойством, заключающимся в том, что «последние аргументы» B ₁ появляются во всех возможных комбинациях из k из них как «первые аргументы» в других B _j s внутри D _n . Для каждого B _i существует D _{n i} с соответствующим свойством.

Следовательно, в модели, которая удовлетворяет всем D _n s, существуют объекты, соответствующие z ₁ , z ₂ ... и каждая комбинация k из них появляется как «первые аргументы» в некотором B _j , что означает, что для каждого k из этих объекты z _{p 1} ... z _{p k} существуют z _{q 1} ... z _{q m} , что делает Φ( z _{p 1} ... z _{p k} , z _{q 1} ... z _{q m} ) удовлетворенным. Взяв подмодель только с этими объектами z ₁ , z ₂ ..., мы получим модель, удовлетворяющую φ .

Расширения

Расширение исчисления предикатов первого порядка с равенством

Гёдель сократил формулу, содержащую экземпляры предиката равенства, до формул без него в расширенном языке. Его метод заключается в замене формулы φ, содержащей некоторые случаи равенства, формулой

$(\forall x)Eq(x,x)\wedge (\forall x,y,z)[Eq(x,y)\rightarrow (Eq(x,z)\rightarrow Eq(y,z))]$ $\wedge (\forall x,y,z)[Eq(x,y)\rightarrow (Eq(z,x)\rightarrow Eq(z,y))]$

$\wedge$

$(\forall x_{1}\ldots x_{k},y_{1}\ldots x_{k})[(Eq(x_{1},y_{1})\wedge \cdots \wedge Eq(x_{k},y_{k}))\rightarrow (A(x_{1}\ldots x_{k})\equiv A(y_{1}\ldots y_{k}))]$

$\wedge \cdots \wedge$

$(\forall x_{1}\ldots x_{m},y_{1}\ldots x_{m})[(Eq(x_{1},y_{1})\wedge \cdots \wedge Eq(x_{m},y_{m}))\rightarrow (Z(x_{1}\ldots x_{m})\equiv Z(y_{1}\ldots y_{m}))]$

$\wedge$

$\varphi '.$

Здесь $A\ldots Z$ обозначаем предикаты, входящие в φ (при этом $k\ldots m$ их соответствующие арности), а φ' — это формула φ, в которой все вхождения равенства заменены новым предикатом Eq . Если эта новая формула опровержима, то и первоначальная φ была опровержимой; то же самое относится и к выполнимости, поскольку мы можем взять фактор удовлетворения модели новой формулы по отношению эквивалентности, представляющему уравнение . Это частное четко определено по отношению к другим предикатам и, следовательно, будет удовлетворять исходной формуле φ.

Распространение на счетные множества формул.

Гёдель также рассмотрел случай, когда имеется счетный набор формул. Используя те же сокращения, что и выше, он смог рассмотреть только те случаи, когда каждая формула имеет степень 1 и не содержит использования равенства. Для счетного набора формул $\varphi ^{i}$ степени 1, мы можем определить $B_{k}^{i}$ как указано выше; затем определите $D_{k}$ быть закрытием $B_{1}^{1}\ldots B_{k}^{1},\ldots ,B_{1}^{k}\ldots B_{k}^{k}$. Остальная часть доказательства прошла так же, как и раньше.

Распространение на произвольные наборы формул

Когда существует несчетно бесконечный набор формул, Аксиома выбора необходима (или, по крайней мере, какая-то ее слабая форма). Используя полный AC, можно хорошо упорядочить формулы и доказать несчетный случай с тем же аргументом, что и счетный, за исключением трансфинитной индукции . Другие подходы можно использовать, чтобы доказать, что теорема о полноте в этом случае эквивалентна булевой теореме о простых идеалах , слабой форме AC.

Ссылки

• Гёдель, К. (1929). О полноте логического исчисления (Докторская диссертация). Венский университет. Первое доказательство теоремы о полноте.
• Гёдель, К. (1930). «Полнота аксиом исчисления логических функций». Ежемесячные журналы по математике (на немецком языке). 37 (1): 349–360. дои : 10.1007/BF01696781 . ЯФМ   56.0046.04 . S2CID   123343522 . Тот же материал, что и диссертация, за исключением более кратких доказательств, более сжатых объяснений и отсутствия длинного введения.

Внешние ссылки

• Стэнфордская энциклопедия философии : « Курт Гёдель » — Джульетты Кеннеди .
• Биография МакТьютора: Курт Гёдель.