математика

Поделиться статьей в социальных сетях:

в избранное

Теоремы Гёделя о неполноте

Ссылка на оригинал: Stanford Encyclopedia of Philosophy

Впервые опубликовано 11 ноября 2013 года; содержательно переработано 20 января 2015 года. 

Две теоремы о неполноте Гёделя составляют один из самых важных результатов в современной логике и имеют колоссальное значение при рассмотрении различных ее проблем. Они касаются пределов доказуемости в формальных аксиоматических теориях. Первая теорема о неполноте гласит, что в любой непротиворечивой формальной системе F, в которой может выполняться определенная часть арифметики, существуют утверждения языка F, которые не могут быть ни доказаны, ни опровергнуты в F. Согласно второй теореме о неполноте, такая формальная система не может доказать собственными средствами свою непротиворечивость (при условии, что она действительно непротиворечива). Эти результаты оказали большое влияние на философию математики и логику. Были попытки применить их также в других философских областях, таких как философия сознания, однако их успех оказался весьма спорным. В настоящей статье рассматриваются две теоремы о неполноте и различные вопросы, связанные с ними. (См. также статью о Курте Гёделе, в которой обсуждаются теоремы о неполноте в рамках более широкого обсуждения математических и философских работ автора.)

Введение

Общие сведения

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

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

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

Гёдель сформулировал две разные, хотя и взаимосвязанные теоремы о неполноте, обычно называемые первой и второй теоремами о неполноте. «Теорема Гёделя» иногда используется для обозначения их совокупности, но может относиться также и к любой из них — обычно первой — по отдельности. С учетом улучшения, внесенного Дж. Баркли Россером в 1936 году, первая теорема может быть сформулирована приблизительно так:

Первая теорема о неполноте

Любая непротиворечивая формальная система F, в пределах которой может быть выполнено определенное количество действий элементарной арифметики, неполна; то есть существуют утверждения языка F, которые не могут быть ни доказаны, ни опровергнуты в F.

Теорема Гёделя не просто заявляет, что такие утверждения существуют: метод доказательства Гёделя эксплицитно производит конкретное предложение, которое недоказуемо и неопровержимо в F; «неразрешимое» утверждение может быть найдено механически из спецификации F. Рассматриваемое предложение является относительно простым утверждением теории чисел, чисто универсальным арифметическим предложением.

Распространено ложное представление, согласно которому первую теорему Гёделя следует понимать как доказательство существования истин, которые нельзя доказать. Однако оно неверно, поскольку теорема о неполноте не связана с доказуемостью в каком-либо абсолютном смысле, а касается только выводимости в какой-либо конкретной формальной или иной системе. Для любого утверждения А, недоказуемого в конкретной формальной системе F, тривиально существуют другие формальные системы, в которых A доказуемо (или A берется в качестве аксиомы). С другой стороны, существует чрезвычайно мощная стандартная система аксиом теории множеств Цермело-Френкеля (обозначаемая как ZF или — при включении аксиомы выбора — ZFC; см. раздел об аксиомах ZFC в статье о теории множеств), которой более чем достаточно для вывода всей обычной математики. Теперь, по первой теореме Гёделя, мы имеем арифметические истины, которые не доказуемы даже в ZFC. Таким образом, их доказательство требует формальной системы, которая включает в себя методы, выходящие за пределы ZFC. Таким образом, существует смысл, в котором такие истины не доказуемы с использованием современных «обычных» математических методов и аксиом и прочих способов, которые математики сегодня считают беспроблемными и убедительными. 

Вторая теорема Гёделя о неполноте касается пределов доказательств непротиворечивости. В упрощенном изложении теорема имеет следующий вид:

Вторая теорема о неполноте

Для любой непротиворечивой системы F, в пределах которой может быть выполнено определенное количество действий элементарной арифметики, непротиворечивость F не может быть доказана в F непосредственно. 

В случае второй теоремы система F должна быть немного более арифметична, чем в случае первой, которая справедлива даже при очень слабых условиях. Важно отметить, что этот результат, как и первая теорема о неполноте, представляет собой теорему о формальной доказуемости или выводимости (которая всегда относится к некоторой формальной системе, в этом случае — к самой F). В ней ничего не говорится о том, что для той или иной теории T, удовлетворяющей условиям теоремы, утверждение «T непротиворечива» может быть доказано в том смысле, что оно представляется истинно убедительным аргументом или доказательством, в целом приемлемым для математиков. Для многих теорий это вполне возможно.

Некоторые формализованные теории

Существование неполных теорий неудивительно. Если взять любую теорию, даже полную (см. примеры ниже), и отбросить какую-либо аксиому, то при условии, что аксиома не избыточна, итоговая система будет неполной. Теоремы о неполноте, однако, касаются гораздо более радикального феномена незавершенности. В отличие от описанных выше тривиально неполных теорий, которые легко можно восполнить, релевантные теории сделать полными не получится; все их расширения все еще являются формальными системами и потому аксиоматизируемыми, а следовательно, они также неполны. Они остаются, так сказать, вечно неполными и никогда не могут быть восполнены. Они «существенно неполны». 

В первых приблизительных формулировках теорем о неполноте, приведенных выше, мы видели расплывчатое требование: «может быть выполнено определенное количество действий элементарной арифметики». Настало время его прояснить.

Арифметические теории

Самой слабой стандартной системой арифметики, которая обычно рассматривается в связи с неполнотой и неразрешимостью, является так называемая арифметика Робинсона (в честь Рафаэля Робинсона, см. Tarski, Mostowski and Robinson 1953), стандартно обозначаемая Q. В качестве аксиом она имеет следующие семь допущений:

Предполагается интерпретировать «x′» как функцию следования, а функции «+» и «×», очевидно, — как функции сложения и умножения соответственно. «0» — единственная константа и обозначает число ноль.

Добавляя к этим элементарным аксиомам схему аксиом индукции:

(IND) φ(0) ∧ ∀x[φ(x) → φ(x′)] → ∀xφ(x), 

— в итоге мы получаем (первопорядковую) арифметику Пеано (PA). Заметим, что PA содержит бесконечно много аксиом, в отличие от Q, поскольку все (бесконечно многие) вхождения схемы индукции, соответствующие каждой формуле φ (x) языка (хотя бы с одной свободной переменной), принимаются как аксиомы. Однако вопрос о том, является ли данное предложение вхождением этой схемы, — предмет рутинной, механической проверки. PA обычно понимается как стандартная система арифметики первого порядка.

Другой естественной и хорошо изученной арифметической системой, которая по силе находится между Q и PA, является примитивная рекурсивная арифметика (PRA). Она содержит не только вышеуказанные аксиомы Q, которые задают следование, сложение и умножение, но также определяющие аксиомы для всех примитивно-рекурсивных функций (см. статью о рекурсивных функциях), а схема индукции в этой системе применяется только в формулах без кванторов, то есть φ(x) не может содержать какие-либо (неограниченные) кванторы.

Однако можно получить ту же по сути систему, если взять только аксиомы Q и схему индукции, применение которой ограничивается сугубо экзистенциальными формулами (-формулами, см. ниже), что впервые было показано в Parsons 1970. Более того, можно продемонстрировать (Paris и Kirby 1978), что -индукция эквивалентна схеме индукции, ограниченной чисто универсальными формулами (-формулами). PRA также можно сформулировать как «логически свободное» эквациональное исчисление. PRA или эквивалентная ей система достаточна для разработки теории синтаксиса формализованных теорий. Ее часто принимают за беспроблемную базовую теорию, в рамках которой изучаются различные другие системы, чья легитимность может быть более спорной.

Более сильная по сравнению с PA система, значимая в контексте оснований математики, упоминаемая здесь и ниже, является арифметикой второго порядка PA2 (также часто обозначается Z2). Ее более чем достаточно для разработки всего обычного анализа и алгебры. Ее язык представляет собой двусортный язык первого порядка (см. статью о логике второго и высшего порядка), то есть содержит два сорта переменных — числовые переменные x1, x2, … (или x, y, z, …) и множественные переменные X1, X2, … (или X, Y, Z, …) — и в качестве аксиом (помимо основных аксиом PA) все вхождения схемы выделения:

∃X∀x[Xx ↔ φ(x)],

где φ(x) может быть любой формулой языка PA2, в которую X не входит свободно.

PA2 — очень сильная теория. С помощью метода интерпретаций (см. ниже) можно показать, что с точки зрения теории доказательств она столь же сильна, как теория множеств Цермело-Френкеля ZFC без аксиомы множества подмножеств, назовем ее ZFC-Pow. В свою очередь, стандартная первопорядковая PA с данной точки зрения эквивалентна ZFC без аксиомы бесконечности, ZFC-Inf. (Ср. раздел об аксиомах ZFC в статье по теории множеств.)

По очевидному допущению, формальные системы также обладают системой правил вывода (и, возможно, некоторыми логическими аксиомами), которой, как правило, служит некоторая стандартная система классической логики (хотя теоремы о неполноте по сути не предполагают классическую логику: они справедливы и для систем с интуиционистской логикой). Вышеупомянутые стандартные системы обладают классической логикой. Стандартная запись F ⊢ A используется для выражения (на метауровне) того, что A выводима в F: существует доказательство A в F или, иными словами, A является теоремой F. Соответственно, F ⊬ A означает, что A не выводима в F.

Подытожим: когда в контексте теорем о неполноте говорится, что в некоторой системе «может быть выполнено некоторое количество действий элементарной арифметики», это обычно означает, что система содержит PRA или по меньшей мере Q. Для первой теоремы о неполноте Q достаточна; для стандартных доказательств второй теоремы требуется как минимум нечто наподобие PRA. Существует версия второй теоремы о неполноте для Q (см. Bezboruah and Shepherdson 1976), однако по вопросу о том, действительно ли при настолько слабой Q можно принять соответствующее утверждение в ней за выражение непротиворечивости, согласие достигнуто не было (см. дискуссии Kreisel 1958, Bezboruah and Shepherdson 1976, Pudlák 1996, Franks 2009).

Теории, не сформулированные в языке арифметики

Конечно, в математике существует много важных и интересных теорий, которые даже не сформулированы в языке арифметики. Однако применимость теорем о неполноте может быть существенно расширена вне языка арифметики первого порядка и ее расширений, если отмечается, что необходимо лишь, чтобы слабые теории, такие как Q или PRA, могли интерпретироваться в обсуждаемой системе. Что самое важное, данный пункт включает различные системы теории множеств. Например, теоремы о неполноте сохраняют свою справедливость для ZFC–Inf (для ZFC без аксиомы бесконечности) и всех ее расширений, сколь бы сильными (при условии, что они аксиоматизируемы) они ни были.

Упрощенно говоря, теория T1 интерпретируема в другой теории T2, если примитивные понятия и диапазон переменных T1 определимы в T2 так, что можно перевести каждую теорему из T1 в теорему T2. Не следует думать, что такие интерпретации предоставляют нам нечто наподобие интуитивной синонимии. Две теории могут иметь радикально отличающиеся предполагаемые содержания, но поскольку они представляют собой формальные системы, одна из них может оказаться интерпретируемой в другой. (Так, простая генеалогия может быть представлена как формальная система, интерпретированная в арифметике; однако вполне очевидно, что прабабушки и т.п. в действительности не являются числами). Важно то, что интерпретируемость сохраняет некоторые элементарные формальные свойства теорий, а главное — последовательность: если T1 интерпретируема в T2, а T2 непротиворечива, то T1 также непротиворечива. И любая система, в рамках которой возможно проинтерпретировать Q, гарантированно будет существенно неполной. Для любой подобной теории неполнота может быть доказана и непосредственно; например, в различных теориях теории множеств можно кодировать формулы и выводы вместо чисел множествами — «множествами Гёделя» — и далее действовать как обычно (см., напр., Fitting 2007). Однако для большинства задач гораздо проще установить интерпретируемость Q в рассматриваемой теории.

В целом, когда утверждается, что «в системе может быть выполнено некоторое количество действий элементарной арифметики», подразумевается либо то, что система служит аксиоматизируемым расширением Q, либо то, что Q можно в ней интерпретировать. (В случае (стандартных доказательств) второй теоремы о неполноте следует заменить Q на PRA).

