философы

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

в избранное

Программа Гильберта

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

Впервые опубликовано 31 июля 2003 года; содержательно переработано 6 января 2015 года.

В начале 1920-х годов немецкий математик Давид Гильберт (1862–1943) выдвинул новый проект обоснования классической математики, который впоследствии стал известен как программа Гильберта. Программа призывала формализовать всю математику в аксиоматическом виде, а затем доказать, что полученная аксиоматизация непротиворечива. Доказательство при этом должно опираться лишь на «финитные», как их назвал Гильберт, методы. Особые эпистемологические свойства финитных рассуждений позволят прийти к искомому обоснованию классической математики. Хотя Гильберт выдвинул программу в данном виде только в 1921 году, различные ее аспекты прослеживаются в его трудах по основаниям математики вплоть до 1900 года. Именно тогда им впервые было указано, что необходимо предоставить прямое доказательство непротиворечивости математического анализа. Работа над программой значительно продвинулась в 1920-е годы благодаря вкладу таких логиков, как Пауль Бернайс, Вильгельм Аккерман, Джон фон Нейман и Жак Эрбран. Кроме того, она оказала огромное влияние на Курта Гёделя, чья работа над теоремами о неполноте была вдохновлена программой Гильберта. К сочинениям Гёделя обычно обращаются, чтобы показать неосуществимость программы Гильберта. Тем не менее, последняя остается влиятельной позицией в философии математики, и начиная с трудов Герхарда Генцена 1930-х годов работа над т.н. ограниченными (relativized) программами Гильберта играла важную роль в развитии такой области знания, как теория доказательств.

Историческое развитие программы Гильберта

Ранняя работа над основаниями математики

Работа Гильберта над основаниями математики берет начало в трудах 1890-х годов, посвященных геометрии. Эти исследования были подытожены в его авторитетном учебнике под названием «Основания геометрии» (Hilbert 1899). Гильберт верил: для того чтобы должным образом разработать любую научную тему, строжайше требуется использовать аксиоматический подход. Как только аксиоматическое изложение будет обеспечено, теория будет разработана независимо от интуиции, а анализ логических отношений между основными понятиями и аксиомами будет облегчен. Первостепенно важным для аксиоматического изложения, согласно Гильберту, является исследование независимости и, самое главное, непротиворечивости аксиом. Непротиворечивость аксиом геометрии может быть доказана посредством интерпретации всей системы в вещественной плоскости — следовательно, непротиворечивость геометрии сводится к непротиворечивости математического анализа. Основание анализа, разумеется, само требует аксиоматизации и доказательства непротиворечивости. Гильберт предоставил такую аксиоматизацию в докладе «О понятии количества» (1900b), однако довольно скоро стало ясно, что доказательство непротиворечивости анализа столкнулось со значительными трудностями. В частности, излюбленный способ обоснования анализа в работах Дедекинда опирался на сомнительные допущения, схожие с теми, что вели к парадоксам в теории множеств и к парадоксу Рассела в основаниях арифметики Фреге.

Тогда Гильберт осознал, что необходимо прямое доказательство непротиворечивости анализа (т.е. не основывающееся на сведении его к другой теории). Он выдвинул проблему нахождения такого доказательства под номером 2 {{1}} из 23 математических проблем, сформулированных им в выступлении на Международном математическом конгрессе (1900а), и представил его набросок в гейдельбергской речи (1905). Ряд обстоятельств приостановил дальнейшее развитие программы Гильберта по поиску оснований. Одним из них, вероятно, послужила критика со стороны Пуанкаре (Poincaré 1906): тот счел, что применение индукции в набросанном Гильбертом доказательстве непротиворечивости опирается на порочный круг (см. Steiner 1975: Appendix). Гильберт также осознал, что аксиоматические исследования требуют безукоризненно проработанного логического формализма. На тот момент он руководствовался представлением о логике, берущим начало в алгебраической традиции. В частности, Гильберт полагался на работу Шрёдера, которая не вполне подходила на роль формализма для аксиоматизации математики. (По поводу раннего этапа развития программы Гильберта см. Peckhaus 1990.)

Влияние Principia Mathematica

Публикация труда Рассела и Уайтхеда Principia Mathematica{{2}}предоставила логический инструментарий, требуемый для обновленного подступа к проблемам, связанным с поиском оснований математики. Начиная с 1914 года ученик Гильберта Генрих Беман и другие математики изучают систему Principia (по поводу роли Бемана в школе Гильберта см. Mancosu 1999). Сам Гильберт вернулся к проблемам поиска оснований в 1917 году и в сентябре отправил Шведскому математическому обществу доклад, озаглавленный «Аксиоматическое мышление» (Hilbert 1918а). Это был первый вклад в проект по поиску оснований математики, опубликованный им после 1905 года. В нем Гильберт вновь подчеркивает необходимость доказательств непротиворечивости для аксиоматических систем: «Принципиальное требование аксиоматики должно быть направлено в будущее [вместо того чтобы обходить стороной выявленные парадоксы], а именно на установление того обстоятельства, что противоречия вообще не могут быть возможны в области знания, базирующейся на установленной системе аксиом» (Гильберт 1988: 101). Гильберт также вновь называет доказательство непротиворечивости арифметики (и теории множеств) одной из главных неисследованных проблем. В случае обеих теорий кажется, будто бы у нас нет ничего более фундаментального, к чему можно свести непротиворечивость, нежели сама логика. И поэтому Гильберт предположил, что проблема была по сути решена Расселом в Principia. Как бы то ни было, другие принципиальные проблемы аксиоматики оставались нерешенными — включая проблему «разрешимости любого математического вопроса», зарождение которой тоже прослеживается в выступлении Гильберта 1900 года.

Эти нерешенные проблемы аксиоматики подтолкнули Гильберта приложить значительные усилия к разработкам в области логики в последующие годы. В 1917 году Пауль Бернайс присоединился к нему в Гёттингене в качестве ассистента. В серии курсов, проводившихся в 1917–1921 годы, при содействии Бернайса и Бемана Гильберт совершил значительный и оригинальный вклад в формальную логику. Курс 1917 года (1918b), в частности, содержит тщательную разработку логики первого порядка, а впоследствии на него будет опираться учебник Гильберта и Аккермана «Основы теоретической логики» (1928; рус. пер.: Гильберт, Аккерман 2010). (См. Ewald and Sieg 2013, Sieg 1999, а также Zach 1999, 2003.)

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

В течение следующих нескольких лет, тем не менее, Гильберт пришел к отрицанию логицистского решения проблемы непротиворечивости арифметики Расселом. В то же время получала распространение интуиционистская математика Брауэра. В частности, бывший ученик Гильберта Герман Вейль обратился в интуиционизм. Так, на статью Вейля «О новом кризисе оснований математики» (Weyl 1921) Гильберт ответил в трех докладах, прочитанных в Гамбурге летом 1921 года (Hilbert 1922b). В них Гильберт представил собственный подход к проблеме оснований математики. Данный проект объединял идеи Гильберта 1904 года, касающиеся прямых доказательств непротиворечивости, его концепцию аксиоматических систем, а также технические разработки аксиоматизации математики в трудах Рассела — равно как и дальнейшие разработки, проделанные им и его коллегами. Новизна же заключалась в том, как именно Гильберт придавал своему проекту доказательства непротиворечивости философское значение, необходимое для отвода критики Брауэра и Вейля: с финитной точки зрения.

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

…внелогических дискретных объектов, которые сами существуют интуитивно — подобно непосредственному опыту, предшествующему всякой мысли. Для того, чтобы логические выводы были надежны, эти объекты должны быть полностью во всех своих частях обозримыми; их показ, их различие, их следование друг за другом и существование одного из них наряду (concatenated) с другими даются непосредственно, наглядно (intuitively), вместе с объектами как нечто, не могущее быть сведенным ни к чему другому и не нуждающееся в таком сведении. (Hilbert 1922b: 202; отрывок воспроизводится практически дословно в Hilbert 1926: 376; 1928; 464; а также в 1931b: 267; цит. по Виганд 1998: 222–223.)

