Противоречие Брауэра и Гильберта - Brouwer–Hilbert controversy

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

Задний план

Фон для разногласий был положен аксиоматизацией геометрии Дэвидом Гильбертом в конце 1890-х годов. В своей биографии Курта Гёделя , Джон У. Доусон младший суммирует результат следующим образом : «На вопрос в иногда ожесточенные споры было отношение математики к логике, а также фундаментальные вопросы методологии, например, как кванторы должны были быть истолковал, в какой степени, если вообще, неконструктивные методы были оправданы, и существуют ли важные связи, которые должны быть установлены между синтаксическими и семантическими понятиями ".

Доусон отмечает, что «в дебатах приняли участие сторонники трех основных философских позиций» - логики ( Готлоб Фреге и Бертран Рассел ), формалисты ( Давид Гильберт и его «школа» сотрудников) и конструктивисты ( Анри Пуанкаре и Герман Вейль). ); Внутри этой конструктивистской школы был радикальный самоназванный «интуиционист» Л. Д. Брауэр .

Краткая история Брауэра и интуиционизма

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

В 1908 году: «... Брауэр в статье, озаглавленной« Ненадежность принципов логики », оспаривал веру в то, что правила классической логики, дошедшие до нас по существу от Аристотеля (384–322 до н.э.), имеют абсолютная действительность, независимо от предмета, к которому они применяются ".

«После завершения диссертации (1907: см. Ван Дален) Брауэр принял сознательное решение временно скрыть свои спорные идеи и сосредоточиться на демонстрации своего математического мастерства» (Дэвис (2000), стр. 95); к 1910 г. он опубликовал ряд важных работ, в частности теорему о неподвижной точке . Гильберт - формалист, с которым интуиционист Брауэр в конечном итоге провел годы в конфликте, - восхищался этим молодым человеком и помог ему получить регулярное академическое назначение (1912 г.) в Амстердамском университете. Именно тогда «Брауэр почувствовал себя свободным вернуться к своему революционному проекту, который он теперь называл интуиционизмом ».

В конце 1920-х годов Брауэр стал участником публичного и унизительного спора с Гильбертом по поводу редакционной политики в Mathematische Annalen , в то время ведущем научном журнале . Он стал относительно изолированным; Развитием интуиционизма в его истоках занялась его ученица Аренд Гейтинг .

Истоки разногласий

Природа доказательства Гильберта теоремы о базисе (датированного 1888 годом) оказалась более противоречивой, чем Гильберт мог представить в то время. Хотя Кронекер и признал, Гильберт позже ответил на аналогичную критику других о том, что «многие различные конструкции объединены одной фундаментальной идеей» - другими словами (цитируя Рейда): «Посредством доказательства существования Гильберт смог получить строительство"; «доказательство» (то есть символы на странице) было «объектом».

Не все были убеждены. В то время как Кронекер вскоре умрет, его конструктивистское знамя будет нести острая критика со стороны Пуанкаре, а затем и крик молодого Брауэра и его развивающейся интуиционистской «школы» - в частности, Вейля, к большому мучению Гильберта в его более поздние годы ( Reid 1996, стр. 148–149). Действительно, Гильберт потерял своего «одаренного ученика» Вейля из-за интуиционизма: «Гильберт был обеспокоен увлечением его бывшего ученика идеями Брауэра, которое пробудило в Гильберте память о Кронекере».

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

Действие закона исключенного третьего

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

Но затем Гильберт доходит до сути - запрета закона исключенного среднего (LoEM): «Самый резкий и страстный вызов интуиционизму - это вызов, который он бросает против законности принципа исключенного среднего ...».

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

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

Более глубокие философские различия

Философское поражение в поисках «истины» в выборе аксиом.