Некоторые исключения: полные теории

С другой стороны, не все теории арифметики неполны. Например, теория, включающая лишь сложение натуральных чисел, но не умножение (часто называемая «арифметикой Пресбургера»), полна (и разрешима) (Presburger 1929), так же как и теория умножения положительных целых чисел Скулема (Skolem 1930). Эти теории, однако, крайне слабы. Но в любом случае требуется по меньшей мере теория, в которой рассматриваются и сложение, и умножение. Значительно интереснее то, что естественная первопорядковая теория арифметики действительных чисел (как со сложением, так и с умножением), так называемая теория вещественно замкнутых полей (RCF), полна и разрешима, как показал Тарский (Tarski 1948); он также продемонстрировал, что первопорядковая теория евклидовой геометрии в том числе является полной и разрешимой. Таким образом, следует иметь в виду, что существуют некоторые нетривиальные интересные теории, в отношении которых теоремы Гёделя неприменимы.

Релевантность тезиса Чёрча — Тьюринга

Гёдель первоначально установил лишь неполноту конкретной, хотя и довольно развернутой формализованной теории P, варианта теории типов Рассела — системы PM (от Principia Mathematica, см. разделы «Парадоксы и теории типов Рассела» в статьях по теории типов и Principia Mathematica), и всего расширения P с тем же языком, чье множество аксиом примитивно-рекурсивно. Он также предположил, хотя и не подтвердил, что доказательство может быть адаптировано для применения также в стандартных аксиоматических системах теории множеств, таких как ZFC. Хотя выясняется, что Гёдель на самом деле уже обладал довольно общим по своему характеру результатом, в то время было неясно, о какой именно общности на деле идет речь (см. также раздел 5).

Для характеризации понятия произвольной формальной системы недоставало анализа интуитивного представления о разрешимости. Напомним, что множество аксиом и отношение доказательства формализованной системы должны быть разрешимыми. Математики и логики с древности неявно использовали интуитивное понимание метода решения, и, пока кто-либо искал положительное решение, было достаточно, чтобы один из них предложил конкретный метод, который интуитивно был бы воспринят всеми как механический. Однако для общих предельных результатов, таких как общие теоремы неполноты или результаты неразрешимости (см. 4.2), потребуется точная математическая экспликация понятия. Вместо разрешимых множеств или свойств зачастую рассматриваются эффективные или вычислимые функции либо операции, но на самом деле это всего лишь две стороны одной медали: обсуждение одних можно легко перевести в разговор о других.

Гёдель (Gödel 1934), Алонзо Чёрч (Church 1936a, 1936b) и Алан Тьюринг (Turing 1936–7) независимо друг от друга пришли к разным проектам точного математического определения вычислимых функций и, следовательно, разрешимых множеств (чисел). Однако эти проекты оказались эквивалентными. Обстоятельный понятийный анализ Тьюринга, в котором использовались вымышленные и абстрактные вычислительные машины (в настоящее время их принято называть «машины Тьюринга»; см. статью о машинах Тьюринга), был особенно важен, как подчеркивал сам Гёдель (см., напр., Gödel 1963). Уравнение интуитивного понятия вычислимости и некоторых из этих математических интерпретаций часто называют тезисом Чёрча — Тьюринга. Термин «рекурсивная функция» по историческим причинам преобладал в текстах по логике. В этой связи разрешимые множества нередко называют «рекурсивными множествами». (См. статьи о вычислимости, рекурсивных функциях и тезисе Чёрча — Тьюринга.)

Чтобы правильно понять результаты, касающиеся неполноты и неразрешимости, важно уловить разницу между двумя ключевыми представлениями, связанными со множествами. Во-первых, может существовать механический метод, который решает, принадлежит ли какое-либо данное число рассматриваемому множеству или нет (в этом случае множество называется разрешимым или рекурсивным). Во-вторых, может существовать механический метод, который порождает или перечисляет элементы множества от числа к числу. В последнем случае множество именуется рекурсивно перечислимым (r.e.), то есть его можно эффективно сгенерировать либо же оно «полуразрешимо». Это фундаментальный результат теории вычислимости (или «теории рекурсивных функций»), согласно которому существуют полуразрешимые множества, которые могут быть эффективно сгенерированы (рекурсивно перечислимы), но не разрешимы (не рекурсивны). Фактически в этом и состоит сущность первой теоремы о неполноте на самом абстрактном уровне. Однако если оба множества и их дополнение рекурсивно перечислимы, множество рекурсивно, то есть разрешимо.

Первая теорема о неполноте

В этом разделе приведены основные шаги доказательства первой теоремы о неполноте.

Предварительные замечания

Формальный терм («нумерал»), канонически обозначающий натуральное число n, сокращенно изображается как n. В используемом здесь стандартном языке арифметики число n обозначается термом 0′…′, где символ следования «′» повторяется n раз. То есть цифры 1, 2, 3, … выглядят как 0′, 0′′, 0′′′, … и сокращаются до 1, 2, 3, …

В первоначальном доказательстве Гёдель использовал свое специфическое понятие ω-непротиворечивости, и в некоторых контекстах по-прежнему удобно следовать его первоначальному подходу. Формализованная теория F является ω-непротиворечивой, если для некоторой формулы A(x) неверно, что и F ⊢¬A(n) для всех n, и F ⊢ ∃xA(x). ω-непротиворечивость естественным образом подразумевает обыкновенную непротиворечивость и следует из допущения, что натуральные числа удовлетворяют аксиомам F.

На самом деле здесь достаточно простого частного случая ω-непротиворечивости: допущение необходимо только в отношении того, что логики называют -формулами; упрощенно говоря, это чисто экзистенциальные формулы; если точнее, формулы вида ∃x1∃x2…∃xnA, где A не содержит неограниченных кванторов (A может содержать ограниченные кванторы всеобщности ∀x < t и ограниченные кванторы существования ∃x < t). Эта ограниченная ω-непротиворечивость называется 1-непротиворечивостью.

ω-непротиворечивость и 1-непротиворечивость представляют собой сугубо синтаксические понятия. Если допускается использование понятий истины и ложности, допущение 1-непротиворечивости может быть интуитивно выражено просто как требование, чтобы рассматриваемая формальная система не доказывала никаких ложных -предложений (то есть система состоятельна как минимум в случае таких предложений). С этого момента предполагается, что рассматриваемые формализованные системы содержат Q и считаются по крайней мере 1-непротиворечивыми, если не указано иное. 

Представимость

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

Множество S натуральных чисел сильно представимо в F, если существует формула A(x) языка F с одной свободной переменной x такая, что для любого натурального числа n:

n ∈ S ⇒ F ⊢ A(n); 

n ∉ S ⇒ F ⊢ ¬A(n), 

Множество S натуральных чисел слабо представимо в F, если существует формула A(x) языка F с одной свободной переменной x такая, что для любого натурального числа n:

n ∈ S ⇔ F ⊢ A(n); 

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

[Внимание! Здесь терминология в литературе сильно варьируется: «Сильную представимость» иногда именуют, например, «представимостью», «нумерической выражаемостью», «бинумеруемостью», «определимостью» или «сильной определимостью»; «слабая представимость», в свою очередь, также выражается, например, как «представимость», «определимость», «слабая определимость» или «нумеруемость». Здесь следует соблюдать осторожность и сосредоточиться на соответствующих определениях, а не позволять словам вводить в заблуждение.]

В случае обоих видов представимости (слабых и сильных) всегда существует простая экзистенциальная -формула, которая (слабо или сильно) представляет рассматриваемое множество, и обычно такая формула используется для представления S.

Хотя эти понятия относятся к формальной системе, оказалось, что сильная и слабая представимость чрезвычайно стабильны. Вполне независимо от выбранной конкретной формальной системы именно разрешимые или рекурсивные множества (или отношения) сильно представимы и именно полуразрешимые или рекурсивно перечислимые множества (отношения) представимы слабо. Это справедливо для всех формализованных систем, которые содержат арифметику Робинсона Q, от самой арифметики Робинсона до сильнейших аксиоматических систем теории множеств, таких как ZFC и далее (при условии, что они рекурсивно аксиоматизируемы). Вместо того, чтобы использовать понятие «представимости», Гёдель придерживался иного подхода. Он утверждал, что множества «разрешимы в формальной системе F» («entscheidungsdefinit»). Если доказательства F систематически производятся, в конечном итоге для любого заданного числа n будет определено, принадлежит ли оно S или нет — если S сильно представима в F. 

В итоге перед нами:

Теорема представимости

В любой непротиворечивой формальной системе, содержащей Q: 

множество (или отношение) сильно представимо тогда и только тогда, когда оно является рекурсивным; 

множество (или отношение) слабо представимо тогда и только тогда, когда оно рекурсивно перечислимо. 

Оба понятия представимости — сильное и слабое — должны четко отличаться от простой определимости (в стандартном смысле слова). Множество S определимо на языке арифметики, если в языке есть такая формула A(x), что A(n) истинно в стандартной структуре натуральных чисел (в предполагаемой интерпретации), если и только если n ∈ S. Существует большое количество множеств, которые могут быть определены на языке арифметики, но не представимы (даже слабо) в любой F, таких как множество непротиворечивых формул, множество предложений, недоказуемых в системе F, или множество диофантовых уравнений без решений (см. ниже).

Арифметизация формального языка

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

Упрощенно говоря, происходит нечто следующее. Во-первых, примитивные символы языка сопрягаются с различными натуральными числами, «номерами символов». Затем достаточно прибегнуть к теории чисел, чтобы кодировать последовательности номеров единичными номерами. Далее, правильно построенным формулам, как последовательностям примитивных символов, присваивается уникальный номер. Наконец, выводы или доказательства системы, являющиеся последовательностями формул, арифметизируются, и им также присваиваются конкретные номера. Такой код, «гёделев номер» формулы A, обозначается как ⌈A⌉ (и аналогично для выводов).

Синтаксические свойства, отношения и операции отражаются таким образом в арифметике: например, neg(x) — это арифметическая функция, переводящая гёделев номер формулы в гёделев номер ее отрицания; другими словами, neg(⌈A⌉) = (⌈¬A⌉); аналогично, impl(x,y) — функция, отображающая гёделевы номера пары формул на гёделев номер импликации формул: impl(⌈A⌉,⌈B⌉) = ⌈A → B⌉; и т.д. Существует арифметическая формула, назовем ее Fmla(x), которая верна для n тогда и только тогда, когда n — гёделев номер правильно построенной формулы системы. Существует также арифметическая формула M(x, y, z), которая истинна только в том случае, если имеет место правильное применение правила вывода modus ponens для некоторых формул A и B с x = ⌈A⌉, y = ⌈A → B⌉ и z = ⌈B⌉; и т.д. Таким образом, синтаксические свойства и операции можно симулировать на уровне номеров, и, кроме того, они сильно представимы во всех теориях, которые содержат Q.

Ввиду разрешимости данной последовательности формул (по определению формальных систем), независимо от того, является ли она доказательством данного предложения, согласно правилам выбранной формальной системы F, бинарное отношение «x есть (гёделев номер) доказательства формулы (с гёделевым номером) y» может быть сильно представлено во всех системах, содержащих Q, и, следовательно, в F в частности. Обозначим формулу, которая строго представляет это отношение в самой F, как PrfF(x, y). Свойство обладания доказуемостью в F можно далее определить как ∃xPrfF(x, y). Сократим формализованный предикат доказуемости до ProvF(x). Отсюда следует, что последнее слабо (хотя и не сильно, как выясняется) представимо:

F ⊢ A ⇒ F ⊢ ProvF(⌈A⌉). 

Всегда можно выбрать предикат доказуемости ProvF(x) в качестве -формулы.

Диагонализация или «самореференция»

Следующим и, возможно, несколько неожиданным компонентом доказательства Гёделя является важная приводимая ниже лемма (мы все еще предполагаем, что F — формальная система, содержащая Q):

Лемма диагонализации

Пусть A(x) — произвольная формула языка F только с одной свободной переменной. Тогда предложение D может быть построено механически таким образом, что 

F ⊢ D ↔ A(⌈D⌉). 

