Теоремы Гёделя о неполноте: различия между версиями

Материал из Википедии — свободной энциклопедии
Перейти к навигации Перейти к поиску
[отпатрулированная версия][отпатрулированная версия]
Содержимое удалено Содержимое добавлено
Отмена — так в источниках
Метка: отмена
м Исправление псевдозаголовков (см. Википедия:Доступность#Заголовки)
 
(не показаны 33 промежуточные версии 22 участников)
Строка 1: Строка 1:
{{Значения|Теорема Гёделя}}
{{Значения|Теорема Гёделя}}
'''Теорема Гёделя о неполноте''' и '''вторая теорема Гёделя'''{{#tag:ref|Иногда упоминается как вторая теорема Гёделя «о доказательствах непротиворечивости»<ref>Клини 1957 с.513</ref>, «о неполноте»<ref>[http://lpcs.math.msu.su/vml2009/ чл.-корр. РАН Лев Дмитриевич Беклемишев в «Введении в математическую логику»]</ref><ref>Толковый словарь по вычислительным системам - Page 205</ref><ref>Доклады Академии наук СССР, Volume 262 - Page 799 (1982)</ref>, «о неполноте арифметики»<ref>Известия Академии наук СССР, Volume 50 - Page 1140 (1986)</ref>.|group=~}} — две теоремы [[Математическая логика|математической логики]] о принципиальных ограничениях [[Формальная арифметика|формальной арифметики]] и, как следствие, всякой [[Формальная система|формальной системы]], в которой можно определить основные арифметические понятия: [[натуральные числа]], [[0 (число)|0]], [[1 (число)|1]], [[сложение]] и [[умножение]].
'''Теорема Гёделя о неполноте''' и '''вторая теорема Гёделя'''{{#tag:ref|Иногда упоминается как вторая теорема Гёделя «о доказательствах непротиворечивости»<ref>Клини 1957 с.513</ref>, «о неполноте»<ref>{{Cite web |url=http://lpcs.math.msu.su/vml2009/ |title=чл.-корр. РАН Лев Дмитриевич Беклемишев в «Введении в математическую логику» |access-date=2010-01-07 |archive-date=2009-03-21 |archive-url=https://web.archive.org/web/20090321120047/http://lpcs.math.msu.su/vml2009/ |deadlink=no }}</ref><ref>Толковый словарь по вычислительным системам - Page 205</ref><ref>Доклады Академии наук СССР, Volume 262 - Page 799 (1982)</ref>, «о неполноте арифметики»<ref>Известия Академии наук СССР, Volume 50 - Page 1140 (1986)</ref>.|group=~}} — две теоремы [[Математическая логика|математической логики]] о принципиальных ограничениях [[Формальная арифметика|формальной арифметики]] и, как следствие, всякой [[Формальная система|формальной системы]], в которой можно определить основные арифметические понятия: [[натуральные числа]], [[0 (число)|0]], [[1 (число)|1]], [[сложение]] и [[умножение]].


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


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


Обе эти теоремы были доказаны [[Гёдель, Курт|Куртом Гёделем]] в 1930 году (опубликованы в 1931) и имеют непосредственное отношение ко [[Вторая проблема Гильберта|второй проблеме]] из знаменитого [[Проблемы Гильберта|списка Гильберта]].
Обе эти теоремы были доказаны [[Гёдель, Курт|Куртом Гёделем]] в 1930 году (опубликованы в 1931) и имеют непосредственное отношение ко [[Вторая проблема Гильберта|второй проблеме]] из знаменитого [[Проблемы Гильберта|списка Гильберта]].

== История ==
Ещё в начале XX века [[Давид Гильберт]] провозгласил цель аксиоматизировать всю математику, и для завершения этой задачи оставалось доказать непротиворечивость и [[Формальная система|логическую полноту]] арифметики [[Натуральное число|натуральных чисел]]. 7 сентября 1930 года в [[Кёнигсберг]]е проходил научный конгресс по основаниям математики, и на этом конгрессе 24-летний [[Курт Гёдель]] впервые обнародовал две фундаментальные теоремы о неполноте, показавшие, что программа Гильберта не может быть реализована: при любом выборе аксиом арифметики существуют теоремы, которые невозможно ни доказать, ни опровергнуть простыми (''финитными'') средствами, предусмотренными Гильбертом, а финитное доказательство непротиворечивости арифметики невозможно<ref name="PIN13" />.

Это выступление не было заявлено заранее и произвело ошеломляющий эффект, Гёдель сразу стал всемирной знаменитостью, а программа Гильберта по формализации основ математики потребовала срочного пересмотра. 23 октября 1930 года результаты Гёделя были представлены [[Венская академия наук|Венской академии наук]] [[Хан, Ханс|Хансом Ханом]]. Статья с обеими теоремами («''О принципиально неразрешимых положениях в системе Principia Mathematica и родственных ей системах''») была опубликована в научном ежемесячнике ''Monatshefte für Mathematik und Physik'' в 1931 году. Хотя доказательство второй теоремы Гёдель дал только в виде идеи, его результат был настолько ясен и неоспорим, что не вызвал сомнений ни у кого. Гильберт сразу признал ценность открытий Гёделя. Первые полные доказательства обеих теорем были опубликованы в книге Гильберта и [[Бернайс, Пауль|Бернайса]] «Основания математики» в 1938 году. В предисловии ко второму тому авторы признали, что для достижения поставленной цели финитных методов недостаточно, и добавили в число логических средств [[Трансфинитная индукция|трансфинитную индукцию]]. В 1936 году [[Герхард Генцен]] сумел {{нп5|Доказательство непротиворечивости Генцена|доказать||Gentzen's consistency proof}} непротиворечивость аксиом [[Арифметика Пеано|арифметики первого порядка]], однако логическая полнота так и осталась недостижимой{{sfn |Пиньейро|2015|с=13, 48—49, 66, 89—90|name=PIN13}}.


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


=== В первоначальной форме ===
=== В первоначальной форме ===
В своей формулировке теоремы о неполноте Гёдель использовал понятие ω-непротиворечивой формальной системы — более сильное условие, чем просто непротиворечивость. Формальная система называется ''ω-непротиворечивой'', если для всякой формулы ''A''(''x'') этой системы невозможно одновременно вывести формулы ''А''('''0'''), ''А''('''1'''), ''А''('''2'''), … и ∃''x'' ¬''A''(''x'') (другими словами, из того, что для каждого натурального числа ''n'' выводима формула ''A''('''''n'''''), следует невыводимость формулы ∃''x'' ¬''A''(''x'')). Легко показать, что ω-непротиворечивость влечёт простую непротиворечивость (то есть, любая ω-непротиворечивая формальная система непротиворечива)<ref name=autogenerated1>Клини 1957 с.187</ref>.
В своей формулировке теоремы о неполноте Гёдель использовал понятие ω-непротиворечивой формальной системы — более сильное условие, чем просто непротиворечивость. Формальная система называется ''ω-непротиворечивой'', если для всякой формулы ''A''(''x'') этой системы невозможно одновременно вывести формулы ''А''('''0'''), ''А''('''1'''), ''А''('''2'''), … и ∃''x'' ¬''A''(''x'') (другими словами, из того, что для каждого натурального числа ''n'' выводима формула ''A''('''''n'''''), следует невыводимость формулы ∃''x'' ¬''A''(''x'')). Легко показать, что ω-непротиворечивость влечёт простую непротиворечивость (то есть любая ω-непротиворечивая формальная система непротиворечива)<ref name=autogenerated1>Клини 1957 с.187</ref>.


В процессе доказательства теоремы строится такая формула ''A'' арифметической формальной системы S, что<ref name=autogenerated1 />:
В процессе доказательства теоремы строится такая формула ''A'' арифметической формальной системы S, что<ref name=autogenerated1 />:
Строка 20: Строка 25:


==== Интерпретация неразрешимой формулы ====
==== Интерпретация неразрешимой формулы ====

В стандартной интерпретации<ref group=~ name="si">Интерпретация формул теории S называется стандартной, если её областью является множество неотрицательных целых чисел, символ 0 интерпретируется числом 0, функциональные буквы ', +, • интерпретируются прибавлением единицы, сложением и умножением соответственно, предикатная буква = интерпретируется отношением тождества.</ref> формула ''A'' означает «не существует вывода формулы ''A''», то есть утверждает свою собственную невыводимость в S. Следовательно, по теореме Гёделя, если только система S непротиворечива, то эта формула и в самом деле невыводима в S и потому истинна в стандартной интерпретации. Таким образом, для натуральных чисел формула ''A'' верна, но в S невыводима<ref>Это рассуждение заимствовано из Мендельсон 1971 с.160</ref>.
В стандартной интерпретации<ref group=~ name="si">Интерпретация формул теории S называется стандартной, если её областью является множество неотрицательных целых чисел, символ 0 интерпретируется числом 0, функциональные буквы ', +, • интерпретируются прибавлением единицы, сложением и умножением соответственно, предикатная буква = интерпретируется отношением тождества.</ref> формула ''A'' означает «не существует вывода формулы ''A''», то есть утверждает свою собственную невыводимость в S. Следовательно, по теореме Гёделя, если только система S непротиворечива, то эта формула и в самом деле невыводима в S и потому истинна в стандартной интерпретации. Таким образом, для натуральных чисел формула ''A'' верна, но в S невыводима<ref>Это рассуждение заимствовано из Мендельсон 1971 с.160</ref>.


=== В форме Россера ===
=== В форме Россера ===

В процессе доказательства теоремы строится такая формула ''B'' арифметической формальной системы S, что<ref>См., например, Клини 1957 с.188</ref>:
В процессе доказательства теоремы строится такая формула ''B'' арифметической формальной системы S, что<ref>См., например, Клини 1957 с.188</ref>:


Строка 32: Строка 35:


==== Интерпретация неразрешимой формулы ====
==== Интерпретация неразрешимой формулы ====

В стандартной интерпретации<ref group=~ name="si" /> формула ''B'' означает «если существует вывод формулы ''B'', то существует вывод формулы ¬''B''». Согласно же теореме Гёделя в форме Россера, если формальная система S непротиворечива, то формула ''B'' в ней невыводима; поэтому, если система S непротиворечива, то формула ''B'' верна в стандартной интерпретации<ref>Мендельсон 1971 с.162-163</ref>.
В стандартной интерпретации<ref group=~ name="si" /> формула ''B'' означает «если существует вывод формулы ''B'', то существует вывод формулы ¬''B''». Согласно же теореме Гёделя в форме Россера, если формальная система S непротиворечива, то формула ''B'' в ней невыводима; поэтому, если система S непротиворечива, то формула ''B'' верна в стандартной интерпретации<ref>Мендельсон 1971 с.162-163</ref>.


=== Обобщённые формулировки ===
=== Обобщённые формулировки ===

Доказательство теоремы Гёделя обычно проводят для конкретной формальной системы (не обязательно одной и той же), соответственно утверждение теоремы оказывается доказанным только для одной этой системы. Исследование достаточных условий, которым должна удовлетворять формальная система для того, чтобы можно было провести доказательство её неполноты, приводит к обобщениям теоремы на широкий класс формальных систем. Пример обобщённой формулировки<ref>Мендельсон 1971 с.176</ref>:
Доказательство теоремы Гёделя обычно проводят для конкретной формальной системы (не обязательно одной и той же), соответственно утверждение теоремы оказывается доказанным только для одной этой системы. Исследование достаточных условий, которым должна удовлетворять формальная система для того, чтобы можно было провести доказательство её неполноты, приводит к обобщениям теоремы на широкий класс формальных систем. Пример обобщённой формулировки<ref>Мендельсон 1971 с.176</ref>:


Строка 44: Строка 45:


=== Полиномиальная форма ===
=== Полиномиальная форма ===
После того, как [[Юрий Матиясевич]] доказал [[диофантовость]] любого эффективно перечислимого множества и были найдены примеры универсальных [[диофантово уравнение|диофантовых уравнений]], появилась возможность сформулировать теорему о неполноте в полиномиальной (или диофантовой) форме<ref>[http://www.ams.org/bull/1980-03-02/S0273-0979-1980-14832-6/S0273-0979-1980-14832-6.pdf Jones J. P., Undecidable diophantine equations]</ref><ref>[http://www.uc09.uac.pt/Presentations/Tutorials/Martin_Davis/Tutorial_I.pdf Martin Davis, Diophantine Equations & Computation]</ref><ref>[http://www.ams.org/notices/200604/fea-davis.pdf Martin Davis, The Incompleteness Theorem]</ref><ref>[http://www.ltn.lv/~podnieks/gt_rus/gram6.htm#glava65 К. Подниекс, Теорема Геделя в диофантовой форме]</ref>:
После того как [[Юрий Матиясевич]] доказал [[диофантовость]] любого эффективно перечислимого множества, и были найдены примеры универсальных [[диофантово уравнение|диофантовых уравнений]], появилась возможность сформулировать теорему о неполноте в полиномиальной (или диофантовой) форме<ref>[http://www.ams.org/bull/1980-03-02/S0273-0979-1980-14832-6/S0273-0979-1980-14832-6.pdf Jones J. P., Undecidable diophantine equations]</ref><ref>{{Cite web |url=http://www.uc09.uac.pt/Presentations/Tutorials/Martin_Davis/Tutorial_I.pdf |title=Martin Davis, Diophantine Equations & Computation |access-date=2009-11-17 |archive-date=2010-05-24 |archive-url=https://web.archive.org/web/20100524162921/http://www.uc09.uac.pt/Presentations/Tutorials/Martin_Davis/Tutorial_I.pdf |deadlink=yes }}</ref><ref>{{Cite web |url=http://www.ams.org/notices/200604/fea-davis.pdf |title=Martin Davis, The Incompleteness Theorem |access-date=2011-11-30 |archive-date=2016-03-04 |archive-url=https://web.archive.org/web/20160304052239/http://www.ams.org/notices/200604/fea-davis.pdf |deadlink=no }}</ref><ref>{{Cite web |url=http://www.ltn.lv/~podnieks/gt_rus/gram6.htm#glava65 |title=К. Подниекс, Теорема Геделя в диофантовой форме |access-date=2009-11-17 |archive-date=2017-09-10 |archive-url=https://web.archive.org/web/20170910065127/http://www.ltn.lv/~podnieks/gt_rus/gram6.htm#glava65 |deadlink=no }}</ref>:


: ''Для каждой непротиворечивой теории ''T'' можно указать такое целое значение параметра K, что уравнение
: ''Для каждой непротиворечивой теории ''T'' можно указать такое целое значение параметра K, что уравнение
Строка 65: Строка 66:


=== Набросок доказательства ===
=== Набросок доказательства ===
В своей статье Гёдель даёт набросок основных идей доказательства<ref>{{статья |автор = Gödel, Kurt |заглавие = On Formally Undecidable Propositions of the Principia Mathematica and Related Systems. I |год = 1931}} в книге {{книга |автор = Davis, Martin (ed.) |заглавие = The Undecidable: Basic Papers On Undecidable Propositions, Unsolvable Problems And Computable Functions |ссылка = https://archive.org/details/undecidablebasic0000davi |место = New York |издательство = Raven Press |год = 1965 |страницы = [https://archive.org/details/undecidablebasic0000davi/page/6 6]-8}}</ref>, который приведён ниже с незначительными изменениями.

В своей статье Гёдель даёт набросок основных идей доказательства<ref>{{статья |автор = Gödel, Kurt |заглавие = On Formally Undecidable Propositions of the Principia Mathematica and Related Systems. I |год = 1931}} в книге {{книга |автор = Davis, Martin (ed.) |заглавие = The Undecidable: Basic Papers On Undecidable Propositions, Unsolvable Problems And Computable Functions |место = New York |издательство = Raven Press |год = 1965 |страницы = 6-8}}</ref>, который приведён ниже с незначительными изменениями.


Каждому примитивному символу, выражению и последовательности выражений некоторой формальной системы<ref group=~>Гёдель использовал систему [[Principia Mathematica]] Уайтхеда и Рассела с оговоркой, что рассуждения применимы к широкому классу формальных систем</ref> S поставим в соответствие определённое натуральное число<ref group=~>Подобное сопоставление формул и натуральных чисел называется арифметизацией математики и было осуществлено Гёделем впервые. Эта идея впоследствии стала ключом к решению многих важных задач математической логики. См. [[Нумерация Гёделя|Гёделева нумерация]]</ref>. Математические понятия и утверждения таким образом становятся понятиями и утверждениями о натуральных числах, и, следовательно, сами могут быть выражены в символизме системы S. Можно показать, в частности, что понятия «формула», «вывод», «выводимая формула» определимы внутри системы S, то есть можно восстановить, например, формулу ''F''(''v'') в S с одной свободной натурально-числовой переменной ''v'' такую, что ''F''(''v''), в интуитивной интерпретации, означает: ''v'' — выводимая формула. Теперь построим неразрешимое предложение системы S, то есть предложение ''A'', для которого ни ''A'', ни ''не-A'' невыводимы, следующим образом:
Каждому примитивному символу, выражению и последовательности выражений некоторой формальной системы<ref group=~>Гёдель использовал систему [[Principia Mathematica]] Уайтхеда и Рассела с оговоркой, что рассуждения применимы к широкому классу формальных систем</ref> S поставим в соответствие определённое натуральное число<ref group=~>Подобное сопоставление формул и натуральных чисел называется арифметизацией математики и было осуществлено Гёделем впервые. Эта идея впоследствии стала ключом к решению многих важных задач математической логики. См. [[Нумерация Гёделя|Гёделева нумерация]]</ref>. Математические понятия и утверждения таким образом становятся понятиями и утверждениями о натуральных числах, и, следовательно, сами могут быть выражены в символизме системы S. Можно показать, в частности, что понятия «формула», «вывод», «выводимая формула» определимы внутри системы S, то есть можно восстановить, например, формулу ''F''(''v'') в S с одной свободной натурально-числовой переменной ''v'' такую, что ''F''(''v''), в интуитивной интерпретации, означает: ''v'' — выводимая формула. Теперь построим неразрешимое предложение системы S, то есть предложение ''A'', для которого ни ''A'', ни ''не-A'' невыводимы, следующим образом:
Строка 72: Строка 72:
Формулу в S с точно одной свободной натурально-числовой переменной назовём ''класс-выражением''. Упорядочим класс-выражения в последовательность каким-либо образом, обозначим ''n''-е через ''R''(''n''), и заметим, что понятие «класс-выражение», также как и отношение упорядочения ''R'' можно определить в системе S. Пусть α — произвольное класс-выражение; через [α;''n''] обозначим формулу, которая образуется из класс-выражения α заменой свободной переменной на символ натурального числа ''n''. Тернарное отношение ''x'' = [''y'';''z''] тоже оказывается определимым в S. Теперь определим класс ''K'' натуральных чисел следующим образом:
Формулу в S с точно одной свободной натурально-числовой переменной назовём ''класс-выражением''. Упорядочим класс-выражения в последовательность каким-либо образом, обозначим ''n''-е через ''R''(''n''), и заметим, что понятие «класс-выражение», также как и отношение упорядочения ''R'' можно определить в системе S. Пусть α — произвольное класс-выражение; через [α;''n''] обозначим формулу, которая образуется из класс-выражения α заменой свободной переменной на символ натурального числа ''n''. Тернарное отношение ''x'' = [''y'';''z''] тоже оказывается определимым в S. Теперь определим класс ''K'' натуральных чисел следующим образом:


: ''n''∈''K'' ≡ ¬Bew[''R''(''n'');''n'']    (*)
: ''n''∈''K'' ≡ ¬Bew[''R''(''n'');''n''] (*)


(где Bew ''x'' означает: ''x'' — выводимая формула<ref group=~>«Bew» сокр. от нем. «Beweisbar» — ''доказуемый'', ''выводимый''</ref>). Так как все определяющие понятия из этого определения можно выразить в S, то это же верно и для понятия ''K'', которое из них построено, то есть имеется такое класс-выражение ''C'', что формула [''C'';''n''], интуитивно интерпретируемая, обозначает, что натуральное число ''n'' принадлежит ''K''. Как класс-выражение, ''C'' идентично некоторому определённому ''R''(''q'') в нашей нумерации, то есть
(где Bew ''x'' означает: ''x'' — выводимая формула<ref group=~>«Bew» сокр. от нем. «Beweisbar» — ''доказуемый'', ''выводимый''</ref>). Так как все определяющие понятия из этого определения можно выразить в S, то это же верно и для понятия ''K'', которое из них построено, то есть имеется такое класс-выражение ''C'', что формула [''C'';''n''], интуитивно интерпретируемая, обозначает, что натуральное число ''n'' принадлежит ''K''. Как класс-выражение, ''C'' идентично некоторому определённому ''R''(''q'') в нашей нумерации, то есть
Строка 81: Строка 81:


=== Связь с парадоксами ===
=== Связь с парадоксами ===

В стандартной интерпретации<ref group=~ name="si" /> гёделева неразрешимая формула ''A'' означает «не существует вывода формулы ''A''», то есть утверждает свою собственную невыводимость в системе S. Таким образом, ''A'' является аналогом [[парадокс лжеца|парадокса лжеца]]. Рассуждения Гёделя в целом очень похожи на [[парадокс Ришара]]. Более того, для доказательства существования невыводимых утверждений может быть использован любой [[семантический парадокс]]<ref name="Гёдель 1931">Гёдель 1931</ref>.
В стандартной интерпретации<ref group=~ name="si" /> гёделева неразрешимая формула ''A'' означает «не существует вывода формулы ''A''», то есть утверждает свою собственную невыводимость в системе S. Таким образом, ''A'' является аналогом [[парадокс лжеца|парадокса лжеца]]. Рассуждения Гёделя в целом очень похожи на [[парадокс Ришара]]. Более того, для доказательства существования невыводимых утверждений может быть использован любой [[семантический парадокс]]<ref name="Гёдель 1931">Гёдель 1931</ref>.


Следует отметить, что выражаемое формулой ''A'' утверждение не содержит порочного круга, поскольку изначально утверждается только, что некоторая конкретная формула, явную запись которой получить несложно (хоть и громоздко), недоказуема. «Только впоследствии (и, так сказать, по воле случая) оказывается, что эта формула в точности та, которой выражено само это утверждение»<ref name="Гёдель 1931"/>.
Выражаемое формулой ''A'' утверждение не содержит порочного круга, поскольку изначально утверждается только, что некоторая конкретная формула, явную запись которой получить несложно (хоть и громоздко), недоказуема. «Только впоследствии (и, так сказать, по воле случая) оказывается, что эта формула в точности та, которой выражено само это утверждение»<ref name="Гёдель 1931"/>.


== Вторая теорема Гёделя ==
== Вторая теорема Гёделя ==
Строка 95: Строка 94:
=== Набросок доказательства ===
=== Набросок доказательства ===
Сначала строится формула ''Con'', содержательно выражающая невозможность вывода в теории S какой-либо формулы вместе с её отрицанием. Тогда утверждение первой теоремы Гёделя выражается формулой ''Con'' ⊃ ''G'', где ''G'' — Гёделева неразрешимая формула. Все рассуждения для доказательства первой теоремы могут быть выражены и проведены средствами S, то есть в S выводима формула ''Con'' ⊃ ''G''. Отсюда, если в S выводима ''Con'', то в ней выводима и ''G''. Однако, согласно первой теореме Гёделя, если S непротиворечива, то ''G'' в ней невыводима. Следовательно, если S непротиворечива, то в ней невыводима и формула ''Con''.
Сначала строится формула ''Con'', содержательно выражающая невозможность вывода в теории S какой-либо формулы вместе с её отрицанием. Тогда утверждение первой теоремы Гёделя выражается формулой ''Con'' ⊃ ''G'', где ''G'' — Гёделева неразрешимая формула. Все рассуждения для доказательства первой теоремы могут быть выражены и проведены средствами S, то есть в S выводима формула ''Con'' ⊃ ''G''. Отсюда, если в S выводима ''Con'', то в ней выводима и ''G''. Однако, согласно первой теореме Гёделя, если S непротиворечива, то ''G'' в ней невыводима. Следовательно, если S непротиворечива, то в ней невыводима и формула ''Con''.

== История ==
Ещё в начале XX века [[Давид Гильберт]] провозгласил цель аксиоматизировать всю математику, и для завершения этой задачи оставалось доказать непротиворечивость и [[Формальная система|логическую полноту]] арифметики [[Натуральное число|натуральных чисел]]. 7 сентября 1930 года в [[Кёнигсберг]]е проходил научный конгресс по основаниям математики, и на этом конгрессе 24-летний [[Курт Гёдель]] впервые обнародовал две фундаментальные теоремы о неполноте, показавшие, что программа Гильберта не может быть реализована: при любом выборе аксиом арифметики существуют теоремы, которые невозможно ни доказать, ни опровергнуть простыми (''финитными'') средствами, предусмотренными Гильбертом, а финитное доказательство непротиворечивости арифметики невозможно<ref name=PIN13/>.

Это выступление не было заявлено заранее и произвело ошеломляющий эффект, Гёдель сразу стал всемирной знаменитостью, а программа Гильберта по формализации основ математики потребовала срочного пересмотра. 23 октября 1930 года результаты Гёделя были представлены [[Венская академия наук|Венской академии наук]] [[Хан, Ханс|Хансом Ханом]]. Статья с обеими теоремами («''О принципиально неразрешимых положениях в системе Principia Mathematica и родственных ей системах''») была опубликована в научном ежемесячнике ''Monatshefte für Mathematik und Physik'' в 1931 году. Хотя доказательство второй теоремы Гёдель дал только в виде идеи, его результат было настолько ясен и неоспорим, что не вызвал сомнений ни у кого. Гильберт сразу признал ценность открытий Гёделя; первые полные доказательства обеих теорем были опубликованы в книге Гильберта и [[Бернайс, Пауль|Бернайса]] «Основания математики» (1938). В предисловии ко второму тому авторы признали, что для достижения поставленной цели финитных методов недостаточно, и добавили в число логических средств [[Трансфинитная индукция|трансфинитную индукцию]]; в 1936 году [[Герхард Генцен]] сумел доказать с помощью этой аксиомы непротиворечивость арифметики, однако логическая полнота так и осталась недостижимой{{sfn |Пиньейро|2015|с=13, 48—49, 66, 89—90|name=PIN13}}


== Историческое влияние ==
== Историческое влияние ==
Специалисты дают самые разные, иногда даже полярные оценки исторической значимости теорем Гёделя. Часть учёных считает, что эти теоремы «перевернули» основания математики или даже всю [[Эпистемология|теорию познания]], и значение гениального открытия Гёделя будет постепенно открываться ещё долгое время<ref>{{cite web|author=[[Stephen Hawking]]|title=Godel and the End of the Universe|url=http://www.hawking.org.uk/godel-and-the-end-of-physics.html|accessdate=2018-04-08}}</ref>. Другие же (например, [[Бертран Рассел]]) призывают не преувеличивать, поскольку теоремы опираются на финитный формализм Гильберта<ref>{{книга|автор=Михайлова Н. В.|часть=Проблема обоснования современной математики в контексте новых философско-методологических кризисов |заглавие=Философия математики: актуальные проблемы. Математика и реальность. Тезисы Третьей всероссийской научной конференции; 27-28 сентября 2013 г. |ссылка=http://www.pyrkov-professor.ru/Portals/0/Knigi/filosofiya/filosofiya_matematiki_aktualnye_problemy_matematika_i_realno.pdf |место=М.|издательство=Центр стратегической конъюнктуры |год=2013|страниц=270|страницы=187|isbn=978-5-906233-39-4}}</ref>{{sfn|Музыкантский А.}}.
Специалисты дают самые разные, иногда даже полярные оценки исторической значимости теорем Гёделя. Часть учёных считает, что эти теоремы «перевернули» основания математики или даже всю [[Эпистемология|теорию познания]], и значение гениального открытия Гёделя будет постепенно открываться ещё долгое время<ref>{{cite web|author=[[Stephen Hawking]]|title=Godel and the End of the Universe|url=http://www.hawking.org.uk/godel-and-the-end-of-physics.html|accessdate=2018-04-08|archive-date=2020-05-29|archive-url=https://web.archive.org/web/20200529232552/http://www.hawking.org.uk/godel-and-the-end-of-physics.html|deadlink=yes}}</ref>. Другие же (например, [[Бертран Рассел]]) призывают не преувеличивать, поскольку теоремы опираются на финитный формализм Гильберта<ref>{{книга|автор=Михайлова Н. В.|часть=Проблема обоснования современной математики в контексте новых философско-методологических кризисов|заглавие=Философия математики: актуальные проблемы. Математика и реальность. Тезисы Третьей всероссийской научной конференции; 27-28 сентября 2013 г.|ссылка=http://www.pyrkov-professor.ru/Portals/0/Knigi/filosofiya/filosofiya_matematiki_aktualnye_problemy_matematika_i_realno.pdf|место=М.|издательство=Центр стратегической конъюнктуры|год=2013|страниц=270|страницы=187|isbn=978-5-906233-39-4|archive-date=2017-12-16|archive-url=https://web.archive.org/web/20171216201334/http://www.pyrkov-professor.ru/Portals/0/Knigi/filosofiya/filosofiya_matematiki_aktualnye_problemy_matematika_i_realno.pdf}}</ref>{{sfn|Музыкантский А.}}.


{{начало цитаты}}
{{начало цитаты}}
Вопреки распространенному заблуждению, теоремы о неполноте Гёделя не предполагают, что некоторые истины так и останутся навеки непознанными. Кроме того, из этих теорем не следует, что человеческие способности к познанию так или иначе ограниченны. Нет, теоремы всего лишь показывают слабости и недостатки формальных систем<ref>{{книга |автор=Ливио, Марио. |место=М. |издательство=АСТ |год=2016 |страниц=384 |заглавие=Был ли Бог математиком? Глава «Истина в неполноте»|isbn=978-5-17-095136-9 |серия=Золотой фонд науки}}</ref>.
Вопреки распространённому заблуждению, теоремы о неполноте Гёделя не предполагают, что некоторые истины так и останутся навеки непознанными. Кроме того, из этих теорем не следует, что человеческие способности к познанию так или иначе ограничены. Нет, теоремы всего лишь показывают слабости и недостатки формальных систем<ref>{{книга |автор=Ливио, Марио. |место=М. |издательство=АСТ |год=2016 |страниц=384 |заглавие=Был ли Бог математиком? Глава «Истина в неполноте»|isbn=978-5-17-095136-9 |серия=Золотой фонд науки}}</ref>.
{{конец цитаты}}
{{конец цитаты}}


Рассмотрим, например, следующее доказательство непротиворечивости арифметики{{sfn |Пиньейро|2015|с=155—162|name=PIN}}.
Рассмотрим, например, следующее доказательство непротиворечивости арифметики{{sfn|Пиньейро|2015|с=155—162|name=PIN}}.
{{начало цитаты}}
{{начало цитаты}}
Допустим, что [[аксиоматика Пеано]] для арифметики противоречива. Тогда из неё можно вывести любое утверждение, в том числе ложное. Однако все аксиомы Пеано очевидным образом истинны, а из истинных утверждений не могут следовать ложный вывод — получаем противоречие. Следовательно, арифметика непротиворечива.
Допустим, что [[аксиоматика Пеано]] для арифметики противоречива. Тогда из неё можно вывести любое утверждение, в том числе ложное. Однако все аксиомы Пеано очевидным образом истинны, а из истинных утверждений не может следовать ложный вывод — получаем противоречие. Следовательно, арифметика непротиворечива.
{{конец цитаты}}
{{конец цитаты}}
С точки зрения повседневной человеческой логики, это доказательство приемлемо и убедительно. Но оно не может быть записано по правилам теории доказательств Гильберта, поскольку в этих правилах семантика заменена на синтаксис, а истинность — на «выводимость»<ref name=PIN/>. В любом случае теоремы Гёделя подняли философию математики на новый уровень.
С точки зрения повседневной человеческой логики, это доказательство приемлемо и убедительно. Но оно не может быть записано по правилам теории доказательств Гильберта, поскольку в этих правилах семантика заменена на синтаксис, а истинность — на «выводимость»<ref name=PIN/>. В любом случае теоремы Гёделя подняли философию математики на новый уровень.


== См. также ==
== См. также ==
{{кол}}
* [[Антиномия]]
* [[Антиномия]]
* [[Натуральное число]]
* [[Натуральное число]]
Строка 125: Строка 120:
* [[Теорема Хайтина о неполноте]]
* [[Теорема Хайтина о неполноте]]
* [[Формальная теория]]
* [[Формальная теория]]
{{кол|конец}}


== Примечания ==
== Примечания ==
; Комментарии
'''Комментарии'''
{{примечания|group=~}}
{{примечания|group=~}}


; Источники
'''Источники'''
{{примечания|2}}
{{примечания|2}}


Строка 137: Строка 133:
|заглавие=Жар холодных чисел и пафос бесстрастной логики. Формализация мышления от античных времен до эпохи кибернетики |место= М. |издательство=Едиториал УРСС |год= 2004 |страниц= 232 |isbn = 5-354-00310-5
|заглавие=Жар холодных чисел и пафос бесстрастной логики. Формализация мышления от античных времен до эпохи кибернетики |место= М. |издательство=Едиториал УРСС |год= 2004 |страниц= 232 |isbn = 5-354-00310-5
|ref= Бирюков }}
|ref= Бирюков }}
* [[Ершов, Юрий Леонидович|Ершов Ю. Л.]] ''[https://web.archive.org/web/20090719063356/http://rutube.ru/tracks/1543805.html Доказательность в математике]'', программа [[Гордон, Александр Гарриевич|А. Гордона]] от 16 июня 2003 года.
* [[Ершов, Юрий Леонидович|Ершов Ю. Л.]] ''[https://web.archive.org/web/20090719063356/http://rutube.ru/tracks/1543805.html Доказательность в математике]'', программа [[Гордон, Александр Гарриевич|А. Гордона]] от 16 июня 2003 года.
* {{книга
* {{книга
| автор = [[Ершов, Юрий Леонидович|Ершов Ю. Л.]], [[Палютин, Евгений Андреевич|Палютин Е.А.]]
| автор = [[Ершов, Юрий Леонидович|Ершов Ю. Л.]], [[Палютин, Евгений Андреевич|Палютин Е.А.]]
Строка 177: Строка 173:
|автор = Davis, Martin (ed.)
|автор = Davis, Martin (ed.)
|заглавие = The Undecidable: Basic Papers On Undecidable Propositions, Unsolvable Problems And Computable Functions
|заглавие = The Undecidable: Basic Papers On Undecidable Propositions, Unsolvable Problems And Computable Functions
|ссылка = https://archive.org/details/undecidablebasic0000davi
|место = New York
|место = New York
|издательство = Raven Press
|издательство = Raven Press
Строка 184: Строка 181:
|автор = Heijenoort, Jean van (ed.)
|автор = Heijenoort, Jean van (ed.)
|заглавие = From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931
|заглавие = From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931
|ссылка = https://archive.org/details/fromfregetogodel0000vanh
|место = Cambridge, Massachusetts
|место = Cambridge, Massachusetts
|издательство = Harvard University Press
|издательство = Harvard University Press
Строка 195: Строка 193:
== Библиография — статьи Гёделя ==
== Библиография — статьи Гёделя ==
* 1931, ''Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I.'' ''Monatshefte für Mathematik und Physik 38'': 173—198.
* 1931, ''Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I.'' ''Monatshefte für Mathematik und Physik 38'': 173—198.
* 1931, ''Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I.'' and ''On formally undecidable propositions of Principia Mathematica and related systems I'' in [[Феферман, Соломон|Solomon Feferman]], ed., 1986. ''Kurt Gödel Collected works, Vol. I''. Oxford University Press: 144—195.
* 1931, ''Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I.'' and ''On formally undecidable propositions of Principia Mathematica and related systems I'' in [[Феферман, Соломон|Solomon Feferman]], ed., 1986. ''Kurt Gödel Collected works, Vol. I''. Oxford University Press: 144—195. — Оригинальный немецкий текст с параллельным английским переводом, с элементарным введением, написанным [[Клини, Стивен Коул|Стивеном Клини]].
* Hirzel, Martin, 2000, ''[http://www.research.ibm.com/people/h/hirzel/papers/canon00-goedel.pdf On formally undecidable propositions of Principia Mathematica and related systems I.]''. — Современный перевод Марина Херцеля.
Оригинальный немецкий текст с параллельным английским переводом, с элементарным введением, написанным [[Клини, Стивен Коул|Стивеном Клини]].
** Hirzel, Martin, 2000, ''[http://www.research.ibm.com/people/h/hirzel/papers/canon00-goedel.pdf On formally undecidable propositions of Principia Mathematica and related systems I.]''. Современный перевод Марина Херцеля.
* 1951, ''Some basic theorems on the foundations of mathematics and their implications'' in [[Феферман, Соломон|Solomon Feferman]], ed., 1995. ''Kurt Gödel Collected works, Vol. III''. Oxford University Press: 304—323.
* 1951, ''Some basic theorems on the foundations of mathematics and their implications'' in [[Феферман, Соломон|Solomon Feferman]], ed., 1995. ''Kurt Gödel Collected works, Vol. III''. Oxford University Press: 304—323.


Строка 204: Строка 201:
[[Категория:Теория алгоритмов]]
[[Категория:Теория алгоритмов]]
[[Категория:Метаматематика]]
[[Категория:Метаматематика]]
[[Категория:Теоремы метаматематики|Гёделя о неполноте]]
[[Категория:Основания математики]]
[[Категория:Основания математики]]
[[Категория:Именные законы и правила|Гёделя о неполноте]]
[[Категория:Именные законы и правила|Гёделя о неполноте]]
[[Категория:Теория доказательств]]
[[Категория:Метатеоремы|Гёделя]]

Текущая версия от 21:01, 10 октября 2024

Теорема Гёделя о неполноте и вторая теорема Гёделя[~ 1] — две теоремы математической логики о принципиальных ограничениях формальной арифметики и, как следствие, всякой формальной системы, в которой можно определить основные арифметические понятия: натуральные числа, 0, 1, сложение и умножение.

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

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

Обе эти теоремы были доказаны Куртом Гёделем в 1930 году (опубликованы в 1931) и имеют непосредственное отношение ко второй проблеме из знаменитого списка Гильберта.

Ещё в начале XX века Давид Гильберт провозгласил цель аксиоматизировать всю математику, и для завершения этой задачи оставалось доказать непротиворечивость и логическую полноту арифметики натуральных чисел. 7 сентября 1930 года в Кёнигсберге проходил научный конгресс по основаниям математики, и на этом конгрессе 24-летний Курт Гёдель впервые обнародовал две фундаментальные теоремы о неполноте, показавшие, что программа Гильберта не может быть реализована: при любом выборе аксиом арифметики существуют теоремы, которые невозможно ни доказать, ни опровергнуть простыми (финитными) средствами, предусмотренными Гильбертом, а финитное доказательство непротиворечивости арифметики невозможно[6].

Это выступление не было заявлено заранее и произвело ошеломляющий эффект, Гёдель сразу стал всемирной знаменитостью, а программа Гильберта по формализации основ математики потребовала срочного пересмотра. 23 октября 1930 года результаты Гёделя были представлены Венской академии наук Хансом Ханом. Статья с обеими теоремами («О принципиально неразрешимых положениях в системе Principia Mathematica и родственных ей системах») была опубликована в научном ежемесячнике Monatshefte für Mathematik und Physik в 1931 году. Хотя доказательство второй теоремы Гёдель дал только в виде идеи, его результат был настолько ясен и неоспорим, что не вызвал сомнений ни у кого. Гильберт сразу признал ценность открытий Гёделя. Первые полные доказательства обеих теорем были опубликованы в книге Гильберта и Бернайса «Основания математики» в 1938 году. В предисловии ко второму тому авторы признали, что для достижения поставленной цели финитных методов недостаточно, и добавили в число логических средств трансфинитную индукцию. В 1936 году Герхард Генцен сумел доказать[англ.] непротиворечивость аксиом арифметики первого порядка, однако логическая полнота так и осталась недостижимой[6].

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

[править | править код]

В первоначальной форме

[править | править код]

В своей формулировке теоремы о неполноте Гёдель использовал понятие ω-непротиворечивой формальной системы — более сильное условие, чем просто непротиворечивость. Формальная система называется ω-непротиворечивой, если для всякой формулы A(x) этой системы невозможно одновременно вывести формулы А(0), А(1), А(2), … и ∃x ¬A(x) (другими словами, из того, что для каждого натурального числа n выводима формула A(n), следует невыводимость формулы ∃x ¬A(x)). Легко показать, что ω-непротиворечивость влечёт простую непротиворечивость (то есть любая ω-непротиворечивая формальная система непротиворечива)[7].

В процессе доказательства теоремы строится такая формула A арифметической формальной системы S, что[7]:

Если формальная система S непротиворечива, то формула A невыводима в S; если система S ω-непротиворечива, то формула ¬A невыводима в S. Таким образом, если система S ω-непротиворечива, то она неполна[~ 2] и A служит примером неразрешимой формулы.

Формулу A иногда называют гёделевой неразрешимой формулой[8].

Интерпретация неразрешимой формулы

[править | править код]

В стандартной интерпретации[~ 3] формула A означает «не существует вывода формулы A», то есть утверждает свою собственную невыводимость в S. Следовательно, по теореме Гёделя, если только система S непротиворечива, то эта формула и в самом деле невыводима в S и потому истинна в стандартной интерпретации. Таким образом, для натуральных чисел формула A верна, но в S невыводима[9].

В форме Россера

[править | править код]

В процессе доказательства теоремы строится такая формула B арифметической формальной системы S, что[10]:

Если формальная система S непротиворечива, то в ней невыводимы обе формулы B и ¬B; иначе говоря, если система S непротиворечива, то она неполна[~ 2], и B служит примером неразрешимой формулы.

Формулу B иногда называют россеровой неразрешимой формулой[11]. Эта формула немного сложнее гёделевой.

Интерпретация неразрешимой формулы

[править | править код]

В стандартной интерпретации[~ 3] формула B означает «если существует вывод формулы B, то существует вывод формулы ¬B». Согласно же теореме Гёделя в форме Россера, если формальная система S непротиворечива, то формула B в ней невыводима; поэтому, если система S непротиворечива, то формула B верна в стандартной интерпретации[12].

Обобщённые формулировки

[править | править код]

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

Всякая достаточно сильная рекурсивно аксиоматизируемая непротиворечивая теория первого порядка неполна.

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

Полиномиальная форма

[править | править код]

После того как Юрий Матиясевич доказал диофантовость любого эффективно перечислимого множества, и были найдены примеры универсальных диофантовых уравнений, появилась возможность сформулировать теорему о неполноте в полиномиальной (или диофантовой) форме[14][15][16][17]:

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

Степень данного уравнения может быть понижена до 4 ценой увеличения количества переменных.

Набросок доказательства

[править | править код]

В своей статье Гёдель даёт набросок основных идей доказательства[18], который приведён ниже с незначительными изменениями.

Каждому примитивному символу, выражению и последовательности выражений некоторой формальной системы[~ 4] S поставим в соответствие определённое натуральное число[~ 5]. Математические понятия и утверждения таким образом становятся понятиями и утверждениями о натуральных числах, и, следовательно, сами могут быть выражены в символизме системы S. Можно показать, в частности, что понятия «формула», «вывод», «выводимая формула» определимы внутри системы S, то есть можно восстановить, например, формулу F(v) в S с одной свободной натурально-числовой переменной v такую, что F(v), в интуитивной интерпретации, означает: v — выводимая формула. Теперь построим неразрешимое предложение системы S, то есть предложение A, для которого ни A, ни не-A невыводимы, следующим образом:

Формулу в S с точно одной свободной натурально-числовой переменной назовём класс-выражением. Упорядочим класс-выражения в последовательность каким-либо образом, обозначим n-е через R(n), и заметим, что понятие «класс-выражение», также как и отношение упорядочения R можно определить в системе S. Пусть α — произвольное класс-выражение; через [α;n] обозначим формулу, которая образуется из класс-выражения α заменой свободной переменной на символ натурального числа n. Тернарное отношение x = [y;z] тоже оказывается определимым в S. Теперь определим класс K натуральных чисел следующим образом:

nK ≡ ¬Bew[R(n);n] (*)

(где Bew x означает: x — выводимая формула[~ 6]). Так как все определяющие понятия из этого определения можно выразить в S, то это же верно и для понятия K, которое из них построено, то есть имеется такое класс-выражение C, что формула [C;n], интуитивно интерпретируемая, обозначает, что натуральное число n принадлежит K. Как класс-выражение, C идентично некоторому определённому R(q) в нашей нумерации, то есть

C = R(q)

выполняется для некоторого определённого натурального числа q. Теперь покажем, что предложение [R(q);q] неразрешимо в S. Так, если предложение [R(q);q] предполагается выводимым, тогда оно оказывается истинным, то есть, в соответствии со сказанным выше, q будет принадлежать K, то есть, в соответствии с (*), будет выполнено ¬Bew[R(q);q], что противоречит нашему предположению. С другой стороны, если предположить выводимым отрицание [R(q);q], то будет иметь место ¬qK, то есть Bew[R(q);q] будет истинным. Следовательно, [R(q);q] вместе со своим отрицанием будет выводимо, что снова невозможно.

Связь с парадоксами

[править | править код]

В стандартной интерпретации[~ 3] гёделева неразрешимая формула A означает «не существует вывода формулы A», то есть утверждает свою собственную невыводимость в системе S. Таким образом, A является аналогом парадокса лжеца. Рассуждения Гёделя в целом очень похожи на парадокс Ришара. Более того, для доказательства существования невыводимых утверждений может быть использован любой семантический парадокс[19].

Выражаемое формулой A утверждение не содержит порочного круга, поскольку изначально утверждается только, что некоторая конкретная формула, явную запись которой получить несложно (хоть и громоздко), недоказуема. «Только впоследствии (и, так сказать, по воле случая) оказывается, что эта формула в точности та, которой выражено само это утверждение»[19].

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

[править | править код]

В формальной арифметике S можно построить такую формулу, которая в стандартной интерпретации[~ 3] является истинной в том и только в том случае, когда теория S непротиворечива. Для этой формулы справедливо утверждение второй теоремы Гёделя:

Если формальная арифметика S непротиворечива, то в ней невыводима формула, содержательно утверждающая непротиворечивость S.

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

Набросок доказательства

[править | править код]

Сначала строится формула Con, содержательно выражающая невозможность вывода в теории S какой-либо формулы вместе с её отрицанием. Тогда утверждение первой теоремы Гёделя выражается формулой ConG, где G — Гёделева неразрешимая формула. Все рассуждения для доказательства первой теоремы могут быть выражены и проведены средствами S, то есть в S выводима формула ConG. Отсюда, если в S выводима Con, то в ней выводима и G. Однако, согласно первой теореме Гёделя, если S непротиворечива, то G в ней невыводима. Следовательно, если S непротиворечива, то в ней невыводима и формула Con.

Историческое влияние

[править | править код]

Специалисты дают самые разные, иногда даже полярные оценки исторической значимости теорем Гёделя. Часть учёных считает, что эти теоремы «перевернули» основания математики или даже всю теорию познания, и значение гениального открытия Гёделя будет постепенно открываться ещё долгое время[20]. Другие же (например, Бертран Рассел) призывают не преувеличивать, поскольку теоремы опираются на финитный формализм Гильберта[21][22].

Вопреки распространённому заблуждению, теоремы о неполноте Гёделя не предполагают, что некоторые истины так и останутся навеки непознанными. Кроме того, из этих теорем не следует, что человеческие способности к познанию так или иначе ограничены. Нет, теоремы всего лишь показывают слабости и недостатки формальных систем[23].

Рассмотрим, например, следующее доказательство непротиворечивости арифметики[24].

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

С точки зрения повседневной человеческой логики, это доказательство приемлемо и убедительно. Но оно не может быть записано по правилам теории доказательств Гильберта, поскольку в этих правилах семантика заменена на синтаксис, а истинность — на «выводимость»[24]. В любом случае теоремы Гёделя подняли философию математики на новый уровень.

Примечания

[править | править код]

Комментарии

  1. Иногда упоминается как вторая теорема Гёделя «о доказательствах непротиворечивости»[1], «о неполноте»[2][3][4], «о неполноте арифметики»[5].
  2. 1 2 Формальная система, содержащая неразрешимую, то есть невыводимую и неопровержимую, формулу, называется неполной.
  3. 1 2 3 4 Интерпретация формул теории S называется стандартной, если её областью является множество неотрицательных целых чисел, символ 0 интерпретируется числом 0, функциональные буквы ', +, • интерпретируются прибавлением единицы, сложением и умножением соответственно, предикатная буква = интерпретируется отношением тождества.
  4. Гёдель использовал систему Principia Mathematica Уайтхеда и Рассела с оговоркой, что рассуждения применимы к широкому классу формальных систем
  5. Подобное сопоставление формул и натуральных чисел называется арифметизацией математики и было осуществлено Гёделем впервые. Эта идея впоследствии стала ключом к решению многих важных задач математической логики. См. Гёделева нумерация
  6. «Bew» сокр. от нем. «Beweisbar» — доказуемый, выводимый

Источники

  1. Клини 1957 с.513
  2. чл.-корр. РАН Лев Дмитриевич Беклемишев в «Введении в математическую логику». Дата обращения: 7 января 2010. Архивировано 21 марта 2009 года.
  3. Толковый словарь по вычислительным системам - Page 205
  4. Доклады Академии наук СССР, Volume 262 - Page 799 (1982)
  5. Известия Академии наук СССР, Volume 50 - Page 1140 (1986)
  6. 1 2 Пиньейро, 2015, с. 13, 48—49, 66, 89—90.
  7. 1 2 Клини 1957 с.187
  8. Мендельсон 1971 с.165
  9. Это рассуждение заимствовано из Мендельсон 1971 с.160
  10. См., например, Клини 1957 с.188
  11. Мендельсон 1971 с.162
  12. Мендельсон 1971 с.162-163
  13. Мендельсон 1971 с.176
  14. Jones J. P., Undecidable diophantine equations
  15. Martin Davis, Diophantine Equations & Computation. Дата обращения: 17 ноября 2009. Архивировано из оригинала 24 мая 2010 года.
  16. Martin Davis, The Incompleteness Theorem. Дата обращения: 30 ноября 2011. Архивировано 4 марта 2016 года.
  17. К. Подниекс, Теорема Геделя в диофантовой форме. Дата обращения: 17 ноября 2009. Архивировано 10 сентября 2017 года.
  18. Gödel, Kurt. On Formally Undecidable Propositions of the Principia Mathematica and Related Systems. I. — 1931. в книге Davis, Martin (ed.). The Undecidable: Basic Papers On Undecidable Propositions, Unsolvable Problems And Computable Functions. — New York: Raven Press, 1965. — С. 6-8.
  19. 1 2 Гёдель 1931
  20. Stephen Hawking. Godel and the End of the Universe. Дата обращения: 8 апреля 2018. Архивировано из оригинала 29 мая 2020 года.
  21. Михайлова Н. В. Проблема обоснования современной математики в контексте новых философско-методологических кризисов // Философия математики: актуальные проблемы. Математика и реальность. Тезисы Третьей всероссийской научной конференции; 27-28 сентября 2013 г.. — М.: Центр стратегической конъюнктуры, 2013. — С. 187. — 270 с. — ISBN 978-5-906233-39-4. Архивировано 16 декабря 2017 года.
  22. Музыкантский А..
  23. Ливио, Марио. Был ли Бог математиком? Глава «Истина в неполноте». — М.: АСТ, 2016. — 384 с. — (Золотой фонд науки). — ISBN 978-5-17-095136-9.
  24. 1 2 Пиньейро, 2015, с. 155—162.

Литература

[править | править код]

Библиография — статьи Гёделя

[править | править код]
  • 1931, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. Monatshefte für Mathematik und Physik 38: 173—198.
  • 1931, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. and On formally undecidable propositions of Principia Mathematica and related systems I in Solomon Feferman, ed., 1986. Kurt Gödel Collected works, Vol. I. Oxford University Press: 144—195. — Оригинальный немецкий текст с параллельным английским переводом, с элементарным введением, написанным Стивеном Клини.
  • Hirzel, Martin, 2000, On formally undecidable propositions of Principia Mathematica and related systems I.. — Современный перевод Марина Херцеля.
  • 1951, Some basic theorems on the foundations of mathematics and their implications in Solomon Feferman, ed., 1995. Kurt Gödel Collected works, Vol. III. Oxford University Press: 304—323.