Для Гильберта такими объектами являлись знаки. Область теории содержательных чисел состоит из финитных нумералов, т.е. последовательностей штрихов. Они не обладают значением, т.е. не замещают абстрактные объекты, но ими можно оперировать (например, конкатенировать — объединять в ряд) и их можно сравнивать. Знание их свойств и отношений интуитивно и не опосредовано логическим выводом. Согласно Гильберту, развитая таким образом теория содержательных чисел надежна: противоречия не могут возникнуть в ней просто потому, что в предложениях теории содержательных чисел нет логической структуры.

Интуитивно-содержательные операции со знаками составляют основу метаматематики Гильберта. Как теория содержательных чисел оперирует последовательностями штрихов, так и метаматематика оперирует последовательностями символов (формул, доказательств). Формулами и доказательствами можно оперировать синтаксически, а свойства и взаимоотношения формул и доказательств аналогичным образом опираются на внелогическую интуитивную способность, которая гарантирует достоверность знания о формулах и доказательствах, полученных в результате подобных синтаксических операций. Математика сама по себе, тем не менее, оперирует абстрактными понятиями (такими как кванторы, множества, функции) и использует логический вывод, основывающийся на принципах (таких как математическая индукция или принцип исключенного третьего). Эти «понятийные образования» и способы рассуждения были раскритикованы Брауэром и другими математиками за то, что они заранее предполагают бесконечные совокупности уже данными и включают непредикативные определения (с точки зрения критиков, последние включали в себя порочный круг). Гильберт стремился оправдать их использование. Соответственно, он отмечает, что их можно формально представить в виде аксиоматических систем (подобных системам из Principia или же тем, которые Гильберт развил сам). В таком случае математические предложения и доказательства превращаются в формулы и выводы из аксиом согласно строго установленным правилам вывода. Математика, по мнению Гильберта, «становится перечнем доказуемых формул». Доказательства в математике подвергаются метаматематическому содержательному (contentual) рассмотрению. Цель программы Гильберта — найти содержательное метаматематическое доказательство невыводимости противоречия, т.е. невозможности формального вывода формулы А и ее отрицания ¬A.

Этот набросок целей программы воплощался Гильбертом и его коллегами в течение следующих десяти лет. Понятийная составляющая финитной точки зрения и стратегии доказательства непротиворечивости была тщательно разработана в Hilbert 1928, 1923, 1926, а также в Bernays 1928b, 1922, 1930. Наиболее подробно финитная точка зрения разрабатывается в статье Гильберта «О бесконечности» (Hilbert 1926). Помимо Гильберта и Бернайса в техническую работу над программой было вовлечено немало других людей. В лекциях, прочитанных в Гёттингене (Hilbert and Bernays 1923; Hilbert 1922a), Гильберт и Бернайс построили ε-исчисление в качестве исчерпывающего формализма для аксиоматических систем в арифметике и анализе. В лекциях Гильберт также изложил подход к доказательству непротиворечивости с использованием т.н. метода ε-подстановки. Аккерман попробовал расширить идеи Гильберта до системы математического анализа (Ackermann 1924). Доказательство, однако, оказалось ошибочным (см. Zach 2003). Джон фон Нейман, посещавший в то время Гёттинген, исправил доказательство непротиворечивости для системы ε-формализма (не включавшей, тем не менее, аксиому индукции) в 1925 году (см. von Neumann 1927). Опираясь на работу фон Неймана, Аккерман сформулировал новую процедуру ε-подстановки, о которой сообщил Бернайсу (см. Bernays 1928b). В докладе «Проблемы обоснования математики» на Международном конгрессе математиков в Болонье в 1928 году Гильберт оптимистично провозглашал, что работы Аккермана и фон Неймана установили непротиворечивость теории чисел и что доказательство для анализа было выполнено Аккерманом «до той степени, что единственная остающаяся нерешенной задача состоит в доказательстве того, что теорема элементарной финитности относится сугубо к арифметике» (Hilbert 1929).

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

Теоремы о неполноте Гёделя показали, что оптимизм Гильберта был несвоевременным. В сентябре 1930 года Курт Гедёль выступил с докладом о своей первой теореме о неполноте на конференции в Кёнигсберге. Фон Нейман, присутствовавший в аудитории, сразу же оценил значение результата Гёделя для программы Гильберта. Вскоре после конференции он написал Гёделю, сообщая, что обнаружил непосредственное следствие из его результата. Гёдель, однако, сам пришел к тому же выводу ранее. Речь идет о второй теореме о неполноте, в соответствии с которой система Principia неспособна доказать формализацию утверждения о том, что система Principia непротиворечива (при условии, что она такова). Однако до сей поры считалось, что все методы финитного рассуждения, применявшиеся в доказательствах непротиворечивости, формализуемы в Principia. Следовательно, если непротиворечивость Principia доказуема при помощи использованных в доказательстве Аккермана методов, должна иметься возможность формализовать это доказательство при помощи Principia. Однако именно отсутствие подобной возможности утверждает вторая теорема о неполноте. Бернайс также осознал важность результатов Гёделя сразу, как только прочел его работу в январе 1931 года, и написал ему, что теорема о неполноте демонстрирует (если принять в качестве допущения, что формализация финитного рассуждения в рамках Principia возможна): финитное доказательство непротиворечивости Principia невозможно. Вскоре после этого фон Нейман указал на изьяны в доказательстве непротиворечивости Аккермана и предоставил контрпример для предложенной процедуры ε-подстановки (см. Zach 2003).

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

Финитная точка зрения

Финитная точка зрения является как краеугольным камнем философии математики Гильберта, так и существенно новым аспектом его мышления об основаниях (начиная с работы Hilbert 1922b и далее). Эта методологическая точка зрения состоит в ограничении математического мышления объектами, которые «существуют наглядно, в качестве непосредственных переживаний до какого бы то ни было мышления», а также операциями над ними и методами рассуждения о них, которые не требуют введения абстрактных понятий (в частности, обращения к завершенным бесконечным совокупностям).

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

• 1. Чем являются объекты финитного мышления?

• 2.Что представляют собой осмысленные финитистские предложения?

• 3.Какие методы построения и рассуждения приемлемы в рамках финитизма?

Финитные объекты и эпистемология финитизма

Гильберт определяет область применения финитного рассуждения в хорошо известном абзаце, который примерно в одной и той же формулировке появляется во всех остальных, более философских работах Гильберта начиная с 1920-х годов (Hilbert 1931b, 1922b, 1928, 1926):

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

1, 11, 111, 11111

На вопрос о том, как именно Гильберт понимал нумералы, сложно ответить. Они не являются физическими объектами (реальными штрихами на бумаге, к примеру), однако должна иметься возможность расширить нумерал добавлением еще одного штриха (и, как утверждается также в 1926, заявления о том, что физическая вселенная бесконечна, сомнительны). Согласно Гильберту, их «форма может быть в большинстве случаев достоверно распознана нами — независимо от пространства и времени, от особых условий производства знака, от незначительных различий в конечном продукте» (1922b: 202). Нумералы не являются и чисто мыслительными конструкциями, поскольку их свойства объективны, хотя их существование и зависит от интуитивного построения (см. Bernays 1923: 226). Как бы то ни было, они логически примитивны, т.е. не являются ни понятиями (как числа у Фреге), ни множествами. В первую очередь важно не их метафизическое положение (абстрактное либо конкретное — в сегодняшнем смысле этих терминов), но то обстоятельство, что они не вступают в логические отношения, т.е. не могут ни для чего выступать предикатами. В наиболее зрелом представлении финитизма у Бернайса (Hilbert and Bernays 1939; Bernays 1930) объекты финитизма определяются как формальные объекты, которые рекурсивно порождаются процессом повторения; штриховые символы в рамках этого описания выступают конкретными репрезентациями формальных объектов.