В литературе лемму иногда также называют «самореферентной леммой» или «леммой о неподвижной точке». Она имеет много важных приложений помимо теорем о неполноте.

Зачастую утверждают, что при данном свойстве, обозначенном A(x), предложение D является самореферентным предложением, которое «говорит о себе» то, что оно обладает свойством A. Такие фигуры речи могут быть эвристически полезны, но они также легко могут ввести в заблуждение и предполагать слишком многое. Например, следует обратить внимание на то, что лемма лишь обеспечивает (доказуемую) материальную эквивалентность D и A(⌈D⌉) (которая гласит, что обе стороны должны иметь одно значение истинности) и не претендует на установление какого-либо тождества предметного значения. В частности, D и A (⌈D⌉) ни в коем случае не являются тождественными, равно как и ⌈D⌉ и ⌈A(⌈D⌉)⌉. 

Первая теорема о неполноте — завершение доказательства

Для завершения доказательства к отрицательному предикату доказуемости ¬ProvF(x) применяется лемма диагонализации: в итоге мы получаем предложение GF такое, что

(G) F ⊢ GF ↔ ¬ProvF(⌈GF⌉). 

Таким образом, даже в рамках F можно показать, что предложение GF истинно тогда и только тогда, когда оно недоказуемо в F.

Нетрудно показать, что GF недоказуемо и неопровержимо в F, если F только 1-непротиворечива. 

Для первой половины предположим, что GF предсказуемы. Тогда, благодаря слабой представимости доказуемости-в-F для ProvF(x), F также докажет ProvF(⌈GF⌉). Однако, поскольку F фактически также доказывает эквивалентность (G), то есть F ⊢ GF ↔ ¬ProvF(⌈GF⌉), F также докажет ¬GF. Но это будет означать, что F противоречива. В общем случае, если F непротиворечива, то GF недоказуемо в F. Для первой половины достаточно допущения простой непротиворечивости F.

Для второй половины следует предположить, что F 1-непротиворечива (если ProvF(⌈GF⌉) выбран так, что является -предложением, иначе потребуется более общее допущение ω-непротиворечивости).

Предположим, что F ⊢ ¬GF. Тогда F не может доказать GF, иначе F была бы просто противоречива. Следовательно, никакое натуральное число n не является гёделевым номером доказательства GF, и поскольку отношение доказательства сильно представимо, для всех n верно, что F ⊢¬ PrfF(n, ⌈GF⌉). Если также F ⊢ ∃xPrfF(x, ⌈GF⌉), F не является 1-непротиворечивой, вопреки допущению. Поэтому F не доказывает ∃xPrfF(x, ⌈GF⌉), другими словами, по определению ProvF(x), F не доказывает ProvF(⌈GF⌉). Согласно ключевой эквивалентности (G), F также не доказывает ¬GF.

Первая теорема Гёделя о неполноте

Предположим, что F — формализованная система, содержащая арифметику Робинсона Q. Тогда из F можно механически построить такое предложение GF языка F, что: 

Если F непротиворечива, то F ⊬ GF. 

Если F непротиворечива, то F ⊬ ¬GF .

Такое независимое или «неразрешимое» (ни доказуемое, ни опровержимое в F) предложение GF в F часто называют «гёделевым предложением» F.

На самом деле в благоприятных обстоятельствах можно показать, что GF истинно, при условии, что F действительно непротиворечива. Это имеет место, если, например, предикат доказуемости ProvF(x) был выбран в качестве -формулы. Тогда гёделево предложение доказуемо эквивалентно универсальной формуле ∀x¬PrfF(x, ⌈GF⌉). Такие формулы могут быть доказаны как ложные, если фактически являются ложными: если они ложны, то найдется число n такое, что F ⊢ PrfF(n, ⌈GF⌉) (это уже выполняется в Q). Тем не менее это бы противоречило теореме о неполноте. А значит, GF не может быть ложным и должно быть истинным. По этой причине гёделево предложение нередко называют «истинным, но недоказуемым».

Здесь не следует путать: «теорема Гёделя» — общий результат Гёделя, касающийся неполноты, который относится к большому классу формальных систем, а «гёделево предложение» — это построенное формально неразрешимое предложение, которое варьируется от одной формальной системы к другой. Вот почему важно включить индекс F в GF. Более того, нельзя смешивать два разных смысла «неразрешимого» в этом контексте. С одной стороны, конкретное предложение, такое как гёделево предложение, может быть неразрешимым в смысле независимости — ни доказуемым, ни опровержимым в выбранной системе. С другой стороны, теория может быть неразрешимой (см. ниже) в том смысле, что не существует метода решения для определения того, выводимо ли произвольное данное предложение языка в теории (так что второе значение «неразрешимости» затрагивает, так сказать, бесконечный класс утверждений).

В неформальных объяснениях первой теоремы о неполноте часто говорят, что гёделево предложение GF «само говорит о себе, что оно недоказуемо». Однако такие неточные заявления должны восприниматься по меньшей мере с долей скепсиса. По ряду причин можно заключить, что как минимум в целом гёделевы предложения действительно не говорят ничего содержательного о себе (Milne 2007 — тщательный анализ таких вопросов); например, как отмечалось ранее в случае леммы диагонализации, обычно мы здесь имеем дело только с материальными эквивалентностями.

Усовершенствование Россера — от ω-непротиворечивости до непротиворечивости

В 1936 году Дж. Баркли Россер сделал важное усовершенствование, позволяющее избавиться от несколько неуклюжего допущения ω-непротиворечивости в доказательстве первой теоремы Гёделя. С этой целью Россер представил новый и несколько искусственный «предикат доказуемости» Prov*(x), который был построен, если говорить неформально, следующим образом:

Существует такое y, что y — гёделев номер доказательства формулы с гёделевым номером x,

И

не существует z, меньшего чем y, для которого z является гёделевым номером доказательства отрицания формулы с гёделевым номером x.

Более формально:

Prov*(x) =def ∃y[PrfF(y, x) ∧ ∀z < y(¬PrfF(z, neg(x)))], 

где PrfF(y, x) — более стандартное отношение доказательства, обсуждавшееся ранее.

Таким образом, если рассматриваемая формальная система F действительно непротиворечива, предикат доказуемости Россера коэкстенсионален с обычным предикатом доказуемости. Применение леммы диагонализации к отрицанию предиката доказуемости Россера Prov*(x) дает:

Модификация Россера первой теоремы (Rosser 1936)

Пусть F — непротиворечивая формализованная система, содержащая Q. Тогда существует предложение RF языка F такое, что ни RF, ни ¬RF не доказуемы в F. 

Неполнота и нестандартные модели

Было бы полезно рассмотреть первую теорему о неполноте также с позиций теоретико-модельной перспективы, хотя сама теорема этого никоим образом не требует. А именно, можно заключить, что любая теория F, удовлетворяющая условиям теоремы, должна содержать помимо предполагаемой интерпретации или «стандартной модели» (в случае арифметических теорий — структуры натуральных чисел) непредполагаемые интерпретации или «нестандартные модели» — никакая такая теория не может исключить последние и однозначно установить предполагаемую интерпретацию. Так, если существуют независимые утверждения, такие как GF, то F должна включать и модели, удовлетворяющие GF, и модели, которые отвечают скорее ¬GF. Поскольку ¬GF эквивалентно ∃xPrfF(x, ⌈GF⌉), последние модели должны обладать элементами, которые удовлетворяют формуле PrfF(x, ⌈GF⌉). И все же мы знаем, что для любого нумерала n система F может доказать ¬PrfF(n, ⌈GF⌉), коль скоро PrfF(x, y) сильно представляет отношение доказательства. Поэтому никакое натуральное число n не может удостоверить формулу. Отсюда следует, что любая такая нестандартная модель должна содержать помимо натуральных чисел (обозначений нумералов n) и после них «бесконечные» ненатуральные числа.

Изучение нестандартных моделей начиналось не с результатов Гёделя. Скулем, в частности, уже был осведомлен о них ранее в другом контексте (в Skolem 1922 он выяснил, что теории первого порядка, описывающие теорию множеств, имеют неестественно малые, а именно счетные модели; ср. статья о парадоксе Скулема). Однако первая теорема о неполноте объясняет существование нестандартных моделей в контексте арифметики, в то время как нестандартные модели уточняют первую теорему о неполноте. Нестандартные модели с тех пор стали обширной областью исследований в математической логике (см., напр., Булос, Джеффри 1994: гл. 17; Kaye 1991).

Вторая теорема о неполноте

Предварительные замечания

Неформально рассуждения, приводящие ко второй теореме о неполноте, относительно просты. Когда дан предикат арифметизированной доказуемости, также легко представить утверждение об арифметизированной непротиворечивости: выберем некоторую явно противоречивую формулу (в арифметических теориях стандартный выбор — (0 = 1)); обозначим ее через ⊥; непротиворечивость системы (ее арифметизированный аналог) можно затем определить как ¬ProvF(⌈⊥⌉). Сократим формулу до Cons(F). Таким образом, доказательство первой части первой теоремы о неполноте (вышеприведенный случай) может быть в принципе формализовано в рамках F (на практике это, конечно, было бы сложно осуществить). Тем самым мы получаем:

F ⊢ Cons(F) → GF, 

где GF — гёделево предложение для F, заданное первой теоремой. Если Cons(F) была доказуема в F, то и GF тоже (здесь логика элементарна). Это противоречило бы первой теореме Гёделя. Следовательно, Cons(F) нельзя доказать и в F.

Вторая теорема Гёделя о неполноте

Предположим, что F является непротиворечивой формализованной системой, которая содержит элементарную арифметику. Тогда F ⊬ Cons(F). 

Следует упомянуть важный философский вопрос, возникающий в данном контексте. В ее нынешнем виде вторая теорема о неполноте Гёделя устанавливает недоказуемость одного предложения, Cons(F). Но действительно ли оно выражает, что F непротиворечива? (Ср. замечание выше, что GF, строго говоря, не выражает собственную недоказуемость.) Кроме того, разве не могут существовать другие предложения, которые являются доказуемыми и также выражают непротиворечивость F?

Однако строгое доказательство второй теоремы в более общем виде, охватывающее все такие предложения, оказалось очень сложным. Основная причина состоит в том, что, в отличие от первой теоремы, для формализации требования непротиворечивости сгодится не любой экстенсионально подходящий предикат доказуемости. Способ представления имеет значение. Например, вышеуказанный предикат доказуемости Россера для этой задачи не подходит; можно доказать «непротиворечивость» F в F, если непротиворечивость выражается в терминах предиката доказуемости Россера. Таким образом, необходимо добавить ряд условий для предиката доказуемости, чтобы доказательство второй теоремы о неполноте работало. Вслед за Феферманом (Feferman 1960) принято говорить, что, хотя первая теорема и родственные ей обобщения являются экстенсиональными, вторая теорема является интенсиональной: должна наличествовать возможность считать, что Cons(F) в некотором смысле выражает непротиворечивость F, то есть оно действительно означает, что F непротиворечива.

 Условия выводимости

Доказательство второй теоремы о неполноте требует, чтобы предикат доказуемости в F удовлетворял ряду условий, которые используются в деталях доказательства. Существует несколько различных наборов условий, которые будут выполняться.

Первое подробное доказательство второй теоремы о неполноте (написанное в основном Бернайсом) появилось во втором томе «Оснований математики» (см. Гильберт, Бернайс 1982), хотя и только для одной конкретной теории, PA. Для предиката доказуемости оно использует довольно неудобный набор условий. Cкорее, они представляют собой технические леммы для нужд конкретного доказательства, чем какой-либо анализ «естественных» предикатов доказуемости. Значительно более элегантный, ставший уже стандартным список «условий выводимости» был представлен Лёбом (Löb 1955), хотя предполагаемое использование этих условий было несколько иным (см. ниже).

Условия выводимости Лёба

(D1) F ⊢ A ⇒ F ⊢ ProvF(⌈A⌉). 

(D2) F ⊢ ProvF(⌈A⌉) → ProvF(⌈ProvF(⌈A⌉)⌉). 

(D3) F ⊢ ProvF(⌈A⌉) ∧ ProvF(⌈A → B⌉) → ProvF(⌈B⌉). 

