Cтраница 3
Такой тип доказательства ( который, исходя из упомянутой аксиоматической системы, приводит к требуемому результату) называется доказательством в смысле Гильберта. Аксиоматическая система, рассматриваемая в этом параграфе, не содержит аксиом, зато использует немало правил вывода. Тип доказательства, связанный с такой системой, называется доказательством в смысле Генцена. [31]
В книге частично представлено содержание нескольких курсов по интуиционистской математике, которые автор читал в течение ряда лет на механико-математическом факультете МГУ. Книга содержит пять частей и два дополнения. В первой части излагаются чисто синтаксические методы исследования интуиционистской логики предикатов, основанные на теореме Генцена об устранении сечения. В частности, доказана теорема Харропа о свойствах дизъюнктивности и экзистенциальности логики предикатов. Во второй части, посвященной интуиционистской арифметике, основным инструментом исследования является принадлежащий Клини метод реализуемости. [32]
Изученные ранее исчисления представляют собой естественные формализации правил логики. Однако для более глубокого изучения самого понятия доказательства более удобными являются другие формы исчислений. В настоящем параграфе мы изучим одно из таких исчислений G, близкое к исчислению, предложенному Генценом. [33]
Допущение более широких ( но корректных с точки зрения брауэровского интуициониз ма) средств пришло позднее, особенно под влиянием результатов Геделя о неполноте. Генценовское доказательство непротиворечивости арифметики [10] показало, как можно примирить ограничения, налагаемые теоремой Геделя, с требованием фи-нитности: привлеченный Генценом принцип ( бескванторная индукция до е0), выходящий за рамки формальной арифметики первого порядка, формулируется в языке финитных предложений. [34]
Генцен все же доказал ее непротиворечивость. [35]
Это рассуждение использует вторую теорему Геделя. Генцен показал, что с помощью некоторой модификации доказательства непротиворечивости можно и без ссылки на эту теорему Геделя убедиться в том, что обобщенный принцип индукции существенным образом не укладывается в рамки арифметического формализма. [36]
Это более раннее доказательство, гранки которого сохранились, содержится в английском издании собрания сочинений Генцена, вскоре выходящем в свет под редакцией Манфреда Сабо. [37]
Оставшийся пробел в то время казался вполне безобидным, и были разработаны подробные планы вторжения в анализ. Но тут разразилась катастрофа: предположив, что непротиворечивость установлена, К. Метод Геделя применим к формализму Гильберта, равно как и к любому другому не слишком органичительному формализму. Генцен восполнил пробел в доказательстве непротиворечивости арифметики, оказавшийся, как показало открытие К. [38]
Разрешения проблемы) и служит основой для всех известных в наст, время алгоритмов выводимости. Этим объясняется чрезвычайно важное значение С. Из других приложений С.и. в первую очередь следует упомянуть о полученных самим Генценом и другими учеными ( П. С. Новиков, К. Аккерман и др.) доказательствах непротиворечивости различных арифметических формальных систем, обходящих в известном смысле трудности, обусловленные теоремой К. [39]
Кальмар использует для этого рассуждение, с помощью которого Генцен в его работе: Qentzen G. Сам Генцен тоже ссылается на это рассуждение в своем более позднем доказательстве непротиворечивости, однако здесь он говорит об этом способе обоснования как о предварительном, с намерением когда-нибудь вернуться к рассмотрению этого вопроса. Мы в Дальнейшем воспользуемся рассуждением, которое - в отличив от упомянутого рассуждения Генцена, а также от приведенного в гл. [40]