Теоремы Гёделя о неполноте — это две теоремы математической логики , которые касаются пределов доказуемости в формальных аксиоматических теориях. Эти результаты, опубликованные Куртом Гёделем в 1931 году, важны как для математической логики, так и для философии математики . Теоремы широко, но не универсально, интерпретируются как показывающие, что программа Гильберта по поиску полного и непротиворечивого набора аксиом для всей математики невозможна.
Первая теорема о неполноте утверждает, что никакая непротиворечивая система аксиом , теоремы которой могут быть перечислены эффективной процедурой (т. е. алгоритмом ), не способна доказать все истины об арифметике натуральных чисел . Для любой такой непротиворечивой формальной системы всегда будут существовать утверждения о натуральных числах, которые истинны, но которые недоказуемы внутри системы.
Вторая теорема о неполноте, являющаяся расширением первой, показывает, что система не может продемонстрировать собственную непротиворечивость.
Используя диагональный аргумент , теоремы Гёделя о неполноте были первыми из нескольких тесно связанных теорем об ограничениях формальных систем. За ними последовали теорема Тарского о невыразимости формальной невыразимости истины, доказательство Чёрча о том, что проблема Entscheidungsproblem Гильберта неразрешима, и теорема Тьюринга о том, что не существует алгоритма для решения проблемы остановки .
Теоремы о неполноте применяются к формальным системам , которые достаточно сложны для выражения базовой арифметики натуральных чисел и которые являются последовательными и эффективно аксиоматизированными. В частности, в контексте логики первого порядка формальные системы также называются формальными теориями . В общем, формальная система — это дедуктивный аппарат, состоящий из определенного набора аксиом вместе с правилами символической манипуляции (или правилами вывода), которые позволяют выводить новые теоремы из аксиом. Одним из примеров такой системы является арифметика Пеано первого порядка , система, в которой все переменные предназначены для обозначения натуральных чисел. В других системах, таких как теория множеств , только некоторые предложения формальной системы выражают утверждения о натуральных числах. Теоремы о неполноте касаются формальной доказуемости в этих системах, а не «доказуемости» в неформальном смысле.
Формальная система может обладать несколькими свойствами, включая полноту, непротиворечивость и существование эффективной аксиоматизации. Теоремы о неполноте показывают, что системы, содержащие достаточное количество арифметики, не могут обладать всеми тремя этими свойствами.
Формальная система называется эффективно аксиоматизированной (еще ее называют эффективно сгенерированной ), если ее набор теорем рекурсивно перечислим . Это означает, что существует компьютерная программа, которая, в принципе, могла бы перечислить все теоремы системы, не перечисляя никаких утверждений, которые не являются теоремами. Примерами эффективно сгенерированных теорий являются арифметика Пеано и теория множеств Цермело–Френкеля (ZFC). [1]
Теория, известная как истинная арифметика, состоит из всех истинных утверждений о стандартных целых числах на языке арифметики Пеано. Эта теория является последовательной и полной и содержит достаточное количество арифметики. Однако она не имеет рекурсивно перечислимого множества аксиом и, таким образом, не удовлетворяет гипотезам теорем о неполноте.
Набор аксиом является ( синтаксически или отрицательно ) полным , если для любого утверждения на языке аксиом это утверждение или его отрицание доказуемо из аксиом. [2] Это понятие относится к первой теореме Гёделя о неполноте. Его не следует путать с семантической полнотой, которая означает, что набор аксиом доказывает все семантические тавтологии данного языка. В своей теореме о полноте (не следует путать с теоремами о неполноте, описанными здесь) Гёдель доказал, что логика первого порядка семантически полна. Но она не является синтаксически полной, поскольку существуют предложения, выражаемые на языке логики первого порядка, которые не могут быть ни доказаны, ни опровергнуты из одних только аксиом логики.
Такие мыслители, как Гильберт, считали, что в системе математики нахождение такой аксиоматизации, которая позволит либо доказать, либо опровергнуть (путем доказательства ее отрицания) каждую математическую формулу, — это лишь вопрос времени.
Формальная система может быть синтаксически неполной по замыслу, как это обычно бывает с логикой. Или она может быть неполной просто потому, что не все необходимые аксиомы были обнаружены или включены. Например, евклидова геометрия без постулата о параллельности неполна, потому что некоторые утверждения в языке (например, сам постулат о параллельности) не могут быть доказаны из оставшихся аксиом. Аналогично, теория плотных линейных порядков не является полной, но становится полной с дополнительной аксиомой, утверждающей, что в порядке нет конечных точек. Гипотеза континуума — это утверждение в языке ZFC , которое не доказуемо в рамках ZFC, поэтому ZFC не является полным. В этом случае нет очевидного кандидата на новую аксиому, которая решает проблему.
Теория арифметики Пеано первого порядка кажется последовательной. Предполагая, что это действительно так, отметим, что она имеет бесконечный, но рекурсивно перечислимый набор аксиом и может кодировать достаточно арифметики для гипотез теоремы о неполноте. Таким образом, по первой теореме о неполноте арифметика Пеано не является полной. Теорема дает явный пример утверждения арифметики, которое не является ни доказуемым, ни опровергаемым в арифметике Пеано. Более того, это утверждение верно в обычной модели . Кроме того, никакое эффективно аксиоматизированное, последовательное расширение арифметики Пеано не может быть полным.
Набор аксиом (просто) непротиворечив , если нет такого утверждения, что и утверждение, и его отрицание доказуемы из аксиом, и непротиворечив в противном случае. То есть непротиворечивая аксиоматическая система — это система, свободная от противоречий.
Арифметика Пеано доказуемо непротиворечива из ZFC, но не изнутри себя. Аналогично, ZFC не доказуемо непротиворечива изнутри себя, но ZFC + «существует недостижимый кардинал » доказывает, что ZFC непротиворечива, потому что если κ — наименьший такой кардинал, то V κ, находящееся внутри вселенной фон Неймана, является моделью ZFC, а теория непротиворечива тогда и только тогда, когда у нее есть модель.
Если взять все утверждения на языке арифметики Пеано в качестве аксиом, то эта теория является полной, имеет рекурсивно перечислимый набор аксиом и может описывать сложение и умножение. Однако она не является последовательной.
Дополнительные примеры противоречивых теорий возникают из парадоксов , возникающих, когда в теории множеств предполагается аксиоматическая схема неограниченного понимания .
Теоремы о неполноте применяются только к формальным системам, которые способны доказать достаточный набор фактов о натуральных числах. Одним из достаточных наборов является набор теорем арифметики Робинсона Q. Некоторые системы, такие как арифметика Пеано, могут напрямую выражать утверждения о натуральных числах. Другие, такие как теория множеств ZFC, способны интерпретировать утверждения о натуральных числах на своем языке. Любой из этих вариантов подходит для теорем о неполноте.
Теория алгебраически замкнутых полей заданной характеристики является полной, непротиворечивой и имеет бесконечное, но рекурсивно перечислимое множество аксиом. Однако в эту теорию невозможно закодировать целые числа, и теория не может описать арифметику целых чисел. Похожий пример — теория вещественных замкнутых полей , которая по сути эквивалентна аксиомам Тарского для евклидовой геометрии . Таким образом, сама евклидова геометрия (в формулировке Тарского) является примером полной, непротиворечивой, эффективно аксиоматизированной теории.
Система арифметики Пресбургера состоит из набора аксиом для натуральных чисел с единственной операцией сложения (умножение опущено). Арифметика Пресбургера является полной, непротиворечивой и рекурсивно перечислимой и может кодировать сложение, но не умножение натуральных чисел, показывая, что для теорем Гёделя нужна теория, кодирующая не только сложение, но и умножение.
Дэн Уиллард (2001) изучил некоторые слабые семейства арифметических систем, которые допускают достаточно арифметики в виде отношений для формализации нумерации Гёделя, но которые недостаточно сильны, чтобы иметь умножение в качестве функции, и поэтому не могут доказать вторую теорему о неполноте; то есть эти системы непротиворечивы и способны доказать свою собственную непротиворечивость (см. самопроверяющиеся теории ).
При выборе набора аксиом одна из целей состоит в том, чтобы иметь возможность доказать как можно больше правильных результатов, не доказывая никаких неправильных результатов. Например, мы могли бы представить себе набор истинных аксиом, которые позволяют нам доказать каждое истинное арифметическое утверждение о натуральных числах (Smith 2007, стр. 2). В стандартной системе логики первого порядка несогласованный набор аксиом докажет каждое утверждение на своем языке (иногда это называют принципом взрыва ) , и, таким образом, автоматически является полным. Однако набор аксиом, который является как полным, так и непротиворечивым, доказывает максимальный набор непротиворечивых теорем. [ требуется цитата ]
Шаблон, проиллюстрированный в предыдущих разделах с помощью арифметики Пеано, ZFC и ZFC + «существует недоступный кардинал», в общем случае не может быть нарушен. Здесь ZFC + «существует недоступный кардинал» не может быть доказано само по себе непротиворечивым. Он также не является полным, как показано в гипотезе континуума, которая неразрешима [3] в ZFC + «существует недоступный кардинал».
Первая теорема о неполноте показывает, что в формальных системах, которые могут выражать базовую арифметику, полный и непротиворечивый конечный список аксиом никогда не может быть создан: каждый раз, когда добавляется дополнительное, непротиворечивое утверждение в качестве аксиомы, есть другие истинные утверждения, которые все еще не могут быть доказаны, даже с новой аксиомой. Если когда-либо добавляется аксиома, которая делает систему полной, это происходит за счет того, что система становится непоследовательной. Невозможно даже, чтобы бесконечный список аксиом был полным, непротиворечивым и эффективно аксиоматизированным.
Первая теорема Гёделя о неполноте впервые появилась как «Теорема VI» в статье Гёделя 1931 года « О формально неразрешимых предложениях Principia Mathematica и связанных с ними системах I». Гипотезы теоремы были вскоре улучшены Дж. Баркли Россером (1936) с использованием приема Россера . Полученная теорема (включающая улучшение Россера) может быть перефразирована на английский язык следующим образом, где «формальная система» включает предположение, что система эффективно сгенерирована.
Первая теорема о неполноте : «Любая непротиворечивая формальная система F, в рамках которой может быть выполнено определенное количество элементарной арифметики, является неполной; то есть существуют утверждения языка F , которые не могут быть ни доказаны, ни опровергнуты в F ». (Раатикайнен 2020)
Недоказуемое утверждение G F, на которое ссылается теорема, часто называют «предложением Гёделя» для системы F. Доказательство конструирует конкретное предложение Гёделя для системы F , но в языке системы существует бесконечно много утверждений, которые обладают теми же свойствами, например, конъюнкция предложения Гёделя и любого логически допустимого предложения.
Каждая эффективно сгенерированная система имеет свое собственное предложение Гёделя. Можно определить большую систему F' , которая содержит все F плюс G F как дополнительную аксиому. Это не приведет к полной системе, потому что теорема Гёделя будет также применяться к F' , и, таким образом, F' также не может быть полным. В этом случае G F действительно является теоремой в F' , потому что это аксиома. Поскольку G F утверждает только то, что она недоказуема в F , ее доказуемость в F' не представляет противоречия . Однако, поскольку теорема о неполноте применима к F' , будет новое утверждение Гёделя G F ' для F' , показывающее, что F' также неполно. G F ' будет отличаться от G F тем, что G F ' будет ссылаться на F' , а не на F .
Предложение Гёделя предназначено для косвенного указания на себя. Предложение утверждает, что когда определенная последовательность шагов используется для построения другого предложения, это построенное предложение не будет доказуемо в F . Однако последовательность шагов такова, что построенное предложение оказывается самим G F . Таким образом, предложение Гёделя G F косвенно утверждает свою собственную недоказуемость в F (Smith 2007, p. 135).
Для доказательства первой теоремы о неполноте Гёдель продемонстрировал, что понятие доказуемости в системе может быть выражено исключительно в терминах арифметических функций, которые оперируют с гёделевыми числами предложений системы. Следовательно, система, которая может доказывать определенные факты о числах, может также косвенно доказывать факты о своих собственных утверждениях, при условии, что она эффективно сгенерирована. Вопросы о доказуемости утверждений в системе представлены как вопросы об арифметических свойствах самих чисел, которые были бы разрешимы системой, если бы она была полной.
Таким образом, хотя предложение Гёделя косвенно ссылается на предложения системы F , при прочтении как арифметического утверждения предложение Гёделя напрямую ссылается только на натуральные числа. Оно утверждает, что никакое натуральное число не имеет определенного свойства, где это свойство задается примитивным рекурсивным отношением (Smith 2007, p. 141). Таким образом, предложение Гёделя может быть записано на языке арифметики с простой синтаксической формой. В частности, его можно выразить как формулу на языке арифметики, состоящую из ряда ведущих кванторов общности, за которыми следует тело без кванторов (эти формулы находятся на уровне арифметической иерархии ). С помощью теоремы MRDP предложение Гёделя может быть переписано как утверждение, что конкретный многочлен от многих переменных с целыми коэффициентами никогда не принимает значения ноль, когда вместо его переменных подставляются целые числа (Franzén 2005, p. 71).
Первая теорема о неполноте показывает, что предложение Гёделя G F соответствующей формальной теории F недоказуемо в F . Поскольку, будучи интерпретировано как утверждение об арифметике, эта недоказуемость является именно тем, что (косвенно) утверждает предложение, предложение Гёделя на самом деле истинно (Smoryński 1977, стр. 825; см. также Franzén 2005, стр. 28–33). По этой причине предложение G F часто называют «истинным, но недоказуемым» (Raatikainen 2020). Однако, поскольку предложение Гёделя само по себе не может формально указать свою предполагаемую интерпретацию, истинность предложения G F может быть достигнута только посредством метаанализа извне системы. В общем случае этот метаанализ можно провести в рамках слабой формальной системы, известной как примитивная рекурсивная арифметика , которая доказывает импликацию Con ( F )→ G F , где Con ( F ) — каноническое предложение, утверждающее непротиворечивость F (Smoryński 1977, стр. 840, Kikuchi & Tanaka 1994, стр. 403).
Хотя предложение Гёделя последовательной теории истинно как утверждение о предполагаемой интерпретации арифметики, предложение Гёделя будет ложным в некоторых нестандартных моделях арифметики , как следствие теоремы Гёделя о полноте (Franzén 2005, стр. 135). Эта теорема показывает, что когда предложение не зависит от теории, теория будет иметь модели, в которых предложение истинно, и модели, в которых предложение ложно. Как было описано ранее, предложение Гёделя системы F является арифметическим утверждением, которое утверждает, что не существует числа с определенным свойством. Теорема о неполноте показывает, что это утверждение будет независимым от системы F , и истинность предложения Гёделя следует из того факта, что никакое стандартное натуральное число не обладает рассматриваемым свойством. Любая модель, в которой предложение Гёделя ложно, должна содержать некоторый элемент, который удовлетворяет свойству в пределах этой модели. Такая модель должна быть «нестандартной» – она должна содержать элементы, которые не соответствуют ни одному стандартному натуральному числу (Raatikainen 2020, Franzén 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. [4] Эта теорема сильнее первой теоремы о неполноте, поскольку утверждение, построенное в первой теореме о неполноте, не выражает непосредственно непротиворечивость системы. Доказательство второй теоремы о неполноте получается путем формализаций доказательства первой теоремы о неполноте в самой системе F.
Во второй теореме о неполноте есть техническая тонкость, касающаяся способа выражения согласованности F в виде формулы на языке F. Существует много способов выразить согласованность системы, и не все из них приводят к одному и тому же результату. Формула Cons( F ) из второй теоремы о неполноте является частным выражением согласованности.
Другие формализации утверждения о том, что F является непротиворечивым, могут быть неэквивалентными в F , а некоторые могут быть даже доказуемыми. Например, арифметика Пеано первого порядка (PA) может доказать, что «наибольшее непротиворечивое подмножество PA» является непротиворечивым. Но поскольку PA является непротиворечивым, наибольшее непротиворечивое подмножество PA — это просто PA, так что в этом смысле PA «доказывает, что оно является непротиворечивым». Чего PA не доказывает, так это того, что наибольшее непротиворечивое подмножество PA — это, по сути, весь PA. (Термин «наибольшее непротиворечивое подмножество PA» здесь подразумевает наибольший непротиворечивый начальный сегмент аксиом PA при некотором конкретном эффективном перечислении.)
Стандартное доказательство второй теоремы о неполноте предполагает, что предикат доказуемости Prov A ( P ) удовлетворяет условиям доказуемости Гильберта–Бернейса . Если #( P ) представляет собой гёделевский номер формулы P , то условия доказуемости гласят:
Существуют системы, такие как арифметика Робинсона, которые достаточно сильны, чтобы соответствовать предположениям первой теоремы о неполноте, но которые не доказывают условия Гильберта–Бернейса. Арифметика Пеано, однако, достаточно сильна, чтобы проверить эти условия, как и все теории, более сильные, чем арифметика Пеано.
Вторая теорема Гёделя о неполноте также подразумевает, что система F 1 , удовлетворяющая техническим условиям, описанным выше, не может доказать непротиворечивость любой системы F 2 , которая доказывает непротиворечивость F 1 . Это происходит потому, что такая система F 1 может доказать, что если F 2 доказывает непротиворечивость F 1 , то F 1 на самом деле непротиворечива. Ведь утверждение о том, что F 1 непротиворечива, имеет вид «для всех чисел n , n имеет разрешимое свойство не быть кодом для доказательства противоречия в F 1 ». Если бы F 1 была на самом деле непротиворечива, то F 2 доказала бы для некоторого n , что n является кодом противоречия в F 1 . Но если бы F 2 также доказала, что F 1 непротиворечива (то есть, что такого n не существует ), то она сама была бы непротиворечивой. Это рассуждение можно формализовать в F 1 , чтобы показать, что если F 2 непротиворечива, то F 1 непротиворечива. Поскольку по второй теореме о неполноте F 1 не доказывает своей непротиворечивости, она не может доказать и непротиворечивость F 2 .
Это следствие второй теоремы о неполноте показывает, что нет никакой надежды доказать, например, непротиворечивость арифметики Пеано, используя любые финитные средства, которые могут быть формализованы в системе, непротиворечивость которой доказуема в арифметике Пеано (PA). Например, система примитивной рекурсивной арифметики (PRA), которая широко принята как точная формализация финитной математики, доказуемо непротиворечива в PA. Таким образом, PRA не может доказать непротиворечивость PA. Этот факт обычно рассматривается как подразумевающий, что программа Гильберта , которая была направлена на оправдание использования «идеальных» (инфинитных) математических принципов в доказательствах «реальных» (финитных) математических утверждений путем предоставления финитного доказательства того, что идеальные принципы непротиворечивы, не может быть выполнена. [5]
Следствие также указывает на эпистемологическую значимость второй теоремы о неполноте. Она не дала бы никакой интересной информации, если бы система F доказала свою непротиворечивость. Это происходит потому, что непротиворечивые теории доказывают все, включая свою непротиворечивость. Таким образом, доказательство непротиворечивости F в F не дало бы нам никакого ключа к разгадке того, является ли F непротиворечивой; никакие сомнения относительно непротиворечивости F не были бы разрешены таким доказательством непротиворечивости. Интерес к доказательствам непротиворечивости заключается в возможности доказательства непротиворечивости системы F в некоторой системе F', которая в некотором смысле менее сомнительна, чем сама F , например, слабее, чем F . Для многих естественно возникающих теорий F и F' , таких как F = теория множеств Цермело–Френкеля и F' = примитивная рекурсивная арифметика, непротиворечивость F' доказуема в F , и, таким образом, F' не может доказать непротиворечивость F с помощью приведенного выше следствия второй теоремы о неполноте.
Вторая теорема о неполноте не исключает полностью возможность доказательства непротиворечивости другой системы с другими аксиомами. Например, Герхард Генцен доказал непротиворечивость арифметики Пеано в другой системе, которая включает аксиому, утверждающую, что ординал, называемый ε 0, является обоснованным ; см. доказательство непротиворечивости Генцена . Теорема Генцена стимулировала развитие ординального анализа в теории доказательств.
В математике и информатике есть два различных смысла слова «неразрешимый». Первый из них — это смысл теории доказательств, используемый в отношении теорем Гёделя, когда утверждение не является ни доказуемым, ни опровергаемым в указанной дедуктивной системе . Второй смысл, который здесь обсуждаться не будет, используется в отношении теории вычислимости и применяется не к утверждениям, а к проблемам принятия решений , которые представляют собой счетные бесконечные наборы вопросов, каждый из которых требует ответа «да» или «нет». Такая проблема называется неразрешимой, если не существует вычислимой функции , которая правильно отвечает на каждый вопрос в наборе проблем (см. неразрешимая проблема ).
Из-за двух значений слова «неразрешимый» термин « независимый» иногда используется вместо «неразрешимый» в смысле «ни доказуемый, ни опровержимый».
Неразрешимость утверждения в конкретной дедуктивной системе сама по себе не решает вопрос о том, является ли истинностное значение утверждения четко определенным или его можно определить другими способами. Неразрешимость подразумевает лишь то, что рассматриваемая конкретная дедуктивная система не доказывает истинность или ложность утверждения. Существуют ли так называемые «абсолютно неразрешимые» утверждения, истинностное значение которых никогда не может быть известно или плохо определено, является спорным моментом в философии математики .
Совместная работа Гёделя и Пола Коэна дала два конкретных примера неразрешимых утверждений (в первом смысле этого термина): континуум-гипотеза не может быть ни доказана, ни опровергнута в ZFC (стандартная аксиоматизация теории множеств ), а аксиома выбора не может быть ни доказана, ни опровергнута в ZF (которая включает в себя все аксиомы ZFC, за исключением аксиомы выбора). Эти результаты не требуют теоремы о неполноте. Гёдель доказал в 1940 году, что ни одно из этих утверждений не может быть опровергнуто в ZF или теории множеств ZFC. В 1960-х годах Коэн доказал, что ни одно из них не доказуемо из ZF, и континуум-гипотеза не может быть доказана из ZFC.
Шелах (1974) показал, что проблема Уайтхеда в теории групп неразрешима в первом смысле этого термина в стандартной теории множеств. [6]
Грегори Хайтин создал неразрешимые утверждения в алгоритмической теории информации и доказал еще одну теорему о неполноте в этой постановке. Теорема Хайтина о неполноте утверждает, что для любой системы, которая может представлять достаточно арифметики, существует верхняя граница c, такая, что в этой системе нельзя доказать, что ни одно конкретное число имеет сложность Колмогорова больше, чем c . В то время как теорема Гёделя связана с парадоксом лжеца , результат Хайтина связан с парадоксом Берри .
Это естественные математические эквиваленты предложения Гёделя "истинно, но неразрешимо". Они могут быть доказаны в более крупной системе, которая обычно принимается как допустимая форма рассуждения, но неразрешимы в более ограниченной системе, такой как арифметика Пеано.
В 1977 году Пэрис и Харрингтон доказали, что принцип Пэрис-Харрингтона , версия бесконечной теоремы Рамсея , неразрешим в арифметике Пеано (первого порядка) , но может быть доказан в более сильной системе арифметики второго порядка . Кирби и Пэрис позже показали, что теорема Гудстейна , утверждение о последовательностях натуральных чисел, несколько более простое, чем принцип Пэрис-Харрингтона, также неразрешима в арифметике Пеано.
Теорема о дереве Крускала , которая имеет приложения в информатике, также неразрешима из арифметики Пеано, но доказуема в теории множеств. Фактически, теорема о дереве Крускала (или ее конечная форма) неразрешима в гораздо более сильной системе ATR 0 , кодифицирующей принципы, приемлемые на основе философии математики, называемой предикативизмом . [7] Связанная, но более общая теорема о миноре графа (2003) имеет последствия для теории вычислительной сложности .
Теорема о неполноте тесно связана с несколькими результатами о неразрешимых множествах в теории рекурсии .
Клини (1943) представил доказательство теоремы Гёделя о неполноте, используя основные результаты теории вычислимости. Один из таких результатов показывает, что проблема остановки неразрешима: ни одна компьютерная программа не может правильно определить, если в качестве входных данных задана любая программа P , остановится ли P в конечном итоге при запуске с определенными входными данными. Клини показал, что существование полной эффективной системы арифметики с определенными свойствами согласованности заставило бы проблему остановки быть разрешимой, противоречие. [8] Этот метод доказательства также был представлен Шоенфилдом (1967); Чарльзвортом (1981); и Хопкрофтом и Ульманом (1979). [9]
Францен (2005) объясняет, как решение Матиясевича 10-й проблемы Гильберта может быть использовано для получения доказательства первой теоремы Гёделя о неполноте. [10] Матиясевич доказал, что не существует алгоритма, который, имея многомерный многочлен p ( x 1 , x 2 ,..., x k ) с целыми коэффициентами, определял бы, существует ли целочисленное решение уравнения p = 0. Поскольку многочлены с целыми коэффициентами и сами целые числа напрямую выражаются на языке арифметики, если многомерное целочисленное многочленное уравнение p = 0 имеет решение в целых числах, то любая достаточно сильная система арифметики T докажет это. Более того, предположим, что система T является ω-непротиворечивой. В этом случае она никогда не докажет, что конкретное многочленное уравнение имеет решение, когда решения в целых числах нет. Таким образом, если бы T была полной и ω-непротиворечивой, можно было бы алгоритмически определить, имеет ли полиномиальное уравнение решение, просто перечисляя доказательства T до тех пор, пока не будет найдено либо « p имеет решение», либо « p не имеет решения», что противоречит теореме Матиясевича. Отсюда следует, что T не может быть ω-непротиворечивой и полной. Более того, для каждой непротиворечивой эффективно сгенерированной системы T можно эффективно сгенерировать многомерный полином p над целыми числами, такой , что уравнение p = 0 не имеет решений над целыми числами, но отсутствие решений не может быть доказано в T. [11]
Сморыньский (1977) показывает, как существование рекурсивно неразделимых множеств может быть использовано для доказательства первой теоремы о неполноте. Это доказательство часто расширяется, чтобы показать, что такие системы, как арифметика Пеано, по сути неразрешимы . [12]
Теорема неполноты Хайтина дает другой метод получения независимых предложений, основанный на сложности Колмогорова . Как и доказательство, представленное Клини, которое было упомянуто выше, теорема Хайтина применима только к теориям с дополнительным свойством, что все их аксиомы истинны в стандартной модели натуральных чисел. Теорема неполноты Гёделя отличается своей применимостью к непротиворечивым теориям, которые, тем не менее, включают ложные утверждения в стандартной модели; такие теории известны как ω-непротиворечивые .
Доказательство от противного состоит из трех основных частей. Для начала выберите формальную систему, которая соответствует предложенным критериям:
Основная проблема в конкретизации доказательства, описанного выше, заключается в том, что на первый взгляд кажется, что для построения утверждения p , эквивалентного « p не может быть доказано», p каким-то образом должен содержать ссылку на p , что может легко привести к бесконечному регрессу. Метод Гёделя заключается в том, чтобы показать, что утверждения могут быть сопоставлены с числами (часто называемыми арифметизацией синтаксиса ) таким образом, что «доказательство утверждения» может быть заменено на «проверку того, обладает ли число заданным свойством» . Это позволяет построить самореферентную формулу таким образом, чтобы избежать любого бесконечного регресса определений. Этот же метод позже использовал Алан Тьюринг в своей работе над Entscheidungsproblem .
Проще говоря, можно разработать метод, при котором каждая формула или утверждение, которые можно сформулировать в системе, получит уникальный номер, называемый ее номером Гёделя , таким образом, что можно будет механически преобразовывать формулы и номера Гёделя туда и обратно. Числа, которые в них участвуют, могут быть действительно очень длинными (с точки зрения количества цифр), но это не является препятствием; важно только то, что такие числа можно построить. Простой пример — как английский язык можно хранить в виде последовательности чисел для каждой буквы , а затем объединять в одно большее число:
В принципе, доказательство истинности или ложности утверждения может быть показано как эквивалентное доказательству того, что число, соответствующее утверждению, имеет или не имеет заданное свойство. Поскольку формальная система достаточно сильна, чтобы поддерживать рассуждения о числах в целом , она может поддерживать рассуждения о числах, которые представляют формулы и утверждения, а также. Важно, что, поскольку система может поддерживать рассуждения о свойствах чисел , результаты эквивалентны рассуждениям о доказуемости их эквивалентных утверждений .
Показав, что в принципе система может косвенно делать утверждения о доказуемости, путем анализа свойств чисел, представляющих утверждения, теперь можно показать, как создать утверждение, которое действительно это делает.
Формула F ( x ), содержащая ровно одну свободную переменную x , называется формой утверждения или классовым знаком . Как только x заменяется определенным числом, форма утверждения превращается в добросовестное утверждение, и тогда оно либо доказуемо в системе, либо нет. Для некоторых формул можно показать, что для каждого натурального числа n , истинно тогда и только тогда, когда это можно доказать (точное требование в исходном доказательстве слабее, но для наброска доказательства этого будет достаточно). В частности, это верно для каждой конкретной арифметической операции между конечным числом натуральных чисел, такой как «2 × 3 = 6».
Формы утверждений сами по себе не являются утверждениями и, следовательно, не могут быть доказаны или опровергнуты. Но каждой форме утверждения F ( x ) можно присвоить гёделевский номер, обозначаемый как G ( F ) . Выбор свободной переменной, используемой в форме F ( x ) , не имеет значения для присвоения гёделевского номера G ( F ) .
Само понятие доказуемости также может быть закодировано числами Гёделя следующим образом: поскольку доказательство представляет собой список утверждений, которые подчиняются определенным правилам, можно определить число Гёделя доказательства. Теперь для каждого утверждения p можно спросить, является ли число x числом Гёделя его доказательства. Отношение между числом Гёделя p и x , потенциальным числом Гёделя его доказательства, является арифметическим отношением между двумя числами. Следовательно, существует форма утверждения Bew ( y ) , которая использует это арифметическое отношение для утверждения, что число Гёделя доказательства y существует:
Название Bew является сокращением от beweisbar , немецкого слова, означающего «доказуемый»; это название изначально использовалось Гёделем для обозначения только что описанной формулы доказуемости. Обратите внимание, что « Bew ( y ) » — это всего лишь аббревиатура, представляющая собой конкретную, очень длинную формулу на исходном языке T ; сама строка « Bew » не претендует на то, чтобы быть частью этого языка.
Важной особенностью формулы Bew ( y ) является то, что если утверждение p доказуемо в системе, то Bew ( G ( p )) также доказуемо. Это происходит потому, что любое доказательство p будет иметь соответствующее число Гёделя, существование которого приводит к удовлетворению Bew( G ( p )) .
Следующий шаг в доказательстве — получить утверждение, которое косвенно утверждает свою собственную недоказуемость. Хотя Гёдель построил это утверждение напрямую, существование по крайней мере одного такого утверждения следует из диагональной леммы , которая гласит, что для любой достаточно сильной формальной системы и любого утверждения формы F существует утверждение p такое, что система доказывает
Полагая F отрицанием Bew ( x ) , получаем теорему
и определяемое этим число 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 » в качестве аксиом. Но тогда определение «быть гёделевым номером доказательства» утверждения изменится. Это означает, что формула Bew ( x ) теперь другая. Таким образом, когда мы применяем диагональную лемму к этому новому Bew, мы получаем новое утверждение p , отличное от предыдущего, которое будет неразрешимым в новой системе, если оно ω-непротиворечиво.
Булос (1989) набрасывает альтернативное доказательство первой теоремы о неполноте, которое использует парадокс Берри вместо парадокса лжеца для построения истинной, но недоказуемой формулы. Похожий метод доказательства был независимо открыт Солом Крипке . [13] Доказательство Булоса осуществляется путем построения для любого вычислимо перечислимого множества S истинных предложений арифметики другого предложения, которое является истинным, но не содержится в S. Это дает первую теорему о неполноте как следствие. По словам Булоса, это доказательство интересно, потому что оно дает «другой вид причины» для неполноты эффективных, последовательных теорий арифметики. [14]
Теоремы о неполноте относятся к сравнительно небольшому числу нетривиальных теорем, которые были преобразованы в формализованные теоремы, которые могут быть полностью проверены программным обеспечением- помощником по доказательству . Оригинальные доказательства Гёделя теорем о неполноте, как и большинство математических доказательств, были написаны на естественном языке, предназначенном для чтения людьми.
Компьютерно-проверенные доказательства версий первой теоремы о неполноте были анонсированы Натараджаном Шанкаром в 1986 году с использованием Nqthm (Shankar 1994), Расселом О'Коннором в 2003 году с использованием Coq (O'Connor 2005) и Джоном Харрисоном в 2009 году с использованием HOL Light (Harrison 2009). Компьютерно-проверенное доказательство обеих теорем о неполноте было анонсировано Лоуренсом Полсоном в 2013 году с использованием Isabelle (Paulson 2014).
Основная трудность доказательства второй теоремы о неполноте состоит в том, чтобы показать, что различные факты о доказуемости, используемые в доказательстве первой теоремы о неполноте, могут быть формализованы в системе S с использованием формального предиката P для доказуемости. Как только это сделано, вторая теорема о неполноте следует за формализацией всего доказательства первой теоремы о неполноте в самой системе S.
Пусть p обозначает неразрешимое предложение, построенное выше, и предположим для целей получения противоречия, что непротиворечивость системы S может быть доказана изнутри самой системы S. Это эквивалентно доказательству утверждения «Система S непротиворечива». Теперь рассмотрим утверждение c , где c = «Если система S непротиворечива, то p недоказуемо». Доказательство предложения c может быть формализовано внутри системы S , и поэтому утверждение c , « p недоказуемо» (или тождественно, «не P ( p ) ») может быть доказано в системе S .
Заметьте, что если мы можем доказать, что система S непротиворечива (т. е. утверждение в гипотезе c ), то мы доказали, что p недоказуемо. Но это противоречие, поскольку по 1-й теореме о неполноте это предложение (т. е. то, что подразумевается в предложении c , "" p " недоказуемо") является тем, что мы строим как недоказуемое. Обратите внимание, что именно поэтому мы требуем формализовать первую теорему о неполноте в S : чтобы доказать 2-ю теорему о неполноте, мы получаем противоречие с 1-й теоремой о неполноте, что можно сделать, только показав, что теорема верна в S . Поэтому мы не можем доказать, что система S непротиворечива. И отсюда следует утверждение 2-й теоремы о неполноте.
Результаты неполноты влияют на философию математики , в частности на версии формализма , которые используют единую систему формальной логики для определения своих принципов.
Иногда считается, что теорема о неполноте имеет серьезные последствия для программы логицизма, предложенной Готтлобом Фреге и Бертраном Расселом , которая стремилась определить натуральные числа в терминах логики. [15] Боб Хейл и Криспин Райт утверждают, что это не проблема для логицизма, поскольку теоремы о неполноте в равной степени применимы как к логике первого порядка, так и к арифметике. Они утверждают, что эта проблема существует только у тех, кто считает, что натуральные числа должны определяться в терминах логики первого порядка.
Многие логики полагают, что теоремы Гёделя о неполноте нанесли смертельный удар по второй проблеме Дэвида Гильберта , которая требовала доказательства финитной непротиворечивости математики. Вторая теорема о неполноте, в частности, часто рассматривается как делающая проблему невозможной. Однако не все математики согласны с этим анализом, и статус второй проблемы Гильберта еще не определен (см. « Современные точки зрения на статус проблемы »).
Авторы, включая философа Дж. Р. Лукаса и физика Роджера Пенроуза, спорили о том, что, если вообще что-то, теоремы Гёделя о неполноте подразумевают относительно человеческого интеллекта. Большая часть дебатов вращается вокруг вопроса о том, эквивалентен ли человеческий разум машине Тьюринга или, согласно тезису Чёрча-Тьюринга , любой конечной машине вообще. Если это так, и если машина непротиворечива, то теоремы Гёделя о неполноте применимы к ней.
Патнэм (1960) предположил, что хотя теоремы Гёделя не могут быть применены к людям, поскольку они совершают ошибки и, следовательно, непоследовательны, их можно применить к человеческой способности к науке или математике в целом. Если предположить, что они последовательны, то либо их последовательность не может быть доказана, либо их нельзя представить с помощью машины Тьюринга. [16]
Вигдерсон (2010) предложил, что концепция математической «познаваемости» должна основываться на вычислительной сложности , а не на логической разрешимости. Он пишет, что «когда познаваемость интерпретируется по современным стандартам, а именно через вычислительную сложность, явления Гёделя очень близки нам». [17]
Дуглас Хофштадтер в своих книгах «Гёдель, Эшер, Бах и «Я — странная петля » приводит теоремы Гёделя в качестве примера того, что он называет странной петлей , иерархической, самореферентной структурой, существующей в аксиоматической формальной системе. Он утверждает, что это тот же тип структуры, который порождает сознание, чувство «я» в человеческом разуме. В то время как самореферентность в теореме Гёделя исходит из предложения Гёделя, утверждающего его недоказуемость в формальной системе Principia Mathematica, самореферентность в человеческом разуме исходит из того, как мозг абстрагирует и классифицирует стимулы в «символы» или группы нейронов, которые реагируют на концепции, в том, что фактически также является формальной системой, в конечном итоге порождая символы, моделирующие концепцию самой сущности, осуществляющей восприятие. Хофштадтер утверждает, что странная петля в достаточно сложной формальной системе может привести к "нисходящей" или "перевернутой" причинности, ситуации, в которой обычная иерархия причин и следствий переворачивается с ног на голову. В случае теоремы Гёделя это проявляется, вкратце, следующим образом:
Просто зная значение формулы, можно сделать вывод об ее истинности или ложности без каких-либо усилий, чтобы вывести ее старомодным способом, который требует методичного продвижения «вверх» от аксиом. Это не просто странно; это поразительно. Обычно нельзя просто посмотреть на то, что говорит математическая догадка, и просто обратиться к содержанию этого утверждения, чтобы сделать вывод, является ли утверждение истинным или ложным. [18]
В случае разума, гораздо более сложной формальной системы, эта «нисходящая причинность» проявляется, по мнению Хофштадтера, как невыразимый человеческий инстинкт, согласно которому причинность нашего разума лежит на высоком уровне желаний, концепций, личностей, мыслей и идей, а не на низком уровне взаимодействий между нейронами или даже фундаментальными частицами, хотя, согласно физике, последние, по-видимому, обладают причинной силой.
Таким образом, в нашем обычном человеческом способе восприятия мира присутствует любопытная перевернутость: мы созданы для восприятия «больших вещей», а не «маленьких вещей», хотя именно в области крошечного, по-видимому, находятся настоящие двигатели, управляющие реальностью. [18]
Хотя теоремы Гёделя обычно изучаются в контексте классической логики, они также играют роль в изучении паранепротиворечивой логики и внутренне противоречивых утверждений ( диалетеи ). Прист (1984, 2006) утверждает, что замена понятия формального доказательства в теореме Гёделя обычным понятием неформального доказательства может быть использована для того, чтобы показать, что наивная математика непоследовательна, и использует это как доказательство диалетеизма . [ 19] Причиной этой непоследовательности является включение предиката истинности для системы в язык системы. [20] Шапиро (2002) дает более смешанную оценку приложений теорем Гёделя к диалетеизму. [21]
Иногда приводятся апелляции и аналогии к неполноте теорем в поддержку аргументов, выходящих за рамки математики и логики. Несколько авторов негативно отозвались о таких расширениях и интерпретациях, включая Францена (2005), Раатикайнена (2005), Сокала и Брикмонта (1999); и Стэнгрума и Бенсона (2006). [22] Сокала и Брикмонта (1999) и Стэнгрума и Бенсона (2006), например, цитируют комментарии Ребекки Голдштейн о несоответствии между признанным платонизмом Гёделя и антиреалистическим использованием, которому иногда подвергаются его идеи. Сокала и Брикмонта (1999) критикуют обращение Режиса Дебре к теореме в контексте социологии; Дебрей защищал такое использование как метафорическое (там же). [23]
После того, как Гёдель опубликовал доказательство теоремы о полноте в качестве своей докторской диссертации в 1929 году, он обратился ко второй проблеме для своей хабилитации . Его первоначальной целью было получить положительное решение второй проблемы Гильберта . [24] В то время теории натуральных чисел и действительных чисел, подобные арифметике второго порядка, были известны как «анализ», в то время как теории одних только натуральных чисел были известны как «арифметика».
Гёдель был не единственным человеком, работавшим над проблемой непротиворечивости. Аккерман опубликовал ошибочное доказательство непротиворечивости для анализа в 1925 году, в котором он попытался использовать метод ε-подстановки, первоначально разработанный Гильбертом. Позже в том же году фон Нейман смог исправить доказательство для системы арифметики без каких-либо аксиом индукции. К 1928 году Аккерман передал измененное доказательство Бернайсу; это измененное доказательство заставило Гильберта объявить в 1929 году о своей вере в то, что непротиворечивость арифметики была продемонстрирована и что вскоре, вероятно, последует непротиворечивое доказательство анализа. После того, как публикация теорем о неполноте показала, что измененное доказательство Аккермана должно быть ошибочным, фон Нейман привел конкретный пример, показывающий, что его основная техника была несостоятельной. [25]
В ходе своих исследований Гёдель обнаружил, что хотя предложение, утверждающее свою ложность, приводит к парадоксу, предложение, утверждающее свою недоказуемость, не приводит. В частности, Гёдель знал о результате, который теперь называется теоремой Тарского о неопределенности , хотя он никогда не публиковал его. Гёдель объявил о своей первой теореме о неполноте Карнапу, Фейгелю и Вайсману 26 августа 1930 года; все четверо посетили Вторую конференцию по эпистемологии точных наук , ключевую конференцию в Кёнигсберге на следующей неделе.
Конференция в Кёнигсберге 1930 года была совместным заседанием трех академических обществ, в котором приняли участие многие ключевые логики того времени. Карнап, Гейтинг и фон Нейман выступили с часовыми докладами о математических философиях логицизма, интуиционизма и формализма соответственно. [26] На конференции также прозвучало обращение Гильберта к выходу на пенсию, поскольку он покидал свою должность в Геттингенском университете. Гильберт использовал эту речь, чтобы доказать свою веру в то, что все математические проблемы могут быть решены. Он закончил свое выступление словами:
Для математика нет Ignorabimus , и, по моему мнению, для естествознания тоже нет. ... Истинная причина, по которой [никому] не удалось найти неразрешимую проблему, заключается, по моему мнению, в том, что неразрешимых проблем нет. В отличие от глупого Ignorabimus , наше кредо гласит: Мы должны знать. Мы узнаем!
Эта речь быстро стала известна как резюме убеждений Гильберта в математике (ее последние шесть слов, « Wir müssen wissen. Wir werden wissen! », были использованы в качестве эпитафии Гильберту в 1943 году). Хотя Гёдель, вероятно, присутствовал на выступлении Гильберта, они никогда не встречались лицом к лицу. [27]
Гёдель объявил о своей первой теореме о неполноте на круглом столе на третий день конференции. Объявление привлекло мало внимания, за исключением фон Неймана, который отвел Гёделя в сторону для разговора. Позже в том же году, работая независимо, зная первую теорему о неполноте, фон Нейман получил доказательство второй теоремы о неполноте, о чем он объявил Гёделю в письме от 20 ноября 1930 года. [28] Гёдель независимо получил вторую теорему о неполноте и включил ее в свою представленную рукопись, которая была получена Monatshefte für Mathematik 17 ноября 1930 года.
Статья Гёделя была опубликована в Monatshefte в 1931 году под названием «Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I» (« О формально неразрешимых предложениях в Principia Mathematica и связанных с ними системах I »). Как следует из названия, Гёдель изначально планировал опубликовать вторую часть статьи в следующем томе Monatshefte ; быстрое принятие первой статьи стало одной из причин, по которой он изменил свои планы. [29]
Гёдель прочитал серию лекций о своих теоремах в Принстоне в 1933–1934 годах перед аудиторией, в которую входили Чёрч, Клини и Россер. К этому времени Гёдель понял, что ключевым свойством, требуемым его теоремами, является то, что система должна быть эффективной (в то время использовался термин «общая рекурсивность»). В 1936 году Россер доказал, что гипотеза ω-непротиворечивости, которая была неотъемлемой частью оригинального доказательства Гёделя, может быть заменена простой непротиворечивостью, если предложение Гёделя соответствующим образом изменить. Эти разработки оставили теоремы о неполноте в их современной форме.
Генцен опубликовал свое доказательство непротиворечивости для арифметики первого порядка в 1936 году. Гильберт принял это доказательство как «финитное», хотя (как уже показала теорема Гёделя) его нельзя формализовать в рамках системы арифметики, непротиворечивость которой доказывается.
Влияние теорем о неполноте на программу Гильберта было быстро осознано. Бернайс включил полное доказательство теорем о неполноте во второй том Grundlagen der Mathematik (1939), вместе с дополнительными результатами Аккермана по методу ε-подстановки и доказательством непротиворечивости арифметики Генцена. Это было первое полное опубликованное доказательство второй теоремы о неполноте.
Финслер (1926) использовал версию парадокса Ричарда , чтобы построить выражение, которое было ложным, но недоказуемым в определенной неформальной структуре, которую он разработал. [30] Гёдель не знал об этой статье, когда доказывал теоремы о неполноте (Собрание сочинений, т. IV, стр. 9). Финслер написал Гёделю в 1931 году, чтобы сообщить ему об этой статье, которая, по мнению Финслера, имела приоритет для теоремы о неполноте. Методы Финслера не полагались на формализованную доказуемость и имели лишь поверхностное сходство с работой Гёделя. [31] Гёдель прочитал статью, но нашел ее глубоко ошибочной, и в своем ответе Финслеру высказал опасения по поводу отсутствия формализации. [32] Финслер продолжал отстаивать свою философию математики, которая избегала формализации, до конца своей карьеры.
В сентябре 1931 года Эрнст Цермело написал Гёделю, чтобы объявить о том, что он назвал «существенным пробелом» в аргументации Гёделя. [33] В октябре Гёдель ответил 10-страничным письмом, в котором указал, что Цермело ошибочно предположил, что понятие истины в системе определимо в этой системе; это неверно в общем случае по теореме Тарского о неопределимости . [34] Однако Цермело не смягчился и опубликовал свою критику в печати с «довольно уничтожающим абзацем в адрес своего молодого конкурента». [35] Гёдель решил, что дальнейшее изучение этого вопроса бессмысленно, и Карнап согласился. [36] Большая часть последующей работы Цермело была связана с логикой, более сильной, чем логика первого порядка, с помощью которой он надеялся показать как последовательность, так и категоричность математических теорий.
Людвиг Витгенштейн написал несколько отрывков о теоремах о неполноте, которые были опубликованы посмертно в его « Заметках об основаниях математики» 1953 года , в частности, один раздел, иногда называемый «печально известным параграфом», где он, кажется, путает понятия «истинный» и «доказуемый» в системе Рассела. Гёдель был членом Венского кружка в период, когда ранняя философия идеального языка Витгенштейна и « Логико-философский трактат» доминировали в мышлении кружка. Были некоторые споры о том, неправильно ли Витгенштейн понял теорему о неполноте или просто выразился неясно. Работы в «Nachlass» Гёделя выражают убеждение, что Витгенштейн неправильно понял его идеи.
Множество комментаторов считали, что Витгенштейн неправильно понимает Гёделя , хотя Флойд и Патнэм (2000), а также Прист (2004) предоставили текстовые прочтения, утверждая, что большинство комментариев неправильно понимают Витгенштейна. [37] После своего освобождения Бернайс, Дамметт и Крайзель написали отдельные рецензии на замечания Витгенштейна, все из которых были крайне негативными. [38] Единодушие этой критики привело к тому, что замечания Витгенштейна о теоремах о неполноте оказали небольшое влияние на логическое сообщество. В 1972 году Гёдель заявил: «Витгенштейн сошел с ума? Он серьезно это говорит? Он намеренно произносит тривиально бессмысленные утверждения», и написал Карлу Менгеру , что комментарии Витгенштейна демонстрируют неправильное понимание теорем о неполноте, написав:
Из приведенных вами отрывков ясно, что Витгенштейн не понял [первую теорему о неполноте] (или сделал вид, что не понял). Он интерпретировал ее как своего рода логический парадокс, хотя на самом деле это как раз наоборот, а именно математическая теорема в рамках абсолютно бесспорной части математики (теории конечных чисел или комбинаторики). [39]
После публикации Nachlass Витгенштейна в 2000 году ряд статей по философии пытались оценить, была ли оправдана первоначальная критика замечаний Витгенштейна. Флойд и Патнэм (2000) утверждают, что Витгенштейн имел более полное понимание теоремы о неполноте, чем предполагалось ранее. Они особенно обеспокоены интерпретацией предложения Гёделя для ω-несовместимой системы как «Я недоказуем», поскольку система не имеет моделей, в которых предикат доказуемости соответствует фактической доказуемости. Родич (2003) утверждает, что их интерпретация Витгенштейна исторически не обоснована. Берто (2009) исследует связь между работами Витгенштейна и теориями паранепротиворечивой логики. [40]
Ни один из следующих переводов не совпадает во всех переведенных словах и в типографике. Типографика — серьезный вопрос, потому что Гёдель явно хотел подчеркнуть «те метаматематические понятия, которые были определены в их обычном смысле до ...» (van Heijenoort 1967, стр. 595). Существует три перевода. О первом Джон Доусон утверждает, что: «Перевод Мельцера был серьезно несовершенным и получил разгромную рецензию в Journal of Symbolic Logic »; «Гёдель также жаловался на комментарий Брейтуэйта (Dawson 1997, стр. 216). «К счастью, перевод Мельцера вскоре был заменен лучшим, подготовленным Эллиоттом Мендельсоном для антологии Мартина Дэвиса «Неразрешимое » ... он нашел перевод «не совсем таким хорошим», как ожидал ... [но из-за ограничений по времени он] согласился на его публикацию» (там же). (В сноске Доусон заявляет, что «он пожалеет о своем согласии, поскольку опубликованный том был испорчен неряшливой типографикой и многочисленными опечатками» (там же)). Доусон утверждает, что «перевод, который предпочел Гёдель, был сделан Жаном ван Хейеноортом» (там же). Для серьезного студента существует еще одна версия в виде набора лекционных заметок, записанных Стивеном Клини и Дж. Б. Россером «во время лекций, прочитанных Гёделем в Институте перспективных исследований весной 1934 года» (ср. комментарий Дэвиса 1965, стр. 39 и начало на стр. 41); эта версия называется «О неразрешимых предложениях формальных математических систем». В порядке их публикации:
перепечатано в Boolos (1998, стр. 383–388)
`