(D1) является просто повторением требования из доказательства первой теоремы о том, что доказуемость слабо представима. Упрощенно говоря, (D2) требует, чтобы вся демонстрация (D1) для предполагаемого предиката доказуемости ProvF могла сама быть формализована в рамках F. Наконец, (D3) требует, чтобы предикат доказуемости был замкнут относительно modus ponens.

Если предикат арифметизированной доказуемости действительно удовлетворяет этим условиям, то вторая теорема может быть доказана. Пусть GF вновь является гёделевым предложением для F, задаваемым первой теоремой. Достаточно легко показать, опираясь на условия выводимости, что:

F ⊢ GF ↔ Cons(F). 

Учитывая первую теорему о неполноте, мы сразу получаем недоказуемость Cons(F). 

Более того, Джерослоу (Jeroslow 1973) продемонстрировал с помощью остроумного приема, что на самом деле можно установить вторую теорему и без (D3). Однако в некоторых других случаях (например, при доказательстве теоремы Лёба; см. ниже) и в логике доказуемости все три условия по-прежнему необходимы.

Альтернативный подход Фефермана ко второй теореме

Относительно легко доказать соответствующий случай второй теоремы о неполноте при допущении, что предикат доказуемости для теории удовлетворяет условиям выводимости (или, согласно приему Джерослоу, как минимум D1 и D2). Однако на практике требуется установить, действительно ли предлагаемый предикат арифметизированной доказуемости удовлетворяет условиям в каждом случае, и обычно это длинный и утомительный процесс.

Данный недостаток среди прочего (см. Feferman 1997) привел Фефермана в конце 1950-х годов к поиску альтернативного подхода к второй теореме (см. Feferman 1960). Феферман подходит к проблеме в два этапа. Во-первых, он изолирует формулы ProvFOL(x), которые арифметизируют некоторое стандартное понятие выводимости в логике первого порядка, чтобы было можно установить одну выбранную формулу для доказуемости в логике. Вопрос о том, как представлено множество внелогических аксиом рассматриваемой системы, на данном этапе остается открытым. Во-вторых, Феферман ищет подходящее ограничение для представления аксиом. Среди формул языка арифметики он изолирует то, что он называет PR- и RE-формулами; первые соответствуют каноническим примитивно-рекурсивным (PR) определениям в арифметике, а вторые — экзистенциальным обобщениям первых. Каждое рекурсивно перечислимое (RE) множество может быть задано формулой последнего вида; это просто -формулы. Данные два класса легко отличить друг от друга по одной только синтаксической форме. (На самом деле, согласно теореме MRDP (см. ниже), вместо RE-формул можно было бы сосредоточиться на еще более простом классе диофантовых уравнений, связанных квантором существования.)

Выше мы отметили тот важный факт, что во всех арифметических теориях F, содержащих Q, множество сильно представимо в F тогда и только тогда, когда оно рекурсивно, а множество рекурсивно перечислимо, если и только если оно слабо представимо. Кроме того, всегда можно принять формулу, слабо или сильно представляющую множество, в качестве RE-формулы (т.е. -формулы, а по теореме MRDP — даже связанного квантором диофантова уравнения). Тогда естественно требовать, чтобы такой формулой было представлено множество внелогических аксиом рассматриваемой системы. Если арифметизированное определение множества гёделевых номеров аксиом отражает, каким образом аксиомы, в случае бесконечного их количества, определены индуктивно, то результирующая формула будет . (Для теорий, аксиоматизируемых с конечным числом аксиом, существует единственное представление аксиом в виде списка и, следовательно, единственное утверждение непротиворечивости относительно ProvFOL(x).) В отличие от определения того, выполняются ли условия выводимости, — относительно рутинной задачей является установление того факта, что данная формула, формализующая аксиомы, действительно имеет искомую форму ().

Теперь версия второй теоремы о неполноте, представленная в Feferman 1960, имеет следующий вид:

Вариант второй теоремы о неполноте (Feferman 1960)

Пусть F — непротиворечивое расширение PA, пусть AxF(x) — -формула, слабо представляющая аксиомы F, а Cons(F) — утверждение непротиворечивости, построенное из AxF(x) и ProvFOL(x). Тогда Cons(F) не доказуемо в F. 

Другие подходы ко второй теореме неполноты см. в Feferman 1982, 1989; Visser 2011. Некоторые философские проблемы, связанные со второй теоремой, см. в Detlefsen 1979, 1986, 1990, 2001; Auerbach 1985, 1992; Roeper 2003; Franks 2009 (см. также раздел о неполноте в статье о программе Гильберта).

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

Теорема Тарского о неопределенности истины

Гёдель впервые пришел к теоремам о неполноте (см. раздел 5 ниже), заметив, что истина (языка системы) должна быть неопределимой в системе — данный результат условно приписывают Тарскому (в силу того, что способ представления проблемы Тарским имеет ряд неоспоримых достоинств; см. Gómez Torrente 2004). Теперь рассмотрим результат в контексте подхода к истине Тарского.

Тарский четко разделял язык-объект (язык истины, состоятельность предложений которого стоит под вопросом) и метаязык, в котором описывается первый. Он также потребовал (см. статью об определениях истины по Тарскому), чтобы любое удовлетворительное определение истины True(x) для языка-объекта удовлетворяло его «Условию Т», то есть оно должно иметь в качестве следствия все эквивалентности («T-эквивалентности») вида

(T) True(⌈A⌉) ↔ B, 

где ⌈A⌉ — имя предложения объектного языка, а B — его перевод в метаязыке. Если метаязык идентичен языку-объекту или является его расширением, B просто является самим A, а T-эквивалентности имеют вид:

True(⌈A⌉) ↔ A. 

В свою очередь, теорема неопределенности показывает, что язык-объект и метаязык не могут совпадать, но должны быть самостоятельными.

Теорема неопределимости Тарского

Пусть F — непротиворечивая формализованная система, содержащая достаточное количество арифметики. Тогда на языке F нет такой формулы Tr(x), чтобы для любого предложения A языка F: 

F ⊢ Tr(⌈A⌉) ↔ A.

Идея доказательства: если бы существовала такая формула языка F, простое применение леммы диагонализации к ее отрицанию привело бы к парадоксальному предложению L (для «лжеца», см. парадокс лжеца):

F ⊢ ¬Tr(⌈L⌉) ↔ L,

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

Аналогично можно доказать, что множество истинных предложений F неопределимо в предполагаемой интерпретации F — в ставшем теперь стандартным смысле «определимости» (см. выше). 

Результаты, касающиеся неразрешимости

Средства, используемые при доказательстве теорем Гёделя, также дают различные важные результаты, касающиеся неразрешимости. Теория называется разрешимой, если множество ее теорем (выводимых в ней предложений) разрешимо, то есть (по тезису Чёрча — Тьюринга) рекурсивно. В противном случае теория неразрешима. Неформально разрешимость означает, что существует механическая процедура, позволяющая решить, является ли данное произвольное предложение языка теории теоремой или нет.

Если теория полна, она разрешима (схема доказательства: при данном предложении A систематически порождайте теоремы теории; по полноте, в итоге за конечное время будут произведены либо A, либо ¬A). Обратное, однако, не всегда выполняется: существуют неполные теории, которые разрешимы. И все же неполнота как минимум оставляет возможность неразрешимости. Более того, все теории, содержащие арифметику Робинсона Q (либо непосредственно, либо Q можно интерпретировать в них), являются и неполными, и неразрешимыми. Таким образом, для очень широкого класса теорий неполнота и неразрешимость связаны неразрывно.

Один из изящных и простых способов продемонстрировать неразрешимость расширений Q в общих чертах выглядит так. Пусть F — любая непротиворечивая теория, содержащая Q. Предположим тогда, что множество ее теорем разрешимо, то есть (согласно тезису Чёрча — Тьюринга) рекурсивно. Отсюда следует, что множество (гёделевых номеров) теорем F сильно представимо в самой F. Напомним, отсюда следует, что существует некоторая формула B(x) языка F такая, что не только F ⊢ B(⌈A⌉), когда F ⊢ A (что обеспечивает даже слабая представимость), но также и F ⊢¬B(⌈A⌉), когда F ⊬ A. Однако метод, использованный при доказательстве первой теоремы о неполноте, показывает к тому же, что всегда имеются предложения, для которых последнее не выполняется: можно построить гёделево предложение GB относительно B(x) для F такое, что:

(D) F ⊢ GB ↔ ¬B(⌈GB⌉). 

Как и ранее, отсюда вытекает, что F ⊬ GB. Предполагалось, что B(x) сильно представляет множество теорем, а значит, F ⊢ ¬B(⌈GB⌉), и потому, согласно (D), мы получаем F ⊢ GB — то есть противоречие. Следовательно, F должна быть неразрешима. 

Теория F именуется существенно неразрешимой, если любое ее непротиворечивое расширение в языке F неразрешимо. Приведенная выше схема доказательства фактически устанавливает, что Q существенно неразрешима. (Есть некоторые очень слабые теории, которые неразрешимы, но не существенно.)

Вспомним, что Q имеет только конечное число аксиом, и пусть AQ обозначает единичное предложение, состоящее из конъюнкции аксиом Q. Тогда для любого предложения B языка арифметики

Q ⊢ B тогда и только тогда, когда теоремой логики первого порядка является то, что AQ → B. 

Но тогда разрешающая процедура для первопорядковой логики предоставит разрешающий метод для Q. Однако последнее, как уже было показано, невозможно. Поэтому отсюда следует:

Теорема Чёрча

Логика предикатов первого порядка неразрешима. 

(Этот результат, касающийся неразрешимости, был впервые установлен в Church 1936a, 1936b; метод его получения через неразрешимость Q разработан в Tarski, Mostowski and Robinson 1953.)

Впоследствии было показано, что ряд теорий и проблем из разных областей математики неразрешимы (см., напр., Davis 1977; Murawski 1999: ch. 3). 

Принципы отражения и теорема Лёба

Эвристически можно взглянуть на гёделево предложение GF как на выражение собственной недоказуемости — высказывание типа «я не доказуемо», — однако, как уже подчеркивалось, такие утверждения должны приниматься с долей скепсиса. Леон Хенкин задал вопрос, является ли предложение, выражающее собственную доказуемость («я доказуемо»), истинным или ложным и доказуемо оно или нет (Henkin 1952). Георг Крайзель вскоре отметил, что это зависит от того, каким образом выражена доказуемость; с разными вариантами получаются противоположные ответы (Kreisel 1953). 

Статья Мартина Лёба (Löb 1955), дополненная комментариями рецензента, ознаменовала значительное продвижение на разных фронтах. Во-первых, она вводит условия выводимости Лёба, ныне стандартные, обсуждавшиеся ранее в контексте второй теоремы о неполноте. Во-вторых, в ней содержится решение Лёбом проблемы Хенкина, затрагивающей предложения, которые «выражают собственную доказуемость». В-третьих, она содержит обобщение, которое теперь называется «теоремой Лёба», хотя на деле Лёб приписал его анонимному рецензенту (которым оказался не кто иной, как сам Хенкин; всю историю см. в Smoryński 1991).

Чтобы правильно понять теорему Лёба, полезно сначала рассмотреть так называемые «принципы симметрии». Выше основное внимание уделялось выражению в рамках формальной системы того факта, что система непротиворечива, то есть Cons(F). Но, естественно, теория должна быть не просто непротиворечивой, но и состоятельной — должна доказывать только истинные предложения. Как следует выражать состоятельность системы — положение о том, что все выводимое в системе истинно? Если кто-либо захочет сделать это в языке самой системы, нельзя обойтись лишь одним утверждением, говорящим об этом, потому что в силу неопределимости истины в языке отсутствует подходящий предикат истинности. Различные ограниченные и неограниченные требования состоятельности могут, однако, быть выражены в форме схемы, в так называемых принципах отражения:

(Ref) ProvF(⌈A⌉) → A. 

Принимая A в качестве ⊥ и отмечая, что ⊥ опровержима в F, легко видеть, что принцип отражения влечет за собой непротиворечивость утверждения Cons(F), то есть ¬ProvF(⌈⊥⌉); следовательно, она вообще не может быть доказана в системе.