Трудно сказать и то, каков эпистемологический статус у объектов финитизма. В целях обеспечения надежного обооснования инфинитистской математики доступ к финитным объектам должен быть непосредственным и несомненным. В философском отношении Гильберт во многом был кантианцем — как и Бернайс, который находился в тесных отношениях с неокантианской школой философии, сложившейся вокруг Леонарда Нельсона в Гёттингене. В определении финитизма Гильберт часто ссылается на кантовское понятие интуиции (созерцания), а объекты финитизма в качестве объектов даны интуитивно. В самом деле, в эпистемологии Канта непосредственность является характерной особенностью интуитивного познания. Вопрос лишь в том, о какого рода интуиции здесь идет речь. В этой связи Манкозу указывает на сдвиг в понимании интуиции у Гильберта (Mancosu 1998b). Он настаивает, что если в ранних работах Гильберта интуиция относилась к восприятию, то в более поздних работах (напр., Bernays 1928a) она отождествляется с формой чистого созерцания в кантовском смысле. Тем не менее, примерно в то же время Гильберт продолжает определять этот вид интуиции как относящийся к восприятию (Hilbert 1928: 469). Гильберт рассматривает финитный способ мышления в качестве независимого источника априорного знания наряду с чистым созерцанием (например, пространства) и рассудком. Тем самым он заявляет, что «исследовал и описал третий источник знания, сопутствующий опыту и логике» (1931b: 266–267). И Бернайс, и Гильберт обосновывали финитное знание в кантианских терминах (хотя и не доходили до проведения трансцендентальной дедукции), описывая финитное рассуждение как особый вид рассуждения, на котором основывается всякое математическое и в целом научное мышление: без него последнее было бы невозможно. (См. разбор эпистемологии финитизма в Kitcher 1976 и Parsons 1998. Исторический и философский контекст теории знаков Гильберта приводится в Patton 2014.)

Финитистски осмысленные предложения и финитное рассуждение

Самые базовые суждения о финитных нумералах — это суждения о равенстве и неравенстве. Кроме них финитная точка зрения допускает операции над финитными объектами. Из них наиболее базовая — объединение в ряды, т.н. конкатенация. Конкатенация нумералов 11 и 111 передается как «2 + 3», а утверждение «11 конкатенировано с 111» приводит к тому же нумералу, что и у «111 конкатенировано с 11», который передается как «2 + 3 = 3 + 2». В реальной теоретико-доказательной практике (равно как и в работах Hilbert and Bernays 1934, Bernays 1930) эти базовые операции обобщаются до операций, определяемых через рекурсию — как правило, примитивную: задействующую умножение или возведение в степень (см. разбор философских затруднений, которые возникают из-за степенных выражений, в Parsons 1998). Схожим образом финитные суждения могут включать в себя не только равенство или неравенство, но и базовые разрешимые свойства, такие как «быть простым числом». Это финитистски допустимо до тех пор, пока характеристическая функция такого свойства сама является финитной. Например, операция, преобразующая нумерал в 1, если тот представляет собой простое число, и в 11 в противном случае, может быть задана посредством примитивной рекурсии, а следовательно, является финитной. Подобные финитные предложения могут быть совмещены при помощи обычных логических операций, таких как конъюнкция, дизъюнкция и негация, а также ограниченной квантификации. Гильберт приводит в качестве примера предложение «существует простое число между p + 1 и р! + 1», где р — некоторое большое простое число. Утверждение финитистски приемлемо, поскольку «служит лишь для сокращения предложения» (Hilbert 1926), которое гласит, что р + 1, либо р + 2, либо р + 3, либо … либо р! + 1 является простым числом.

Сомнительными считаются финитные предложения, которые выражают общие факты насчет нумералов — такие как «для любого данного нумерала n, 1 + n = n + 1». Оно сомнительно, поскольку к нему «с финитной точки зрения невозможно построить отрицание» (Hilbert 1926: 378). Тем самым Гильберт настаивает, что противоположное по смыслу предложение — «существует нумерал n, для которого 1 + n ≠ n + 1» — не является финитистски осмысленным: «В конце концов, невозможно проверить все числа». По той же причине общие финитные предложения следует рассматривать не как бесконечные конъюнкции, но «лишь как гипотетические суждения, утверждающие нечто только тогда, когда дан нумерал» (Hilbert 1928: 470). Пускай они сомнительны в таком смысле, общие финитные предложения важны для теории доказательств Гильберта, поскольку подобную общую форму имеет утверждение непротиворечивости формальной системы S: для любой данной последовательности формул Р верно, что Р не является выводом к противоречию в S.

Финитные операторы и финитное доказательство

Крайне важным для понимания как финитизма, так и теории доказательств Гильберта является вопрос о том, какие операции и какие правила доказательства следует считать допустимыми с финитистской точки зрения. О необходимости ответа ясно говорят требования теории доказательств Гильберта: не следует ожидать, будто в данной формальной математической системе (или даже одной последовательности формул) можно с легкостью «увидеть» ее непротиворечивость (или невозможность подлинного вывода из нее противоречия) — подобно тому, как мы видим, к примеру, что 11 + 111 = 111 + 11. Для доказательства непротиворечивости требуется операция, которая превращает всякий данный формальный вывод в вывод особого вида, и доказательство того, что, во-первых, операция делает именно это и, во-вторых, выводы особого вида не являются доказательствами противоречивости. Чтобы вместе они могли считаться финитным доказательством непротиворечивости, операция сама должна быть приемлемой с финитной точки зрения, а требуемые ей доказательства должны применять лишь финитистски приемлемые правила.

Гильберт никогда не приводил общий перечень финитистски приемлемых операций и методов доказательства — лишь только примеры тех операций и методов вывода из теории содержательных финитных чисел, которые считал приемлемыми в качестве финитных. Содержательная индукция была принята им в применении к финитным суждениям гипотетического и общего вида (Hilbert 1922b). Гильберт также полагал, что интуитивное мышление «включает рекурсию и интуитивную индукцию для совокупностей, существующих финитным образом» (1923: 1139), и использовал возведение в степень в своих примерах (1928). Бернайс объяснил, как рассмотреть возведение в степень в качестве финитной операции над нумералами (Bernays 1930). Гильберт и Бернайс дают единственное общее изложение теории содержательных финитных чисел. В соответствии с ним финитистски приемлемыми являются операции, задаваемые посредством примитивной рекурсии, а также доказательства, применяющие индукцию. Все эти методы могут быть формализованы в рамках системы, известной как примитивно рекурсивная арифметика (PRA), допускающая определение функций через примитивную рекурсию и индукцию по бескванторным формулам (Hilbert and Bernays 1934). Тем не менее, Гильберт и Бернайс ни разу не утверждали, что финитными считаются исключительно примитивно рекурсивные операции: фактически они использовали некоторые непримитивно рекурсивные методы в преподносимых как финитные доказательствах непротиворечивости уже в 1923 году (см. Tait 2002 и Zach 2003).

Куда более интересным концептуальным вопросом является следующий: какие операции должны считаться финитными. Поскольку сам Гильберт не выразился достаточно однозначно по поводу того, в чем именно состоит финитная точка зрения, остается некоторое пространство для маневров в установлении ограничений — эпистемологических и пр., — которым должен удовлетворять анализ финитных операций и доказательств. Гильберт описывает объекты теории финитных чисел как «интуитивно данные» и «обозримые во всех своих частях», а также говорит, что имеющиеся у них базовые свойства должны для нас «существовать интуитивно». Бернайс предположил, что в финитной математике лишь «простое интуитивное познание играет роль» (Bernays 1922: 216), и в контексте финитизма прибегал к выражению «точка зрения интуитивной очевидности» (1930: 250). Данная характеристика финитизма — как в основе своей имеющего дело с интуицией и интуитивным знанием — подчеркивалась среди прочих Парсонсом. Он настаивал: финитными в приведенном понимании считаются лишь арифметические операции, которые могут быть определены через сложение и умножение с использованием ограниченной рекурсии. В частности, согласно ему возведение в степень и общая примитивная рекурсия не являются финитистски приемлемыми (Parsons 1998).

