Теоремы Гёделя не дезавуируют программу Гильберта | Вестн. Том. гос. ун-та. Философия. Социология. Политология. 2017. № 40. DOI: 10.17223/1998863Х/40/29

Теоремы Гёделя не дезавуируют программу Гильберта

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

Godel's incompleteness theorems do not disrupt Hilbert’s program.pdf Введение Программа финитного обоснования математики, провозглашенная Д. Гильбертом в начале 1920-х гг., преследовала цель снять всякие сомнения в достоверности математического знания, зародившиеся благодаря парадоксам, открытым к тому времени в теории множеств. Принятые в математике утверждения и методы доказательства Гильберт разделяет на «реальные» (финитные) и «идеальные» (более сложные). При этом под финитными доказательствами он понимает те, в которых не используется апелляция к актуальной (завершенной) бесконечности. Финитная часть математики полагается Гильбертом свободной от каких-либо сомнений. Однако для обеспечения применимости классической логики, в частности, закона исключенного третьего, «идеальные» доказательства также следует допустить. Необходимо только доказать, что такое допущение не приведет к выводу финитных утверждений, которые не могут быть доказаны финитными средствами, например, не приведет к выводу противоречия, если к нему не приводят финитные доказательства. При этом, что принципиально важно, искомое доказательство непротиворечивости само должно быть осуществлено финитными методами. Хрестоматийной, азбучной истиной современной философии математики является убеждение в том, что знаменитые теоремы К. Гёделя о неполноте формальных систем бесспорно и однозначно засвидетельствовали невозможность реализации гильбертовской программы в ее изначальной постановке: «Работы Гёделя повсеместно используются для демонстрации невыполнимости гильбертовской программы» [1. С. 1]. Ранее мы установили некорректность аргументации невыполнимости программы Гильберта, основанной на второй теореме Гёделя о неполноте [2, 3]. В настоящей работе мы усилим этот результат и покажем, что первая теорема о неполноте также не может служить легитимной основой аргументации против реализуемости гильбертовской программы финитного обоснования математики. § 1. Предварительные сведения В этой статье мы рассматриваем вопрос о реализуемости программы Гильберта и о том, какую роль играют в этом вопросе теоремы Гёделя, применительно к наиболее популярной формализации математической теории - формальной арифметике Дедекинда - Пеано РА (определение см., напр., в [4]). Напомним, что теория называется непротиворечивой, если в ней имеется хотя бы одна недоказуемая формула, или, что эквивалентно, в ней ни для какой формулы A не могут одновременно быть доказаны формулы A и - A. Теория называется а -непротиворечивой, если в ней ни для какой формулы Ф(х) с одной свободной переменной не могут одновременно быть доказаны формулы Ф(1),Ф(2),..., -УхФ(x). Имеются различные изложения теорем Гёделя о неполноте, отличающиеся обозначениями, формулировками и способами доказательства. В несколько упрощенной формулировке теоремы о неполноте таковы: Первая теорема Гёделя о неполноте арифметики [5. Theorem VI]. Если PA а-непротиворечива, то она неполна, т. е. в РА имеется некоторая замкнутая формула G такая, что ни она, ни ее отрицание не доказуемы в PA. Вторая теорема Гёделя о неполноте арифметики [5. Theorem XI]. Если PA непротиворечива, то в ней не доказуема формула, выражающая непротиворечивость PA. Для доказательства своих теорем Гёдель использует три основных приема: 1. Арифметизация синтаксиса. Она осуществляется путем числового кодирования языка формальной арифметики и её логики (Гёделева нумерация). При кодировании языковым выражениям PA ставятся в соответствие числа (гёделевы номера) так, чтобы разным выражениям сопоставлялись различные числа и по выбранному числу можно было бы эффективно восстановить выражение, номером которого данное число является. 2. Введение понятия выразимости (определимости). Определение. Предикат F(xb ..., xk), заданный на множестве натуральных чисел, называется выразимым (представимым, формализуемым - использующиеся в литературе синонимы) по Гёделю, или G-выразимым в РА, если в PA найдётся формула Ф(хь ..., xk), такая что для любого набора натуральных чисел (и 1, ., nk) справедливы условия: (1) если F(nb ., nk) выполняется, то Ь Ф(пь ., nk); (2) если F(n 1, ., nk) не выполняется, то Ь -Ф(п ь ., nk). Здесь, как и во всей статье, знак Ь означает доказуемость (в PA). Нумерал, соответствующий числу п, принято обозначать через п. Выражение г A далее будет обозначать нумерал, соответствующий гёделеву номеру формулы А. 3. Введение предиката доказуемости. Гёдель вводит предикат доказуемости (здесь и далее с точностью до обозначений) Pr(x, у), который выполняется тогда и только тогда, когда x является гёделевым номером некоторой формулы, а у - гёделевым номером ее доказательства. Предикат Pr(x, у) G-выразим в PA с помощью некоторой арифметической формулы Prov(x, у), т.е. для любых натуральных чисел n, к верны условия: (1) если Pr(n, к) выполняется, то Ь Prov(n, k); (2) если Pr(n, к) не выполняется, то Ь -.Prov(n, k). С помощью формулы Prov(x, у) непротиворечивость формальной арифметики G-выражается арифметической формулой ЗxVy-Prov( x, у). (Consis) Consis G-выражает факт существования в PA формулы, не являющейся заключительной ни в каком выводе, т. е. существование в РА недоказуемой формулы. С использованием формулы Consis современная формулировка второй теоремы о неполноте применительно к PA выглядит следующим образом: если PA непротиворечива, то формула Consis, в которой Prov(x, у) G-выражает предикат доказуемости, удовлетворяющий условиям Гильберта -Бернайса - Лёба (см., напр.: [6. С. 15]), не может быть доказана в PA. § 2. Вторая теорема в аргументации против осуществимости программы Гильберта Убеждение в том, что вторая теорема Гёделя о неполноте дает решающий аргумент в доказательстве несостоятельности выдвинутой Гильбертом программы финитного обоснования математики, имеет широчайшее признание среди логиков и философов. Приведем самые недавние свидетельства. «Основанием для всех философских заключений служит простой факт: для любой адекватной формальной дедуктивной системы Т, если Т непротиворечива, тогда эта непротиворечивость выразима в Т, но не доказуема в ней» [7. С. 390]. «Многие считают, что программа Гильберта была остановлена на своем пути второй теоремой Гёделя о неполноте» [8. P. 299]. Дж. фон Нейман был первым, кто связал вторую теорему Гёделя о неполноте с вопросом о реализуемости программы Гильберта (см. [9. P. 418]). Он полагал, что всякое финитное рассуждение, которое могло бы использоваться в доказательстве непротиворечивости РА, должно быть формализуемым в рамках РА. Поэтому если бы непротиворечивость РА была установлена финитными методами, такое доказательство было бы формализуемо в РА доказуемой формулой, что невозможно, согласно второй теореме о неполноте. Нужно понимать, что всегда, когда Гёдель и его последователи говорят о формализации в языке арифметики метаязыковых понятий таких, как (не)доказуемость, ими подразумевается использование исключительно G-выразимого предиката доказуемости. И никакие другие способы формализации, например, с использованием каких-либо иных G-выразимых предикатов, ни фон Нейманом, ни Гёделем, ни их последователями, ни современными авторами вообще не рассматриваются. Именно такого рода «формализацию» имеет в виду фон Нейман, когда аргументирует неосуществимость программы Гильберта, апеллируя ко второй теореме. Далее мы будем рассуждать, оставаясь именно в этих, до сих пор общепринятых рамках. В «Стэнфордской энциклопедии философии» (см.: [1. § 4]) аргумент фон Неймана реконструируется следующим образом (с точностью до обозначений): «Непротиворечивость системы РА должна финитно выражать то, что никакая выбранная последовательность символов не является выводом в РА формулы 0 = 1. Формализацией этого требования является формула -iProv(r0 = 1п, у) с одной свободной переменной у. Если бы существовало финитное доказательство непротиворечивости РА, то формализация этого доказательства привела бы к доказательству в РА формулы -Prov(r0 = 1п, у), из которой просто по закону универсального обобщения по у в РА выводилась бы формула Consis. Однако вывод в РА формулы Con-sis запрещен второй теоремой о неполноте». Мы покажем, что такого рода стандартная аргументация некорректна, поскольку она может приводить к абсурдным следствиям. Ранее мы доказали простое следствие второй теоремы о неполноте: Утверждение 1 (см. [10. С. 186-187]). Если PA непротиворечива, то для любой формулы A формула, G-выражающая недоказуемость A, недоказуема в PA. Если PA со -непротиворечива, то для любой недоказуемой в PA формулы A формула, G-выражающая недоказуемость A, неразрешима в PA. Основываясь на этом утверждении, докажем Утверждение 2. Вторая теорема Гёделя о неполноте не может использоваться в доказательстве нереализуемости гильбертовской финитистской программы. ДОКАЗАТЕЛЬСТВО. Если исходить из последовательной финитистской позиции, то доказательство непротиворечивости РА, полученное Г. Генценом с помощью трансфинитной индукции [11], не является вполне надежным. Поэтому твердо мы не знаем, непротиворечива РА или противоречива. Но из определения непротиворечивости мы точно знаем, что РА может быть либо противоречивой, либо непротиворечивой. Третьего не дано. Рассмотрим обе возможности. Пусть РА противоречива. Тогда вторая теорема о неполноте вообще не может применяться, поскольку в ее формулировке в явном виде содержится условие непротиворечивости РА. Предположим, что РА непротиворечива. При этом не важно, имеется ли у нас какое-либо доказательство ее непротиворечивости или нет. Рассмотрим формулу -(0 = 0) и повторим слово в слово стандартную аргументацию по отношению к этой формуле. Предположим, что найдется неформальное финитное доказательство невыводимости этой формулы в PA. Тогда формула -iProv(r-1(0 = 0)п, y), G-выражающая факт невыводимости формулы -(0 = 0), должна быть доказуемой в РА. Однако, согласно утверждению 1, эта формула не может быть доказана в PA. Отсюда ровно на тех же основаниях, по которым обычно делается вывод о невозможности финитного доказательства непротиворечивости PA, мы вправе сделать вывод о несуществовании неформального финитного доказательства невыводимости в PA формулы -(0 = 0) в предположении о непротиворечивости РА. Однако если РА непротиворечива, такое неформальное доказательство существует! Вот оно: предположим, что формула -(0 = 0) доказуема. Тогда, учитывая, что в РА доказуема также формула (0 = 0), в РА оказалась бы доказуемой формула (0 = 0)& -(0 = 0), т. е. PA была бы противоречивой, что противоречит нашему предположению. Поэтому в предположении о непротиворечивости РА формула -(0 = 0) в ней недоказуема. Очевидно, что данное тривиальное доказательство финитно. В нём никак не используются ни аксиома индукции, ни, тем более, трансфинитная индукция. Таким образом, мы пришли к противоречию: если РА непротиворечива, то из второй теоремы о неполноте по стандартной аргументации следует несуществование неформального финитного доказательства недоказуемости в РА формулы -(0 = 0) . Но такое доказательство существует! Это означает, что основанная на второй теореме аргументация против осуществимости программы Гильберта некорректна. Поэтому вторая теорема Гёделя о неполноте не может использоваться в доказательстве нереализуемости гильбертов-ской программы. Следует заметить, что доказательство утверждения 2 в целом также финитно. § 3. Доказательство первой теоремы о неполноте не может быть финитным Как мы уже отметили, именно вторая теорема о неполноте традиционно рассматривается как решающий контраргумент в вопросе о реализуемости программы Гильберта. В то же время в ряде современных работ доказывается, что уже из первой теоремы следует вывод о невыполнимости гильбертовской программы (см., напр., [6. С. 14]). Но для того чтобы быть убедительным опровержением финитистской программы, первая теорема, очевидно, сама должна быть доказана финитными методами. Как настаивает С. Клини: «... очень важно иметь строго финитное математическое доказательство теоремы Гёделя» [12. С. 185]. Сам Клини, по-видимому, считает оригинальное гёделево доказательство финитным: «Если это метаматематическое доказательство рассмотреть во всех деталях, то оно окажется по своей природе обыкновенным математическим доказательством. ... (Это) доказательство, хотя чрезвычайно длительное и утомительное в этих терминах, не подвержено никаким возражениям, которые в равной мере не относились бы к частям традиционной математики, почитаемым за наиболее достоверные» ([12. С. 185-186]). Тем не менее в литературе существуют и другие мнения по этому вопросу (см., напр., [13]). Мы не будем углубляться в анализ различных точек зрения по вопросу о финитности доказательства первой теоремы, тем более, что в литературе имеется достаточно много различных ее доказательств, и разбирать их все у нас нет никакой возможности. Мы просто докажем общее Утверждение 3. Не существует финитного доказательства первой теоремы о неполноте РА. ДОКАЗАТЕЛЬСТВО. Рассмотрим неразрешимую гёделеву формулу G и по отношению к ней опять проведем стандартную аргументацию. Предположим, что первая теорема может быть доказана «строго финитно», т.е. найдется неформальное финитное доказательство невыводимости формулы G в PA. Тогда формула -Prov(rGn, у), G-выражающая факт невыводимости формулы G, должна быть доказуемой в РА. Однако, согласно утверждению 1, эта формула не может быть доказана в PA. Эти же рассуждения относятся и к формуле -G: формула - Prov(r-Gn, у) не может быть доказана в РА по утверждению 1, поэтому не существует неформального финитного доказательства невыводимости формулы -G в PA. Таким образом, для формул G и -G не существуют неформальные финитные доказательства их невыводимости в PA. Но это и означает несуществование финитного доказательства первой теоремы о неполноте арифметики. На основании доказанного утверждения мы вправе заключить, что использование первой теоремы о неполноте в аргументации против реализуемости гильбертовской программы в ее оригинальной постановке нелигитим-но. Поскольку эта теорема в принципе не может быть доказана финитным образом, с позиции последовательного финитизма все ее имеющиеся доказательства сомнительны. Этот вывод позволяет усилить заключение § 2. Поскольку вторая теорема о неполноте обычно доказывается как следствие первой, вывод о сомнительности с точки зрения последовательного финитизма в полной мере относится и к доказательству второй теоремы. В настоящей работе мы, конечно, не доказали, что провозглашенная Гильбертом программа финитного обоснования математики может быть полностью реализована. Мы показали лишь, что теоремы Гёделя о неполноте формальной арифметики, тотально оцениваемые как бесспорные свидетельства невозможности реализации гильбертовской программы, в действительности таковыми не являются.