Схема также может быть ограничена. Например, эквивалент предположения о 1-непротиворечивости, или -достоверность, является принципом отражения, ограниченным -предложениями (т.е. предложение A в схеме должно быть Σ01-предложением). Или оно может быть ограничено универсальными -предложениями; и так далее.

Если точно, какие экземпляры схемы отражения фактически доказуемы в системе? Теорема Лёба дает точный ответ на этот вопрос (предполагая, что ProvF(x) удовлетворяет условиям выводимости):

Теорема Лёба 

Пусть A — произвольное предложение языка F. Тогда: F ⊢ ProvF(⌈A⌉) → A, если и только если F ⊢ A. 

Следовательно, вхождения состоятельности (принцип отражения), доказуемые в системе, относятся именно к предложениям, которые сами доказуемы в системе. Как следствие, это также определяет первоначальную проблему Хенкина: при условии, что предикат арифметизированной доказуемости вновь «нормален» (то есть удовлетворяет условиям выводимости Лёба), все предложения, «утверждающие собственную доказуемость», доказуемы.

На самом деле теорему Лёба можно доказать достаточно быстро, как следствие второй теоремы о неполноте. Крайзель также отметил, что в противоположном направлении вторая теорема о неполноте также легко может быть получена как следствие теоремы Лёба.

Десятая проблема Гильберта и теорема MRDP

Десятая из знаменитого списка Гильберта важных нерешенных проблем математики 1900 года касается метода решения так называемых диофантовых уравнений. Несмотря на малознакомый термин «диофантов», стоящее за ним содержание на самом деле элементарно. Рассмотрим любое уравнение с одной или несколькими переменными и с целыми коэффициентами, которое включает в себя только сложение и умножение, такое как x2 + y2 = 2 или 3x2 + 5y2 + 2xy = 0. Если искать решения с вещественными числами, обычно говорят просто об «уравнении». Однако в теории чисел обычно требуется поиск решения, состоящего только из целых чисел. Тем самым привносится большое различие. Первое из приведенных выше уравнений имеет бесконечное число решений среди действительных чисел, но только четыре целочисленных. Уравнение x2 + y2 = 3 также имеет бесконечно много действительных решений, но не имеет целочисленных. Когда основное внимание уделяется целочисленным решениям, речь идет о «диофантовых уравнениях» (по имени древнего теоретика чисел Диофанта Александрийского). 

Для прямого решения десятой проблемы Гильберта достаточно представить конкретный метод, который был бы «механическим» разрешающим методом. Новаторский анализ понятия разрешающего метода, проведенный Тьюрингом, сосредотачивался тем не менее на возможности отрицательного решения. Начиная с начала 1950-х годов Джулия Робинсон и Мартин Дэвис уже работали над данной проблемой, позже к ним присоединился Хилари Патнэм. По итогам их сотрудничества был достигнут первый важный результат в этом направлении. Уравнение называют экспоненциальным диофантовым уравнением, если оно включает в себя операции возведения в степень, а также сложение и умножение (в качестве показателей можно указать как постоянные, так и переменные); естественно, основное внимание уделяется целочисленным решениям. В Davis, Putnam and Robinson 1961 было показано, что проблема решаемости экспоненциальных диофантовых уравнений неразрешима. В 1970 году Юрий Матиясевич добавил последний недостающий фрагмент и продемонстрировал, что проблема решаемости диофантовых уравнений неразрешима. В итоге общий результат часто называют теоремой MRDP (по первым буквам фамилий авторов; изложение см., напр., в Davis 1973, Matiyasevich 1993).

Существенным формальным достижением было то, что всем полуразрешимым (рекурсивно перечислимым) множествам можно дать диофантово представление, то есть представить их простой формулой вида ∃x1…∃xn(s = t), где (s = t) выступает диофантовым уравнением. Точнее, для любого данного рекурсивно перечислимого множества S существует диофантово уравнение (s(y, x1, … , xn) = t(y, x1, … , xn)) такое, что n ∈ S тогда и только тогда, когда ∃x1…∃xn(s(n, x1, … , xn) = t(n, x1, … , xn)).

Поскольку существуют полуразрешимые (рекурсивно перечислимые) множества, которые неразрешимы (рекурсивны), сразу следует общий вывод: 

Теорема MRDP

Не существует общего способа определить, имеет ли данное диофантово уравнение решение. 

Отсюда также вытекает изящный вариант теорем о неполноте, касающихся диофантовых уравнений:

Следствие

Для любой 1-непротиворечивой аксиоматизируемой формальной системы F существуют диофантовы уравнения, которые не имеют решений, но для которых в F не может быть доказано, что они не имеют решений. 

(Вопрос об исключении требования 1-непротиворечивости здесь весьма сложен, см. Dyson, Jones and Shepherson 1982.)

Конкретные случаи недоказуемых утверждений

Неразрешимые предложения, представленные доказательствами Гёделя, являются (при расшифровке) чрезвычайно сложными формулами без интуитивного значения, истолковываемыми исключительно в целях доказательств незавершенности. Возникает вопрос, существуют ли простые и естественные математические утверждения, которые также неразрешимы в выбранных базовых теориях, например, в PA. В настоящее время существуют различные конкретные утверждения с ясным математическим содержанием, которые, как известно, неразрешимы в некоторых стандартных теориях (хотя вопрос о том, насколько они естественны, весьма спорный; см. Feferman 1989b). Ниже приведены некоторые хорошо известные естественные примеры начиная с некоторых вполне естественных математических утверждений, которые не зависят от PA, и заканчивая все более и более мощными теориями. Иногда такие результаты именуются вариантами теоремы Гёделя, а их доказательства независимости — альтернативными доказательствами теоремы Гёделя, однако считать их таковыми было бы ошибкой: какими интересными они бы ни были, они не обладают, собственно, той же общностью, что теоремы Гёделя, но только предоставляют утверждения, независимые от конкретной теории.

Нередко утверждается, что до знаменитой теоремы Пэриса —Харрингтона (см. ниже) такие естественные независимые математические утверждения не были известны. Однако, строго говоря, это неверно. Гораздо раньше, около 1935 года, Герхард Генцен высказал такое утверждение (см. статью об истории развития теории доказательств). Очень естественно обобщить идею индукции из области натуральных чисел в область порядковых чисел. В теории множеств такие обобщения называются принципами трансфинитной индукции. Хотя отдельные конструктивисты скептически относятся к легитимности полной теории множеств, существуют ограниченные и более конкретные случаи трансфинитной индукции (имеющие дело только с некоторыми четко определенными классами счетных порядковых чисел), которые вполне приемлемы даже с точки зрения конструктивистов или интуиционистов. Одним из важных случаев является принцип трансфинитной индукции вплоть до ординала ε0. Генцен показал, что непротиворечивость PA может быть доказана при допущении принципа трансфинитной индукции. Поэтому, как это следует из второй теоремы о неполноте, сам принцип в PA не может быть доказан (Gentzen 1936).

Теорема Рамсея является результатом бесконечной комбинаторики, установленным Фрэнком Рамсеем (Ramsey 1930), и рассматривает возможности «раскраски» для определенных графов. Джефф Пэрис и Лео Харрингтон сформулировали финитный вариант теоремы Рамсея и показали, что она недоказуема в PA (Paris and Harrington 1977). Это дает вполне естественную формулировку конечной комбинаторики, независимой от PA. Возможно, еще более чистым примером является теорема Гудстейна (Goodstein 1944), которая носит чисто теоретико-числовой характер. Она определяет некоторый естественный класс последовательностей натуральных чисел, которые сегодня называются «последовательностями Гудстейна». Теорема утверждает, что всякая последовательность Гудстейна в конечном итоге заканчивается нулем. Теорема Гудстейна, безусловно, является естественным математическим утверждением, поскольку она была сформулирована и доказана (очевидно, методами доказательства, выходящими за пределы PA) Гудстейном значительно раньше (в 1944 году), а в 1982-м было показано, что теорема недоказуема в PA (Kirby & Paris 1982). 

Переходя теперь к более сильным теориям за пределами PA, можно упомянуть, к примеру, теорему Крускала. Это теорема, касающаяся некоторых упорядочений конечных деревьев (Kruskal 1960). Харви Фридман показал, что эта теорема недоказуема даже в подсистемах арифметики второго порядка, которые намного сильнее, чем PA (см. Simpson 1985). В частности, она не доказуема ни в одной предикативно обоснованной теории (в широкой трактовке понятия «предикативность»; ср. раздел о предикативизме в статье о философии математики).

Существуют некоторые конкретные примеры математических утверждений, которые не были разрешены даже в более сильных теориях, в так называемой дескриптивной теории множеств. Эта область математики связана с топологией и была инициирована французскими полуинтуиционистами (Лебегом, Бэром, Борелем; см. раздел о дескриптивной теории множеств и т.п. в статье об интуиционизме в философии математики). Она изучает множества с относительно простыми определениями (в отличие от идей произвольных множеств и различных высших множеств подмножеств, которые полуинтуиционисты отвергли как бессмысленные), называемые проективными или аналитическими множествами. Классически они были определены как множества, которые могут быть построены из счетного пересечения открытых множеств из непрерывных отображений и дополнений конечное число раз; они совпадают с множествами, определяемыми на языке PA2. В частности, так называемые множества Бореля можно просто определить как формулой вида ∃XA(x), так и формулой вида ∀XB(x), где A и B не содержат каких-либо множественных переменных (в логической терминологии множества Бореля являются множествами Δ11). Аналогично определяется функция Бореля (см., напр., Martin 1977).

Харви Фридман предложил следующую теорему: упрощенно говоря, если S является множеством Бореля, то существует такая функция Бореля f, что граф f либо включен в S, либо не пересекается с S. Фридман показал, что эта простая формулировка недоказуема даже в полной арифметике второго порядка PA2, но доказательство данного факта обязательно потребует полной мощности ZFC (см. Simpson 1999). 

Кроме того, существовал традиционный вопрос дескриптивной теории множеств (который может быть сформулирован на языке арифметики второго порядка): все ли проективные множества (см. выше) измеримы по Лебегу. Он оставался открытым на протяжении многих десятилетий по веской причине: оказалось, что утверждение независимо даже от полной теории множеств ZFC (см. Solovay 1970). Только постулируя существование некоторых чрезвычайно больших кардиналов (так называемых кардиналов Вудина), можно доказать гипотезу о том, что все проективные множества являются измеримыми по Лебеку (это было достигнуто в результате работы над так называемой проективной определенностью; см. Woodin 1988; Martin and Steel 1988, 1989). 

Известен знаменитый результат Пола Коэна о том, что континуум-гипотеза не зависит от ZFC (Cohen, 1963, 1964). Однако это совсем иной случай. Во всех приведенных выше результатах независимости соответствующие утверждения остаются теоремами математики, принятыми истинными (последний случай, требующий аксиом больших кардиналов вне пределов ZFC, более спорный; тем не менее многие теоретики в области теории множеств находят такие аксиомы правдоподобными). Из первой теоремы о неполноте как таковой легко следует истинность недоказуемого утверждения при условии, что допущение о непротиворечивости системы верно. Однако в случае результата Коэна нет абсолютно никаких указаний на то, следует ли считать континуум-гипотезу истинной, ложной или, возможно, не имеющей истинностного значения. 

История вопроса и ранние отклики на теоремы о неполноте

Результаты Гёделя оказались неожиданными, но феномен неполноты в некотором роде таковым не был. Возможность неполноты в контексте теории множеств обсуждалась Бернайсом и Тарским уже в 1928 году, а фон Нейман, несмотря на преобладающие в программе Гильберта настроения, считал возможным, что логика и математика не являются разрешимыми. Сам Гёдель упомянул о возможности существования неразрешимой проблемы с вещественными числами в своей диссертации в 1929 году (см. Dawson 1985). Гильберт (Hilbert 1928), с другой стороны, предположил, что арифметика Пеано и другие стандартные теории являются полными. По-видимому, Гёдель был также впечатлен Брауэром, который в своей лекции в Вене в 1928 году предположил, что математика неисчерпаема и не может быть полностью формализована (см. Wang 1987 и раздел о взглядах Брауэра на программу формализма в статье о развитии интуиционистской логики).