Тезис, в соответствии с которым финитизм совместим с примитивно рекурсивными рассуждениями, получил существенную поддержку со стороны Тэта (Tait 1981; см. также 2002, 2005b). В отличие от Парсонса, Тэт не считает интуитивную представимость основной характеристикой финитности. Вместо этого он объявляет финитное рассуждение «минимальным видом рассуждения, заранее предполагаемым любыми нетривиальными математическими рассуждениями о числах». Согласно его анализу, само понятие числа как вида конечной последовательности подразумевает финитные операции и методы доказательства. В пользу такого анализа говорит заявление Гильберта о том, что финитное рассуждение обуславливает всякое логико-математическое и в целом научное мышление (Hilbert 1931b: 267). Коль скоро финитное рассуждение является той частью математики, которая заранее предполагается любыми нетривиальными рассуждениями о числах, оно оказывается, согласно Тэту, «несомненным» в смысле Декарта. И для того чтобы предоставить математике эпистемологическое основание, как того хотел Гильберт, финитному рассуждению требуется лишь подобная несомненность.

Другой интересный анализ финитного доказательства (тем не менее, в философском отношении не столь глубокий) был предложен Крайзелем (Kreisel 1960). Он пришел к следующему выводу: финитными являются те и только те функции, для которых может быть доказана всеобщность в первопорядковой арифметике PA. Результат основывается на теоретико-доказательном понятии принципа рефлексии. (См. подробности в Zach 2006, а также разбор в Dean (forthcoming).) Крайзель предоставляет еще один анализ, сосредотачиваясь на том, что «поддается наглядному представлению» (Kreisel 1970: sec. 3.5). Вывод из него следует тот же самый: выясняется, что финитная доказуемость коэкстенсивна доказуемости в PA.

Технический анализ Тэта приходит к заключению, что финитными являются именно примитивно рекурсивные функции, а финитными теоретико-числовыми истинами — суждения, доказуемые в теории примитивно рекурсивной арифметики PRA. Важно подчеркнуть, что этот анализ не производится исходя из самой финитной точки зрения. Поскольку общие понятия «функции» и «доказательства» как таковые не являются финитными, для приверженца финитизма тезис Тэта, в соответствии с которым все доказуемое в PRA финитистски истинно, не будет иметь смысла. Согласно Тэту, правильный анализ финитной доказуемости не должен допускать, будто бы в самом финитизме имеется доступ к таким нефинитным понятиям. Подход Крайзеля и некоторые критические замечания в адрес Тэта, опирающиеся на принцип рефлексии или ω-правила, не удовлетворяют этому требованию (см. Tait 2002, 2005b). С другой стороны, можно возразить: PRA — теория слишком сильная и потому не может считаться формализацией того, что «предполагается любыми нетривиальными математическими рассуждениями о числах». Есть более слабые и вместе с тем нетривиальные теории, которые относятся к меньшим по объему классам функций, нежели примитивно рекурсивные — например, PV и EA, относящиеся к полиноминальным по времени и элементарным по Кальмару функциям соответственно (см. Avigad 2003 касательно того, как много математики может быть воплощено в EA). Используя анализ аналогично Тэту, Ганеа приходит к связанному классу элементарных по Кальмару функций, являющихся финитными (Ganea 2010).

Формализм, редукционизм и инструментализм

Вейль примирительно отреагировал на проект Гильберта (представленный в Hilbert 1922b, 1923), однако при этом высказал важную критику. В его описании проект Гильберта предстал как замещение содержательной математики бессмысленной игрой в формулы. Вейль заметил, что Гильберт хотел «обезопасить не истину, но непротиворечивость анализа» (Weyl 1925), и озвучил ряд замечаний, созвучных с высказанными ранее Фреге. Почему непротиворечивость формальной системы математики должна выступать основанием для веры в истинность протоформальной математики, которую она упорядочивает? Разве бессмысленный перечень формул Гильберта — не «бескровный призрак анализа»? Вейль предложил следующее решение:

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

Гильберт ввел в употребление различие между реальными и идеальными формулами в работе Hilbert 1926, которое не присутствовало в 1922b и лишь проскальзывало в 1923. В последнем тексте Гильберт излагает первую формальную систему бескванторной теории чисел, о которой говорит: «Все доказуемые формулы, полученные нами таким путем, имеют свойство конечных» (1139). Затем трансфинитные аксиомы (т.е. кванторы) добавляются для упрощения и завершения теории (1144). Здесь он впервые проводит аналогию с методом идеальных элементов: «В моей теории доказательств трансфинитные доказательства и формулы присоединены к конечным аксиомам — как в теории комплексного переменного мнимые элементы присоединены к реальным, так и в геометрии идеальные построения присоединяются к действительным» (1144). Вводя в употребление понятие идеальных предложений (Hilbert 1926) и впервые говоря о реальных предложениях в дополнение к идеальным (1928), Гильберт однозначно заявляет: реальная часть теории состоит лишь из разрешимых бескванторных формул. Предполагается, что они «доступны для прямого подтверждения» — сродни предложениям, выведенным из законов природы и допускающим опытную проверку (1928: 475). Новый образ программы Гильберта был следующим: классическую математику следует формализовать в виде системы, включающей в себя формализацию всех подтверждаемых напрямую (через вычисление) предложений теории содержательных финитных чисел. Доказательство непротиворечивости должно показывать, что все доказуемые идеальными методами реальные предложения истинны, т.е. могут быть напрямую удостоверены конечным вычислением. (Актуальные доказательства, такие как ε-подстановка, всегда являлись таковыми: они обеспечивали финитные процедуры, которые исключали трансфинитные элементы из доказательств реальных утверждений — в частности, 0 = 1.) Кроме того, Гильберт ясно понимал, что верно нечто даже более сильное: доказательство непротиворечивости не только устанавливает истинность реальных формул, доказуемых идеальными методами, но и приводит к финитным доказательствам общих финитных предложений — если связанная формула со свободными переменными выводима идеальными методами (1928: 474).

В дополнение к консервативности Гильберт предложил такие ограничения теории, как простота, краткость доказательств, «экономия мышления» и математическая продуктивность. Формальная система трансфинитной логики не произвольна: «Эта игра в формулы воплощается согласно определенным и несомненным правилам, в которых выражена техника нашего мышления. <…> Фундаментальной идеей моей теории доказательств было не что иное, как описать деятельность нашего понимания, создать протокол правил, которым наше мышление в действительности следует» (1928: 475). Когда Вейль в конечном счете отвернулся от интуиционизма (см. Weyl 1928, а также Mancosu and Ryckman 2002 касательно его мотивов), в гильбертовой теории доказательств он подчеркнул именно это побуждение: превратить математику не в бессмысленную игру символами, но в теоретическую науку, которая упорядочивает научную (математическую) практику.

Таким образом, формализм Гильберта являлся довольно утонченным. Он избегал двух наиболее острых возражений. Во-первых, если формулы системы бессмысленны, как может выводимость в самой системе произвести какую бы ни было убежденность в них? Во-вторых, почему принята система PA, а не любая другая непротиворечивая система? Оба возражения знакомы еще с работ Фреге; на оба вопроса был дан (частичный) ответ при помощи доказательства консервативности реальных утверждений. Более того, для отвода второго возражения у Гильберта был натуралистический критерий приемлемости: мы ограничены в выборе систем соображениями простоты, результативности, единообразия — и тем, что математики делают в действительности. Вейль добавил бы, что наивысшей проверкой теории была бы ее полезность для физики.