Ключевые слова

программа Гильберта, тезис фон Неймана, вторая теорема Гёделя о неполноте, первая теорема Гёделя о неполноте, финитное доказательство, Hilbert’s program, von Neumann’s thesis, Godel's second incompleteness theorem, Godel's first incompleteness theorem, finitary proof

Авторы

ФИООрганизацияДополнительноE-mail
Бессонов Александр ВладимировичНовосибирский государственный университет; Институт философии и права Сибирского отделения Российской академии наукдоктор философских наук, старший научный сотрудник, профессор кафедры философии Института философии и права; ведущий научный сотрудник отдела философииtrt@academ.org
Всего: 1

Ссылки

Клини С. Введение в метаматематику / пер. с англ. А.С. Есенин-Вольпин. М.: Изд-во иностранной литературы, 1957.
Detlefsen M. Formalism // S. Shapiro (ed.) The Oxford Handbook of Philosophy of Mathematics and Logic. New York: Oxford University Press. 2005. P. 236-317.
Бессонов А.В. К интерпретации теорем Гёделя о неполноте арифметики // Вестник Томского ун-та. Философия. Социология. Политология. 2011. № 4. C. 177-189.
Gentzen G. Die Widerspruchsfreiheit der reinen Zahlentheorie // Mathematische Annalen. 1936. Bd. 112. S. 493-565.
In Memoriam: Georg Kreisel // The Bulletin of Symbolic Logic. 2016. Vol. 22, No. 2. P. 298299.
Zach R. Hilbert’s Program Then and Now // D. Jacquette (ed.). Handbook of Philosophy of Science. Vol. 5: Philosophy of Logic. Amsterdam: Elsevier, 2006. P. 411-447.
Ершов Ю.Л., Целищев В.В. Алгоритмы и вычислимость в человеческом познании. Новосибирск: Изд-во СО РАН, 2012.
Godel K. Uber formal unentscheidbare Satze der Principia Mathematica und verwandter Systeme I // Monatshefte fur Mathematik und Physik. 1931. Bd. 38. S. 173-198.
Сморинский К. Теоремы о неполноте // Справочная книга по математической логике. Т. IV: Теория доказательств и конструктивная математика. М.: Наука, 1983. С. 9-53.
Bessonov A.V. Godel's second incompleteness theorem cannot be used as an argument against Hilbert's program // Logic Colloquium 2017, Programme and abstracts (Stockholm, August 14-20, 2017). Stockholm, 2017. P. 86-87.
Бессонов А.В. О двух неверных догмах, связанных со второй теоремой Гёделя о неполноте. I // Философия науки. 2014. № 4(63). C. 12-31.
Zach R. Hilbert’s program // E.N. Zalta (ed.). The Stanford Encyclopedia of Philosophy // URL: http://plato.stanford.edu/archives/sum2015/entries/hilbert-program/. Accessed: 2017/01/09.
Бессонов А.В. О двух неверных догмах, связанных со второй теоремой Гёделя о неполноте. II // Философия науки. 2016. № 2(69). C. 42-61.
 Теоремы Гёделя не дезавуируют программу Гильберта | Вестн. Том. гос. ун-та. Философия. Социология. Политология. 2017. № 40. DOI:  10.17223/1998863Х/40/29

Теоремы Гёделя не дезавуируют программу Гильберта | Вестн. Том. гос. ун-та. Философия. Социология. Политология. 2017. № 40. DOI: 10.17223/1998863Х/40/29