Как бы то ни было, представляется, что в действительности Гёдель пришел к первым точным наблюдениям о незавершенности другим путем, пытаясь внести свой вклад в программу Гильберта, а не подорвать ее (см. Dawson 1997). А именно, в 1930 году Гёдель предпринял попытку продвинуть программу Гильберта, пытаясь доказать непротиворечивость анализа (или арифметики второго порядка) средствами арифметики и тем самым редуцировать непротиворечивость первого до непротиворечивости последней. В своем предполагаемом доказательстве Гёдель нуждался в понятии истины. Гёдель вскоре столкнулся с различными парадоксами (такими как парадокс лжеца) и вынужден был сделать вывод, что арифметическая истина не может быть определена в арифметике. Следовательно, Гёдель первым пришел к разновидности теоремы о неопределимости истинности, которую обычно связывают с Тарским (ср. Murawski 1998). Это дает слабую версию результата неполноты: множество предложений, доказуемых в арифметике, может быть определено в языке арифметики, но множество истинных арифметических предложений не может; поэтому они не могут совпадать. Более того, из допущения истинности всех доказуемых предложений следует, что должны существовать и недоказуемые истинные предложения. Однако этот подход не рассматривает какое-либо конкретное предложение.

Однако интеллектуальную среду Гёделя составлял Венскин кружок с его радикально антиметафизической позицией. В частности, даже понятие истины в то время считалось подозрительным или вовсе бессмысленным по крайней мере некоторыми логическими позитивистами (напр., Нейратом и Гемпелем). Поэтому Гёдель упорно старался исключить любое обращение к понятию истины и пытался обойтись без него. С данной целью он ввел понятие ω-непротиворечивости, которое может быть определено строго и чисто синтаксически. Это привело к созданию теорем о неполноте в том виде, в котором они теперь известны.

Что касается леммы диагонализации, то сам Гёдель изначально продемонстрировал только ее частный случай, то есть только для предиката доказуемости. Общая лемма была, по-видимому, впервые открыта в Carnap 1934 (см. Gödel 1934, 1935). Еще более общие версии для формул со свободными переменными были представлены в Ehrenfeucht and Feferman 1960 и Montague 1962 (см. Smoryński 1981).

Реакция на результаты Гёделя была смешанной. Некоторые важные фигуры в области логики и оснований математики довольно быстро усвоили результаты и осознали их значимость, но также было довольно много недоразумений и сопротивления (подробные разборы откликов см. в Dawson 1985, Mancosu 1999).

Гёдель показал свои результаты Карнапу в Вене 26 августа 1930 года и вскользь объявил о результате (первая теорема) в дискуссии на знаменитой Кенигсбергской конференции 7 сентября 1930 года. Джон фон Нейман, который находился в аудитории и в то время работал в контексте программы Гильберта, сразу же осознал огромную значимость открытия. 20 ноября он написал письмо Гёделю о «замечательном» следствии открытия Гёделя, который он обнаружил: недоказуемость непротиворечивости (вторая теорема). Тем не менее сам Гёдель обнаружил ту же идею и уже отправил для публикации окончательный вариант своей статьи, в котором теперь также содержалось утверждение второй теоремы о неполноте. Статья была опубликована в январе 1931 года (Gödel 1931; полезные вводные материалы к ней представлены в Kleene 1986 и Zach 2005). Начали распространяться эти результаты, по-видимому имевшие большое значение для основ математики, хотя взгляды на то, чему именно они учат, разнились. Пол Бернайс — возможно, самый значимый сотрудник Гильберта — проявил большой интерес к результатам, хотя поначалу ему было трудно понять их правильно. Его активная переписка с Гёделем также показывает, что Гёдель уже в то время полностью осознавал неопределимость истины.

Поскольку первоначальный подход Гёделя был сфокусирован на его конкретной, хотя и весьма развернутой системе P и ее (примитивно-рекурсивных) расширениях, ряд авторов сомневался в общности результатов Гёделя. Алонзо Чёрч, например, в письме к Гёделю в июле 1932 года предположил, что результаты Гёделя не будут применяться к его системе λ-конверсии (противоречивость системы была позже доказана Клини и Россером). Гёдель стремился обобщить свои открытия и распространил результаты на более широкий класс систем в статьях Gödel 1932, 1934. Он также предположил, что его методы применимы к стандартным системам теории множеств (однако только после удовлетворительной оценки разрешимости и тезиса Чёрча — Тьюринга несколько лет спустя, когда стало возможно дать полностью общую формулировку теорем о неполноте (см. выше); это было впервые сделано в Kleene 1936). Выдающийся теоретик в области теории множеств Эрнст Цермело выдвинул довольно резкую критику в отношении работы Гёделя, однако они также состояли в переписке по теме. Представляется, что у Цермело были серьезные трудности в понимании релевантных понятий и результатов.

В марте 1933 года Гёдель получил письмо от Пауля Финслера из Цюриха, который предположил, что он уже ранее (в Finsler 1926) занимался тесно связанной работой, но с более общей актуальностью. Гёдель ответил, что система Финслера на самом деле даже не определена. В разгоряченном ответе Финслер утверждал, что для изучения системы не требуется, чтобы она была четко определена, и что принципиальное различие между его идеями и идеями Гёделя отсутствует. Оглядываясь назад, можно с легкостью признать, что подходы Финслера и Гёделя радикально отличались: для работы Гёделя понятие формализованной системы было существенным, тогда как Финслер отвергал само это понятие как искусственно ограничительное. На самом деле далеко не очевидно, что идеи Финслера вообще имеют какой-либо смысл — несмотря на расплывчатые параллели с доказательством Гёделя.

С другой стороны, необходимо отметить, что открытий Гёделя в некоторых отношениях ожидал Эмиль Пост. Он пришел к краткой версии результатов неполноты, видимо, уже в 1922 году. В частности, Пост отметил, что его методы приводят к утверждению, неразрешимому в Principia Mathematica. Эти результаты, однако, были основаны на его собственной версии «тезиса Чёрча — Тьюринга», которой Пост был недоволен, и его работа по этой причине осталась неопубликованной. Она была издана намного позже в Post 1941. 

Достоверность теорем Гёделя оставалась предметом оживленных дискуссий в течение 1930-х годов (см. Dawson 1985). В 1939 году появился второй том «Основ математики» Гильберта и Бернайса, в котором, помимо прочего, было изложено подробное доказательство второй теоремы о неполноте. Впоследствии серьезное неприятие выводов Гёделя исчезло, по крайней мере среди тех, кто активно работал в области математической логики и оснований математики. Однако в философских кругах некоторое сопротивление осталось. Наиболее известный их представитель, Витгенштейн, сделал ряд критических замечаний относительно теоремы Гёделя в посмертно опубликованных «Замечаниях по основаниям математики». Преобладающая первоначальная реакция заключалась в том, что Витгенштейн просто не понял результат. Затем появились более благожелательные интерпретации, но тема остается предметом оживленных дискуссий (см. раздел о Гёделе и неразрешимых пропозициях в статье о философии математики Витгенштейна).

Философское значение — фактическое и предполагаемое

Философия математики

Среди различных областей философии теоремы Гёделя, очевидно, наиболее актуальны для философии математики. Прежде всего они создают, по крайней мере на первый взгляд, серьезные проблемы для программы Гильберта (этот вопрос достаточно подробно разобран в разделе о влиянии неполноты в статье о программе Гильберта). Опять же, они имеют важные последствия для интуиционизма (см. Гёдель 2014а, Gödel 1941, Raatikainen 2005).

Шли дискуссии по поводу того, действительно ли теоремы Гёделя окончательно опровергают логицизм (см. статью о логицизме). Хенкин (Henkin 1962) и Масгрейв (Musgrave 1977), например, утверждают, что это так; Стернфельд (Sternfeld 1976) и Родригес-Консуэгра (Rodríguez-Consuegra 1993) с ними не согласны (см. также Hellman 1981, Raatikainen 2005).

Сам Гёдель разработал аргумент против конвенционалистской философии математики логического позитивизма, в частности Карнапа, на основании результатов неполноты (Gödel 1953/9). Этот вопрос обсуждался в публикациях Goldfarb and Ricketts 1992; Ricketts 1995; Goldfarb 1995; Crocco 2003; Awodey and Carus 2003, 2004; Tennant 2008. 

Самоочевидные и аналитические истины

Можно также предложить более общие эпистемологические интерпретации теорем Гёделя. Куайн и Уллиан, например, рассматривают традиционную философскую картину, согласно которой все истины могут быть доказаны самоочевидными шагами из самоочевидных истин и наблюдений. Затем они показывают, что даже истины элементарной теории чисел, по-видимому, вообще не выводятся самоочевидными шагами из самоочевидных истин (Quine and Ullian 1978). В свою очередь, Хилари Патнэм (Putnam 1975) утверждает, что при определенном естественном понимании «аналитичности» из теорем Гёделя следует, что в математике должны существовать и синтетические истины. На самом деле сам Гёдель замечал в очень схожем ключе, что даже теория целых чисел явно неаналитична (Гёдель 2014б).

«Гёделева» аргументация против механицизма

Неоднократно предпринимались попытки применить теоремы Гёделя с тем, чтобы показать, что силы человеческого сознания опережают любой механизм или формальную систему. Такая «гёделева» аргументация против механицизма рассматривалась еще Тьюрингом в конце 1940-х годов, даже если лишь затем, чтобы опровергнуть ее (см. Piccinini 2003). Из теорем о неполноте был сделан неуточненный антимеханистический вывод в широко распространенном популярном изложении «Теорема Гёделя» в 1958 году (Нагель, Ньюмен 2010). Вскоре после этого Дж. Р. Лукас провозгласил, что теорема о неполноте Гёделя

По его словам:

Совсем недавно аналогичные утверждения были высказаны Роджером Пенроузом (Пенроуз 2003, 2005). Джон Сёрл (Searle 1997) присоединился к обсуждению и частично защитил Пенроуза от его критиков. Криспин Райт (Wright 1994, 1995) придерживался схожих идей с интуиционистской позиции (критику см. в Detlefsen 1995). Все они настаивают на том, что в теоремах Гёделя подразумевается, что человеческое сознание бесконечно превосходит мощность любой конечной машины или формальной системы.

Однако подобная гёделева антимеханицистская аргументация проблематична, и существует широкий консенсус в отношении того, где она терпит неудачу. Стандартное опровержение звучит примерно так (это возражение восходит к Патнэм 1999, см. также Boolos 1968, Shapiro 1998): данная аргументация предполагает, что для любой формализованной системы (или конечной машины) существует гёделево предложение, которое недоказуемо в рамках этой системы, но чья истинность доступна человеческому сознанию. Тем не менее теорема Гёделя имеет в действительности условную форму, и предполагаемая истинность гёделева предложения с позиций системы зависит от допущения ее непротиворечивости. А значит, антимеханицистская аргументация требует, чтобы человеческое сознание также всегда могло видеть, является ли некоторая данная формализованная теория непротиворечивой. Однако это крайне неправдоподобно (ср. Davis 1990). Лукас, Пенроуз и другие попытались ответить на такую критику (см., напр., Lucas 1996; Penrose 1995, 1997). Обстоятельную критику Пенроуза см. в работах Boolos 1990; Davis 1990, 1993; Feferman 1995; Lindström 2001; Pudlák 1999; Shapiro 2003; многие из этих соображений также актуальны в отношении утверждений Лукаса.

Гёдель и Бенасерраф о механицизме и платонизме

Интересно, что сам Гёдель также представил аргумент против механицизма, хотя он был более осторожен, и эта работа была опубликована только посмертно (в т. III собрания сочинений в 1995 году). В своей Гиббсовской лекции 1951 года Гёдель выводит следующее дизъюнктивное заключение из теорем неполноты: 

Либо… человеческий ум (даже в области чистой математики) бесконечно превосходит возможности любой конечной машины, или же существуют абсолютно неразрешимые диофантовы проблемы… (Гёдель 2014в: 177)