Большинство философов математики видят в Гильберте инструменталиста (включая Kitcher 1976, Resnik 1980, Giaquinto 1983, Sieg 1990 и в особенности Detlefsen 1986), поскольку из объяснения, что идеальные предложения «не имеют значения сами по себе» (Hilbert 1926, 381), они делают вывод, будто для Гильберта классическая математика представляет собой лишь инструмент и что утверждения трансфинитной математики не имеют истинностного значения. Даже если Гильберт и является инструменталистом, то прежде всего — в методологии. Успешное исполнение теоретико-доказательной программы показало бы — математику и впрямь можно рассматривать так, как если бы она была бессмысленной. А значит, сравнение с физикой предполагает не то, что трансфинитные предложения не имеют значения (как и предложения, включающие теоретические термины), а то, что им не требуется никакого интуитивного смысла: нет необходимости непосредственно усматривать электрон, чтобы рассуждать о нем. Принимая во внимание как влияние математической мысли XIX столетия (из которого вышел Гильберт), так и публикованные и неизданные источники за всю карьеру Гильберта (в особенности Hilbert 1992, где метод идеальных элементов разбирается наиболее развернуто) Халлет пришел к следующему заключению:

Программа Гильберта и теоремы Гёделя о неполноте

Значение теорем Гёделя о неполноте для программы Гильберта было предметом множества дискуссий, равно как и вопрос о том, какая из двух — первая или вторая теорема о неполноте — вызвала переворот. Бесспорно, мнения людей, напрямую вовлеченных в разработку программы, сходились в одном: теоремы имели решающее воздействие. Гёдель изложил вторую теорему о неполноте в тезисах, опубликованных в октябре 1930 года: ни одно доказательство непротиворечивости Principia, теории множеств Цермело–Френкеля или систем, исследованных Аккерманом и фон Нейманом, нельзя осуществить при помощи методов, которые могут быть сформулированы в этих системах. В полной версии работы Гёдель допускает, что в принципе могут существовать финитные методы, не формализуемые в этих системах и тем не менее ведущие к требуемым доказательствам непротиворечивости (Gödel 1931). Первой реакцией Бернайса в письме Гёделю в январе 1931 было следующее: «Если, подобно фон Нейману, счесть несомненным, что все без исключения финитные соображения могут быть формализованы в системе Р, — как и вы, я не расцениваю это как факт, — придется заключить, что финитная демонстрация непротиворечивости Р невозможна» (Gödel 2003a: 87).