Как бы то ни было, «истина» окончательно определена, некоторым математикам формализм Гильберта, казалось, избегал этого понятия. И, по крайней мере, что касается его выбора аксиом, можно утверждать, что он действительно избегает этого понятия. Фундаментальный вопрос заключается в том, как выбрать «аксиомы»? Пока Гильберт не предложил свой формализм, аксиомы выбирались на «интуитивной» (эмпирической) основе. Аристотелевская логика является хорошим примером: исходя из жизненного опыта, кажется «логичным», что объект дискурса либо обладает заявленным свойством (например, «Этот грузовик желтый»), либо не имеет этого свойства («Этот грузовик не желтый "), но не оба одновременно (Аристотелевский закон непротиворечия). Примитивная форма аксиомы индукции - другая: если предикат P (n) истинен для n = 0 и если для всех натуральных чисел n, если истинность P (n) влечет истинность P (n + 1), то P (n) верно для всех натуральных чисел n.

Аксиоматическая система Гильберта - его формализм - отличается. Вначале он декларирует свои аксиомы. Но он не требует, чтобы выбор этих аксиом был основан на «здравом смысле», априорном знании (интуитивно полученное понимание или осознание, врожденное знание, рассматриваемое как «истина, не требующая каких-либо доказательств из опыта») или наблюдательного опыта ( эмпирические данные). Скорее, математик так же, как физик-теоретик, волен принять любой (произвольный, абстрактный) набор аксиом, который они так выберут. В самом деле, Вейль утверждает, что Гильберт «формализовал [редактировал] ее [классическую математику], тем самым превратив ее в принципе из системы интуитивных результатов в игру с формулами, которая происходит по фиксированным правилам». Итак, спрашивает Вейль, чем можно руководствоваться при выборе этих правил? «Что побуждает нас взять за основу именно ту систему аксиом, которую разработал Гильберт?». Вейль предлагает «последовательность - действительно необходимое, но недостаточное условие», но он не может ответить более полно, за исключением того, что отмечает, что «конструкция» Гильберта «произвольна и смелая». Наконец, он отмечает курсивом, что философский результат «построения» Гильберта будет следующим: «Если точка зрения Гильберта преобладает над интуиционизмом, как это, кажется, имеет место, то я вижу в этом решительное поражение философской позиции чистой феноменологии , которая, таким образом, оказывается недостаточной для понимания творческой науки даже в области познания, которая является наиболее первичной и наиболее открытой для доказательств - математикой ».

Другими словами: роль врожденных чувств и тенденций (интуиция) и наблюдательного опыта (эмпиризм) в выборе аксиом будет удалена, за исключением глобального смысла - «конструкция» лучше сработает, если подвергнуть ее проверке: «только теоретическую систему в целом ... можно противопоставить опыту ".

Закон исключенного среднего распространяется до бесконечности

Кантор (1897) расширил интуитивное понятие «бесконечности» - одна ступня за другой в бесконечном марше к горизонту - до понятия «завершенная бесконечность» - прибытие «полностью, далеко оттуда». "одним махом, и он символизировал это понятие одним знаком ℵ 0 (алеф-ноль). Брауэр считал, что принятие Гильбертом понятия «оптовая торговля» было «бездумным». Брауэр в своей работе (1927a) «Интуиционистские размышления о формализме» утверждает: «ВТОРОЕ ЗНАНИЕ Отказ от бездумного использования логического принципа исключенного третьего, а также признание, во-первых, того факта, что исследование вопроса« почему? упомянутый принцип оправдан и насколько он действителен, составляет существенный объект исследования в области основ математики, и, во-вторых, того факта, что в интуитивной (содержательной) математике этот принцип действителен только для конечных систем. Отождествление принципа исключенного третьего с принципом разрешимости каждой математической задачи ».

Это третье понимание относится ко второй проблеме Гильберта и продолжающейся попытке Гильберта аксиоматизировать всю арифметику и с помощью этой системы открыть «доказательство непротиворечивости» для всей математики - подробнее см. Ниже. Итак, в эту схватку (начатую Пуанкаре) Брауэр с головой погрузился с Вейлем в качестве подстраховки.

Их первая жалоба (Второе понимание Брауэра, см. Выше) возникла из-за расширения Гильбертом «Закона исключенного среднего» (и «двойного отрицания») Аристотеля - до сих пор ограниченного конечными областями аристотелевского дискурса - до бесконечных областей дискурса ». В конце 1890-х годов Гильберт успешно аксиоматизировал геометрию. Затем он успешно (по крайней мере, так думал Гильберт) использовал канторианское понятие завершенной бесконечности для получения элегантных, радикально сокращенных доказательств в анализе (1896 г. и позже). себя вполне оправдал в том, что он сделал (в дальнейшем он называет этот тип доказательства доказательством существования): «... Я сформулировал общую теорему (1896 г.) об алгебраических формах, которая является чистым утверждением существования и по самой своей природе не может быть преобразованным в заявление о конструктивности. Чисто с помощью этой теоремы существования я избежал длинных и неясных аргументов Вейерштрасса и очень сложных вычислений Дедекинда, и, кроме того, я полагаю, только мое доказательство раскрывает внутреннюю причину справедливости утверждений, сформулированных Гауссом и сформулированных им. Вейерштрасс и Дедекинд ».« Ценность чистых доказательств существования состоит как раз в том, что они исключают индивидуальную конструкцию и что многие различные конструкции объединяются в одну фундаментальную идею, так что ясно выделяется только то, что существенно для доказательства; краткость и экономия мышления является смысл существования из доказательств существования «.

От чего Гильберту пришлось отказаться, так это от «конструктивности» - его доказательства не будут производить «объекты» (за исключением самих доказательств - т. Е. Цепочек символов), но скорее они приведут к противоречиям в предпосылках и должны будут действовать путем reductio ad absurdum, распространенного на бесконечное.

Поиски Гильберта обобщенного доказательства непротиворечивости аксиом арифметики

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

Следствием этого чудесного доказательства / процедуры P будет следующее: для любой произвольной математической теоремы T (формула, процедура, доказательство), помещенной в P (таким образом, P (T)), включая сам P (таким образом, P (P)), P будет окончательно определить, была ли теорема T (и P) доказуемой, т. е. выводимой из ее посылок, аксиом арифметики. Таким образом, для всех T, T будет доказуемо с помощью P или не доказуемо с помощью P и при всех условиях (то есть для любого присвоения числовых значений переменным T). Это прекрасная иллюстрация использования закона исключенного среднего, распространенного на бесконечность, фактически расширенного дважды - во-первых, для всех теорем (формул, процедур, доказательств) и, во-вторых, для данной теоремы, для всех присваиваний ее переменных. На этот момент, упущенный Гильбертом, сначала указал ему Пуанкаре, а затем Вейль в своих комментариях 1927 года к лекции Гильберта: «В конце концов, Гильберт тоже не просто озабочен, скажем, 0 'или 0', но с любым 0 ' ... ', с произвольно конкретно заданным числом. Здесь можно подчеркнуть «конкретно данное»; с другой стороны, столь же важно, чтобы содержательные аргументы в теории доказательств проводились в гипотетической общности , о любом доказательстве, о любом числительном ... Мне кажется, что теория доказательств Гильберта показывает, что Пуанкаре был полностью прав в этом вопросе ".

В своем обсуждении, предшествовавшем комментариям Вейля 1927 года, ван Хейеноорт объясняет, что Гильберт настаивал на том, что он обращался к вопросу о том, «приводит ли формула, взятая в качестве аксиомы, к противоречию, вопрос в том, можно ли представить доказательство, ведущее к противоречию, меня".

«Но [пишет ван Хейеноорт] в доказательстве непротиворечивости аргумент не касается одной конкретной формулы; его нужно распространить на все формулы. Это то, что имеет в виду Вейль ...».

В случае успеха поиск приведет к замечательному результату: при таком обобщенном доказательстве вся математика может быть заменена автоматом, состоящим из двух частей: (i) генератора формул для создания формул одну за другой, а затем (ii) обобщенное доказательство непротиворечивости, которое дало бы «Да - действительно (т.е. доказуемо)» или «Нет - недействительно (не доказуемо)» для каждой представленной ему формулы (и каждого возможного присвоения чисел ее переменным). Другими словами: математика прекратит свое творчество и превратится в машину.

Проблема закона исключенного среднего по индукции

В комментарии ван Хейенурта, предшествовавшем работе Вейля (1927) «Комментарии к второй лекции Гильберта об основах математики», Пуанкаре указывает Гильберту (1905), что существует два типа «индукции» (1) интуитивная логика животных - следование ногам - футовая версия, которая дает нам ощущение, что всегда есть еще один шаг после последнего шага, и (2) формальная версия - например, версия Пеано: строка символов. Группа из трех человек - Пуанкаре, Вейль и Брауэр - утверждала, что Гильберт молчаливо и необоснованно принял в качестве одной из своих предпосылок формальную индукцию (строку Kleensymbol). Пуанкаре (1905) утверждал, что, сделав это, рассуждения Гильберта стали круговыми. Согласие Вейля (1927) и полемика Брауэра в конечном итоге вынудили Гильберта и его учеников Гербранда, Бернейса и Аккермана пересмотреть свое понятие «индукции» - отказаться от предположения о «совокупности всех объектов x бесконечного набора» и (интуитивно) Предположим, что общие аргументы повторяются один x за другим, до бесконечности (van Heijenoort, стр. 481, сноска a). Фактически это так называемая «схема индукции», используемая в понятии «рекурсия», которое все еще находилось в разработке в то время ( ср. Van Heijenoort, стр. 493) - эта схема была приемлема для интуиционистов, поскольку она была выведена от «интуиции».

Чтобы продолжить это различие, Клини 1952/1977 различает три типа математической индукции: (1) формальное правило индукции (аксиома Пеано, пример см. В следующем разделе), (2) индуктивное определение (примеры: счет "," Доказательство по индукции "), и (3) определение по индукции (рекурсивное определение" теоретико-числовых функций или предикатов). Что касается (3), Клини рассматривает примитивно рекурсивные функции :

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

Ряд натуральных чисел 0, 0 ', 0 ' ' , 0 ' ' ' , ... или 0, 1, 2, 3, ... мы описали как класс объектов, созданных из одного примитивного объекта 0 с помощью одной примитивной операции 'или +1. Это составляет индуктивное определение класса натуральных чисел.

Доказательство по индукции ... непосредственно соответствует этому способу генерации чисел. Определение по индукции (не путать с «индуктивным определением» ...) - это аналогичный метод определения теоретико-числовой функции φ (y) или предиката P (y). [Теоретико-числовая функция или предикат принимает в качестве переменных только выборку из натуральных чисел и в свою очередь производит только одно натуральное число]. Сначала задается φ (0) или P (0) (значение функции или предиката для 0 в качестве аргумента). Тогда для любого натурального числа y φ (y ') или P (y') (следующее значение после y) выражается через y и φ (y) или P (y) (значение y) . ... Две части определения позволяют нам, генерируя любое натуральное число y, одновременно определять значение φ (y) или P (y) »(стр. 217).

Отголоски полемики

Настаивание Брауэра на «конструктивности» в поисках «доказательства непротиворечивости арифметики» привело к чувствительности к проблеме, что отражено в работах Финслера и Гёделя. В конце концов Гёдель «оцифровал» свои формулы; Затем Гедель использовал примитивную рекурсию (и ее реализацию интуитивной конструктивной формы индукции - то есть подсчет и пошаговое вычисление) вместо строки символов, представляющих формальную индукцию. Гёдель был настолько чувствителен к этому вопросу, что в 1931 году он приложил немало усилий, чтобы указать, что его теорема VI (так называемая «Первая теорема о неполноте») «конструктивна 45a , то есть интуиционистски доказали следующее. неприемлемым образом ... " Затем он демонстрирует то, что, по его мнению, является конструктивным характером его «формулы обобщения» 17 Gen r. Сноска 45a подкрепляет его точку зрения.

Гедель 1931 года действительно включает в себя формалистскую символьную версию аксиомы индукции Пеано; это выглядит так, где "." - логическое И, f - знак-преемник, x 2 - функция, x 1 - переменная, x 1 Π обозначает «для всех значений переменной x 1 »:

(x 2 (0) .x 1 Π (x 2 (x 1 ) ⊃x 2 (fx 1 )) ⊃x 1 Π (x 2 (x 1 ))

Но, похоже, он не использует это в формалистическом смысле.

Обратите внимание, что по этому поводу есть разногласия. Гёдель определяет эту символьную строку в своем I.3., То есть формализованная аксиома индукции выглядит так, как показано выше, но даже эту строку можно «пронумеровать» с помощью метода Гёделя. С другой стороны, похоже, что он не использует эту аксиому. Скорее, его рекурсия проходит через целые числа, присвоенные переменной k (см. Его (2) на стр. 602). Его скелетное доказательство теоремы V, однако, «использует (я) индукцию по степени φ» и использует «предположение индукции». Без полного доказательства этого нам остается предположить, что его использование «гипотезы индукции» является интуитивной версией, а не символической аксиомой. Его рекурсия просто увеличивает степень функций, интуитивный акт, до бесконечности. Но Нагель и Ньюман отмечают, что доказательства Гёделя бесконечны по своей природе, а не конечны, как требовал Гильберт (см . Вторую проблему Гильберта ), в то время как Гёдель настаивал на том, что они интуитивно удовлетворительны. Это не несовместимые истины, если только LoEM над бесконечностью нигде не упоминается в доказательствах.

Несмотря на продолжающуюся абстракцию математики в последней половине двадцатого века, проблема не исчезла полностью. Вот два примера. Во-первых, посылки аргумента - даже те, которые считаются бесспорными - всегда справедливы. Внимательный взгляд на предпосылки работ Тьюринга 1936–1937 годов привел Робина Ганди (1980) к предложению своих «принципов для механизмов», которые ограничивают скорость света. Во-вторых, Брегер (2000) в своем «Неявном знании и математическом прогрессе» глубоко разбирается в вопросе «семантика против синтаксиса» - в своей статье должным образом появляются Гильберт, Пуанкаре, Фреге и Вейль. Он исследует основную проблему: в аксиоматических доказательствах молчаливое допущение опытного мыслящего ума: чтобы добиться успеха, он должен прийти к аргументу, оснащенному предварительным знанием символов и их использования (семантика, лежащая в основе бессмысленного синтаксиса): «Математика как чисто формальная система символов без человека, обладающего ноу-хау для работы с символами, невозможна [согласно химику Поланьи (1969, 195), идеал формы знания, который является строго явным, противоречив, потому что без молчаливого знание всех формул, слов и иллюстраций стало бы бессмысленным] »(скобки в оригинале, Breger 2000: 229).

Клини о Брауэре – Гильберте

Серьезное исследование этого фундаментального противоречия можно найти во « Введении в метаматематику» Стивена Клини , особенно в главе III: «Критика математических рассуждений». Он обсуждает §11. Парадоксы , §12. Первые выводы из парадоксов [непредикативные определения, логицизм и т. Д.], §13. Интуиционизм , §14. Формализм , §15. Формализация теории . Клини серьезно относится к дебатам, и на протяжении всей своей книги он фактически строит две «формальные системы», например, на странице 119 он показывает те логические законы, такие как двойное отрицание, которые запрещены в интуиционистской системе.

Заметки

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

  • WS Anglin 1994, Математика: краткая история и философия , Springer-Verlag, Нью-Йорк. ISBN   0-387-94280-7 .
  • Герберт Брегер , 2000. «Неявные знания и математический прогресс», опубликованные в E. Groshoz and H. Breger (eds.) 2000, The Growth of Mathematical Knowledge , Kluwer Academic Publishers, Dordrecht, Нидерланды, ISBN   0-7923-6151-2 , страницы 221–230.
  • Мартин Дэвис , 1965. Неразрешимое: основные статьи о неразрешимых предложениях, неразрешимых задачах и вычислимых функциях , Raven Press, Нью-Йорк, без ISBN. Это включает в себя:
    • Эмиль Пост , 1936. «Конечный комбинаторный процесс. Формулировка I», с комментарием (стр. 288ff)
    • Эмиль Пост , 1941, не публиковавшийся до 1965 года. «Абсолютно неразрешимые проблемы и относительно неразрешимые предположения: отчет об ожидании», с комментарием (стр. 338ff)
  • ван Дален, Дирк (1990). «Война лягушек и мышей, или кризис Mathematische annalen ». Математический интеллигент . 12 (4): 17–31. DOI : 10.1007 / BF03024028 . S2CID   123400249 . О битве за редакторский контроль над журналом Mathematische Annalen между Гильбертом и Брауэром, частично вызванной их фундаментальными различиями. Название этой работы - отсылка к Batrachomyomachia , классической пародии на Илиаду .
  • Мартин Дэвис , 2000. Двигатели логики , WW Norton, Лондон, ISBN   0-393-32229-7 pbk. Ср. Глава пятая: «Гильберт приходит на помощь», в которой Дэвис обсуждает Брауэра и его отношения с Гильбертом и Вейлем с краткой биографической информацией Брауэра.
  • Джон У. Доусон-младший , 1997. Логические дилеммы: жизнь и работа Курта Гёделя , А.К. Петерс, Уэлсли, Массачусетс, ISBN   1-56881-256-6 .
  • Робин Ганди , 1980. «Тезис Черча и принципы механизмов», опубликованные в J. Barwise , HJ Keisler и K. Kunen , eds., 1980, The Kleene Symposium , North-Holland Publishing Company, стр. 123–148.
  • Стивен Хокинг , 2005. Бог создал целые числа: математические открытия, изменившие историю: отредактировано с комментариями Стивеном Хокингом , Running Press, Филадельфия, ISBN   978-0-7624-1922-7 . Комментарий Хокинга и отрывок из «Вкладов Кантора в создание теории трансфинитных чисел» появляются на стр. 971ff.
  • Дэвид Гильберт (1927), «Основы математики», опубликованный по адресу http://www.marxists.org/reference/subject/philosophy/works/ge/hilbert.htm и, очевидно, взятый из Sohotra Sarkar (ed.) 1996, The Возникновение логического эмпиризма: с 1900 года до Венского кружка , Garland Publishing Inc, [без местонахождения издателя, без ISBN]. Знаменитая речь Гильберта, в которой он представляет и подробно обсуждает свои аксиомы формализма, уделяя особое внимание двойному отрицанию и Закону исключенного среднего (LoEM) и его «электронной аксиоме». [Этот онлайн-документ содержит типографские ошибки; лучше версия - Гильберт ван Хейенорта (1927).]
  • Стивен Клини , 1952 г. с исправлениями 1971 г., 10-е переиздание 1991 г., Введение в метаматематику , издательство North-Holland Publishing Company, Амстердам, Нидерланды, ISBN   0-7204-2103-9 . Ср. в частности, глава III: Критика математического мышления, §13 «Интуиционизм» и §14 «Формализм».
  • Жан ван Хейеноорт , 1976 (2-е издание с исправлениями), От Фреге до Гёделя: Справочник по математической логике, 1879–1931 , Издательство Гарвардского университета, Кембридж, Массачусетс, ISBN   0-674-32449-8 (pbk.). Следующие статьи и комментарии имеют отношение к делу и предлагают краткий график публикации. (Важные дополнительные дополнения Гёделя относительно его принятия машин Тьюринга как формальной логической системы, заменяющей его систему (Аксиомы Пеано + рекурсия), появляются в Мартине Дэвисе, Неразрешимость )
    • Гильберта (1904). Об основах логики и арифметики, стр. 129
    • Брауэр (1923, 1954, 1954a). О значении принципа исключенного третьего в математике, особенно в теории функций, с. 334
    • Брауэр (1927). Об областях определения функций с. 446
    • Гильберта (1927). Основы математики с. 464. (Знаменитая речь Гильберта).
    • Вейля (1927). Комментарии к второй лекции Гильберта об основах математики с. 480.
    • Бернейс (1927). Приложение к лекции Гильберта «Основы математики» с. 485
    • Брауэр (1927а). Интуиционистские размышления о формализме с. 490
    • Гёдель (1930a, 1931, 1931a). Некоторые метаматематические результаты о полноте и последовательности. О формально неразрешимых предложениях Principia mathematica и родственных систем I, а также о полноте и непротиворечивости с. 592
    • Брауэр (1954, 1954a). Дополнения и исправления, а также дополнительные дополнения и исправления, стр. 334ff
  • Эрнест Нагель и Джеймс Ньюманн 1958, Доказательство Гёделя , New York University Press, без ISBN, номер карточки Библиотеки Конгресса в каталоге 58-5610.
  • Констанс Рид 1996. Гильберт , Спрингер , ISBN   0-387-94674-8 . Биография на английском языке.
  • Бертран Рассел , первоначально опубликованный в 1912 году, с комментариями Джона Перри в 1997 году . Проблемы философии , Oxford University Press, Нью-Йорк, ISBN   0-19-511552-X .