Гёдель говорит об этом утверждении как о «математически установленном факте» (Гёдель 2014в: 177, более подробное обсуждение дизъюнктивного заключения Гёделя см., напр., в Shapiro 1998). Согласно Гёделю, вторая альтернатива 

…кажется, опровергает взгляд, что математика является нашим собственным творением… <…> …математические объекты и факты… существуют объективно и независимо от наших ментальных актов и решений… (Гёдель 2014в: 180)

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

Гёдель оказался, в отличие от более поздних сторонников так называемого гёделевского антимеханицистского аргумента, достаточно восприимчив, чтобы признать, что и механицизм, и его альтернатива, согласно которой существуют абсолютно нерешаемые с человеческой точки зрения проблемы, не противоречат теоремам о неполноте. Фундаментальные причины неприятия им последней альтернативы значительно более философичны. Гёдель, по-видимому, предположил, что человеческий ум был бы фатально иррациональным, если бы он задавал вопросы, на которые не смог бы ответить (критический разбор см. в Kreisel 1967, Boolos 1995, Raatikainen 2005).

В ответ на аргумент Лукаса, но до публикации Гиббсовской лекции Гёделя, Пол Бенасерраф (Benacerraf 1967) привел более уточненные заключения, которые весьма напоминают некоторые идеи Гёделя. По его утверждению, факты согласуются с тем, что я действительно являюсь машиной Тьюринга, но при этом нельзя определить, какой именно из машин. Критическое обсуждение см. в Chihara 1972 и Hanson 1971.

Мистицизм и существование Бога?

Иногда из теорем Гёделя извлекаются весьма фантастические выводы. Было даже высказано предположение, что теоремы Гёделя если не доказывают, то по крайней мере создают существенную поддержку мистицизму или существованию Бога. Эти трактовки, по-видимому, предполагают одно или несколько недоразумений, которые уже обсуждались выше: либо допускается, что Гёдель представил абсолютно недоказуемое предложение, либо же допускается, что теоремы Гёделя подразумевают платонизм, или антимеханицизм, или и то, и другое.

Более подробно о философских аспектах теорем о неполноте см. Raatikainen 2005 и Franzén 2005.

Библиография

На русском языке

Булос Дж., Джеффри Р. (1984) Вычислимость и логика. М.: Мир.

Гёдель К. (2014а) Современное положение дел в основаниях математики // Хинтикка Я., Гёдель К. О Гёделе. Статьи. М.: Канон+. С. 108–124.

–—. (2014б) Расселовская математическая логика // Хинтикка Я., Гёдель К. О Гёделе. Статьи. М.: Канон+. С. 125–165.

–—. (2014в) Некоторые основные теоремы в основаниях математики и их следствия // Хинтикка Я., Гёдель К. О Гёделе. Статьи. М.: Канон+. С. 166–200.

Гильберт Д., Бернайс П. (1982) Основания математики. М.: Наука. Т. 2. 

Нагель Э., Ньюмен Дж. (2010) Теорема Гёделя. М.: Красанд.

Патнэм Х. (1999) Сознание и машины // Он же. Философия сознания. М.: Дом интеллектуальной книги. С. 23–52.

Пенроуз Р. (2003) Новый ум короля. О компьютерах, мышлении и законах физики. М.: Едиториал УРСС.

–—. (2005) Тени разума. В поисках науки о сознании. М.; Ижевск: Институт компьютерных исследований.

На английском языке

Auerbach, David, 1985, “Intensionality and the Gödel theorems,” Philosophical Studies, 48 (3):337–51.

–––, 1992, “How to say things with formalisms,” in Proof, Logic, and Formalization, M. Detlefsen (ed.), London: Routledge, 77–93 [available online].

Awodey, S. & A.W. Carus, 2003, “Carnap versus Gödel on Syntax and Tolerance,” in Logical Empiricism: Historical and Contemporary Perspectives, P. Parrini et al. (eds.), Pittsburgh: University of Pittsburgh Press, pp. 57–64 [available online].

–––, 2004, “How Carnap Could Have Replied to Gödel,” in S. Awodey and C. Klein (eds.), Carnap Brought Home: The View from Jena, LaSalle, IL: Open Court, pp. 203–223 [available online].

Barzin, M., 1940, “Sur la portée du théorème de M. Gödel,” Académie Royale de Belgique, Bulletin de la Classe des Sciences, Series 5, 26: 230–39.

Benacerraf, P., 1967, “God, the Devil, and Gödel,” The Monist, 51: 9–32 [available online].

Bezboruah, A. and J.C. Shepherdson, 1976, “Gödel's Second Incompleteness Theorem for Q,” The Journal of Symbolic Logic, 41: 503–512.

Boolos, G., 1968, “Review of ‘Minds, Machines and Gödel’, by J.R. Lucas, and ‘God, the Devil, and Gödel’,” Journal of Symbolic Logic, 33: 613–15.

–––, 1990, “On ‘Seeing’ the Truth of Gödel Sentence,” Behavioral and Brain Sciences, 13: 655–656.

–––, 1995, “Introductory Note to *1951,” in Gödel 1995: 290–304.

Carnap, R., 1934, Logische Syntax der Sprache, Vienna: Julius Springer.

Chihara, C., 1972, “On Alleged Refutations of Mechanism Using Gödel's Incompleteness Results,” Journal of Philosophy, 69: 507–26.

Church, A., 1936a, “An Unsolvable Problem of Elementary Number Theory,” American Journal of Mathematics, 58: 354–363. Republished in Davis 1965, 89–107.

–––, 1936b, “A Note on Entscheidungsproblem,” Journal of Symbolic Logic, 1: 40–41; correction, ibid., 101–102. Republished in Davis 1965, 110–115.

Cohen, P. J., 1963, “The Independence of the Continuum Hypothesis I,” Proceedings of the National Academy of Sciences, (U.S.A.), 50(6): 1143–48.

–––, 1964, “The Independence of the Continuum Hypothesis II,” Proceedings of the National Academy of Sciences, (U.S.A.), 51(1): 105–110.

Crocco, G., 2003, “Gödel, Carnap, and the Fregean Heritage,” Synthese, 137: 21–41.

Davis, M., 1965, The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions, Hewlett, NY: Raven Press.

–––, 1973, “Hilbert's Tenth Problem is Unsolvable,” The American Mathematical Monthly, 80: 233–269.

–––, 1977, “Unsolvable Problems,” in Handbook of Mathematical Logic, J. Barwise (ed.), Amsterdam: North-Holland, pp. 567–594.

–––, 1990, “Is Mathematical Insight Algorithmic?” Behavioral and Brain Sciences, 13: 659–660.

–––, 1993, “How Subtle is Gödel's Theorem? More on Roger Penrose,” Behavioral and Brain Sciences, 16: 611–612.

Davis, M., H. Putnam, and J. Robinson, 1961, “The decision problem for exponential diophantine equations,” Annals of Mathematics (2), 74(3): 425–436.

Dawson, J., 1985, “The Reception of Gödel's Incompleteness Theorems,” PSA: Proceedings of the Biennial Meeting of the Philosophy of Science Association 1984, vol. II, pp. 253–271.

–––, 1997, Logical Dilemmas: The Life and Work of Kurt Gödel, Natick, MA: A. K. Peters.

Detlefsen, M., 1979, “On Interpreting Gödel's Second Theorem,” Journal of Philosophical Logic, 8(1): 297–313.

–––, 1986, Hilbert's Program: An Essay in Mathematical Instrumentalism, Dordrecht: Reidel.

–––, 1990, “On an Alleged Refutation of Hilbert's Program Using Gödel's First Incompleteness Theorem,” Journal of Philosophical Logic, 19(4): 343–377.

–––, 1995, “Wright on the Non-mechanizability of Intuitionist Reasoning,” Philosophia Mathematica, 3(1): 103–118.

–––, 2001, “What Does Gödel's Second Theorem Say?” Philosophia Mathematica, 9: 37–71.

Dyson, V., J.P. Jones, and J.C. Shepherdson, 1982, “Some Diophantine Forms of Gödel's Theorem,” Archiv für Mathematische Logik und Grundlagenforschung, 22: 51–60.

Ehrenfeucht, A. and S. Feferman, 1960, “Representability of recursively enumerable sets in formal theories”, Arch. Math. Logik Grundlag., 5(1–2), 37–41.

Feferman, S., 1960, “Arithmetization of Metamathematics in a General Setting,” Fundamenta Mathematicae, 49: 35–92.

–––, 1982, “Inductively Presented Systems and the Formalization of Meta-mathematics,” in Logic Colloquium ’80, D. van Dalen et al. (eds.), Amsterdam: North-Holland, pp. 95–128.

–––, 1989a, “Finitary Inductively Presented Logics,” in Logic Colloquium ‘88, R. Ferro, et al. (eds.), Amsterdam: North-Holland, pp. 191–220. [available online]

–––, 1989b, “Infinity in Mathematics: Is Cantor Necessary?” Philosophical Topics, 17(2): 23–45.

–––, 1995, “Penrose's Gödelian argument: A Review of Shadows of Mind, by Roger Penrose,” Psyche, 2 (7).

–––, 1997, “My Route to Arithmetization,” Theoria, 63: 168–181.

Finsler, P., 1926, “Formale Beweise und die Entscheidbarkeit,” Mathematische Zeitschrift, 25: 676–82.

Fitting, M., 2007, Incompleteness in the land of sets, London: College Publications. Series: Studies in logic ; v. 5.

Franks, C., 2009, The Autonomy of Mathematical Knowledge. Hilbert's Program Revisited, Oxford: Oxford University Press.

Gaifman, H., 2006, “Naming and Diagonalization, From Cantor to Gödel to Kleene,”Logic Journal of the IGPL, 14: 709–728. [available online]

Gentzen, G., 1936, “Die Widerspruchsfreiheit der reinen Zahlentheorie,” Mathematische Annalen, 112: 493–565.

Gödel, K., 1931, “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I,” Monatshefte für Mathematik Physik, 38: 173–198. English translation in van Heijenoort 1967, 596–616, and in Gödel 1986, 144–195.

–––, 1932, “Über Vollständigkeit und Widerspruchsfreiheit,” Ergebnisse eines mathematischen Kolloquiums, 3: 12–13. English translation “On Completeness and Consistency” in Gödel 1986: 235–7.

–––, 1934, “On Undecidable Propositions of Formal Mathematical Systems” (mimeographed lecture notes; taken by S. Kleene and J. Rosser), reprinted with corrections in Davis 1965, 41–81, and Gödel 1986, 346–371.

–––, 1935, “Review of Carnap 1934,” in Gödel 1986: 389.

–––, 1941, “In What Sense is Intuitionistic Logic Constructive?” in Gödel 1995: 189–200.

–––, 1953/9, “Is Mathematics a Syntax of Language?,” lecture manuscript (two versions), in Gödel 1995: 334–362.

–––, 1963, “Note added 28 August 1963” (to Gödel 1931), in Gödel 1986: 195.

–––, 1986, Collected Works I. Publications 1929–1936, S. Feferman et al. (eds.), Oxford: Oxford University Press.

–––, 1990, Collected Works II. Publications 1938–1974, S. Feferman et al. (eds.), Oxford: Oxford University Press.

–––, 1995, Collected Works III. Unpublished Essays and Lectures, S. Feferman et al. (eds.), Oxford: Oxford University Press.

Goldfarb, W., 1995, “Introductory Note to *1953/9,” in Gödel 1995: 324–334.

Goldfarb, W. and T. Ricketts, 1992, “Carnap and the Philosophy of Mathematics,” in Science and Subjectivity, D. Bell and W. Vossenkuhl (eds.), Berlin: Akademie Verlag, pp. 61–78.

Gómez Torrente, M., 2004, “The Indefinability of Truth in the Wahrheitsbegriff,”Annals of Pure and Applied Logic, 126(1–3): 27–37. [available online]

Goodstein, R., 1944, “On the Restricted Ordinal Theorem,” The Journal of Symbolic Logic, 9: 33–41.

Grelling, K., 1937, “Gibt es eine Gödelsche Antinomie?,” Theoria, 3: 297–306.

Hanson, W.H., 1971, “Mechanism and Gödel's theorems,” The British Journal for the Philosophy of Science, 22: 9–16.

