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

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

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

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

Вторая теорема о неполноте, являющаяся расширением первой, показывает, что система не может продемонстрировать свою непротиворечивость.

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

Формальные системы: полнота, непротиворечивость и эффективная аксиоматизация

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

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

Эффективная аксиоматизация

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

Теория, известная как истинная арифметика, состоит из всех истинных утверждений о стандартных целых числах на языке арифметики Пеано. Эта теория непротиворечива и полна и содержит достаточное количество арифметики. Однако он не имеет рекурсивно перечислимого набора аксиом и, следовательно, не удовлетворяет гипотезам теорем о неполноте.

Полнота

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

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

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

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

Последовательность

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

Арифметика Пеано доказуемо непротиворечива из ZFC, но не внутри себя. Точно так же ZFC не является доказуемо непротиворечивым изнутри себя, но ZFC + «существует недоступный кардинал » доказывает, что ZFC непротиворечив, потому что, если κ является наименьшим таким кардиналом, то V _κ, находящийся внутри вселенной фон Неймана , является моделью ZFC, и теория непротиворечива тогда и только тогда, когда у нее есть модель.

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

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

Системы, содержащие арифметику

Теоремы о неполноте применимы только к формальным системам, которые способны доказать достаточный набор фактов о натуральных числах. достаточных наборов является набор теорем арифметики Робинсона Q. Одним из Некоторые системы, такие как арифметика Пеано, могут напрямую выражать утверждения о натуральных числах. Другие, такие как теория множеств ZFC, способны интерпретировать утверждения о натуральных числах на свой язык. Любой из этих вариантов подходит для теорем о неполноте.

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

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

Дэн Уиллард ( 2001 ) изучил некоторые слабые семейства арифметических систем, которые допускают достаточно арифметических отношений в качестве отношений для формализации нумерации Гёделя, но которые недостаточно сильны, чтобы использовать умножение как функцию, и поэтому не могут доказать вторую теорему о неполноте; иными словами, эти системы непротиворечивы и способны доказать свою непротиворечивость (см. самопроверяющиеся теории ).

Противоречивые цели

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

Шаблон, показанный в предыдущих разделах с арифметикой Пеано, ZFC и ZFC + «существует недоступный кардинал», обычно не может быть нарушен. Здесь ZFC + «существует недоступный кардинал» не может быть доказан само по себе непротиворечивым. Она также не является полной, как это иллюстрирует гипотеза континуума, которая неразрешима. в ZFC+ "существует недоступный кардинал".

Первая теорема о неполноте показывает, что в формальных системах, которые могут выражать базовую арифметику, никогда не может быть создан полный и непротиворечивый конечный список аксиом: каждый раз, когда в качестве аксиомы добавляется дополнительное непротиворечивое утверждение, появляются другие истинные утверждения, которые все еще не могут быть определены. быть доказана, даже с учетом новой аксиомы. Если когда-либо добавляется аксиома, которая делает систему полной, то это происходит за счет того, что система становится несовместимой. Бесконечный список аксиом даже не может быть полным, непротиворечивым и эффективно аксиоматизированным.

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

См. Также: Схема доказательства первой теоремы Гёделя о неполноте.

Первая теорема Гёделя о неполноте впервые появилась как «Теорема VI» в статье Гёделя 1931 года « О формально неразрешимых утверждениях принципов математики и родственных систем I». Гипотезы теоремы вскоре были улучшены Дж. Баркли Россером ( 1936 ) с использованием приёма Россера . Полученную теорему (включающую усовершенствование Россера) можно перефразировать на английском языке следующим образом, где «формальная система» включает предположение о том, что система эффективно генерируется.

Первая теорема о неполноте : «Любая непротиворечивая формальная система F , внутри которой может быть выполнена определенная часть элементарной арифметики, является неполной; т.е. существуют утверждения языка F , которые нельзя ни доказать, ни опровергнуть в F ». (Раатикайнен 2020)

Недоказуемое утверждение G _F, упомянутое в теореме, часто называют «предложением Гёделя» для системы F . Доказательство строит конкретное предложение Гёделя для системы F , но в языке системы существует бесконечно много утверждений, которые обладают одинаковыми свойствами, например, соединение предложения Гёделя и любого логически допустимого предложения.

Каждая эффективно сгенерированная система имеет свое собственное предложение Гёделя. Можно определить более крупную систему F' содержит все F плюс GF _{, которая} в качестве дополнительной аксиомы. Это не приведет к созданию полной системы, поскольку теорема Гёделя применима и к F' , и, следовательно, F' также не может быть полной. этом случае GF _В действительно является теоремой в F' , поскольку это аксиома. Поскольку GF _{утверждает только ,} что оно недоказуемо в F не представляет никакого противоречия , его доказуемость в F' . Однако, поскольку теорема о неполноте применима к F' , появится новое утверждение Гёделя G _{F '} для F' , показывающее, что F' также является неполным. GF _{GF '} будет отличаться от GF _к тем, что ' _{F будет} к ' , а не F. относиться

Синтаксическая форма предложения Гёделя

Предложение Гёделя предназначено для косвенной ссылки на самого себя. В предложении говорится, что когда определенная последовательность шагов используется для построения другого предложения, это построенное предложение не будет доказуемо в F . что построенное предложение оказывается самим GF _{Однако последовательность шагов такова ,} . Таким образом, предложение Гёделя косвенно _GF заявляет о своей недоказуемости внутри F ( Смит 2007 , стр. 135).

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

Таким образом, хотя предложение Гёделя косвенно относится к предложениям системы F , если его читать как арифметическое утверждение, предложение Гёделя напрямую относится только к натуральным числам. Он утверждает, что ни одно натуральное число не обладает особым свойством, если это свойство задается примитивно-рекурсивным отношением ( Смит 2007 , стр. 141). Таким образом, предложение Гёделя может быть записано на языке арифметики в простой синтаксической форме. В частности, ее можно выразить формулой на языке арифметики, состоящей из ряда ведущих кванторов всеобщности, за которыми следует бескванторное тело (эти формулы находятся на уровне $\Pi _{1}^{0}$ ) арифметической иерархии . С помощью теоремы MRDP предложение Гёделя можно переписать как утверждение, что конкретный полином от многих переменных с целыми коэффициентами никогда не принимает нулевое значение, когда его переменные заменяются целыми числами ( Franzén 2005 , стр. 71).

Истинность предложения Гёделя

Первая теорема о неполноте показывает, что гёделевское предложение соответствующей _GF формальной теории F недоказуемо в F . Поскольку при интерпретации как утверждения об арифметике эта недоказуемость является именно тем, что утверждает данное предложение (косвенно), предложение Гёделя на самом деле истинно ( Smoryński 1977 , стр. 825; также см. Franzén 2005 , стр. 28–33). . По этой причине предложение G _F часто называют «истинным, но недоказуемым». ( Раатикайнен 2020 ). Однако, поскольку предложение Гёделя само по себе не может формально определить предполагаемую интерпретацию, истинность предложения G _F может быть достигнута только посредством метаанализа вне системы. В общем, этот метаанализ может быть проведен в рамках слабой формальной системы, известной как примитивно-рекурсивная арифметика доказывает импликацию Con ( F ) → GF _{, которая} , где Con ( F ) — каноническое предложение, утверждающее непротиворечивость F ( Смориньский 1977 , стр. 840, Кикучи и Танака 1994 , стр. 403).

Хотя предложение Гёделя непротиворечивой теории верно как утверждение о предполагаемой интерпретации арифметики, предложение Гёделя будет ложным в некоторых нестандартных моделях арифметики , как следствие теоремы Гёделя о полноте ( Францен 2005 , стр. 135). Эта теорема показывает, что, когда предложение не зависит от теории, теория будет иметь модели, в которых это предложение истинно, и модели, в которых это предложение ложно. Как описано ранее, предложение Гёделя системы F представляет собой арифметическое утверждение, утверждающее, что не существует числа с определенным свойством. Теорема о неполноте показывает, что это утверждение будет независимым от системы F , а истинность предложения Гёделя следует из того факта, что ни одно стандартное натуральное число не обладает рассматриваемым свойством. Любая модель, в которой предложение Гёделя ложно, должна содержать некоторый элемент, удовлетворяющий свойству этой модели. Такая модель должна быть «нестандартной» — она должна содержать элементы, не соответствующие ни одному стандартному натуральному числу ( Раатикайнен 2020 , Франзен 2005 , стр. 135).