Какое влияние теоремы Гёделя оказали на программу Гильберта? Благодаря тщательной («гёделевской») нумерации последовательностей символов (формул, доказательств) Гёдель показал, что в теориях Т, которые в достаточной степени содержат арифметику, допустимо произвести формулу Pr(x, y), «утверждающую», что х (номер) является доказательством y (формулы, имеющей данный номер). В частности, если ⌈0 = 1⌉ является номером формулы 0 = 1, тогда ConT = ∀x ¬Pr(x,⌈0 = 1⌉) может «утверждать», что Т непротиворечива (никакой номер не кодирует вывод из Т, что 0 = 1). Вторая теорема Гёделя о неполноте (G2) утверждает, что — при определенных допущениях относительно Т и способа нумерации — Т не доказывает ConT. Теперь предположим, что есть финитное доказательство непротиворечивости Т. Методы, задействованные в нем, предположительно формализуемы в Т (грубо говоря, «формализуемость» означает: если доказательство применяет финитную операцию f к выводам, которые преобразуют любой вывод D в вывод f(D) упрощенной формы, тогда есть формула F(x,y) такая, что все выводы D,T ⊢ F(⌈D⌉,⌈f (D)⌉). Непротиворечивость Т может быть финитно выражена как общее условие следующего вида: если D — любая данная последовательность символов, D не является выводимым из Т для формулы 0 = 1. Формализацией данного предложения является формула ¬Pr(x,⌈0 = 1⌉), в которой переменная х оказывается несвязанной. Если бы финитное доказательство непротиворечивости Т существовало, его формализация приводила бы к выводу в Т о том, что ¬PrT(x,⌈0 = 1⌉), из которого ConT может быть выведена в Т простым универсальным обобщением по х. Тем не менее, вывод ConT в Т исключен G2.

Как ранее указывалось, изначально Гёдель и Бернайс полагали, что трудности в получении доказательства непротиворечивости PA может быть преодолены при использовании методов, которые являются финитными, хотя и не формализуемыми в PA. Могут ли подобные методы быть сочтены финитными в соответствии с исходной концепции финитизма или же они выступают расширением исходной точки зрения финитизма — вопрос дискуссионный. Новые методы, о которых идет речь, включали в себя финитную версию ω-правила, предложенную Гильбертом (Hilbert 1931b, 1931a). Тем не менее, справедливости ради стоит отметить: после 1934 года почти повсеместно было принято, что все методы доказательства, обозначенные в качестве финитных до результатов Гёделя, формализуемы в PA. Доводы в пользу расширения исходной точки зрения финитизма выдвигались во многом на финитных основаниях: например, Генцен отстаивал применение трансфинитной индукции до ε0 в своем доказательстве непротиворечивости PA как «неоспоримое» (Gentzen 1936); Такеути предложил другую защиту (Takeuti 1987). Гёдель представил еще одно расширение финитной точки зрения (Gödel 1958). Работы Крайзеля, упомянутые выше, могут быть также рассмотрены как попытка расширить финитизм, желающая сохранить дух первоначального замысла Гильберта.

Еще один способ обойти вторую теорему Гёделя о неполноте был предложен для программы Гильберта Детлефсеном (Detlefsen 1986, 2001, 1979). Он представил несколько линий защиты, одна из которых близка к вышеописанной и состоит в заявлении, что версия ω-правила финитистски приемлема, хотя не может быть формализована (однако см. Ignjatovic 1994). Другой аргумент Детлефсена против распространенной интерпретации второй теоремы Гёделя сосредотачивает внимание на понятии формализации: из того, что конкретная формализация «Т является непротиворечивой» в гёделевской формуле ConT недоказуема, еще не следует, что не может быть других доказуемых в Т формул, имеющих столько же оснований выступать в качестве «формализации непротиворечивости Т». Они опираются на формализации предиката доказуемости PrT, отличные от стандартных. Известно, что формализованные утверждения о непротиворечивости недоказуемы до тех пор, пока предикат доказуемости подчиняется определенным общим условиям выводимости. Предикат не нуждается в таких условиях, настаивает Детлефсен, чтобы считаться подлинным предикатом доказуемости — в самом деле, существуют предикаты доказуемости, которые нарушают условия доказуемости и вместе с тем приводят к формулам непротиворечивости, доказуемым в соответствующих им теориях. Все это построение, однако, зависит от нестандартных концепций доказуемости, которые, скорее всего, не были бы приняты Гильбертом (см. также Resnik 1974, Auerbach 1992 и Steiner 1991).

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

Первая теорема Гёделя о неполноте (G1) устанавливает: для любой достаточно сильной непротиворечивой формальной теории S найдется предложение GS, которое будет истинным, но невыводимым из S. GS — реальное предложение, согласно определению Сморински. Теперь рассмотрим теорию Т, которая формализует идеальную математику. и ее подтеорию S, которая формализует реальную математику. S удовлетворяет условиям G1; следовательно, из S невыводимо GS. Тем не менее, Т, будучи формализацией всей математики (включая ту ее часть, которая необходима для удостоверения истинности GS), выводит GS. Тем самым у нас оказывается реальное утверждение, которое доказуемо в идеальной математике и недоказуемо в реальной.

Детлефсен пытался отвести и это возражение против программы Гильберта (Detlefsen 1986: app.; см. также 1990). Детлефсен утверждал, что «гильбертианский» инструментализм избегает аргумента G1, поскольку, по его мнению, идеальная математика не должна быть консервативной по сравнению с реальной частью: от нее требуется лишь корректность в отношении к реальной части. В рамках инструментализма Гильберта идеальная теория просто не должна доказывать ничего из того, что вступало бы в противоречие с реальной теорией; она вовсе не обязана доказывать исключительно реальные утверждения, которые также доказываются реальной теорией. (Более подробный разбор вопросов, касающихся консервативности и непротиворечивости, см. в Zach 2006; дальнейшее обсуждение см. в соотв. разделе статьи про Гёделя; схожую защиту и переоценку проекта Гильберта см. в Franks 2009.)

Пересмотренные программы Гильберта

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

Редуктивная теория доказательств в этом смысле опиралась на две традиции. Во-первых, большинство последователей Генцена и Шютте развили программу под названием анализ ординалов. Ее примером служит первое доказательство непротиворечивости PA, данное Генценом, где была использована индукция до ε0. ε0 — определенный трансфинитный (хотя и счетный) ординал; впрочем, «индукция до ε0» в использованном смысле не является подлинно трансфинитной процедурой. Анализ ординалов оперирует не с бесконечными порядковыми числами, а скорее с системами записи ординалов, которые сами могут быть формализованы в очень слабых (по сути, финитных) системах. Анализ ординалов системы Т дан, если: (а) возможно произвести систему записи ординала, имитирующую ординалы, меньшие, чем некоторый ординал αT — таким образом, что (б) может быть финитно доказано, что формализация TI(αT) принципа индукции вплоть до αT подразумевает непротиворечивость Т (т.е. S ⊢ TI(αT)→ConT) и (в) T доказывает TI(β) для всех β < αT (S — теория, которая формализует финитную метаматематику и обычно является слабой подтеорией Т). Чтобы теория обладала значимостью в качестве основания, от нее также требуется возможность дать конструктивное доказательство трансфинитной индукции вплоть до αT. Как отмечено выше, это было проделано Генценом и Такеути для ε0, теоретико-доказательного ординала PA, однако для более сильных теорий нахождение такого доказательства становится более сложным и все более спорным с точки зрения философской значимости.

Более философски удовлетворительное продолжение программы Гильберта в теоретико-доказательных терминах было предложено Крайзелем (Kreisel 1983, 1968) и Феферманом (Feferman 1988, 1993a). Они исходили из более широкого понимания программы Гильберта — как попытки обосновать идеальную математику с помощью ограниченного набора средств. При таком истолковании задача теории доказательства Гильберта состоит в том, чтобы показать: по меньшей мере в отношении одного определенного класса реальных предложений идеальная математика не выходит за пределы реальной. Финитное доказательство непротиворечивости, каким его видел Гильберт, добивается следующего: если идеальная математика доказывает реальное предложение, тогда это предложение уже доказуемо реальными (т.е. финитными) методами. В некотором смысле речь здесь идет о сведении идеальной математики к реальной. Теоретико-доказательная редукция теории Т к теории S показывает: в отношении определенного класса реальных предложений, если Т доказывает предложение, S также его доказывает, и доказательство этого факта само является финитным. Теоретико-доказательная программа Гильберта может быть рассмотрена как поиск теоретико-доказательного сведения всей математики к финитной математике. Ограниченные программы Гильберта пытаются свести более слабые, чем классическая математика, теории к теориям, зачастую даже более сильным, чем финитная математика. Теоретики доказательств предоставили некоторое количество таких результатов — включая редукцию теорий, которые и сами требуют привнесения значительного количества идеальной математики для своего обоснования (например, подсистемы анализа) финитными системами. Феферман использовал подобные результаты в сочетании с другими, которые показывали, что большая часть применимой в науке математики (если не вся математика) может быть воплощена в системы, для которых подобные редукции доступны (Feferman 1993b). Исходя из этого Феферман выступил против аргумента незаменимости в философии математики. В настоящее время философское значение подобных теоретико-доказательных редукций является предметом дискуссий (Hofweber 2000; Feferman 2000).

Программа т.н. обратной математики — разработанная, в частности, Фридманом и Симпсоном — является другим продолжением программы Гильберта. В свете результатов Гёделя, которые показывают, что не вся классическая математика может быть сведена к финитной. они ищут ответ на вопрос о том, какая именно часть классической математики все же редуцируется подобным образом. Обратные математики стремятся дать точный ответ на этот вопрос, пытаясь выяснить, какие теоремы классической математики доказуемы в слабых подсистемах анализа, которые в свою очередь редуцируемы к финитной математике (в указанном выше смысле). Один из результатов гласит, что теорема Хана–Банаха из функционального анализа доказуема в теории, известной как WKL0 (в честь «слабой леммы Кёнига»). WKL0 консервативна относительно PRA по Π02-предложениям (т.е. предложениям формы ∀x∃yA(x, y)). (См. общий обзор Simpson 1988 и технические разъяснения в Simpson 1999.)

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

Вейль Г. (1934) Современное состояние проблемы познания в математике // О философии математики. М.; Л.: ГТТИ, 1934. С. 9–33.

Виганд О. (1998) «Знаки in concreto» — к кантовскому «формалистическому» обоснованию математики // Логическое кантоведение-4: Труды международного семинара / отв. ред. В.Н. Брюшинкин. Калининград: Калининградский государственный университет, 1998. С. 216–238.

Гильберт Д. (1948) Обоснования математики // Он же. Основания геометрии. М.; Л.: ОГИЗ; Государственное издательство технико-теоретической литературы. С. 11–64.

–—. (1969) Математические проблемы // Проблемы Гильберта / под ред. П.С. Александрова. М.: Наука. С.

–—. (1988) Аксиоматическое мышление // Методологический анализ оснований математики / отв. ред. М.И. Панов. М.: Наука. С. 97–103.

Гильберт Д., Аккерман В. (2010) Основы теоретической логики. М.: Издательская группа URSS.

Ackermann, Wilhelm, 1924, “Begründung des ”tertium non datur“ mittels der Hilbertschen Theorie der Widerspruchsfreiheit”, Mathematische Annalen, 93: 1–36.

Auerbach, David, 1992, “How to say things with formalisms”, in Proof, Logic, and Formalization, Michael Detlefsen, ed., London: Routledge, 77–93.

Avigad, Jeremy, 2003, “Number theory and elementary arithmetic”, Philosophia Mathematica, 11: 257–284. [Preprint available online]

Bernays, Paul, 1922, “Über Hilberts Gedanken zur Grundlegung der Arithmetik”, Jahresbericht der Deutschen Mathematiker-Vereinigung, 31: 10–19. English translation in Mancosu (1998a, 215–222).

Bernays, Paul, 1923, “Erwiderung auf die Note von Herrn Aloys Müller: Über Zahlen als Zeichen”, Mathematische Annalen, 90: 159–63. English translation in Mancosu (1998a, 223–226).

Bernays, Paul, 1928a, “Über Nelsons Stellungnahme in der Philosophie der Mathematik”, Die Naturwissenschaften, 16: 142–45.

Bernays, Paul, 1928b, “Zusatz zu Hilberts Vortrag über ‘Die Grundlagen der Mathematik’”,Abhandlungen aus dem Mathematischen Seminar der Universität Hamburg, 6: 88–92. English translation in: van Heijenoort (1967, 485–489).

Bernays, Paul, 1930, “Die Philosophie der Mathematik und die Hilbertsche Beweistheorie”, Blätter für deutsche Philosophie, 4: 326–67. Reprinted in Bernays (1976, 17–61). English translation in Mancosu (1998a, 234–265).

Bernays, Paul, 1976, Abhandlungen zur Philosophie der Mathematik, Darmstadt: Wissenschaftliche Buchgesellschaft.

Dean, Walter, forthcoming, “Arithmetical reflection and the provability of soundness”, Philosophia Mathematica, doi:10.1093/philmat/nku026

Detlefsen, Michael, 1979, “On interpreting Gödel's second theorem”, Journal of Philosophical Logic, 8: 297–313. Reprinted with a postscript in Shanker (1988, 131–154).

Detlefsen, Michael, 1986, Hilbert's Program, Dordrecht: Reidel.

Detlefsen, Michael, 1990, “On an alleged refutation of Hilbert's program using Gödel's first incompleteness theorem”, Journal of Philosophial Logic, 19: 343–377.

Detlefsen, Michael, 2001, “What does Gödel's second theorem say?”, Philosophia Mathematica, 9: 37–71.

Ewald, William Bragg (ed.), 1996, From Kant to Hilbert. A Source Book in the Foundations of Mathematics, vol. 2, Oxford: Oxford University Press.

Ewald, William Bragg and Wilfried Sieg (eds.), 2013, David Hilbert's Lectures on the Foundations of Arithmetic and Logic 1917–1933, Berlin and Heidelberg: Springer.

Feferman, Solomon, 1988, “Hilbert's Program relativized: Proof-theoretial and fondational reductions”, Journal of Symbolic Logic, 53(2): 364–284.

Feferman, Solomon, 1993a, “What rests on what? The proof-theoretic analysis of mathematics”, in Philosophy of Mathematics. Proceedings of the Fifteenth International Wittgenstein-Symposium, Part 1, Johannes Czermak, ed., Vienna: Hölder-Pichler-Tempsky, 147–171. Reprinted in Feferman (1998, Ch. 10, 187–208). [Preprint available online].

Feferman, Solomon, 1993b, “Why a little bit goes a long way: Logical foundations of scientifically applicable mathematics”, PSA 1992, 2: 442–455. Reprinted in Feferman (1998, Ch. 14, 284–298). [Preprint available online].

Feferman, Solomon, 1998, In the Light of Logic, Oxford: Oxford University Press.

Feferman, Solomon, 2000, “Does reductive proof theory have a viable rationale?”, Erkenntnis, 53: 63–96. [Preprint available online].

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

Ganea, Mihai, 2010, “Two (or three) notions of finitism”, Review of Symbolic Logic, 3: 119–144.

Gentzen, Gerhard, 1936, “Die Widerspruchsfreiheit der reinen Zahlentheorie”, Mathematische Annalen, 112: 493–565. English translation in Gentzen (1969, 132–213).

Gentzen, Gerhard, 1969, The Collected Papers of Gerhard Gentzen, Amsterdam: North-Holland.

Giaquinto, Marcus, 1983, “Hilbert's philosophy of mathematics”, British Journal for Philosophy of Science, 34: 119–132.

Gödel, Kurt, 1931, “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I”, Monatshefte für Mathematik und Physik, 38: 173–198. Reprinted and translated inGödel (1986, 144–195).

Gödel, Kurt, 1958, “Über eine bisher noch nicht benütze Erweiterung des finiten standpunktes”, Dialectica, 280–287. Reprinted and translated in Gödel (1990, 217–251).

Gödel, Kurt, 1986, Collected Works, vol. 1, Oxford: Oxford University Press.

Gödel, Kurt, 1990, Collected Works, vol. 2, Oxford: Oxford University Press.

Gödel, Kurt, 2003, Collected Works, vol. 4, Oxford: Oxford University Press.

Hallett, Michael, 1990, “Physicalism, reductionism and Hilbert”, in Physicalism in Mathemtics, Andrew D. Irvine, ed., Dordrecht: Reidel, 183–257.

Hilbert, David, 1899, “Grundlagen der Geometrie”, in Festschrift zur Feier der Enthüllung des Gauss-Weber-Denkmals in Göttingen, Leipzig: Teubner, 1–92, 1st ed.

Hilbert, David, 1900a, “Mathematische Probleme”, Nachrichten von der Königlichen Gesellschaft der Wissenschaften zu Göttingen, Math.-Phys. Klasse, 253–297. Lecture given at the International Congress of Mathematicians, Paris, 1900. Partial English translation in Ewald (1996, 1096–1105).

Hilbert, David, 1900b, “Über den Zahlbegriff”, Jahresbericht der Deutschen Mathematiker-Vereinigung, 8: 180-184. English translation in Ewald (1996, 1089–1096).

Hilbert, David, 1905, “Über die Grundlagen der Logik und der Arithmetik”, in Verhandlungen des dritten Internationalen Mathematiker-Kongresses in Heidelberg vom 8. bis 13. August 1904, A. Krazer, ed., Leipzig: Teubner, 174–85. English translation in van Heijenoort (1967, 129–138).

Hilbert, David, 1918a, “Axiomatisches Denken”, Mathematische Annalen, 78: 405–15. Lecture given at the Swiss Society of Mathematicians, 11 September 1917. Reprinted in Hilbert (1935, 146–156). English translation in Ewald (1996, 1105–1115).

Hilbert, David, 1918b, “Prinzipien der Mathematik”, Lecture notes by Paul Bernays. Winter-Semester 1917/18. Typescript. Bibliothek, Mathematisches Institut, Universität Göttingen. Edited in Ewald and Sieg (2013, 59–221)..

Hilbert, David, 1922a, “Grundlagen der Mathematik”, Vorlesung, Winter-Semester 1921/22. Lecture notes by Paul Bernays. Typescript. Bibliothek, Mathematisches Institut, Universität Göttingen. Edited in Ewald and Sieg (2013, 431–527).

Hilbert, David, 1922b, “Neubegründung der Mathematik: Erste Mitteilung”, Abhandlungen aus dem Seminar der Hamburgischen Universität, 1: 157–177. Series of talks given at the University of Hamburg, July 25–27, 1921. Reprinted with notes by Bernays in Hilbert (1935, 157–177). English translation in Mancosu (1998a, 198–214) and Ewald (1996, 1115–1134).

Hilbert, David, 1923, “Die logischen Grundlagen der Mathematik”, Mathematische Annalen, 88: 151–165. Lecture given at the Deutsche Naturforscher-Gesellschaft, September 1922. Reprinted in Hilbert (1935, 178–191). English translation in Ewald (1996, 1134–1148).

Hilbert, David, 1926, “Über das Unendliche”, Mathematische Annalen, 95: 161–190. Lecture given Münster, 4 June 1925. English translation in van Heijenoort (1967, 367–392).

Hilbert, David, 1928, “Die Grundlagen der Mathematik”, Abhandlungen aus dem Seminar der Hamburgischen Universität, 6: 65–85. Reprinted in Ewald and Sieg (2013, 917–942). English translation in van Heijenoort (1967, 464–479).

Hilbert, David, 1929, “Probleme der Grundlegung der Mathematik”, Mathematische Annalen, 102: 1–9. Lecture given at the International Congress of Mathematicians, 3 September 1928. Reprinted in Ewald and Sieg (2013, 954–966). English translation in Mancosu (1998a, 227–233).

Hilbert, David, 1931a, “Beweis des Tertium non datur”, Nachrichten der Gesellschaft der Wissenschaften zu Göttingen. Math.-phys. Klasse, 120-125. Reprinted in Ewald and Sieg (2013, 967–982).

Hilbert, David, 1931b, “Die Grundlegung der elementaren Zahlenlehre”, Mathematische Annalen, 104: 485–494. Reprinted in Hilbert (1935, 192–195) and Ewald and Sieg (2013, 983–990). English translation in Ewald (1996, 1148–1157).

Hilbert, David, 1935, Gesammelte Abhandlungen, vol. 3, Berlin: Springer.

Hilbert, David, 1992, Natur und mathematisches Erkennen, Basel: Birkhäuser. Vorlesungen, 1919–20.

Hilbert, David and Ackermann, Wilhelm, 1928, Grundzüge der theoretischen Logik, Berlin: Springer.

Hilbert, David and Bernays, Paul, 1923, “Logische Grundlagen der Mathematik”, Vorlesung, Winter-Semester 1922-23. Lecture notes by Paul Bernays, with handwritten notes by Hilbert. Hilbert-Nachlaß, Niedersächsische Staats- und Universitätsbibliothek, Cod. Ms. Hilbert 567.

Hilbert, David and Bernays, Paul, 1934, Grundlagen der Mathematik, vol. 1, Berlin: Springer.

Hilbert, David and Bernays, Paul, 1939, Grundlagen der Mathematik, vol. 2, Berlin: Springer.

Hofweber, Thomas, 2000, “Proof-theoretic reduction as a philosopher's tool”, Erkenntnis, 53: 127–146.

Ignjatovic, Aleksandar, 1994, “Hilbert's program and the omega rule”, Journal of Symbolic Logic, 59: 322–343.

Kitcher, Philip, 1976, “Hilbert's epistemology”, Philosophy of Science, 43: 99–115.

Kreisel, Georg, 1960, “Ordinal logics and the characterization of informal notions of proof”, in Proceedings of the International Congress of Mathematicians. Edinburgh, 14–21 August 1958, J. A. Todd, ed., Cambridge: Cambridge University Press, 289–299.

Kreisel, Georg, 1968, “A survey of proof theory”, Journal of Symbolic Logic, 33: 321–388.

Kreisel, Georg, 1970, “Principles of proof and ordinals implicit in given concepts”, in Intuitionism and Proof Theory, A. Kino, J. Myhill, and R. E. Veseley, eds., Amsterdam: North-Holland.

Kreisel, Georg, 1983, “Hilbert's programme”, in Philosophy of Mathematics, Paul Benacerraf and Hilary Putnam, eds., Cambridge: Cambridge University Press, 207–238, 2nd ed.

Mancosu, Paolo (ed.), 1998a, From Brouwer to Hilbert. The Debate on the Foundations of Mathematics in the 1920s, Oxford: Oxford University Press.

Mancosu, Paolo, 1998b, “Hilbert and Bernays on Metamathematics”, in (Mancosu, 1998a), 149–188. Reprinted in Mancosu (2010).

Mancosu, Paolo, 1999, “Between Russell and Hilbert: Behmann on the foundations of mathematics”, Bulletin of Symbolic Logic, 5(3): 303–330. Reprinted in Mancosu (2010).

Mancosu, Paolo, 2010, The Adventure of Reason: Interplay Between Philosophy of Mathematics and Mathematical Logic, 1900–1940, Oxford: Oxford University Press.

Mancosu, Paolo and Ryckman, Thomas, 2002, “Mathematics and phenomenology: The correspondence between O. Becker and H. Weyl”, Philosophia Mathematica, 10: 130–202. Reprinted in Mancosu (2010).

Parsons, Charles, 1998, “Finitism and intuitive knowledge”, in The Philosophy of Mathematics Today, Matthias Schirn, ed., Oxford: Oxford University Press, 249–270.

Patton, Lydia, 2014, “Hilbert's objectivity”, Historia Mathematica, 41(2): 188–203.

Peckhaus, Volker, 1990, Hilbertprogramm und Kritische Philosophie, Göttingen: Vandenhoeck und Ruprecht.

Poincaré, Henri, 1906, “Les mathématiques et la logique”, Revue de métaphysique et de morale, 14: 294–317. English translation in Ewald (1996, 1038–1052).

Resnik, Michael D., 1974, “On the philosophical significance of consistency proofs”, Journal of Philosophical Logic, 3: 133–47.

Resnik, Michael, 1980, Frege and the Philosophy of Mathematics, Ithaca: Cornell University Press.

Shanker, Stuart G., 1988, Gödel's Theorem in Focus, London: Routledge.

Sieg, Wilfried, 1990, “Reflections on Hilbert's program”, in Acting and Reflecting, Wilfried Sieg, ed., Dordrecht: Kluwer, 171–82. Reprinted in Sieg (2013).

Sieg, Wilfried, 1999, “Hilbert's programs: 1917–1922”, Bulletin of Symbolic Logic, 5(1): 1–44. Reprinted in Sieg (2013).

Sieg, Wilfried, 2013, Hilbert's Programs and Beyond, New York: Oxford University Press.

Simpson, Stephen G., 1988, “Partial realizations of Hilbert's program”, Journal of Symbolic Logic, 53(2): 349–363.

Simpson, Stephen G., 1999, Subsystems of Second Order Arithmetic, Berlin: Springer.

Smorynski, Craig, 1977, “The incompleteness theorems”, in Handbook of Mathematical Logic, Jon Barwise, ed., Amsterdam: North-Holland, 821–865.

Steiner, Mark, 1975, Mathematical Knowledge, Ithaca: Cornell University Press.

Steiner, Mark, 1991, “Review of Hilbert's Program: An Essay on Mathematical Instrumentalism(Detlefsen, 1986)”, Journal of Philosophy, 88(6): 331–336.

Tait, W. W., 1981, “Finitism”, Journal of Philosophy, 78: 524–546. Reprinted in Tait (2005a, 21–42).

Tait, W. W., 2002, “Remarks on finitism”, in Reflections on the Foundations of Mathematics. Essays in Honor of Solomon Feferman, Wilfried Sieg, Richard Sommer, and Carolyn Talcott, eds., Association for Symbolic Logic, LNL 15. Reprinted in Tait (2005a, 43–53). [Preprint available online]

Tait, W. W., 2005a, The Provenance of Pure Reason: Essays in the Philosophy of Mathematics and its History, New York: Oxford University Press.

Tait, W. W., 2005b, “Appendix to Chapters 1 and 2,” in Tait (2005a, 54–60)

Takeuti, Gaisi, 1987, Proof Theory, Studies in Logic 81, Amsterdam: North-Holland, 2nd ed.

van Heijenoort, Jean (ed.), 1967, From Frege to Gödel. A Source Book in Mathematical Logic, 1897–1931, Cambridge, Mass.: Harvard University Press.

von Neumann, Johann, 1927, “Zur Hilbertschen Beweistheorie”, Mathematische Zeitschrift, 26: 1–46.

Weyl, Hermann, 1921, “Über die neue Grundlagenkrise der Mathematik”, Mathematische Zeitschrift, 10: 37–79. Reprinted in Weyl (1968, 143–180). English translation in Mancosu (1998a, 86–118).

Weyl, Hermann, 1925, “Die heutige Erkenntnislage in der Mathematik”, Symposion, 1: 1–23. Reprinted in: Weyl (1968, 511–42). English translation in: Mancosu (1998a, 123–42).

Weyl, Hermann, 1928, “Diskussionsbemerkungen zu dem zweiten Hilbertschen Vortrag über die Grundlagen der Mathematik”, Abhandlungen aus dem Mathematischen Seminar der Universität Hamburg, 6: 86–88. English translation in van Heijenoort (1967, 480–484).

Weyl, Hermann, 1968, Gesammelte Abhandlungen, vol. 1, Berlin: Springer Verlag.

Zach, Richard, 1999, “Completeness before Post: Bernays, Hilbert, and the development of propositional logic”, Bulletin of Symbolic Logic, 5(3): 331–366. [Preprint available online]

Zach, Richard, 2003, “The practice of finitism. Epsilon calculus and consistency proofs in Hilbert's Program”, Synthese, 137: 211–259. [Preprint available online]

Zach, Richard, 2004, “Hilbert's ‘Verunglückter Beweis,’ the first epsilon theorem, and consistency proofs”, History and Philosophy of Logic, 25: 79–94. [Preprint available online]

Zach, Richard, 2006, “Hilbert's program then and now”, in: Dale Jacquette, ed., Philosophy of Logic. Handbook of the Philosophy of Science, vol. 5. Amsterdam: Elsevier, 411–447. [Preprint available online]