Hellman, G., 1981, “How to Gödel a Frege-Russell: Gödel's Incompleteness Theorems and Logicism,” Nous, 15: 451–468.

Helmer, O., 1938, “Perelman versus Gödel,” Mind, 46: 58–60.

Henkin, L., 1952, “Problem,” The Journal of Symbolic Logic, 17: 160.

–––, 1962, “Are Mathematics and Logic Identical?” Science, 138: 788–794.

Hilbert, D., 1928, “Die Grundlagen der Mathematik,” Abhandlungen aus dem Mathematischen Seminar der Hamburgischen Universität, 6: 65–85. English translation in van Heijenoort 1967.

Jeroslow, R., 1973, “Redundancies in the Hilbert-Bernays Derivability Conditions for Gödel's Second Incompleteness Theorem,” Journal of Symbolic Logic, 38: 359–367.

Kaye, R., 1991, Models of Peano Arithmetic, (Oxford Logic Guides), Oxford: Clarendon Press.

Kirby, L. and J. Paris, 1982, “Accessible Independence Results for Peano Arithmetic,” Bull. London. Math. Soc., 14: 285–93.

Kleene, S.C., 1936, “General recursive functions of natural numbers,”, Mathematische Annalen 112(1): 727–742.

–––,1937a, “Review of Perelman 1936,” Journal of Symbolic Logic, 2: 40–41.

–––, 1937b, “Review of Helmer 1937,” Journal of Symbolic Logic, 2: 48–49.

–––, 1986, “Introductory note to 1930b, 1931 and 1932b”, in Gödel 1986, pp. 126–141.

Kreisel, G., 1953, “On a Problem of Henkin's,” Proc. Netherlands Acad. Sci. 56: 405–406.

–––, 1958, “Mathematical significance of consistency proofs,” The Journal of Symbolic Logic, 23: 159–182.

–––, 1967, “Mathematical Logic: What Has it Done For the Philosophy of Mathematics?” in Bertrand Russell: Philosopher of the Century, R. Schoenman (ed.), London: George Allen and Unwin.

Kruskal, J.B., 1960, “Well-quasi-ordering, the Tree Theorem, and Vazsonyi's Conjecture,” Transactions of the American Mathematical Society, 95 (2): 210–225.

Lindström, P., 2001, “Penrose's New Argument,” Journal of Philosophical Logic, 30(3): 241–250.

Lucas, J. R., 1961, “Minds, Machines, and Gödel,” Philosophy, 36(137): 112–137 [available online].

–––, 1996, “Minds, Machines, and Gödel: A Retrospect,” in Machines and Thought. The Legacy of Alan Turing, Vol. 1, P.J.R. Millican and A. Clark (eds.), Oxford: Oxford University Press, 103–124.

Löb, M. H., 1955, “Solution of a Problem of Leon Henkin,” Journal of Symbolic Logic, 20: 115–118.

Mancosu, P., 1999, “Between Vienna and Berlin: The Immediate Reception of Gödel's Incompleteness Theorems,” History and Philosophy of Logic, 20: 33–45.

Martin, D., 1977, “Descriptive Set Theory: Projective Sets,” in Handbook of Mathematical Logic, J. Barwise (ed.), Amsterdam: North-Holland, 783–815.

Martin, D. and Steel, J., 1988, “Projective Determinacy,” Proceedings of the National Academy of Sciences, (U.S.A.), 85: 6582–86.

–––, 1989, “A Proof of Projective Determinacy,” Journal of the A.M.S., 2: 71–125.

Matiyasevich, Y., 1970, “Diofantovost’ perechislimykh mnozhestv,” Dokl. Akad. Nauk SSSR, 191(2): 297–282 (Russian). (English translation, 1970, “Enumerable sets are Diophantine,” Soviet Math. Dokl., 11(2): 354–358.)

–––, 1993, Hilbert's Tenth Problem, Cambridge, MA: MIT Press.

Milne, P., 2007, “On Gödel Sentences and What They Say,” Philosophia Mathematica, 15: 193–226.

Montague, R., 1962, “Theories Incomparable with Respect to Relative Interpretability,” The Journal of Symbolic Logic, 27: 195–211.

Murawski, R., 1998, “Undefinability of Truth. The Problem of Priority: Tarski vs. Gödel,” History and Philosophy of Logic, 19: 153–160.

–––, 1999, Recursive Functions and Metamathematics: Problems of Completeness and Decidability, Gödel's Theorems, Dordrecht: Kluwer.

Musgrave, A., 1977, “Logicism Revisited,” British Journal for the Philosophy of Science, 28: 99–127.

Paris, J. and L. Harrington, 1977, “A Mathematical Incompleteness in Peano Arithmetic,” in Handbook of Mathematical Logic, J. Barwise (ed.), Amsterdam: North-Holland, pp. 1133–1142 [available online].

Paris, J. and L. Kirby, 1978, “Sn Collection Schema in Arithmetic,” in Logic Colloquium ’77, A. McIntyre et al. (eds.), Amsterdam: North-Holland, pp. 199–209.

Parsons, C., 1970, “On Number Choice Schema and its Relation to Induction,” in Intuitionism and Proof Theory, Kino et al. (eds.), Amsterdam: North-Holland, pp. 459–473.

Penrose, R., 1995, “Beyond the Doubting of a Shadow: A Reply to Commentaries of Shadows of the Mind,” Psyche, Vol 2.

–––, 1997, “On understanding understanding”, International Studies in the Philosophy of Science, 11: 7–20.

Perelman, C., 1936, “L'Antinomie de M. Gödel,” Académie Royale de Belgique. Bulletin de la Classe des Sciences (Series 5), 22: 730–36.

Piccinini, G., 2003, “Alan Turing and the Mathematical Objection,” Minds and Machines, 13: 23–48.

Post, E., 1941, “Absolutely Unsolvable Problems and Relatively Unsolvable Propositions: Account of an Anticipation,” published in Davis 1965, 338–433.

Presburger, M., 1929, “Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt,” Sprawozdanie z I Kongresu Matematyków Krajów Slowiańskich, (= Comptes-rendus du I Congrès Mathématiciens des Pays Slaves), Warsaw, pp. 92–101. English translation, 1991,“On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operation,”History and Philosophy of Logic, 12(2): 225–232.

Pudlák, P., 1996, “On the Length of Proofs of Consistency,” Collegium Logicum, Annals of the Kurt-Gödel-Society, 2: 65–86.

–––, 1999, “A Note on Applicability of the Incompleteness Theorem to Human Mind,” Annals of Pure and Applied Logic, 96: 335–342.

Putnam, H., 1975, “What is Mathematical Truth?” Historia Mathematica, 2: 529–545. Reprinted in H. Putnam, 1975, Mathematics, Matter and Method. Philosophical Papers, Vol 1, Cambridge: Cambridge University Press, pp. 60–78.

Quine, W.V. and J.S. Ullian, 1978, The Web of Belief, 2nd ed., New York: Random House.

Raatikainen, P., 2005, “On the Philosophical Relevance of Gödel's Incompleteness Theorems,” Revue Internationale de Philosophie, 59: 513–534.

Ramsey, F. P., 1930, “On a Problem of Formal Logic,” Proceedings of the London Mathematical Society, series 2, 30: 264–286.

Ricketts, T., 1995, “Carnap's Principle of Tolerance, Empiricism, and Conventionalism,” in Reading Putnam, P. Clark & B. Hale (eds.), Cambridge: Blackwell, pp. 176–200.

Rodríguez-Consuegra, F., 1993, “Russell, Gödel and Logicism,” in Philosophy of Mathematics, J. Czermak (ed.), Vienna: Hölder-Pichler-Tempsky, pp. 233–42. Reprinted in, 1998, Bertrand Russell: Critical Assessments, A. Irvine (ed.), vol. 2: Logic and mathematics, London: Routledge, pp. 320–29.

Roeper, P., 2003, “Giving an Account of Provability within a Theory,” Philosophia Mathematica, 11: 332–340.

Rosser, J. B., 1936, “Extensions of Some Theorems of Gödel and Church,” Journal of Symbolic Logic, 1: 87–91.

–––, 1938, “Review: Kurt Grelling, Gibt es eine Godelsche Antinomie? [Grelling 1937/8],” Journal of Symbolic Logic, 3(2): 86.

Searle, J., 1997, “Roger Penrose, Kurt Gödel, and the Cytoskeletons,” in J. Searle: Mystery of Consciousness, New York: New York Review of Books, pp. 55–93.

Shapiro, S., 1998, “Incompleteness, Mechanism, and Optimism,” Bulletin of Symbolic Logic, 4: 273–302.

–––, 2003, “Mechanism, Truth and Penrose's New Argument,” Journal of Philosophical Logic, 32(1): 19–42.

Simpson, S.G., 1985, “Nonprovability of Certain Combinatorial Properties of Finite Trees,” in Harvey Friedman's Research on the Foundations of Mathematics, L. Harrington et al. (eds.), Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland, pp. 87–117

–––, 1999, Subsystems of Second Order Arithmetic, Berlin: Springer.

Skolem, T., 1930, “Über einige Satzfunktionen in der Arithmetik,” Skrifter utgitt av Det Norske Videnskaps-Akademi i Oslo, I, no. 7, 1–28. Reprinted in T. Skolem, 1970, Selected Works in Logic, (J. Fenstad, editor), Oslo: Universitetsforlaget, pp. 281–306.

Smoryński, C., 1977, “The Incompleteness Theorems,” in Handbook of Mathematical Logic, J. Barwise (ed.), Amsterdam: North-Holland, pp. 821–865.

–––, 1981, “Fifty Years of Self-reference in Arithmetic,” Notre Dame Journal of Formal Logic, 22(4): 357–374.

–––, 1991, “The Development of Self-reference: Löb's Theorem,” in Perspectives on the History of Mathematical Logic, T. Drucker (ed.), Birkhauser, pp. 111–133.

Smullyan, R., 1992, Gödel's Incompleteness Theorems, Oxford: Oxford University Press.

Solovay, R.M., 1970, “A Model of Set Theory in which Every Set of Reals is Lebesgue Measurable,” Annals of Mathematics, 92: 1–56.

Sternfeld, R., 1976, “The Logistic Thesis,” in Studien zu Frege/Studies on Frege I, M. Schirn (ed.), Stuttgart-Bad Cannstatt: Frommann-Holzboog, pp. 139–160.

Tarski, A., 1948, A Decision Method for Elementary Algebra and Geometry, manuscript. Santa Monica, CA: RAND Corp., 1948. Republished as A Decision Method for Elementary Algebra and Geometry, 2nd ed. Berkeley, CA: University of California Press, 1951.

Tarski, A., A. Mostowski, and R.M. Robinson, 1953, Undecidable Theories, Amsterdam: North-Holland.

Tennant, Neil, 2008, “Carnap, Gödel, and the Analyticity of Arithmetic”, Philosophia Mathematica, 16: 100–112.

Turing, A.M., 1936–7, “On Computable Numbers, with an Application to the Entscheidungsproblem,” Proceedings of the London Mathematical Society, Series 2, 42: 230–265; correction, ibid., 43: 544–546. Republished in Davis 1965, 115–154.

Van Heijenoort, J. (ed.), 1967, From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931, Cambridge, MA: Harvard University Press.

Visser, A., 2011, “Can We Make the Second Incompleteness Theorem Coordinate Free,” Journal on Logic and Computation, 21(4): 543–560.

Woodin, H., 1988, “Supercompact Cardinals, Sets of Reals, and Weakly Homogeneous Trees,” Proceedings of the National Academy of Sciences, (U.S.A.), 85: 6587–91.

Wright, C., 1994, “About ‘The Philosophical Significance of Gödel's Theorem’: Some Issues,” in The Philosophy of Michael Dummett, B. McGuinness and G. Oliveri (eds.) Dordrecht: Kluwer, pp. 167–202.

–––, 1995, “Intuitionists are not (Turing) Machines,” Philosophia Mathematica, 3: 86–102.

Zach, R., 2005, “Paper on the Incompleteness Theorems,” in Landmark Writings in Western Mathematics, I. Grattan-Guinness (ed.), Amsterdam: Elsevier, pp. 917–25 [available online].