Связь с парадоксом лжеца

Гёдель специально цитирует парадокс Рихарда и парадокс лжеца как семантические аналоги его синтаксической неполноты, приводящей к результату во вводном разделе « О формально неразрешимых суждениях в Principia Mathematica и родственных системах I ». Парадокс лжеца — это предложение «Это предложение ложно». Анализ предложения лжеца показывает, что оно не может быть ни истинным (ибо тогда, как оно утверждает, оно ложно), ни ложным (ибо тогда оно истинно). Предложение Гёделя G для системы F содержит утверждение, аналогичное предложению лжеца, но с заменой истины на доказуемость: G говорит: « G недоказуемо в системе F ». Анализ истинности и доказуемости G представляет собой формализованную версию анализа истинности предложения лжеца.

Невозможно заменить «недоказуемое» на «ложное» в предложении Гёделя, поскольку предикат « Q — число Гёделя ложной формулы» не может быть представлен как арифметическая формула. Этот результат, известный как теорема о неопределимости Тарского , был открыт независимо как Гёделем, когда он работал над доказательством теоремы о неполноте, так и тезкой теоремы Альфредом Тарским .

Расширение исходного результата Гёделя

По сравнению с теоремами, сформулированными в статье Гёделя 1931 года, многие современные формулировки теорем о неполноте являются более общими в двух отношениях. Эти обобщенные утверждения сформулированы так, чтобы применяться к более широкому классу систем, и они сформулированы так, чтобы включать более слабые предположения о непротиворечивости.

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

Оригинальное утверждение Гёделя и доказательство теоремы о неполноте требуют предположения, что система не просто непротиворечива, но и ω-непротиворечива . Система является ω-непротиворечивой, если она не ω-непротиворечива, и является ω-несогласованной, если существует предикат P такой, что для каждого конкретного натурального числа m система доказывает ~ P ( m ) , и тем не менее система также доказывает, что существует существует натуральное число n такое, что P ( n ). То есть система говорит, что число со свойством P существует, но отрицает, что оно имеет какое-либо конкретное значение. Из ω-непротиворечивости системы следует ее непротиворечивость, но из непротиворечивости не следует ω-непротиворечивость. Дж. Баркли Россер ( 1936 ) усилил теорему о неполноте, найдя вариант доказательства ( трюк Россера ), который требует только непротиворечивости системы, а не ω-непротиворечивости. Это представляет в основном технический интерес, потому что все истинные формальные теории арифметики (теории, все аксиомы которых являются истинными утверждениями о натуральных числах) ω-непротиворечивы, и, следовательно, к ним применима первоначально сформулированная теорема Гёделя. Более сильная версия теоремы о неполноте, которая предполагает только непротиворечивость, а не ω-непротиворечивость, теперь широко известна как теорема Гёделя о неполноте и теорема Гёделя–Россера.

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

Для каждой формальной системы F , содержащей базовую арифметику, можно канонически определить формулу Cons( F выражающую непротиворечивость F. ) , Эта формула выражает то свойство, что «не существует натурального числа, кодирующего формальный вывод в системе F , вывод которого представляет собой синтаксическое противоречие». Синтаксическое противоречие часто принимается за «0=1», и в этом случае Cons( F ) утверждает, что «не существует натурального числа, которое кодировало бы вывод '0=1' из аксиом F ».

Вторая теорема Гёделя о неполноте показывает, что при общих предположениях это утверждение канонической непротиворечивости Cons( F ) не будет доказуемо в F . Теорема впервые появилась как «Теорема XI» в статье Гёделя 1931 года « О формально неразрешимых суждениях в Principia Mathematica и родственных системах I ». В следующем утверждении термин «формализованная система» также включает предположение о том, что F эффективно аксиоматизировано. Эта теорема утверждает, что для любой непротиворечивой системы F, внутри которой может быть выполнен определенный объем элементарной арифметики, непротиворечивость F не может быть доказана в F. самой Эта теорема сильнее первой теоремы о неполноте, поскольку утверждение, построенное в первой теореме о неполноте, не выражает напрямую непротиворечивость системы. Доказательство второй теоремы о неполноте получается формализацией доказательства первой теоремы о неполноте внутри системы F. самой

Выражение последовательности

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

Другие формализации утверждения о F непротиворечивости могут быть неэквивалентны в F , а некоторые даже доказуемы. Например, арифметика Пеано первого порядка (PA) может доказать, что «самое большое непротиворечивое подмножество PA» является непротиворечивым. Но поскольку PA непротиворечив, самое большое непротиворечивое подмножество PA - это просто PA, поэтому в этом смысле PA «доказывает, что оно непротиворечиво». Чего PA не доказывает, так это того, что самое большое непротиворечивое подмножество PA фактически представляет собой весь PA. (Термин «наибольшее непротиворечивое подмножество РА» здесь означает самый большой непротиворечивый начальный сегмент аксиом РА при некотором конкретном эффективном перечислении.)

Условия Гильберта–Бернейса

Стандартное доказательство второй теоремы о неполноте предполагает, что предикат доказуемости Prov _A ( P ) удовлетворяет условиям доказуемости Гильберта–Бернейса . Полагая, что #( P ) представляет число Гёделя формулы P , условия доказуемости гласят:

1. Если F доказывает P , то F доказывает Prov _A (#( P )) .
2. F доказывает 1.; то есть F доказывает Prov _A (#( P )) → Prov _A (#( Prov _A (#( P )))) .
3. F доказать Prov _A (#( P → Q )) ∧ Prov _A (#( P )) → Prov _A (#( Q )) (аналог постулирования мод ).

Существуют системы, такие как арифметика Робинсона, которые достаточно сильны, чтобы удовлетворить условиям первой теоремы о неполноте, но не доказывают условия Гильберта-Бернейса. Однако арифметика Пеано достаточно сильна, чтобы проверить эти условия, как и все теории, более сильные, чем арифметика Пеано.

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

Вторая теорема Гёделя о неполноте также подразумевает, что система F1 _, изложенным выше, не может доказать непротиворечивость любой системы F2 _, которая доказывает непротиворечивость F1 _{удовлетворяющая техническим условиям ,} . что такая система F1 _F2 может доказать, что если доказывает _{Это происходит потому} непротиворечивость F1 _, , то фактически _F1 непротиворечива. Ибо утверждение о том, что обладает _{разрешимым} свойством не быть F 1 непротиворечиво, имеет форму «для всех чисел n n кодом для доказательства противоречия в F ₁ ». Если бы F ₁ был на самом деле противоречивым, то F ₂ доказывал бы для некоторого n , что n является кодом противоречия в F ₁ . Но если бы F ₂ также доказал, что F ₁ не существует непротиворечив (т. е. что такого n ), то он сам был бы несовместим. Это рассуждение можно формализовать в F1 _, чтобы показать, что если непротиворечив _F2 , то непротиворечив _F1 . Поскольку по второй теореме о неполноте F ₁ не доказывает свою непротиворечивость, то она не может и доказать непротиворечивость F ₂ .

Это следствие второй теоремы о неполноте показывает, что нет никакой надежды доказать, например, непротиворечивость арифметики Пеано, используя любые финитистские средства, которые могут быть формализованы в системе, непротиворечивость которой доказуема в арифметике Пеано (PA). Например, система примитивно-рекурсивной арифметики (ПРА), которая широко принята как точная формализация финитистской математики, доказуемо непротиворечива в ПА. Таким образом, PRA не может доказать состоятельность PA. Обычно считается, что этот факт подразумевает, что программа Гильберта , целью которой было оправдать использование «идеальных» (инфинитистских) математических принципов в доказательствах «реальных» (финитистских) математических утверждений путем предоставления финитистского доказательства непротиворечивости идеальных принципов, не может быть осуществлено.

Следствие также указывает на эпистемологическую значимость второй теоремы о неполноте. Если бы система F доказала свою непротиворечивость, это не дало бы никакой интересной информации. Это потому, что противоречивые теории доказывают все, включая свою непротиворечивость. Таким образом, доказательство непротиворечивости F в F не даст нам никакой подсказки относительно того, ли F непротиворечиво ; никакие сомнения относительно непротиворечивости F не будут разрешены таким доказательством непротиворечивости. Интерес к доказательствам непротиворечивости заключается в возможности доказать непротиворечивость системы F в некоторой системе F', которая в каком-то смысле менее сомнительна, чем F , например, слабее, чем F. сама Для многих естественных теорий F и F' , таких как F = теория множеств Цермело–Френкеля и F' = примитивно-рекурсивная арифметика, непротиворечивость F' доказуема в F , и, таким образом, F' не может доказать непротиворечивость F с помощью приведенного выше следствие второй теоремы о неполноте.

Вторая теорема о неполноте не исключает полностью возможности доказать непротиворечивость некоторой теории Т , делая это только в теории, непротиворечивость которой сама Т может оказаться непротиворечивой. Например, Герхард Генцен доказал непротиворечивость арифметики Пеано в другой системе, которая включает аксиому, утверждающую, что ординал под названием ε ₀ является хорошо обоснованным ; см . доказательство непротиворечивости Генцена . Теорема Генцена стимулировала развитие порядкового анализа в теории доказательств.

Примеры неразрешимых утверждений

См. также: Список утверждений, независимых от ZFC.

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

Из-за двух значений слова «неразрешимый» термин «независимый» иногда используется вместо слова «неразрешимый» в смысле «ни доказуемый, ни опровержимый».

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

Совместная работа Гёделя и Пауля Коэна дала два конкретных примера неразрешимых утверждений (в первом смысле этого слова): гипотеза континуума не может быть ни доказана, ни опровергнута в ZFC (стандартная аксиоматизация теории множеств ), а аксиома выбор нельзя ни доказать, ни опровергнуть в ZF (что является всеми аксиомами ZFC, кроме аксиомы выбора). Эти результаты не требуют теоремы о неполноте. Гёдель доказал в 1940 году, что ни одно из этих утверждений не может быть опровергнуто ни в теории множеств ZF, ни в теории множеств ZFC. В 1960-х годах Коэн доказал, что ни то, ни другое невозможно доказать с помощью ZF, а гипотезу континуума нельзя доказать с помощью ZFC.

Шела (1974) показал, что проблема Уайтхеда в теории групп неразрешима в первом смысле этого слова в стандартной теории множеств.

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

Неразрешимые утверждения, доказуемые в более крупных системах

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

В 1977 году Пэрис и Харрингтон доказали, что принцип Пэрис-Харрингтона , версия бесконечной теоремы Рамсея , неразрешим в арифметике Пеано (первого порядка) , но может быть доказан в более сильной системе арифметики второго порядка . Кирби и Пэрис позже показали, что теорема Гудштейна , утверждение о последовательностях натуральных чисел, несколько более простое, чем принцип Пэрис-Харрингтона, также неразрешима в арифметике Пеано.

Теорема Краскала о дереве , которая имеет приложения в информатике, также неразрешима с точки зрения арифметики Пеано, но доказуема в теории множеств. Фактически теорема Краскала о дереве (или ее конечная форма) неразрешима в гораздо более сильной системе ATR ₀ , кодифицирующей приемлемые принципы, основанные на философии математики, называемой предикативизмом . Связанная с ней, но более общая второстепенная теорема о графах (2003 г.) имеет последствия для теории сложности вычислений .

Связь с вычислимостью

См. Также: Проблема остановки § Теоремы Гёделя о неполноте

Теорема о неполноте тесно связана с несколькими результатами о неразрешимых множествах в теории рекурсии .

Клини (1943) представил доказательство теоремы Гёделя о неполноте, используя основные результаты теории вычислимости. Один из таких результатов показывает, что проблема остановки неразрешима: ни одна компьютерная программа не может правильно определить, учитывая любую программу P в качестве входных данных, остановится ли P в конечном итоге при запуске с конкретным заданным входным сигналом. Клини показал, что существование полной эффективной системы арифметики с определенными свойствами непротиворечивости сделало бы проблему остановки разрешимой, а это противоречие. Этот метод доказательства также был предложен Шонфилдом (1967) ; Чарльзуорт (1981) ; и Хопкрофт и Ульман (1979) .

Франзен (2005) объясняет, как решение Матиясевича можно 10-й проблемы Гильберта использовать для доказательства первой теоремы Гёделя о неполноте. Матиясевич доказал, что не существует алгоритма, который по многомерному многочлену p ( x ₁ , x ₂ ,..., x _k ) с целыми коэффициентами определял бы, существует ли целочисленное решение уравнения p = 0. Поскольку многочлены с целыми числами коэффициенты и сами целые числа непосредственно выражаются на языке арифметики. Если многомерное целочисленное полиномиальное уравнение p = 0 действительно имеет решение в целых числах, то любая достаточно сильная система арифметики T докажет это. Более того, предположим, что система T ω-совместна. В этом случае никогда не будет доказано, что конкретное полиномиальное уравнение имеет решение, если нет решения в целых числах. Таким образом, если бы T было полным и ω-непротиворечивым, можно было бы алгоритмически определить, имеет ли полиномиальное уравнение решение, просто перечисляя доказательства T до тех пор, пока не будет найдено либо « p имеет решение», либо « p не имеет решения», в противоречие с теоремой Матиясевича. Отсюда следует, что T не может быть ω-непротиворечивым и полным. Более того, для каждой непротиворечивой эффективно порожденной системы T , можно эффективно сгенерировать многомерный полином p над целыми числами такой, что уравнение p = 0 не имеет решений над целыми числами, но отсутствие решений не может быть доказано в T .

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

Теорема Чайтина о неполноте дает другой метод создания независимых предложений, основанный на колмогоровской сложности . Как и доказательство, представленное Клини и упомянутое выше, теорема Чайтина применима только к теориям с дополнительным свойством, заключающимся в том, что все их аксиомы верны в стандартной модели натуральных чисел. Теорема Гёделя о неполноте отличается своей применимостью к непротиворечивым теориям, которые, тем не менее, включают ложные утверждения в стандартную модель; эти теории известны как ω-несогласованные .

Схема доказательства первой теоремы

Основная статья: Схема доказательства первой теоремы Гёделя о неполноте

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

1. Утверждения в системе могут быть представлены натуральными числами (известными как числа Гёделя). Значение этого состоит в том, что свойства утверждений, такие как их истинность и ложность, будут эквивалентны определению того, обладают ли их числа Гёделя определенными свойствами, и поэтому свойства утверждений можно продемонстрировать, исследуя их числа Гёделя. Эта часть завершается построением формулы, выражающей идею о том, что «утверждение S доказуемо в системе» (которая может быть применена к любому утверждению « S » в системе).
2. В формальной системе можно построить число, соответствующее утверждение которого при интерпретации является самореферентным и, по сути, говорит, что оно (т. е. само утверждение) недоказуемо. Это делается с помощью техники, называемой « диагонализация » (названной так из-за своего происхождения от диагонального аргумента Кантора ).
3. В рамках формальной системы это утверждение позволяет продемонстрировать, что оно ни доказуемо, ни опровергнуто в системе, и, следовательно, система на самом деле не может быть ω-непротиворечивой. Следовательно, первоначальное предположение о том, что предлагаемая система соответствует критериям, является ложным.

Арифметизация синтаксиса

Основная проблема при разработке описанного выше доказательства заключается в том, что на первый взгляд кажется, что для построения утверждения p , которое эквивалентно утверждению « p не может быть доказано», p каким-то образом должно содержать ссылку на p , что может легко привести к бесконечный регресс. Техника Гёделя состоит в том, чтобы показать, что утверждения могут быть сопоставлены с числами (часто называемая арифметизацией синтаксиса ) таким образом, что «доказательство утверждения» можно заменить «проверкой того, обладает ли число заданным свойством» . Это позволяет построить самореферентную формулу таким образом, чтобы избежать бесконечного регресса определений. Эту же технику позже использовал Алан Тьюринг в своей работе над проблемой Entscheidungs .

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

• Слово hello кодируется как 104-101-108-108-111 в ASCII , который можно преобразовать в число 104101108108111.
• Логичное утверждение x=y => y=x кодируется как 120-061-121-032-061-062-032-121-061-120 в ASCII , который можно преобразовать в число 120061121032061062032121061120.

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

Построение утверждения о «доказуемости»

Показав, что в принципе система может косвенно делать утверждения о доказуемости, анализируя свойства чисел, представляющих утверждения, теперь можно показать, как создать утверждение, которое действительно это делает.

Формула F ( x ) , содержащая ровно одну свободную переменную x, называется формой утверждения или знаком класса . Как только x заменяется конкретным числом, форма утверждения превращается в добросовестное утверждение, и тогда оно либо доказуемо в системе, либо нет. Для некоторых формул можно показать, что для любого натурального n ⁠ числа $F(n)$⁠ истинно тогда и только тогда, когда его можно доказать (точное требование в исходном доказательстве более слабое, но для наброска доказательства этого будет достаточно). В частности, это верно для каждой конкретной арифметической операции между конечным числом натуральных чисел, например «2 × 3 = 6».

Формы утверждений сами по себе не являются утверждениями и поэтому не могут быть ни доказаны, ни опровергнуты. Но каждому утверждению формы F ( x ) можно присвоить номер Гёделя, обозначаемый G ( F ) . Выбор свободной переменной, используемой в форме F ( x ), не имеет отношения к присвоению числа Гёделя G ( F ) .

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

Bew ( y ) = ∃ x ( y — число Гёделя формулы, а x — число Гёделя доказательства формулы, закодированной y ).

Имя Bew является сокращением от beweisbar , немецкого слова, означающего «доказуемый»; это название первоначально использовалось Гёделем для обозначения только что описанной формулы доказуемости. Обратите внимание, что « Bew ( y ) » — это просто аббревиатура, обозначающая особую, очень длинную формулу на исходном языке T ; сама строка « Bew » не считается частью этого языка.

Важная особенность формулы Bew ( y ) состоит в том, что если утверждение p доказуемо в системе, то Bew ( G ( p )) также доказуемо. Это связано с тем, что любое доказательство p будет иметь соответствующее число Гёделя, существование которого приводит Bew( G ( p )) к удовлетворению .

Диагонализация

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

п ↔ F ( грамм ( п ) ) .

Полагая F отрицанием Bew ( x ) , мы получаем теорему

п ↔ ~ Бью ( G ( п ))

и p, определенное этим, примерно означает, что его собственное число Гёделя является числом Гёделя недоказуемой формулы.

Утверждение p не равно буквально ~ Bew ( G ( p )) ; скорее, p утверждает, что если будет выполнен определенный расчет, результирующее число Гёделя будет числом недоказуемого утверждения. Но когда этот расчет выполняется, полученное число Гёделя оказывается числом Гёделя самого p . Это похоже на следующее предложение на английском языке:

", если ему предшествует само слово в кавычках, недоказуемо.", если ему предшествует само слово в кавычках, недоказуемо.

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

Теперь предположим, что аксиоматическая система ω-непротиворечива , и пусть p — утверждение, полученное в предыдущем разделе.

Если бы p было доказуемо, то Bew ( G ( p )) было бы доказуемо, как утверждалось выше. Но p утверждает отрицание Bew ( G ( p )) . Таким образом, система была бы противоречивой, доказывая как утверждение, так и его отрицание. Это противоречие показывает, что p не может быть доказуемо.

Если бы отрицание p было доказуемо, то Bew ( G ( p )) было бы доказуемо (поскольку p было построено так, чтобы быть эквивалентным отрицанию Bew ( G ( p )) ). Однако для каждого конкретного числа x x . не может быть числом Гёделя доказательства p , поскольку p недоказуемо (из предыдущего абзаца) Таким образом, с одной стороны, система доказывает, что существует число с определенным свойством (что это число Гёделя в доказательстве p ), но с другой стороны, для каждого конкретного числа x мы можем доказать, что оно не имеет этого числа. свойство. Это невозможно в ω-согласованной системе. Таким образом, отрицание p недоказуемо.

Таким образом, утверждение p неразрешимо в нашей аксиоматической системе: его нельзя ни доказать, ни опровергнуть внутри системы.

Фактически, чтобы показать, что p недоказуемо, требуется только предположение о непротиворечивости системы. Более сильное предположение о ω-непротиворечивости необходимо, чтобы показать, что отрицание p недоказуемо. Таким образом, если p построен для конкретной системы:

• Если система ω-непротиворечива, она не может доказать ни p, ни его отрицание, и поэтому p неразрешимо.
• Если система непротиворечива, она может иметь ту же ситуацию или может доказать отрицание p . В последнем случае мы имеем утверждение («не p »), которое ложно, но доказуемо, и система не является ω-непротиворечивой.

Если попытаться «добавить недостающие аксиомы», чтобы избежать неполноты системы, то в качестве аксиом придется добавить либо p , либо «не p ». Но тогда определение утверждения «быть числом Гёделя доказательства» меняется. а это значит, что формула Bew ( x ) теперь другая. Таким образом, применив диагональную лемму к этому новому Bew, мы получим новое утверждение p , отличное от предыдущего, которое будет неразрешимо в новой системе, если она ω-непротиворечива.

Доказательство с помощью парадокса Берри.

Булос (1989) предлагает альтернативное доказательство первой теоремы о неполноте, в котором используется парадокс Берри , а не парадокс лжеца для построения истинной, но недоказуемой формулы . Похожий метод доказательства был независимо открыт Солом Крипке . Доказательство Булоса продолжается путем построения для любого вычислимо перечислимого множества S истинных арифметических предложений другого предложения, которое истинно, но не содержится в S . Следствием этого является первая теорема о неполноте. По мнению Булоса, это доказательство интересно тем, что оно дает «другое объяснение» неполноты эффективных и непротиворечивых теорий арифметики.

Доказательства, проверенные компьютером

См. Также: Автоматическое доказательство теорем.

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

Компьютерно-проверенные доказательства версий первой теоремы о неполноте были анонсированы Натараджаном Шанкаром в 1986 году с использованием Nqthm ( Shankar 1994 ), Расселом О'Коннором в 2003 году с использованием Coq ( O'Connor 2005 ) и Джоном Харрисоном в 2009 году с использованием HOL Light ( Харрисон 2009 ). Компьютерно-проверенное доказательство обеих теорем о неполноте было анонсировано Лоуренсом Полсоном в 2013 году с использованием Изабель ( Paulson 2014 ).

Схема доказательства второй теоремы.

См. Также: Условия доказуемости Гильберта – Бернейса.

Основная трудность в доказательстве второй теоремы о неполноте состоит в том, чтобы показать, что различные факты о доказуемости, используемые при доказательстве первой теоремы о неполноте, могут быть формализованы в рамках системы S с использованием формального предиката P для доказуемости. Как только это будет сделано, последует вторая теорема о неполноте, формализующая все доказательство первой теоремы о неполноте внутри системы S. самой

Обозначим p неразрешимое предложение, построенное выше, и предположим для получения противоречия, что непротиворечивость системы S может быть доказана изнутри системы S. самой Это эквивалентно доказательству утверждения «Система S непротиворечива». Теперь рассмотрим утверждение c , где c = «Если система S непротиворечива, то p недоказуемо». Доказательство предложения c может быть формализовано в системе S , и, следовательно, утверждение c « p недоказуемо» (или, тождественно, «не ( p ) » ) может быть доказано в системе S. P

Заметим тогда, что если мы сможем доказать, что система S непротиворечива (т. е. утверждение в гипотезе c ), то мы докажем, что p недоказуемо. Но это противоречие, поскольку по 1-й теореме о неполноте это предложение (т. е. то, что подразумевается в предложении c , «» p » не доказуемо») является тем, что мы считаем недоказуемым. Обратите внимание, что именно поэтому нам требуется формализовать первую теорему о неполноте в S которое можно сделать, только показав, что эта теорема справедлива в S. : для доказательства 2-й теоремы о неполноте мы получаем противоречие с 1-й теоремой о неполноте , Поэтому мы не можем доказать, что система S непротиворечива. Далее следует утверждение 2-й теоремы о неполноте.

Обсуждение и последствия

Результаты неполноты влияют на философию математики , особенно на версии формализма , которые используют единую систему формальной логики для определения своих принципов.

Последствия для логицизма и вторая проблема Гильберта

Иногда считается, что теорема о неполноте имеет серьезные последствия для программы логицизма, предложенной Готтлобом Фреге и Бертраном Расселом , целью которой было определение натуральных чисел с точки зрения логики. Боб Хейл и Криспин Райт утверждают, что это не проблема для логицизма, поскольку теоремы о неполноте в равной степени применимы как к логике первого порядка, так и к арифметике. Они утверждают, что с этой проблемой сталкиваются только те, кто считает, что натуральные числа следует определять в терминах логики первого порядка.

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

Умы и машины

Основная статья: Механизм (философия) § гёделевские аргументы

Авторы, в том числе философ Дж. Р. Лукас и физик Роджер Пенроуз, обсуждали, что подразумевают теоремы Гёделя о неполноте в отношении человеческого интеллекта. Большая часть дебатов сосредоточена на том, эквивалентен ли человеческий разум машине Тьюринга или, согласно тезису Чёрча-Тьюринга , любой конечной машине вообще. Если это так и если машина непротиворечива, то к ней применимы теоремы Гёделя о неполноте.

Патнэм (1960) предположил, что, хотя теоремы Гёделя не могут быть применены к людям, поскольку они допускают ошибки и, следовательно, непоследовательны, их можно применить к человеческим способностям к естественным наукам или математике в целом. Если предположить, что оно непротиворечиво, то его непротиворечивость либо невозможно доказать, либо его нельзя представить с помощью машины Тьюринга.

Вигдерсон (2010) предположил, что концепция математической «познаваемости» должна основываться на вычислительной сложности, а не на логической разрешимости. Он пишет, что «когда познаваемость интерпретируется современными стандартами, а именно через вычислительную сложность, явления Гёделя очень часто встречаются с нами».

Дуглас Хофштадтер в своих книгах «Гедель, Эшер, Бах» и «Я — странная петля » приводит теоремы Гёделя как пример того, что он называет странной петлей , иерархической, самореферентной структурой, существующей внутри аксиоматической формальной системы. Он утверждает, что это та же самая структура, которая порождает сознание, чувство «я» в человеческом сознании. В то время как самореференция в теореме Гёделя происходит из предложения Гёделя, утверждающего его недоказуемость в рамках формальной системы Principia Mathematica, самореференция в человеческом разуме происходит из-за того, как мозг абстрагирует и классифицирует стимулы в «символы» или группы нейронов. которые реагируют на концепции, что, по сути, также является формальной системой, в конечном итоге порождая символы, моделирующие концепцию самой сущности, осуществляющей восприятие. Хофштадтер утверждает, что странная петля в достаточно сложной формальной системе может привести к возникновению «нисходящей» или «перевернутой» причинности, ситуации, в которой нормальная иерархия причин и следствий переворачивается с ног на голову. В случае теоремы Гёделя это проявляется вкратце следующим образом:

Просто зная значение формулы, можно сделать вывод о ее истинности или ложности, не пытаясь вывести ее старомодным способом, который требует методического продвижения «вверх» от аксиом. Это не просто странно; это удивительно. Обычно нельзя просто посмотреть на то, что говорит математическая гипотеза, и просто обратиться к содержанию этого утверждения само по себе, чтобы сделать вывод, является ли это утверждение истинным или ложным.

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

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

Паранепротиворечивая логика

Хотя теоремы Гёделя обычно изучаются в контексте классической логики, они также играют роль в изучении паранепротиворечивой логики и противоречивых по своей сути утверждений ( диалетейя ). Прист ( 1984 , 2006 ) утверждает, что замена понятия формального доказательства в теореме Гёделя обычным понятием неформального доказательства может быть использована, чтобы показать, что наивная математика непоследовательна, и использует это как доказательство диалетеизма . Причиной этого несоответствия является включение предиката истинности системы в язык системы. Шапиро (2002) дает более неоднозначную оценку применения теорем Гёделя к диалетеизму.

Обращения к теоремам о неполноте в других областях

Апелляции и аналогии иногда приводятся к неполноте теорем в поддержку аргументов, выходящих за рамки математики и логики. Некоторые авторы отрицательно прокомментировали такие расширения и интерпретации, в том числе Франзен (2005) , Раатикайнен (2005) , Сокаль и Брикмонт (1999) ; и Стэнгрум и Бенсон (2006) . Сокал и Брикмонт (1999) и Стангрум и Бенсон (2006) , например, цитируют комментарии Ребекки Гольдштейн Гёделя о несоответствии между общепризнанным платонизмом и антиреалистическим использованием его идей. Сокал и Брикмон (1999) критикуют обращение Режиса Дебре к этой теореме в контексте социологии; Дебре защищал это использование как метафорическое (там же).

История

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

Гёдель был не единственным человеком, работавшим над проблемой непротиворечивости. Акерманн опубликовал ошибочное доказательство непротиворечивости для анализа в 1925 году, в котором он попытался использовать метод ε-замены, первоначально разработанный Гильбертом. Позже в том же году фон Нейман смог исправить доказательство системы арифметики без каких-либо аксиом индукции. К 1928 году Акерманн передал Бернейсу модифицированное доказательство; это модифицированное доказательство побудило Гильберта в 1929 году заявить о своей убежденности в том, что непротиворечивость арифметики была продемонстрирована и что вскоре последует последовательное доказательство анализа. После того, как публикация теорем о неполноте показала, что модифицированное доказательство Аккермана должно быть ошибочным, фон Нейман привел конкретный пример, показывающий, что его основной метод несостоятелен.

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

Объявление

1930 года Кенигсбергская конференция представляла собой совместное заседание трех академических обществ, на котором присутствовали многие ключевые логики того времени. Карнап, Гейтинг и фон Нейман выступили с часовыми докладами по математической философии логицизма, интуиционизма и формализма соответственно. На конференции также было выступление Гильберта на пенсии, когда он покидал свою должность в Геттингенском университете. Гильберт использовал эту речь, чтобы доказать свою веру в то, что все математические проблемы могут быть решены. Свое выступление он закончил словами:

Для математика не существует Ignorabimus , да и для естествознания, по-моему, вовсе нет. ... Истинная причина, по которой [никому] не удалось найти неразрешимую проблему, по моему мнению, заключается в том, что неразрешимых проблем не существует. В отличие от глупых Игнорабимов , наше кредо гласит: Мы должны знать. Мы узнаем!

Эта речь быстро стала известна как краткое изложение взглядов Гильберта на математику (ее последние шесть слов, « Wir müssen wissen. Wir werden wissen! », были использованы в качестве эпитафии Гильберта в 1943 году). Хотя Гёдель, вероятно, присутствовал на выступлении Гильберта, они никогда не встречались лицом к лицу.

Гёдель объявил о своей первой теореме о неполноте на круглом столе в третий день конференции. Это объявление не привлекло особого внимания, за исключением заявления фон Неймана, который отвел Гёделя в сторону для разговора. Позже в том же году, работая независимо, зная первую теорему о неполноте, фон Нейман получил доказательство второй теоремы о неполноте, о котором он объявил Гёделю в письме от 20 ноября 1930 года. Гёдель независимо получил вторую теорему о неполноте и включил ее в представленную ему рукопись, которая была получена Monatshefte für Mathematik 17 ноября 1930 года.

Статья Гёделя была опубликована в Monatshefte в 1931 году под названием «Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I» (« О формально неразрешимых суждениях в Principia Mathematica и родственных системах I »). Как следует из названия, Гёдель первоначально планировал опубликовать вторую часть статьи в следующем томе Monatshefte ; быстрое принятие первой статьи стало одной из причин, по которой он изменил свои планы.

Обобщение и принятие

Гёдель прочитал серию лекций по своим теоремам в Принстоне в 1933–1934 годах перед аудиторией, в которую входили Чёрч, Клини и Россер. К этому времени Гёдель понял, что ключевым свойством, требуемым его теоремами, является то, что система должна быть эффективной (в то время использовался термин «общерекурсивная»). Россер доказал в 1936 году, что гипотеза ω-непротиворечивости, которая была неотъемлемой частью первоначального доказательства Гёделя, может быть заменена простой непротиворечивостью, если предложение Гёделя было соответствующим образом изменено. Эти разработки оставили теоремы о неполноте по существу в их современной форме.

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

Влияние теорем о неполноте на программу Гильберта было быстро осознано. Бернейс включил полное доказательство теорем о неполноте во второй том Grundlagen der Mathematik ( 1939 ), наряду с дополнительными результатами Аккермана о методе ε-замены и доказательстве непротиворечивости арифметики Генцена. Это было первое полное опубликованное доказательство второй теоремы о неполноте.

Критика

Финслер

Финслер (1926) использовал версию парадокса Ричарда для построения выражения, которое было ложным, но недоказуемым в конкретной, разработанной им неформальной структуре. Гёдель не знал об этой статье, когда доказывал теоремы о неполноте (Собрание сочинений, т. IV, стр. 9). Финслер написал Гёделю в 1931 году, чтобы сообщить ему об этой статье, которая, по мнению Финслера, имела приоритет над теоремой о неполноте. Методы Финслера не опирались на формализованную доказуемость и имели лишь поверхностное сходство с работами Гёделя. Гёдель прочитал статью, но нашел в ней глубокие недостатки, а в его ответе Финслеру выражалась обеспокоенность по поводу отсутствия формализации. Финслер продолжал отстаивать свою философию математики, избегающую формализации, до конца своей карьеры.

Цермело

В сентябре 1931 года Эрнст Цермело написал Гёделю, чтобы объявить о том, что он назвал «существенным пробелом» в аргументах Гёделя. В октябре Гёдель ответил 10-страничным письмом, в котором указал, что Цермело ошибочно предположил, что понятие истины в системе определимо в этой системе; вообще говоря, это неверно согласно теореме Тарского о неопределимости . Однако Цермело не уступил и опубликовал свою критику в печати с «довольно резким абзацем в адрес своего молодого конкурента». Гёдель решил, что дальнейшее рассмотрение этого вопроса бессмысленно, и Карнап согласился. Большая часть последующих работ Цермело была связана с логикой, более сильной, чем логика первого порядка, с помощью которой он надеялся показать как последовательность, так и категоричность математических теорий.

Витгенштейн

Людвиг Витгенштейн написал несколько отрывков о теоремах о неполноте, которые были опубликованы посмертно в его «Замечаниях об основах математики» 1953 года , в частности, один раздел, который иногда называют «пресловутым абзацем», где он, кажется, путает понятия «истинно» и «доказуемо» в Система Рассела. Гёдель был членом Венского кружка Витгенштейна в тот период, когда ранняя философия идеального языка и «Логико-философский трактат» доминировали в мышлении кружка. Были некоторые разногласия по поводу того, неправильно ли Витгенштейн понял теорему о неполноте или просто выразился неясно. Гёделя Сочинения в «Наклассе» выражают убежденность в том, что Витгенштейн неверно истолковал его идеи.

Многие комментаторы считали Витгенштейна ошибочным пониманием Гёделя , хотя Флойд и Патнэм (2000) , а также Прист (2004) предоставили текстовые прочтения, утверждая, что большинство комментариев неправильно понимают Витгенштейна. После своего освобождения Бернейс, Даммет и Крейзель написали отдельные рецензии на высказывания Витгенштейна, причем все они были крайне негативными. Единогласие этой критики привело к тому, что замечания Витгенштейна по поводу теорем о неполноте не оказали большого влияния на логическое сообщество. В 1972 году Гёдель заявил: «Неужели Витгенштейн сошел с ума? Он имеет это в виду серьезно? Он намеренно произносит тривиально бессмысленные утверждения», и написал Карлу Менгеру , что комментарии Витгенштейна демонстрируют непонимание написания теорем о неполноте:

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

С момента публикации «Наследия» Витгенштейна в 2000 году ряд философских работ пытались оценить, была ли оправдана первоначальная критика замечаний Витгенштейна. Флойд и Патнэм (2000) утверждают, что Витгенштейн имел более полное понимание теоремы о неполноте, чем предполагалось ранее. Их особенно беспокоит интерпретация предложения Гёделя для ω-несовместимой системы как высказывания «Я недоказуема», поскольку у системы нет моделей, в которых предикат доказуемости соответствует фактической доказуемости. Родич (2003) утверждает, что их интерпретация Витгенштейна исторически не оправдана. Берто (2009) исследует связь между творчеством Витгенштейна и теориями паранепротиворечивой логики.

См. также

• Теорема Чайтина о неполноте
• Гёдель, Эшер, Бах
• машина Гёделя
• Теорема Гёделя о полноте
• Теорема Гёделя об ускорении
• Теорема Леба
• Разум, машины и Гёдель
• Нестандартная модель арифметики
• Теория доказательств
• Логика доказуемости
• Куининг
• Теорема Тарского о неопределимости
• Теория всего#Теорема Гёделя о неполноте
• Типографская теория чисел

Ссылки

Статьи Гёделя

• Курт Гёдель, 1931, «О формально неразрешимых предложениях Principia Mathematica и родственных систем, I», Monthly Books for Mathematica and Physics , v. 38 н. 1, стр. 173–198. дои : 10.1007/BF01700692
• -, 1931, «О формально неразрешимых теоремах Principia Mathematica и связанных с ними систем, I», в издании Соломона Фефермана , 1986. Курт Гёдель Собрание сочинений, Том I. Издательство Оксфордского университета, стр. 144–195. ISBN   978-0195147209 . Оригинал на немецком языке с английским переводом, которому предшествует вступительная записка Стивена Коула Клини .
• -, 1951, «Некоторые основные теоремы об основаниях математики и их следствиях», в Соломоне Фефермане , изд., 1995. Курт Гёдель Собрание сочинений, Vol. III , Oxford University Press, стр. 304–323. ISBN   978-0195147223 .

Прижизненные переводы статьи Гёделя на английский язык.

Ничто из следующего не совпадает во всех переведенных словах и типографике. Типографика — дело серьезное, поскольку Гёдель явно хотел подчеркнуть «те метаматематические понятия, которые были определены в их обычном смысле раньше...» ( ван Хейеноорт 1967 , стр. 595). Существует три перевода. О первом Джон Доусон заявляет, что: «Перевод Мельцера был серьезно несовершенным и получил разгромную рецензию в Журнале символической логики »; «Гедель также жаловался на комментарий Брейтуэйта ( Доусон 1997 , стр. 216). «К счастью, перевод Мельцера вскоре был заменен лучшим переводом, подготовленным Эллиотом Мендельсоном для антологии Мартина Дэвиса « Неразрешимое »… он нашел перевод «не таким хорошим», как он ожидал… [но из-за нехватки времени он ] согласился на его публикацию» (там же). (В сноске Доусон заявляет, что «он пожалеет о своем согласии, поскольку опубликованный том был полностью испорчен неряшливой типографикой и многочисленными опечатками» (там же)). Доусон заявляет, что «перевод, который предпочитал Гёдель, был сделан Жаном ван Хейеноортом» (там же). Для серьезного студента существует другая версия в виде набора конспектов лекций, записанных Стивеном Клини и Дж. Б. Россером «во время лекций, прочитанных Гёделем в Институте перспективных исследований весной 1934 года» (см. комментарий Дэвис 1965 , с. 39 и начиная со стр. 41); эта версия называется «О неразрешимых утверждениях формальных математических систем». В порядке публикации:

• Б. Мельцер (перевод) и Р.Б. Брейтуэйт (Введение), 1962. О формально неразрешимых положениях Principia Mathematica и родственных систем , Dover Publications, Нью-Йорк (Дуврское издание, 1992 г.), ISBN   0-486-66980-7 (pbk.) Он содержит полезный перевод немецких сокращений Гёделя на стр. 33–34. Как отмечалось выше, типографика, перевод и комментарии вызывают подозрение. К сожалению, этот перевод был переиздан со всем его подозрительным содержанием.

• Редактор Стивена Хокинга , 2005. Бог создал целые числа: математические прорывы, которые изменили историю , Running Press, Филадельфия, ISBN   0-7624-1922-9 . Статья Гёделя начинается со стр. 1097, с комментарием Хокинга, начинающимся со стр. 1089.

• Редактор Мартина Дэвиса , 1965. Неразрешимое: основные статьи о неразрешимых предложениях, неразрешимых проблемах и вычислимых функциях , Raven Press, Нью-Йорк, без ISBN. Статья Гёделя начинается на странице 5, которой предшествует одна страница комментариев.
• Редактор Жана ван Хейеноорта , 1967, 3-е издание, 1967. От Фреге до Гёделя: справочник по математической логике, 1879–1931 , издательство Гарвардского университета, Кембридж, Массачусетс, ISBN   0-674-32449-8 (пбк). ван Хейеноорт сделал перевод. Он заявляет, что «профессор Гёдель одобрил перевод, который во многих местах был адаптирован к его пожеланиям». (с. 595). Статья Гёделя начинается на стр. 595; Комментарий ван Хейеноорта начинается на стр. 592.
• Редактор Мартина Дэвиса, 1965 г., там же. «О неразрешимых предложениях формальных математических систем». Копия с исправлениями опечаток Гёделем и добавленными примечаниями Гёделя начинается на странице 41, которой предшествуют две страницы комментария Дэвиса. До тех пор, пока Дэвис не включил это в свой сборник, эта лекция существовала только в виде мимеографированных заметок.

Статьи других

• Булос, Джордж (1989). «Новое доказательство теоремы Гёделя о неполноте». Уведомления Американского математического общества . 36 : 388–390, 676. перепечатано в Boolos (1998 , стр. 383–388).
• Булос, Джордж (1998). Логика, логика и логика . Издательство Гарвардского университета . п. 443. ИСБН  0-674-53766-1 .
• Бернд Бульдт, 2014 г., « Область применения первой теоремы Гёделя о неполноте. Архивировано 6 марта 2016 г. в Wayback Machine », Logica Universalis , т. 8, стр. 499–552. два : 10.1007/s11787-014-0107-3
• Чарльзуорт, Артур (1981). «Доказательство теоремы Гёделя с точки зрения компьютерных программ». Журнал «Математика» . 54 (3): 109–121. дои : 10.2307/2689794 . JSTOR   2689794 .
• Дэвис, Мартин (1965). Неразрешимое: основные статьи о неразрешимых предложениях, неразрешимых проблемах и вычислимых функциях . Рэйвен Пресс. ISBN  978-0-911216-01-1 .
• Дэвис, Мартин (2006). «Теорема о неполноте» (PDF) . Уведомления АМС . 53 (4): 414.
• Финслер, Пол (1926). «Формальные доказательства и разрешимость» . Математический журнал . 25 :676-682. дои : 10.1007/bf01283861 . S2CID   121054124 .
• Граттан-Гиннесс, Айвор , изд. (2005). Знаковые сочинения по западной математике 1640-1940 гг . Эльзевир. ISBN  9780444508713 .
• ван Хейеноорт, Жан (1967). «Теорема Гёделя». Эдвардс, Пол (ред.). Энциклопедия философии . Том. 3. Макмиллан. стр. 348–357.
• Хеллман, Джеффри (1981). «Как Гёдель Фреге-Рассела: теоремы Гёделя о неполноте и логицизм». Нус . 15 (4 - Специальный выпуск по философии математики): 451–468. дои : 10.2307/2214847 . ISSN   0029-4624 . JSTOR   2214847 .
• Дэвид Гильберт , 1900, « Математические проблемы ». Английский перевод лекции, прочитанной перед Международным конгрессом математиков в Париже, содержащей формулировку Гильберта о его второй проблеме.
• Мартин Хирзель, 2000, « О формально неразрешимых утверждениях Principia Mathematica и связанных с ними систем I. ». Английский перевод статьи Гёделя. Архивировано из оригинала . 16 сентября 2004 г.
• Кикучи, Макото; Танака, Казуюки (июль 1994 г.). «О формализации теоретико-модельных доказательств теорем Гёделя» . Журнал формальной логики Нотр-Дама . 35 (3): 403–412. дои : 10.1305/ndjfl/1040511346 . МР   1326122 .
• Клини, Южная Каролина (1943). «Рекурсивные предикаты и кванторы». Труды Американского математического общества . 53 (1): 41–73. дои : 10.1090/S0002-9947-1943-0007371-8 . Перепечатано в Дэвисе, 1965 г. , стр. 255–287.
• Раатикайнен, Пану (2020). «Теоремы Гёделя о неполноте» . Стэнфордская энциклопедия философии . Проверено 7 ноября 2022 г.
• Раатикайнен, Пану (2005). «О философском значении теорем Гёделя о неполноте» . Международное ревю философии . 59 (4): 513–534. дои : 10.3917/rip.234.0513 . S2CID   52083793 .
• Джон Баркли Россер , 1936, «Расширения некоторых теорем Гёделя и Чёрча», перепечатано из Журнала символической логики , т. 1 (1936), стр. 87–91, в книге Мартина Дэвиса 1965, «Неразрешимое» (цит.). стр. 230–235.
• -, 1939, «Неформальное изложение доказательств теоремы Гёделя и теоремы Чёрча», перепечатано из журнала «Символическая логика» , т. 4 (1939), стр. 53–60, в книге Мартина Дэвиса 1965, «Неразрешимое» (loc. cit. ) стр. 223–230.
• Сморинский, К. (1977). «Теоремы о неполноте». В Джоне Барвайзе (ред.). Справочник по математической логике . Амстердам: Паб Северной Голландии. Ко, стр. 821–866. ISBN  978-0-444-86388-1 .
• Уиллард, Дэн Э. (2001). «Самопроверяющиеся системы аксиом, теорема о неполноте и связанные с ней принципы отражения». Журнал символической логики . 66 (2): 536–596. дои : 10.2307/2695030 . JSTOR   2695030 .
• Зак, Ричард (2003). «Практика финитизма: эпсилон-исчисление и доказательства непротиворечивости в программе Гильберта» (PDF) . Синтезируйте . 137 (1). ООО «Спрингер Сайенс энд Бизнес Медиа»: 211–259. arXiv : math/0102189 . дои : 10.1023/а:1026247421383 . ISSN   0039-7857 . S2CID   16657040 .
• Зак, Ричард (2005). «Курт Гёдель, статья о теоремах о неполноте (1931)». В Граттан-Гиннессе, Айвор (ред.). Знаковые сочинения по западной математике 1640-1940 гг . Эльзевир. стр. 917–925. дои : 10.1016/b978-044450871-3/50152-2 . ISBN  9780444508713 .

Книги о теоремах

• Франческо Берто. Что-то есть в Гёделе: полное руководство по теореме о неполноте Джон Уайли и сыновья. 2010.
• Норберт Домейзен, 1990. Логика антиномий . Берн: Питер Лэнг. 142 стр. 1990. ISBN   3-261-04214-1 . Збл   0724.03003 .
• Францен, Торкель (2005). Теорема Гёделя: неполное руководство по ее использованию и злоупотреблениям . Уэлсли, Массачусетс: АК Питерс. ISBN  1-56881-238-8 . МР   2146326 .
• Дуглас Хофштадтер , 1979. Гёдель, Эшер, Бах: Вечная золотая коса . Винтажные книги. ISBN   0-465-02685-0 . Перепечатка 1999 года: ISBN   0-465-02656-7 . МИСТЕР 530196
• —, 2007. Я странная петля . Основные книги. ISBN   978-0-465-03078-1 . ISBN   0-465-03078-5 . МИСТЕР 2360307
• Стэнли Джаки , OSB, 2005. Драма величин . Книги реального просмотра.
• Пер Линдстрем , 1997. Аспекты неполноты , Конспекты лекций по логике, т. 10.
• Дж. Р. Лукас , FBA, 1970. Свобода воли . Кларендон Пресс, Оксфорд, 1970.
• Адриан Уильям Мур , 2022. Теорема Гёделя: очень краткое введение . Издательство Оксфордского университета, Оксфорд, 2022.
• Эрнест Нагель , Джеймс Рой Ньюман , Дуглас Хофштадтер, 2002 (1958). Доказательство Гёделя , переработанное изд. ISBN   0-8147-5816-9 . МИСТЕР 1871678
• Руди Ракер , 1995 (1982). Бесконечность и разум: наука и философия бесконечного . Принстонский университет. Нажимать. МИСТЕР 658492
• Смит, Питер (2007). Введение в теоремы Гёделя . Кембридж, Великобритания: Издательство Кембриджского университета. ISBN  978-0-521-67453-9 . МР   2384958 . Архивировано из оригинала 23 октября 2005 г. Проверено 29 октября 2005 г.
• Шанкар, Н. (1994). Метаматематика, машины и доказательство Гёделя . Кембриджские трактаты по теоретической информатике. Том. 38. Кембридж: Издательство Кембриджского университета. ISBN  0-521-58533-3 .
• Рэймонд Смалльян , 1987. Навсегда нерешительно ISBN   0192801414 - головоломки, основанные на неразрешимости в формальных системах.
• —, 1992. Теоремы Гёделя о неполноте . Оксфордский университет. Нажимать. ISBN   0195046722
• —, 1994. Диагонализация и самореференция . Оксфордский университет. Нажимать. МИСТЕР 1318913 . ISBN   0198534507
• —, 2013. Годелевская книга-головоломка: головоломки, парадоксы и доказательства . Курьерская компания. ISBN   978-0-486-49705-1 .
• Ван, Хао (1996). Логическое путешествие: от Гёделя к философии . МТИ Пресс. ISBN  0-262-23189-1 . МИСТЕР 1433803

Разные ссылки

• Берто, Франческо (2009). «Парадокс Гёделя и причины Витгенштейна». Философия Математика . III (17).
• Доусон, Джон В. младший (1996). Логические дилеммы: Жизнь и творчество Курта Гёделя . Тейлор и Фрэнсис. ISBN  978-1-56881-025-6 .
• Доусон, Джон В. младший (1997). Логические дилеммы: Жизнь и творчество Курта Гёделя . Уэлсли, Массачусетс: АК Питерс . ISBN  978-1-56881-256-4 . ОСЛК   36104240 .
• Ребекка Гольдштейн , 2005, Неполнота: доказательство и парадокс Курта Гёделя , WW Norton & Company. ISBN   0-393-05169-2
• Флойд, Джульетта; Патнэм, Хилари (2000). «Заметка о «печально известном абзаце» Витгенштейна о теореме Гёделя». Журнал философии . 97 (11). JSTOR: 624–632. дои : 10.2307/2678455 . ISSN   0022-362X . JSTOR   2678455 .
• Харрисон, Дж. (2009). Справочник по практической логике и автоматизированным рассуждениям . Кембридж: Издательство Кембриджского университета. ISBN  978-0521899574 .
• Дэвид Гильберт и Пол Бернейс , «Основы математики» , Springer-Verlag.
• Хопкрофт, Джон Э .; Ульман, Джеффри (1979). Введение в теорию автоматов, языки и вычисления . Ридинг, Массачусетс: Аддисон-Уэсли. ISBN  0-201-02988-Х .
• Хофштадтер, Дуглас Р. (2007) [2003]. «Глава 12. О нисходящей причинности» . Я странная петля . Основные книги. ISBN  978-0-465-03078-1 . Архивировано из оригинала 8 мая 2019 г. Проверено 24 октября 2018 г.
• Джонс, Джеймс П. (1980). «Неразрешимые диофантовые уравнения» (PDF) . Бюллетень Американского математического общества . 3 (2): 859–862. дои : 10.1090/S0273-0979-1980-14832-6 .
• Клини, Стивен Коул (1967). Математическая логика . Перепечатано Дувром, 2002 г. ISBN   0-486-42533-9
• О'Коннор, Рассел (2005). «Существенная неполнота арифметики, проверенная Coq». Доказательство теорем в логике высшего порядка . Конспекты лекций по информатике. Том. 3603. стр. 245–260. arXiv : cs/0505034 . дои : 10.1007/11541868_16 . ISBN  978-3-540-28372-0 . S2CID   15610367 .
• Полсон, Лоуренс (2014). «Машинное доказательство теорем Гёделя о неполноте теории наследственно конечных множеств» . Обзор символической логики . 7 (3): 484–498. arXiv : 2104.14260 . дои : 10.1017/S1755020314000112 . S2CID   13913592 .
• Священник, Грэм (1984). «Возвращение к логике парадокса». Журнал философской логики . 13 (2): 153–179. дои : 10.1007/BF00453020 .
• Священник, Грэм (2004). «Замечания Витгенштейна по поводу теоремы Гёделя». В Максе Кельбеле (ред.). Непреходящее значение Витгенштейна . Психология Пресс. стр. 207–227. ISBN  978-1-134-40617-3 .
• Священник, Грэм (2006). В противоречии: исследование непоследовательного . Издательство Оксфордского университета. ISBN  0-19-926329-9 .
• Патнэм, Хилари (1960). «Разум и машины». В Сидни Хуке (ред.). Измерения разума: симпозиум . Издательство Нью-Йоркского университета. Перепечатано в издании Андерсона, Арканзас, 1964 г. «Разумы и машины» . Прентис-Холл: 77.
• Вольфганг Раутенберг , 2010, Краткое введение в математическую логику , 3-е. изд., Спрингер, ISBN   978-1-4419-1220-6
• Родыч, Виктор (2003). «Недоразумение Гёделя: новые аргументы о Витгенштейне и новые замечания Витгенштейна». Диалектика . 57 (3): 279–313. дои : 10.1111/j.1746-8361.2003.tb00272.x . дои : 10.1111/j.1746-8361.2003.tb00272.x
• Шела, Сахарон (1974). «Бесконечные абелевы группы, проблема Уайтхеда и некоторые конструкции» . Израильский математический журнал . 18 (3): 243–256. дои : 10.1007/BF02757281 . МР   0357114 .
• Шапиро, Стюарт (2002). «Неполнота и непоследовательность». Разум . 111 (444): 817–32. дои : 10.1093/mind/111.444.817 .
• Сокал, Алан ; Брикмонт, Жан (1999). Модная чушь : злоупотребление наукой постмодернистскими интеллектуалами . Пикадор. ISBN  0-312-20407-8 .
• Шенфилд, Джозеф Р. (1967). Математическая логика . Натик, Массачусетс: Ассоциация символической логики (опубликовано в 2001 г.). ISBN  978-1-56881-135-2 .
• Стэнгрум, Джереми ; Бенсон, Офелия (2006). Почему истина имеет значение . Континуум. ISBN  0-8264-9528-1 .
• Джордж Турлакис, Лекции по логике и теории множеств, Том 1, Математическая логика , Cambridge University Press, 2003. ISBN   978-0-521-75373-9
• Вигдерсон, Ави (2010). «Явления Гёделя в математике: современный взгляд» (PDF) . Курт Гёдель и основы математики: горизонты истины . Издательство Кембриджского университета.
• Хао Ван , 1996, Логическое путешествие: от Гёделя к философии , MIT Press, Кембридж, Массачусетс, ISBN   0-262-23189-1 .
• Зак, Ричард (2007). «Программа Гильберта тогда и сейчас». В Жакетт, Дейл (ред.). Философия логики . Справочник по философии науки. Том. 5. Амстердам: Эльзевир. стр. 411–447. arXiv : math/0508572 . дои : 10.1016/b978-044451541-4/50014-2 . ISBN  978-0-444-51541-4 . OCLC   162131413 . S2CID   291599 .

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

• Теоремы Гёделя о неполноте в наше время на BBC
• «Курт Гёдель» Запись Джульетты Кеннеди в Стэнфордской энциклопедии философии , 5 июля 2011 г.
• «Теоремы Гёделя о неполноте» Запись Пану Раатикайнена в Стэнфордской энциклопедии философии , 11 ноября 2013 г.
• Паранепротиворечивая логика § Арифметика и запись о теореме Гёделя в Стэнфордской энциклопедии философии .
• Биографии МакТьютора:
  • Курт Гёдель. Архивировано 13 октября 2005 г. в Wayback Machine.
  • Герхард Генцен.
• Что такое математика: Теорема Гёделя и ее окрестности Карлиса Подниекса . Бесплатная онлайн-книга.
• Самое краткое в мире объяснение теоремы Гёделя на примере печатной машины.
• Октябрь 2011 г. Эпизод RadioLab о теореме Гёделя о неполноте или ее включении.
• «Теорема Гёделя о неполноте» , Энциклопедия математики , EMS Press , 2001 [1994]
• доказательство Гёделя Как работает , Натали Волчовер , журнал Quanta , 14 июля 2020 г.
• [1] и [2] Теоремы Гёделя о неполноте, формализованные в Isabelle/HOL.

`