ПРЕДИСЛОВИЕ ПЕРЕВОДЧИКА

В наши дни, когда каждый, кто интересуется математикой, имел дело с языками программирования, вряд ли нужно объяснять важность изучения различных языковых средств (синтаксических конструкций) и различий в их выразительной силе. Не все, однако, знают, что первые точные постановки такого рода вопросов и точные ответы на них появились в рамках математической логики. Книга Э. Энгелера — известного специалиста по теории алгоритмов, знакомит читателя с некоторыми из этих постановок задач и результатов на примерах основных структур математического анализа, геометрии и теории вычислимости. Выразительная сила различных теорий измеряется в книге главным образом их разрешимостью (существованием механического метода, позволяющего распознавать истинность высказываний) или неразрешимостью, однако продемонстрированы и возможности гораздо более тонкой классификации.

Один из основных методов установления разрешимости теорий — так называемая элиминация кванторов, позволяющая постепенно уменьшать логическую сложность испытуемого (на истинность) высказывания до тех пор, пока оно не станет очевидно истинным или ложным. Этот метод подробно разъясняется на примере элементарной теории вещественных чисел, в которую затем погружается и элементарная геометрия.

Еще более молодое направление в математической логике— нестандартный анализ. Он позволил дать точное оформление аппарату актуально бесконечно малых и бесконечно больших величин, которым так успешно пользовались классики анализа. Автор излагает основы нестандартного анализа, предполагая у читателя знакомство лишь с элементами обычной логики (исчисления предикатов).

Глава, посвященная геометрии, содержит разнообразные сведения о выразительной силе геометрических языков и их связи с алгебраическими языками.

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

Познакомившись с небольшой книгой Э. Энгелера, читатель получит хорошее первоначальное представление о рассматриваемых вопросах и сможет при желании перейти к чтению специальной литературы,

13.3.1986 г. Г. Е. Минц

ПРЕДИСЛОВИЕ

Эта книга — не учебник, хотя она и возникла из лекций, которые я читаю уже несколько лет в Высшей технической школе в Цюрихе. Она адресована студентам-математикам второго или третьего семестра не столько с целью познакомить их с математической логикой или аксиоматикой, сколько для того, чтобы пробудить и обострить их критические способности по отношению к математике. Ведь наше воспитание убаюкивает студента. Многолетние занятия техническими приемами школьной алгебры и геометрии, а затем изучение громадного здания математического анализа вызывает почти у каждого ощущение, что он теперь знает, что такое вещественные числа, что такое функция, что такое евклидово пространство, что такое алгоритм.

Я далек от мысли отрицать пользу или даже необходимость общей согласованности в математике. Однако я выступаю против потери фантазии, которая порождается тенденцией бездумно принимать основные понятия и основные точки зрения. Я хочу изложить в этой книге ту систематическую критику оснований математики, которую сделала технически возможной математическая логика XX столетия. Таким образом, термин «метаматематика» в заглавии нашей книги указывает на методы, а «элементарная математика» — на содержание: анализ, геометрия и алгоритмика.

Говоря коротко: эта книга о том, как мы приходим к аксиомам элементарной математики и как их следует рассматривать.

Я признателен Бригитте Кнехт (которая готовила текст) и д-ру Эрнсту Графу (который готовил иллюстрации) за компетентную работу при подготовке этой книги.

Эрвин ЭнгелерЭрвин ЭнгелерЦюрих, май 1982 а,

Эрвин Энгелер

Эрвин Энгелер

Глава IКОНТИНУУМ

Что такое вещественные числа?

Примерно сто лет назад Дедекинд был профессором Швейцарской высшей технической школы в Цюрихе и читал дифференциальное и интегральное исчисление. Он говорил, что именно преподавание поставило его лицом к лицу с проблемой обоснования математического анализа. О его остроумном решении этой проблемы рассказывает небольшая книжка «Что такое вещественные числа и чем они должны быть?», которая и сегодня читается с интересом.

Ответ Дедекинда хорошо известен. Это программа арифметизации континуума, сведения основных понятий анализа к понятиям, относящимся к натуральным числам. Таким образом должно быть неоспоримо доказано существование лежащих в основе анализа математических структур; все свойства континуума, используемые в анализе, должны получаться из указанной Дедекиндом конструкции.

Арифметизация континуума по Дедекинду (набросок)

(a) N = (N, 0, 1, +, *, ^) удовлетворяет аксиомам Пеано:

0 ф х + 1 для всех х е N.

х + 1 = у + 1 только при х = у для всех х, у е N.

Если М = N и М ф 0, то М имеет наименьший в смысле отношения ^ элемент.

х ^ у т. и т. т., когда имеется ге N, такой, что х + г = у.

Сложение и умножение удовлетворяют рекурсивным уравнениям

х(у+1) = (х +у)+1,х+0 —х,

х • (у + 1) = х • у + х, х-0 = 0.

Q — <Q, 0, 1, +, •, jC> ~ упорядоченное поле.

При этом Q состоит из классов эквивалентности троек <а, Ь, с>^№, с#=0, по следующему отношению эквивалентности:

(а, 6, o') г (д', Ь', с,х) т. и т. т., когда

ас' + Ь'с = а'с + Ьс'.

Сложение и умножение определяются равенствами (а, 6, с) + (а', Ь', с'): = 1дс' + а'с, Ьс' + Ь'с, сс'), (д, Ь, с) • (а', Ь', с'): = (да' + bb', ab' + Ьа', сс').

Нуль — это класс эквивалентности, которому принадлежит <0, 0, 1>, единица — класс эквивалентности, которому принадлежит <1,0, 1>.

(а, Ь, с)^(д', Ь', с') т. и т. т., когда

ас' + Ь'с ^ а'с + Ьс'.

R_— <R, 0, 1, +, •, ^>— линейно упорядоченное поле. При этом R состоит из дедекиндовых сечений, т. е. из подмножеств S ^ Q, таких, что S #= 0, S #= Q, S не имеет наибольшего элемента иизх^5иу^х следует у е S.

Сложение: 8-уТ=Цх-Уу; x^S, у^Ту

Нуль:0 = {xgQ: х < 0}.

Единица:1={xgQ: х<1}.

Порядок:5^ Г т. и т. т., когда S^T.

Хочется определить умножение соотношением

s • т = Vх * у*- х е s, у ту

но это приводит к (преодолимым) трудностям (упражнение) .

Интуитивная основа введения множества Q — это, конечно, представление целочисленной дроби (а — Ь)/с как тройки <а, 6, с> и соответствующее определение правил сложения, умножения и сравнения величин. При построении множества R исходят из интуитивного понятия полноты, о котором мы будем говорить ниже (§ 2): суть дела в том, что каждая функция должна иметь вещественный нуль при любой перемене знака. Таким образом, понятие числа зависит от понятия функции. Это ясно уже из названия исходной работы Дедекинда «Stetigkeit und irrationale Zahlen» («Непрерывность и иррациональные числа») (1872).

Главное возражение против программы Дедекинда состоит

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

Правда, математик может принять тезис, что его вообще не интересует, откуда получаются вещественные числа. Его интересует, каковы свойства вещественных чисел. Иными словами, он ожидает от оснований анализа аксиоматизации, т. е. перечисления всех свойств поля вещественных чисел, из которых чисто логически вытекают все используемые в анализе теоремы.

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

Однако по поводу этого аксиоматического подхода следует высказать серьезные сомнения, по существу те же, что и по поводу так называемо?! арифметизации. Действительно, аксиомы относятся не только к исходным понятиям алгебры и теории порядка, таким, как +, •, < и т. д., и к элементам характеризуемого поля, но и к понятиям более высокого типа, таким, как «ограниченное множество» и т. п. Возьмем, например, аксиому Архимеда: «если а, b > 0, то имеется положительное целое число п, такое, что а-n^b». Здесь использовано понятие положительного целого числа. Можно

возразить, что теория натуральных чисел предшествует любой аксиоматике. Но тогда пришлось бы считать, что аксиомы для натуральных чисел не включены в упомянутую аксиоматику лишь условно и что следует мыслить их как бы добавленными туда.

Мы, следовательно, должны были бы добавить, например, аксиомы Пеано, в частности, следующее предложение: «Любое множество натуральных чисел, которое содержит 0 и вместе с любым своим элементом п содержит также n-V 1, — это множество всех натуральных чисел». И вот мы уже опять говорим о множествах! Причем мы делаем это, не ограничив аксиоматически рамки, в которых мы применяем основные понятия теории множеств. Конечно, можно было бы аксиоматизировать лишь ту часть теории множеств, которая нужна в данной связи, и раз и навсегда принять соглашение, что при любой аксиоматизации эти аксиомы молчаливо присутствуют.

На чем основано это соглашение? Точнее говоря, бесспорна ли аксиоматическая основа теории множеств? Конечно, нет (но об этом позже), поэтому мы должны отступить на более скромную позицию. Чтобы оборудовать такое убежище, мы воспользуемся в следующих разделах методом формализации математики.

Неудивительно, скажет конструктивист, что у вас появились трудности при обосновании анализа с помощью теории множеств. Актуально бесконечные совокупности не подлежат нашей интуиции, мы не можем усматривать их свойства непосредственно.

Можно было бы воспринимать бесконечные множества как платоновские идеи, которые присущи всему человечеству, как если бы их нам сообщили в каком-то раю, из которого мы, к сожалению, изгнаны. Это — расплывчатая онтология. При таком подходе континуум стал бы напоминать такие объекты, как птица Рух или дронт: о некоторых из их свойств мы можем прийти к соглашению, по поводу других существует неясность.

Хотя аксиоматическая теория множеств и может устроить нас в чисто техническом отношении в качестве окончательного фундамента математики, она скорее уклоняется от проблем оснований, в частности, от вопросов, связанных с парадоксами, чем проясняет их. Эти уклонения — весьма грубого рода: никак не кажется правдоподобным, что все трудности коренятся в величине противоречивых множеств.

Более того, нельзя доверять даже обычным математическим методам умозаключения; под особым подозрением находится закон исключенного третьего для бесконечных qobq^

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

Как отвечать на это нападение на классическую математику?

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

Прагматический ответ дает большинство математиков. Он содержит следующие положения.

Сомнения по поводу классической математики кажутся более сомнительными, чем она сама. Обычные умозаключения о бесконечном вполне убедительны для понимающего математика. Элиминация понятий, относящихся к бесконечному, даже там, где она возможна, не дает нам дополнительной уверенности в теоремах. Напротив, опыт показывает, что финитизированные, формализованные доказательства приводят к трудно отслеживаемым вычислительным ошибкам. Концептуальные доказательства более убедительны и наглядны, даже если они используют понятия, относящиеся к бесконечности.

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

Наконец, все остальные направления в основаниях математики можно обсуждать в рамках классической математики. Эта универсальность делает ее особенно привлекательной. Пока не станет общепринятым что-то лучшее, нам разумнее оставить все как есть.

Ободряющий ответ. Да, я, конечно, могу себе предста* вить, что поднятые вопросы кого-то пугают. Однако мне кажется, что их лучше всего использовать для выявления новых направлений исследований.

Контратака — тоже ответ. Каждая точная формули-

ровка конструктивной точки зрения, несомненно, имеет свои слабости. Мы на это уже указывали.

Нет особого смысла распространяться об этом дальше здесь и теперь. Кроме того, приходится сознаться в том, что выше мы сформулировали различные точки зрения чрезвычайно поверхностно. Что касается лучших формулировок, я хотел бы, с одной стороны, указать несколько мест в литературе по основаниям математики, а с другой — отложить дискуссию до тех пор, когда обсуждаемый материал будет лежать перед нами.

ЛИТЕРАТУРА

Dedekind R. Stetigkeit und irrationale Zahlen, 1872. In: R. Friche, E. Noether, O. Ore. Dedekind gesammelte mathematische Werke, B. 3, S. 315— 334. — Braunschweig: Vieweg, 1932. [Имеется перевод: Дедекинд P. Непрерывность и иррациональные числа. — Одесса: Матезис, 1923.]

Dedekind R. Was sind und was sollen die Zahlen? 1887. In: R. Friche, E. Noether, O. Ore. Dedekind gesammelte mathematische Werke, B. 3, S. 335—391. — Braunschweig: Vieweg, 1932. [Имеется перевод: Дедекинд P. Что такое числа и для чего они служат? — Казань: Изд-во Импер. ун-та, 1905.]

Hilbert D. Ueber den Zahlbegriff. In: Anhang VI der «Grundlagen der Geometric», 7. Auflage. — Stuttgart: Teubner, 1930. [Имеется перевод: Гильберт Д. О понятии числа. — В кн.: Гильберт Д. Основания геометрии.— М.-Л.: ГИТТЛ, 1948, с. 316—321.]

Hilbert D. Ueber das Unendliche.— /Math. Ann., B. 95, S. 161 —190, 1926. [Имеется перевод сокращенного варианта: Гильберт Д. О бесконечном.— В кн.: Гильберт Д. Основания геометрии. — М.-Л., ГИТТЛ, 1948, с. 338—364.]

Brouwer L. Е. J. Begriindung der Funktionenlehre unabhangig vom logi- schen Satz vom ausgeschlossenen Dritten, 1923. In: A. Heyting. L. E. J. Brouwer collected works, v. 1, p. 246—267. — Amsterdam: North-Holland, 197*5.

Brouwer L. E. J. Zur Begriindung der intuitionistischen Mathematik, I, II & III, 1925—1927. In: A Heyting. L. E. J. Brouwer collected works, v. 1, p. 301—314, 321—340, 352—389. — Amsterdam: North-Holland, 1975.

Bernays P. Sur le Platonisme dans les Mathematiques.— L’Enseignement Mathematiques, v. 34, 1935 Английский перевод в P. Benacerraf, H. Putnam: Philosophy of Mathematics, selected readings, p. 274—286. — Engle- vood Cliffs: Prentice-Hall, 1964.

Weyl H. Ueber die neue Grundlagenkrise der Mathematik. — Math. Z., B. 10, S. 39—79, 1921; а также Selecta Hermann Weyl, S. 211—248. — Basel & Stuttgart: Birkhauser Verlag, 1956.

§ 2. Язык как часть математики

Современная логика обязана своим возникновением подлинно грандиозной мечте Лейбница. Перед тем как я расскажу об этой мечте, позвольте мне описать историческую ситуацию.

Лейбниц жил во времена, когда обычные обозначения современной математики, например алгебры и анализа, еще только вступали на свой победный путь. Вклад самого Лейбница в этот процесс включал знаки для дифференциалов, интеграла и т. п. Лейбниц глубоко осознавал важнейшую особенность этого развития событий: беспримерный взлет новой математики существенно опирался на освобождение от размышлений о содержательном значении математических знаков и на возможность производить вычисления с этими содержательными значениями в самом подлинном смысле этого слова. Время Лейбница было эпохой, когда аксиоматическая геометрия древних греков переживала новый расцвет и ее схема: аксиома — теорема — доказательство — определение — теорема — доказательство — ... оказывала влияние на новые области философии. Вспомним хотя бы о книге Баруха Спинозы «Ethica, ordine geometrico demonstrata», т. e. «Этика, доказанная геометрическим методом».

Нельзя ли, подумал Лейбниц, так сформулировать правила математического доказательства, чтобы при их применении вообще уже не приходилось больше думать о содержательном смысле математических выражений? Нужно было бы создать calculus ratiocinator, т. с. исчисление, в котором естественные, содержательные доказательства были бы заменены формальными вычислениями и тем самым стали бы предметом математики. Такое исчисление, разумеется, предполагает символику, в которой были бы представлены аксиомы, теоремы и определения математики. Такая символика и была целью лейбницевского языка формул, знаменитой cha- racteristica universalis. Увы, она осталась лишь фрагментом и должна была им остаться, ибо даже для такого гения, как Лейбниц, тогда еще нс пришло время создавать современную логику. Формальный язык, в котором все вопросы можно было бы решать вычислением, согласно лейбницевскому лозунгу calculemus, остался мечтой.

На долю XX столетия досталось сделать важнейший шаг в направлении, указанном Лейбницем. Историческая ситуация была похожа на время Лейбница. Появились работы Дедекинда и Кантора, которые сводили всю математику к теории множеств, работы Буля, Пеано, Пирса и Шрёдера, которые вводили рудименты математической символики для законов мышления. Эти работы внушали безграничную веру в мощь формализации. Усилиями таких первоклассных математиков, как Фреге, Рассел, Уайтхед, Гильберт, Бернайс, Гёдель и Чёрч, эта формализация в рамках современных логических исчислений достигла высокой степени точности. Поэтому сегодня уже можно говорить о математическом языке

как о части математики и спорить о реализуемости мечты Лейбница.

Символизм современной логики

Логика высказываний исходит из (не анализируемых далее) высказываний, которые соединяются в новые (составные) высказывания с помощью основных связок V, 1, =э,

Логика классов имеет в качестве основных высказываний констатации свойств А(х): вещь х обладает свойством Л. (Совокупность вещей х со свойством Л можно было бы воспринимать как самостоятельную сущность, класс Л, и оперирование с основными связками соответствует тогда так называемым булевым операциям над соответствующими классами.)

В теории отношений добавляется еще один тип исходных высказываний — констатация отношений между вещами А(х, у), В(х, у, г), ... . При этом зачастую переходят к записи по математическому образцу: х^у, х^у, ... .

В исчислении предикатов добавляются еще операции квантификации предложений, т. е. кванторы Зх, \/у. Тем самым символизм пока что завершен.

Мы предполагаем здесь знание этой символики и се смысла. В меньшей степени предполагается знание основных результатов исчисления предикатов.

Говоря о вере в формализацию, которая побудила одухотворенных и способных математиков к чрезвычайным усилиям, мы имеем в виду «Principia Mathematica» Уайтхеда и Рассела (1910—1913), «Forniulaire de mathematique» Пеано (1894—1908), но особенно мы выделяем первые работы этого рода, ставшие образцом, — книги Фреге «Begriffs- schrift» (1879) и «Grundgesetze der Arithmetik» (1893—1903). В «Grundgesetze» Фреге сделал попытку свести всю математику к логике. Кажется, что это возможно, если отождествить свойства с экстенсионалами (т. е. областями истинности) понятий. Фреге представлял себе универсум всех вещей, которому принадлежат также и экстенсионалы понятий. Вместо того чтобы говорить «а есть В» или короче «В (а)», можно мыслить экстенсионал понятия В реализованным в виде вещи b и писать «а находится в Ь» или формально «а е 6». Какие экстенсионалы будут разрешены, зависит

только от того, какой язык формул будет взят. Теперь берется язык исчисления предикатов и не вводится никаких нелогических предикатов, кроме понятия принадлежности «...есть...», т. е. двуместного предиката е. Понятие равенства— определяемое. Равно то, что неотличимо, т. е. принадлежит одним и тем же экстенсионалам понятий. Следовательно, х равен у, если х принадлежит в точности тем же г, которым принадлежит у. Так как символика Фреге (Ве- griffsschrift) довольно громоздка, мы записываем его систему в наших обозначениях (см. ниже). В чрезвычайно интересном письме от июня 1902 г. Рассел указывает Фреге на то, что его система противоречива. Сведение к логике путем отождествления понятия множества с понятием свойства не удалось.

Идеальное исчисление Фреге (в современной записи)

Язык и логика исчисления предикатов без равенства, переменные х, у, г, ..., исходный предикат е.

Определение', х — у =def V2 (х е 2 = У е гУ

Аксиомы:

Экстенсиональность

^Х^у (V2 (2 ^ х е 2 г у) ZD X = у\

Образование классов

Зу ух (х е у Л (х))

для всех формул Л(х) с единственной свободной переменной х.

В силу (i) и (ii) законно обозначение (х|Л(х)}.

Парадокс Рассела

Рассмотрим /?={х|х^х}. Тогда неверно как ReR, так и R ф R.

Противоречие.

Трудности, обнаружившиеся в подходе Фреге, были закваской, на которой стали подниматься современные исследования оснований математики. Первая удовлетворительная аксиоматизация теории множеств исходит от Цермело, который был профессором в Цюрихе. Она вместе с некоторым дополнением (аксиомой подстановки) стала одним из двух наиболее общепринятых логических обоснований матема-

тики; второе из этих обоснований также исходит из Цюриха, от Бернайса.

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

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

Элементарная теория вещественных чисел

R = (R,+, . , — , -1, о» 1>.

Язык и логика:

Исчисление предикатов первого порядка с равенством.

Индивидные переменные: х, у, г, ... ,

Индивидные константы: 0, 1.

Функциональные символы: +, • (двуместные), —, -1 (одноместные).

Примитивный предикат: ^.

Аксиомы:

Аксиомы поля.

Аксиомы порядка:

Х^Х, X^yKy^X.1DX = y, х<_у л у ^ z. zd х ^ г, х ^ у V у ^ х. х<у=эх + г<у + ^ к х^у. id х • z ^у • z.

Аксиома полноты: Для любой формулы А(х) с единственной свободной переменной х

ЗхА (х) Л 3b у^ (А (х) zd х < b). zd

3b [у*(А (х) з х<6)Л Vе (V*(A (х) zd х < с) zd b^c)Y

Аксиомы из групп (i) и (ii) не требуют особых комментариев. Однако по поводу аксиомы полноты стоит кое-что сказать. Во-первых, понятие полноты сыграло когда-то чрез-

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

Предоставленный в наше распоряжение формальный язык нс позволяет говорить о множествах как элементах области индивидов. Поэтому при рассмотрении множеств мы заимствуем у Фреге метод их метатеоретического введения в качестве экстенсионалов предикатов (но не встаем на сомнительный путь превращения экстенсионально описанных совокупностей в индивиды). Вместо множеств мы говорим об определяющих их свойствах, точнее о выразимых в данном языке свойствах индивидов, а именно вещественных чисел. Например, чтобы сказать, что множество вещественных чисел х, обладающих свойством Л(х), непусто, мы пишем просто Эх Л (х); существование верхней грани выражается формулой 3b \j х (Л (х) а х ^ Ь) и т. д.. Это и дает приведенную выше формулировку аксиомы полноты. Вопрос о том, насколько мы отдалились от «полной» теоретико-множественной аксиомы полноты, —- это, по существу, вопрос о том, каков класс множеств, определимых свойствами Л(х). Мы ответим на него в § 4.

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

Для греческой математики понятие числа было самым тесным образом связано с измерением величин. Полезными и наиболее удовлетворительными для философов, особенно пифагорийцев, были рациональные числа. Открытие иррациональности V2 и трудности с квадратурой круга дали толчок собственно математике измеримых величин. Это — одно из наиболее величественных созданий древности, которое выглядит абсолютно современным. Оно находится в V книге Евклида и исходит от Евдокса. Мы излагаем его здесь в современном обличии, в виде утверждения, что архимедова система величин — это линейно упорядоченная абелева полугруппа, удовлетворяющая аксиоме Архимеда.

Архимедовы системы величин

Подразумеваемые структуры;

G = (G, <, +>

Определение:

Для пе{1, 2, 3, ...} положим

« • а = .^а + а + ... + о.

п раз Аксиомы*.

(i) Абелева полугруппа с относительным дополнением:

х + У = У + х, х + (у + 2) = (х + у) + 2,

х + У=Ах Лх#=утэ. 32 (х -|-2 = у) V

уг (х = у + 2).

(И) Аксиомы порядка:

х^х, х ^у л у ^ х.=э х = у,

Х^У ^У^2.^ Х^2, X^yV у^Х,

Х^у=Эх + 2^у + 2.

(Ш) Аксиома Архимеда:

МхМуЗп^х ^.п • у).

Положительные целые числа, положительные рациональные числа, а также положительные вещественные числа, очевидно, составляют архимедовы системы величин. Ограничение положительными числами связано с тем, что в конечном счете подразумевается измерение величин. Мы еще поговорим о «нечистом» виде аксиомы Архимеда. Евдокс и Евклид показали, как порядок и сложение, определенные в архимедовой системе величин, можно естественным образом распространить на (формальные) отношения х: у. После этого они доказали предложение, которое сегодня можно высказать следующим образом.

Любую архимедову систему величин можно вложить в систему положительных вещественных чисел.

(К этому предложению легко присоединить набросок обещанного доказательства категоричности полного упорядоченного поля. Сначала показывают, что любое полное упорядоченное поле также и архимедово упорядочено. Поэтому оно изоморфно подполю поля R, откуда сопоставлением соответствующих сечений получаем изоморфизм в R.)

Вместо вложения Евклид говорит о «сравнимости» архимедовых систем величин. Очевидно, что в античные времена было трудно в концептуальном отношении говорить о том, содержит ли положительная полуось «достаточно» точек или даже все их. Однако идея полноты присутствовала неявно, как показали методы исчерпывания, разработанные прежде всего Архимедом.

1Аъ\ можем только рассуждать о том, почему еще в античные времена не был сделан шаг к вещественным числам. На ум приходят две причины, которые и позже влияли на развитие математики, — одна философская и одна математическая.

Атомистическая тенденция. Происходящая из натурфилософии идея неделимого наименьшего снова и снова проникает в основания анализа. Еще неутомимые Галилей и Кавальери думали, что им придется применить неделимые для обоснования своих квадратур.

Существование неархимедовых систем величин. Наглядные примеры таких систем были известны уже в античности— это системы вещей, которые легко воспринимаются как измеримые или сравнимые, но упорядочены неархимедово. Следовательно, их отношения а: b невозможно вложить в R.

Рогатые углы

Рассмотрим угол, образованный двумя дугами окружностей, расположенных в данной плоскости и пересекающихся в некоторой точке Р.

Рогатый угол — это пара (а, 1/г), где а — обычный угол между касательными t\ и /2, а г — величина радиуса изображенных выше окружностей. Сравнение

величин производится путем «наложения» рогатых углов. Точнее, мы полагаем

(a, k) ^ (р, I) ^ (а < р) V (а = р Л к ^ /),def

(а, й) + (Р, /) = («+ р, к + 1\

Заметим, что /?• (0, 1) < (л/4, 0) для всех п.

Существование систем измеримых величин, которые тем не менее нельзя измерить с помощью вещественных чисел, воспринималось в античности как парадокс. Об этом свидетельствуют дошедшие до нас замечания Зенона Элейского, Протагора, Демокрита и Евдокса. Этим занимались еще Виет и Галилей в XVI в. и Валлис в XVII в. В современной теории меры это игнорируют и всегда берут R в качестве области значений меры. Возможно, исключения имеются в эконометрике, где «полезности», может быть, следует измерять неархимедовым образом? О неархимедово упорядоченных полях мы поговорим в § 4, причем некоторые из них будут даже удовлетворять всем аксиомам элементарной теории вещественных чисел!

Теперь пришло время изложить вторую аксиоматику. Она существенным образом использует понятие вещественной функции вещественного аргумента и может поэтому рассматриваться как аксиоматика элементарного анализа.

Элементарный анализ

Подразумеваемая структура:

A = <R, Rr, + , •, - , -1, 0, 1,

Язык и логика:

Двухсортное исчисление предикатов первой ступени с равенством.

Индивидные переменные: х, у, 2, ... ; функциональные переменные: f, g, ... ; индивидные константы 0,1. Знаки операций над индивидами: +, -, —, ~1. Аппликация (операция применения функции к аргументу); ,., (...). Исходный предикат: ^.

Аксиомы:

Упорядоченное поле.

Экстенсиональность:

Z = g = Vx(f(x) = gf(x)).

(Hi) Аксиома полноты:

V/ [3z/Vx и (х) < z/) zd Эг {\jx и (х) С г) /\Чу($Х (f (х)< у) 2D 2 < у)}].

(iv) Аксиома свертывания:

Vx3!z/A(x, у^З^хА^х, Цх^.

Содержание аксиомы полноты связано в этой теории с понятием функции, а не с определяемыми свойствами вещественных чисел. Эта формулировка вовсе не находится вне всяких подозрений, и ее современное интуитивное содержание— результат долгого и трудного развития. Основываясь на требовании геометрической чистоты, Декарт твердо стоял на том, что законны только алгебраические функции. При нашей аксиоматизации это соответствует следующему ограничению: в (iv) допускаются лишь формулы А(х, у), не содержащие функциональных переменных. Вскоре, однако, выяснилось, что это действительно ограничение: функция sin оказалась одной из первых, чья трансцендентность была доказана. Введение в обиход функций, возникающих при интегрировании, решений дифференциальных уравнений, разложений в ряды и т. п. далеко не всегда обходилось без болезненных дискуссий. Легко убедиться, что существование каждой из таких функций следует из наших аксиом, если разрешается брать в качестве А(х, у) любую формулу полного языка. (Мы не будем здесь говорить об этом подробнее.) В конце концов историческое развитие, т. е. просто давление приложений, вызвало к жизни функции из «природы», «произвольные функции» и современное понятие функции.

Насколько определенно (definit) это понятие? Следующие ниже вопросы проясняют, в чем здесь трудность. Можно, например, спросить: «Можно (нужно) ли добавлять аксиому выбора?»

(v) Аксиома выбора

Vx3yA(x, у) 3fVx А(х> f(x)).

Есть еще несколько принципов, которые можно или нужно добавлять, так как они расширяют теорию интересными теоремами; как обстоит дело с континуум-гипотезой и т. д,? Об этом мы поговорим в § 5.

ЛИТЕРАТУРА

Frege, Russel. Briefwechsel (переписка о противоречии в теории множеств). In: Jean van Heijenoort. From Frege to Godel. A source book in mathematical logic, 1879—1931, p. 124—128. — Cambridge, Mass.: Harvard University Press, 1967.

Bernays P. Betrachtungen uber das Volistandigkeitsaxiom und verwandte Axiome. — Math. Z., B. 63, S. 219-299, 1955.

Euklid. Die Elemente, Ostwalds Klassiker der exakten Wissenschaften, Nr. 235, 1. Teil, 3. Buch, § 16, S. 57—59; Nr. 236, 2. Teil, 5. Buch. S. 17—36. — Leipzig: Akad. Verlagsgesellschaft, 1932. [Имеется перевод: Начала Евклида, т. 1—3. Пер. с греч. М. — Л.: ГИТТЛ, 1948—1950.] Archimedes. The Works of Archimedes with the Method of Archimedes, под ред. T. L. Heath, особенно введение в приложение, р. 5—11, а также р. 12—51. — New York: Dover. [Имеется перевод трудов Архимеда: Архимед. Сочинения. — М.: Физматгиз, 1962.]

Kasner Е. The Recent Theory of the Horn Angle. — Scripta Mathematica, v. 11, p. 263—267, 1945.

Galilei Galilei on Infinites and Infinitesimals. In: D. J. Struik. A Source Book in Mathematics, 1200—1800, p. 198—207. — Cambridge, Mass.: Harvard University Press, 1969.

§ 3» Элементарная теория вещественных чисел

Приведенная в предыдущем параграфе система аксиом является попыткой аксиоматизировать множество законов, справедливых в подразумеваемой структуре. Насколько это удается? Самый большой успех аксиоматизации достигнут, если с ее помощью удается обосновать эффективную разрешающую процедуру, т. е. процедуру, которая для любого предложения S этого языка распознает за конечное число шагов его истинность в подразумеваемой структуре. Кроме того, самыми информативными оказываются те разрешающие процедуры, которые действуют методом элиминации кванторов. Этот метод в то же время и самый старый: его применили в 20-е годы Ленгфорд для теории плотных порядков и Пресбургер для (аддитивной) теории целых чисел, а в 30-е годы — Тарский для рассматриваемой нами теории. Число его применений с тех пор чрезвычайно выросло: обзор имеется в статье [Ершов Ю. Л. и др. 1965].

Элиминация кванторов

Дано:

Теория первого порядка.

Предположение:

Для любой формулы 4 вида ЗхСДДх^ ... кА^х^ где At (х) — атомарная формула или отрицание атомарной формулы, имеется бескванторная формула В, та-

кая, что в данной теории доказуема эквивалентность А^В.

Процедура элиминации:

Пусть дано предложение S.

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

Привести область действия каждого из этих кванторов к дизъюнктивной нормальной форме.

Распределить кванторы существования по дизъюнктивным членам.

Элиминировать их согласно предположению.

Если результат все еще не является бескванторным, то повторить описанные шаги, начиная с (1); в противном случае рассматриваемое выражение обратилось в истину или ложь.

Метод элиминации кванторов сводит логический вопрос о (раз) решении к математическому вопросу о критериях существования решения совершенно определенной задачи. Как же обстоит дело с критерием существования в вещественной алгебре? Не удивительно, что он имеется уже в классической теории, так как в конечном счете постановка вопроса близка к математической. В нашем случае нужно вспомнить следующее утверждение.

Теорема (Штурм, 1829 г.). Пусть р^ — данный многочлен с целыми коэффициентами. Определим последовательность многочленов р\ (х), р2 (х), ..., первый из которых находится дифференцированием, рх{х);= pf {х), а остальные — с помощью алгоритма Евклида;

Р (х) = qx (х) • Рх (х) — р2 (х),Grad (р2) < Grad (р^,

Pi W = q2 U) • р2 (х) — р3 (х),Grad (р3) < Grad (р2),

pr-ito = qr (х) • рДх\

{Здесь Grad(p) обозначает степень многочлена р.)

Для любого а ряд Штурма определяется как последовательность

р (а), рх (а), р2 (а), ... , рг (а).

Пусть теперь а (а)—число перемен знаков в этой последовательности. Тогда формула ю(6) — ©(c) дает при b < с количество (без учета кратностей') корней многочлена р(х) на интервале (6,с),

Для элиминации кванторов удобна следующая формулировка этой теоремы.

Теорема Штурма

Для каждого многочлена р(х,хх, .... хп) с целыми коэффициентами имеется бескванторная формула 5(хь ..., хп, а, Ь), такая, что эквивалентность

а<Ьтз.В^хх, ... , хп, а, Ь)

= Вх (а < х < Ь л р (х, хх, ... , хп) = 0) следует из аксиом элементарной теории вещественных чисел.

Обобщенная теорема Штурма

Для любой бескванторной формулы А(х, хх, ..., хп) имеется бескванторная формула В(хх, ..., хп,а,Ь^, такая, что

а<Ьзэ.В(хх, ... , хп, а, Ь)

= 3х (а < х < b л А(х, хх, ... , хп^ следует из аксиом элементарной теории вещественных чисел.

В алгебре теорема Штурма доказывается обычно с ссылкой на теорему Вейерштрасса о том, что любая непрерывная функция, меняющая знак, обращается в нуль, т. е. с помощью теоремы из анализа. Чисто алгебраический характер теоремы Штурма (и аналогичных результатов) подсказывал, что следует искать и чисто алгебраическое доказательство, выявляющее фундаментальные алгебраические факты, лежащие в основе этой и аналогичных теорем. Эта программа была завершена в известной работе Артина и Шрейера [Artin, Schreier 1927]. Выясняется, что для завершения программы Артина и Шрейера достаточно приводимых ниже следствий (iii)z и (iii)zz аксиомы полноты (iii).

Элементарная теория вещественно замкнутых полей

Язык и логика:

Логика предикатов первого порядка с равенством.

Индивидные переменные: х, у, г. ... ; индивидные константы: 0, 1.

Функциональные символы: +, •, —, -. Исходный предикат: ^.

Аксиомы:

Аксиомы поля.

Аксиомы порядка.

(Ш)' МхЗу (х = у V — х — у2).

(ш)" Для каждого натурального числа п аксиома

Vx0Vx! ... Vx2n3z/(x0 + хху-\-

+ х^у2 + ... 4- Хгпу2п 4- У2П*1 = 0).

Мы покажем вначале, что возможность элиминации кванторов следует из обобщенной теоремы Штурма. Затем мы докажем эту теорему, применяя лишь элементарные сведения из алгебры вещественных чисел (например, теоремы Вейерштрасса и Ролля). Тот факт, что использованные вспомогательные средства применимы в полной общности для вещественно замкнутых полей, следует из программы Артина — Шрейера, которая проведена в § 79 монографии Ван дер Вардена «Алгебра» °.

Вывод элиминации кванторов из обобщенной теоремы Штурма

Пусть А(х, X], ..., хп)—бескванторная формула, и мы хотим элиминировать квантор Зх из ЭхА(х, хр ... , хп). Очевидно, что в любом упорядоченном поле

ЗхА(х, хи ... , хп^ = А (— 1, хи ... , х„) V А(1, хь ... , хп)

V Эх (— 1 < х < 1 Л А (х, X]х„))

V Зх (— 1 < х < 0 л А (х-1, хь ... , х„)) V Зх (0 < х < 1 л А (х-1, хь .х„)).

Но ведь из этой формулы можно элиминировать кванторы согласно только что доказанной теореме.

Доказательство обобщенной теоремы Штурма

Мы излагаем доказательство в редакции, исходящей от П. Коэна: ее можно найти также в книге Крайзеля и Кри- вина 2). Оно существенно использует понятие степени бескванторной формулы. Атомарные формулы нашего языка

можно очевидным образом понимать как равенства и неравенства между рациональными функциями с целыми коэффициентами. Следовательно, в рамках теории полей они эквивалентны равенствам р = 0 и неравенствам q > 0 для многочленов р, q с целыми коэффициентами. Степень Grad бескванторной формулы Д(х)есть по определению max (Grad (р), Grad(p) + 1 |р = 0 или <7 > О входит в Д в качестве атомарной формулы}, где Gradp— степень многочлена р.

Лемма 1. Пусть рхрк, qx, ..., qt— многочлены от х, хх, .... Хщ с целыми коэффициентами. Тогда формула

р1 = 0лр2 = 0А...Лрй = 0л^1>0Л...Л9/>0

эквивалентна бескванторной формуле, степень которой по х меньше степени по х любого из многочленов рь

Доказательство. Пусть h обозначает сумму степеней многочленов pi, qj. Применим индукцию по А.

А = 0. Доказывать нечего.

А > 0. Разбор случаев в зависимости от А.

А = 0. Доказывать нечего.

А = 1. р = 0М1>0л<72>0Л...Л<7/>0.(*)

Единственный интересный случай получается, когда степень одного из qt, например Grad(^i), больше, чем Grad(p). Пусть р = ахт + ..., qx = bxn + ..., а, b ^ 0, m ^ п. Положим Q = a2qx — abxn-m • р. Тогда рассматриваемая конъюнкция (*) эквивалентна конъюнкции

р = 0 Л Q > 0 Л р2 > 0 Л ... Л qt > 0.

Действительно, пусть p = 0Nqx>0. Тогда p=0nQ= = а^х >0 (так как а^О).

Обратно, пусть р = 0 и Q >• 0. Тогда a2qx > 0, следовательно, и q\ > 0.

Кроме того, Grad(Q) < Grad(^i). Таким образом, мы уменьшили сумму А и можем применить предположение индукции.

А > 2. Пусть рх = а1хт‘ ■+ ... , р2 — ^x"12 + ... , аь а2=^0, 1Пх^т2. Положим P = a2pv —axXm'-m2p2. Тогда данная формула эквивалентна формуле

Р = 0 А р2 = 0 Л ... Л Рд = 0 Л qx > 0 Л ... Л qi > 0

(эквивалентность доказывается так же, как и при А—1). При этом сумма А снова уменьшилась, и мы можем применить предположение индукции. □

Лемма 2. Пусть А(х,хх, ..., хп)— бескванторная формула степени А по х. Пусть а,Ь — параметры, отличные от

х, хх, ..., хп и не входящие в А. Тогда имеется бескванторная формула В^х\, .хп>а.Ь^ степень которой по а и b ограничена числом h+ 1 и которая содержит в каждой атомарной формуле не более одного из параметров а, b и такова, что верно

а<Ьтэ . В Ui, ♦.. , хп, а, 6) = Эк (а < л; < 6 л

Л(х, хъ ... , хпУ-

Доказательство. Применяем индукцию по степени h формулы А по х.

h = 0. Формула А(х,хх хпХ вообще не содержит переменную х, и мы можем взять в качестве В саму формулу А.

h > 0. Не умаляя общности, мы можем предположить, что А имеет вид

рх = 0 Ар2 = 0 Л ... л pfe = 0 Л 9, > 0 Л ... Mt>0,

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

Мы проводим разбор случаев в зависимости от к.

& = 0. Тогда А имеет вид

91 > 0 Л 92 > 0 д ... ^ql>0.

Подлежащая преобразованию формула

Зх (а < х < b л 91 > 0 Л q2 > 0 Л ... Л qt > 0)

требует, чтобы многочлены 91qi были строго положительны в некоторой точке, а значит, и в целом подынтервале /а, р)с=(а, 6). Это может происходить по-разному. Либо

G0(a, b) = ^x(a < х < b о . qx> 0 л ... Л qi > 0), либо найдется /, 1 ^ Z ^ Z, такое, что

Gt (a, b) = Зу (а < о < b л qt (у) = 0 Л Go (а, у))

V Зу (а < о < b л qt (у) = 0 л Go (у, 6)),

либо существуют i, j, l^Z, j^l, такие, что

Hij (а, 6) s ЗиЗу (а < ы < у < 6 л 9г (н) = 0 Л 9у (у) = 0л Л Go (и, у)).

Представим это графически.

Элиминация кванторов из Эх (а < х < b л 91 > 0 Л ...

Л 9/ > 0)

Go (а, by. Vx (а < х <Ьто .qx> 0 л ... \qi> 0).

G^a, ЬУ ЗиЛа < и < b Kqi(v) — O fxG^a, иуч Зи (а < и < bAqt(v) = OAGo(u, ЬУ.

III. Нм(а, ЬУ

3v3u (a<u<v <b к qt (и) —0 hq^v) —0 hG0 (м, и)).

Чг

Таким образом, имеет место

Зх (а < х < b л 91 > 0 л ... Л qi > 0) =

Go (а, 6) v Gx (а, 6) V ... v Gt (a, b)v Нхх(а, 6) V ...

V Н Xi (а, 6) V H2V (a, 6) V ... V Ни (а, ЬУ

Итак, мы получили /2 + /+1 дизъюнктивных членов, которые подлежат редукции.

Редукция формулы G^u,b^

G0(a, 6) = Vх(а < х < b дэ . qv > 0л ... Л qi > 0)

= Vx (а < х < b 2D . qx > 0) л

Vx ^а < х < b zd . q2 > 0) л

Vх ^а < х < b 2D . qi > О).

При этом степень каждого из многочленов <71, ..., qi строго меньше, чем h (так как h — Grad (Л)). Далее заметим, что многочлен q, строго положителен в открытом интервале (я, Ь), если, во первых, qi не обращается в 0 в этом

интервале и, во-вторых, сам q, или первая его не обращающаяся в 0 в точке а производная имеет в этой точке положительное значение. Запишем это в виде формулы:

Vx (а < х < b то . qt > 0) =

1 Эх (а < х < b л qt = 0) Л Un (а) > 0) v (qt (а) = 0 Л

q't (а) > 0) V ... v ^qt (а) = 0 Л q't (а) = 0 Л ... Л q^-^ (а) = 0 л^Ч^О)).

Степень по х в этой последней формуле строго меньше чем h для каждого из qt, 1 ^ / ^ /. Следовательно, по предположению индукции можно редуцировать каждую такую формулу, а значит, и их конъюнкцию Со(я,&). В результате редукции мы получаем формулу вида

M~\Bt (хь ... , хп, а, 6) л Kt i = \

е. формулу вида К (а) /\L(b), степень которой по а и b ограничена числом h (в силу предположения индукции).

Редукция формул Gi(a, b), 1 ^ i ^ /:

Gt (а, 6) = Зу (а < у <Ь л qt (у) = 0 л Go (а, у)) V Зу (а < у < b л qt (у) = 0 л Go (у, 6)).

В силу I Go (а, у) = К (а) Л L (и); G0(o, b^ = К (у) л L (Ь).

Таким образом,

Gt (а, 6) = К (а) Л Зу (а < о < b л qt (и) = 0 л L (у)) V Зу (а < у < b л qt (и) = 0 л К (у) Л L (6)).

Согласно сказанному выше, степень формулы Gi(a, b) по и ограничена числом /г. Применение леммы 1 позволяет ограничить степень всех дизъюнктивных членов числом h—1, после чего мы применяем предположение индукции к Gi(a, b) и можем редуцировать Gi(a, b).

Редукция формул Нч{а, Ь), 1^/^/, 1^/^/: Нц (а, 6) s= ЗиЭу (а < и < v < b Л qt (и) = 0 Л

<7,(у) = ОлСо(и, о)).

В силу I имеет место Go (и, у) = К (и) л L (у). Поэтому получаем

Htjia, b)s3u(a<u<b лу^и) = 0 л К (и) ЛЗу (м < и < b Л qj(v) = 0 Л L (у)).

Степень внутреннего экзистенциального высказывания по у ограничена числом h (в силу I); кроме того, Grad(o;)^ ^ h—1. Применяя лемму 1, можно редуцировать степень внутреннего экзистенциального предложения по у до сте-

пени <7/, так что можно применить предположение индукции. Мы получаем

Hijia, к) = Зя (я < и < к л qt (и) = О Л К (я) Л М (и, 6)).

Степень этого экзистенциального высказывания по и ограничена числом к. Применяя лемму 1, можно понизить эту степень до степени q, (которая ^ к—1), так что снова можно применить предположение индукции и редуцировать Нц^а.ЬУ

к=\. А имеет вид

р = 0л<71>0л...Д^>0.

Не умаляя общности, можно считать, что

Grad(p) = к, Grad(<7,) </г, i—\,l "

(в противном случае мы применили бы лемму 1 и уменьшили бы степень р (которая </г), а затем использовали бы предположение индукции). Тогда

Зхка< x<b К р = 0 К qx>0 N ... Nqt>^^ Зх (а < х < 6 Л р = О Л <70 > О Л ... Л <7; > 0) V Зх(а< х < к Л р = 0 Мо = 0 л ... Л <7/ > 0) V Зx(.a<x<k^p = 0^ — qй>0^ ... Л qi > 0), где qo обозначает производную многочлена р.

Мы обозначаем первый дизъюнктивный член через Ах, второй — через А2, а третий — через Аз.

Редукция Ах

Мы снова рассматриваем вспомогательные формулы Go (a, к) = Vx (а < х < к =э . q0 = 0 л ... л qt > 0), G' (а, 6) s Зи (а < и < к л qt (и) = 0 Л р (я) > 0 Л Go (а, я)), G" (а, 6) = Зп (я < у < к л qt (о) = 0 Л — р (о) > 0 Л Go (о, 6)), Hif (а, Ь) = ЗиЗи (а < и < и < b Л qx (и) = 0 Л q; (о) = 0 Л — р (и) > 0 Л р (у) > 0 Л Go (и, у)).

Тогда

Ах = (— р (а) > 0 л р (6) > 0 Л 60 (а, 6)) V (— р (а) > 0 л G' (a, b)) V

(— р (а) > 0 Л G, (а, к)) v

(рф) >0лСИа, b))V

(р(к)>0лО7(а, k))v Н№ {и, k)v ... v Нц (а, к),

(Мы применяем здесь теорему Вейерштрасса и теорему о том, что любая функция с положительной производной монотонно возрастает.)

Как и в случае к = 0, можно показать, что

G0(a, b^K^NL^,

причем степени этой последней формулы по а и b ограничены числом к. Отсюда вытекает, что можно (как и в случае к = 0) редуцировать G', G", НИ. Следовательно, Л1 можно редуцировать к формуле, степени которой по а и b ограничены числом й + 1. (р(а)>0 имеет степень h + 1 по а.)

Редукция Л2

Применяя лемму 1, получаем формулу степени h — 1 (=Grad(9o))> которая редуцируема по предположению индукции.

Редукция Л3

Производится аналогично редукции Ль

к = 2. Этот случай удается свести к случаю к=\, применяя алгоритм Евклида, так как уравнения pi = 0 и рг — 0 имеют общее решение тогда и только тогда, когда их наибольший общий делитель (степень которого не больше, чем У Рь Рг) имеет корень. □

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

Э*13хг... Зхп (р1 = 0 л ... л рк — 0 л qx > 0 л ... Mi > 0)

можно эквивалентным образом превратить в дизъюнкцию полиномиальных равенств и неравенств. Для этого нужно п раз применить описанное выше преобразование. Другой метод элиминации кванторов найден Зайденбергом. Этот метод использует методы алгебраической геометрии и позволяет

непосредственно элиминировать сколько угодно кванторов существования одновременно. Кроме того, при нем не нужно рассматривать неравенства, так как

р > 0 = Зу (р • у2 — 1).

Ясно, что

р, = О Л ... Л р6 = 0 . =+ ... += О,

и Зайденберг должен показать только, что для любого многочлена р от п переменных можно узнать, обращается ли он в нуль на R”,

3^3x2... Зхп (р = ОУ

Теорема Тарского в математической форме

Для любой системы S равенств и неравенств рациональных функций от хх. .... хп с параметрами ах. ... ..., ащ можно эффективно найти конечное число систем Тх. .... Тк полиномиальных равенств и неравенств, в которые входят только параметры ах. ..., am Uto не переменные хь .... Хп). таких, что S имеет решение относительно хь .... хп тогда и только тогда, когда параметры ах. ,.., am удовлетворяют хотя бы одной из систем Ть

Эта теорема подводит окончательный итог вещественной алгебре в том смысле, что предлагает разрешающий метод, который для каждой задачи дает ответ за конечное число шагов. Следует, правда, заметить, что как раз общность этого разрешающего метода наносит ущерб его эффективности, и следует стремиться искать специальные алгоритмы для конкретных классов задач. Общая теорема имеет прекрасные теоретические приложения. Мы упомянем здесь только приложения к дифференциальным уравнениям в частных производных, которые изложены в книге [Friedmann 1963] и восходят к Розенблуму.

Есть ли польза от самого разрешающего метода? Сначала заметим, что имеются чрезвычайно привлекательные и частично еще не решенные задачи так называемой элементарной математики, к которым этот метод в принципе применим. Мы упомянем две из них; одна восходит к Понселе (основателю элементарной геометрии), другая — к Эйлеру.

Проблема Понселе

Даны два конических сечения. Вопрос: имеется ли замкнутая ломаная, описанная около одного из этих сечений и вписанная в другое?

Эту проблему решил сам Понселе. Позднее ею занимались Якоби и Кэли. Есть и новая работа по этому поводу: Griffits Р., Harris И. L’Einseingnement Mathematiques 26 (1978).

Проблема Эйлера

Сколько точек, находящихся друг от друга на расстоянии не меньше г, можно разместить на поверхности шара радиуса г?

Двенадцать или тринадцать?

Эта проблема была решена лишь в нашем столетии Шютте и Ван дер- Варденом с использованием аналитических средств. На этом примере мы можем проиллюстрировать довольно типичное явление. Гипотезу Эйлера очевидным образом можно записать с помощью формулы очень низкой сте* пени. Мы установили, что доказательство путем элиминации кванторов никогда не приводит к формулам более высокой степени. Напротив, более короткое аналитическое доказа-

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

Как обстоит дело с реализацией разрешающего метода на компьютере? Такой проект, если он вообще ставит практические цели, был бы чрезвычайно широким и претендовал бы на многое. В настоящее время реальные перспективы есть только у системы Коллинза [Collins 1975]. Как заметил уже Тарский, центральный вопрос здесь — оценка роста разрешающего алгоритма в зависимости от сложности разрешаемой формулы. К этому имеет отношение следующий результат, приводимый здесь без доказательства.

Теорема Фишера и Рабина

Имеется такая константа d > 0, что, каков бы ни был разрешающий алгоритм для теорем линейной алгебры, не содержащих знаков умножения и обращения, найдется число п0, обладающее следующим свойством: для любого натурального числа п^ п0 имеется теорема длины п, для которой этот алгоритм должен сделать не меньше 2d*n шагов вычисления.

(Вычислительные потребности метода Коллинза составляют d3a» где г — число переменных, пг— число многочленов, п— максимальная степень многочленов, d— максимальная длина целочисленных коэффициентов, а — число атомарных формул в испытуемой теореме. Это даст для теоремы длины п время работы порядка 22^'", где 6^8.)

Мы переходим теперь к формально-логическому аспекту теоремы Тарского. Как уже отмечено, анализ ее доказательства показывает, что используются лишь тс свойства, которые следуют из аксиом вещественно замкнутых полей.

См. также Воробьев Н. Н. (мл.), Григорьев Д. Ю. Нахождение вещественных решений систем алгебраических неравенств в субэкспонен- циальное время. — ДАН СССР, 1985, т. 283, № 6, с. 1294—1299. — Прим, перев.

Теорема Тарского, логическая форма

Теорема элементарной алгебры истинна в поле вещественных чисел тогда и только тогда, когда она верна во всех вещественно замкнутых полях. Истинность, а тем самым и выводимость из аксиом вещественно замкнутых полей разрешима.

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

Пусть М — замкнутое ограниченное выпуклое множество в R” и /— непрерывное отображение множества М в себя; тогда / имеет в М неподвижную точку.

Путем специализации мы сделаем из этого высказывания теорему элементарной алгебры. Пусть М — множество точек х, которые удовлетворяют данной формуле Л (х).

Ограниченность множества М выражается формулой

Эг (г > 0 л Vx (Л (х) =з | х К г).

Его замкнутость выражается формулой

Vx( П Л (х) =з 3w<w > 0 д V2(| х — z | < w =з П ^(z))))-

Его выпуклость выражается формулой

VxVy (Л (х) а Л (у). zd VuVu (O^h^IaO^p^Ia

u-\-v = \ .zd Aku- x + у • у))).

Непрерывность рациональной функции f = p/q на М выражается формулой

Vx (Л (х) =3 q (х)#=0).

Существование неподвижной точки функции f на М выражается формулой

Эх (f (х) = X А А (х))

Тем самым перевод теоремы Брауэра полностью закончен, и, значит, она верна в этом виде во всех вещественно замкнутых полях (хотя ее доказательство использует топологические средства, которых там нет!).

Теорема Брауэра — Тарского

Пусть М — элементарно определимое замкнутое ограниченное и выпуклое подмножество множества F\ где F — вещественно замкнутое поле. Тогда любая непрерывная на М рациональная функция имеет на нем неподвижную точку. -

(Это предложение можно еще обобщить.)

Еще одно следствие из теоремы Тарского — это сформулированная ниже теорема определимости, отвечающая на поставленный в § 2 вопрос об описании класса множеств, определимых свойствами Л (%) в элементарном языке.

Теорема об определимости

В элементарном языке системы R определимы формулами А [х] в точности те подмножества М ^ R, которые состоят из конечного числа открытых {полуоткрытых, замкнутых) интервалов прямой R с алгебраическими концами.

Эта теорема получается из элиминации кванторов, а из нее непосредственно получается, что множество N натуральных чисел не определимо как подмножество множества R с помощью элементарной формулы N{x).

В заключение упомянем еще полученное Робинсоном и Крайзелем приложение к решению 17-й проблемы Гильберта (которая была решена Артином [Artin 1927]).

17-я проблема Гильберта

Пусть / — рациональная функция от п переменных над R, и пусть / > 0 в R". Существуют ли рациональ

ные функции gi (/ = 1, ..., m), такие, что f = X gp

Ответ Артина положителен. Робинсон с помощью формально-логических методов дал более прямое доказатель*

ство, а Крайзель показал, что число функций gt и максимум степеней многочленов, входящих в gi, можно вычислить, зная максимум степеней многочленов, стоящих в числителе и знаменателе f. Вычисление использует разрешающий метод, хотя оценки, найденные при этом для общего случая, нс являются наилучшими.

ЛИТЕРАТУРА

Tarski A. A Decision Method of Elementary Algebra and Geometry. — Ber- . keley: University of California Press, 1951.

Seidenberg A. A New Decision Method for Elementary Algebra. — Ann.

Math., v 60, p. 365—374, 1954.

Ершов Ю. Л., Лавров И. А., Тайманов А. Д., Тайцлин М. А. Элементарные теории. — УМН, 1965, т. 20, № 4, с. 37—108.

Fischer М. J., Rabin М. О. Super-Exponential Complexity of Presburger Arithmetic. — SIAM-AMS Proceedings, v. 7, p. 27—41, 1974.

Collins G. E. Quantifier Elimination for Real Closed Fields by Cylindrical Algebra Decomposition. — Springer Lecture Notes in Computer Science, v. 33, p. 134—183, 1975.

Hilbert D. Mathematische Probleme (в особенности 17-я): Darstellung definiter Formen durch Quadrate, Ostwalds Klassiker der exakten Wissen- schaften, B. 252, в частности S. 63—64. — Leipzig: Akad. Verlagsgesell- schaft, 1933. [Имеется перевод: Проблемы Гильберта. — М.: Наука, 1969.]'

Artin Е., Schreier О. Algebraische Konstruktion reeller Korper. — Abhand- lungen aus dem mathematischen Seminar der Universitat Hamburg, B. 5, S. 85—99, 1927.

Artin E. Ueber die Zerlegung definiter Funktionen in Quadrate.—Abhand- lungen aus dem mathematischen Seminar der Universitat Hamburg, B. 5, S. 100—115, 1927.

Friedmann A. Generalized Functions and Partial Differential Equations, особенно p. 218—225. — Englewood Cliffs; Prentice-Hall, 1963.

Нестандартный анализ

В первые полтораста лет существования дифференциального и интегрального исчисления его называли анализом бесконечно малых, так что, например, оказывавший большое влияние учебник Эйлера назывался «Introdictio in Analysis Infinitorum» (Лозанна, 1748). Таким образом, бесконечно малые величины, которые уже встречались нам в качестве «атомов прямой» при интегрировании по Кавальери, все еще играют большую роль. Еще предшественники Ньютона и Лейбница нашли новые приложения исчезающе малых величин в задачах о нахождении касательных и определении максимумов и минимумов. Затем Лейбниц ввел эти величины в систему в виде дифференциалов. Он хотел понимать дифференциалы как законные элементы области определения и области значений рассматриваемых функций. Однако ни он, ни его последователи не построили основы для их математической конкретизации. Поэтому бурное развитие анализа

вплоть до момента прояснения его основ несло в себе нечто сомнительно временное. Это привело к известным нападкам остроумного и широко образованного епископа Беркли, который упрекал страдавших интеллектуальной агрессивностью представителей естественных наук в том, что и у них самих есть темные допущения. Дифференциалы он очень метко называл «духами покойных величин» (ghosts of departed quantities).

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

Подходы к узаконению бесконечно малых обнаружились снова только в XX столетии, когда были открыты неархимедовы упорядоченные поля. Однако чистое, элементарное решение проблемы введения бесконечно малых в качестве элементов основной области анализа было найдено лишь в 1960 г. А. Робинсоном.

Является ли система аксиом для элементарной теории вещественных чисел категоричной, т. е. имеется ли у нее модель, отличная от подразумеваемой структуры R? Наличие такой модели следует из общих теорем о логике предикатов первого порядка, в частности из известной теоремы Левен- гейма— Скулема — Мальцева — Тарского. Ниже мы докажем сам этот факт непосредственно. Очевидно что, ограничив понятие непрерывности элементарно определимыми множествами, мы, с одной стороны, сделали саму теорию полной и разрешимой, но, с другой, — так сказать, потеряли из вида подразумеваемую структуру. В этом параграфе мы превратим этот «недостаток» в достоинство, найдя применение существованию неподразумеваемых моделей вещественных чисел. Они, однако, отличаются от R не своими элементарно формулируемыми свойствами, а, вообще говоря, свойствами, скажем, топологической природы. Метод так называемого «нестандартного анализа» состоит в удачном использовании этого факта.

Мы начнем с конструкции моделей данной теории структуры R. При этом данная «конструкция» несет в себе нечто отчетливо неконструктивное, но это вообще обычно для современной математики. В частности, мы будем существенно использовать следующую неконструктивную теорему суще^ ствования.

Лемма Цорна

Пусть Р— частично упорядоченное множество, в котором каждое непустое линейно упорядоченное подмножество имеет верхнюю грань. Тогда Р имеет максимальный элемент.

Известно, что лемма Цорна эквивалентна принципу выбора в теории множеств, о котором мы еще будем говорить. Хорошо известная вспомогательная конструкция в алгебре — построение прямой степени данной алгебраической структуры, например группы; прямая степень группы снова является группой. Однако прямая степень некоторой структуры может иметь совершенно новые свойства. Это проявляется и в следующем примере.

Пример прямой степени

Исходная структура А; Множество, состоящее из двух элементов а, Ь, упорядоченных согласно предписанию а ^ 6, а#=Ь.

Прямая степень Л2: Множество всех пар (х, у), где х, у равны а или Ь, упорядоченное согласно предписанию

(х, у) ^ (u, у) — . х^и ^y^;u.

А2 не является линейно упорядоченным, хотя А было таким.

(а, 6)(6, а)

(а, а)

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

Фильтр и ультрафильтр

Пусть /^ 0 и D — непустое семейство подмножеств множества /. Оно называется фильтром на /, если

0 ^D;

E^DnF ^D .zd E^F ^D;

E D n E F <= 1. zd F D.

D называется ультрафильтром на /, если в дополнение к (а) — (с) имеет место

E^l .^E^D^y-E^D.

В качестве примера фильтра мы упомянем так называемый фильтр Фреше. Он состоит из всех множеств натуральных чисел, имеющих конечное дополнение. Очевидно, что это семейство подмножеств множества N является фильтром. Однако оно не является ультрафильтром: ему не принадлежат ни множество четных чисел, ни множество нечетных чисел. Тем не менее фильтр Фреше можно (неконструктивным образом) расширить до ультрафильтра. Это вытекает из следующего общего утверждения.

Теорема Тарского. Любой фильтр D^ на множестве / можно расширить до ультрафильтра на 1.

Доказательство. Пусть F— множество всех фильтров D' на /, являющихся расширениями Z)o, т. е. таких, что D' з Do. Множество F непусто и частично упорядочено отношением включения с. Любое линейно упорядоченное множество М фильтров из F имеет верхнюю грань в F — объединение семейства М. Таким образом, условия леммы Цорна выполнены, и в F имеется максимальный элемент, который мы обозначим через D. Мы утверждаем, что D — ультрафильтр. Допустим противное: имеется E^D, гакое, что (/ — E)^D. Тогда мы строим множество D' всех множеств X ^ /, таких, что E\JX^D. Оказывается, что D'— фильтр. Действительно,

0 ф D\ так как E^0=E^D\

из EUXeD и EUYeD следует Е U (X П Y) = (£U X) П (EUY^D;-

из Е U X е D и Y ^Х следует E\J X E\}Y D.

По построению D' 3 D, так как из U ^ D следует U е E\JU е D, а тем самым и U^D'. Ввиду максимальности D имеем D = D\ но это невозможно, ибо (I — E)^D, но (I-E^D't так как EUU - Е) = 1 гО. □

Итак, пусть D — ультрафильтр, являющийся расширением фильтра Фреше на N. Мы зафиксируем его и переходим теперь к обещанной конструкции ультрастепеней. С интуитивной точки зрения ультрастепень множества R состоит из последовательностей вещественных чисел, причем две последовательности отождествляются, если они совпадают «почти везде». Определение понятия «почти везде» берется из фильтра D: последовательности. {«J/gn и Vb^ieN считаются «равными», если {/ е N | ai = bi}^ D. На определенных таким образом классах эквивалентности естественным образом вводятся ^, + и т. д. Подробности находятся в следующей рамке.

Ультрастепень структуры R

R = <R,-1, 0, 1>.

N = {О, 1, 2, ... },/>-—ультрафильтр на N, содержащий все дополнения конечных множеств.

R^ — (RN/p, ^d> + d, *d^ -t~d> ^ 0D, lp^ определяется соотношениями -

И/sNp = {M NI 0" s N [а; = ЬД e D},

RN/D = VHt^D\a^R- 1г^У

№ s ^D < D {b,}, JD^V^a^b^ D;

№ s JD + D {bi}, s JD = {a{ + b^^D и т. д.;

0D = {0, 0, 0, ...}/£>; 1D = {1, 1, 1, ...}!D.

Нужно еще проверить корректность этого определения, особенно для' операций +о и т. д. на классах эквивалентности. Во-первых, конструкция ^a^.^JD действительно образует классы эквивалентности: VaAi^JD = VbAiGNID имеет место тогда и только тогда, когда {Z е N | ai = bi}^ D. Транзитивность следует из соотношения

{1 е N | at = 6J П V^ N | bt = с^ г V е N | at == с^,

а симметричность и рефлексивность тривиальны. Определение отношения ^р корректно, так как из Vci^^^D = -{<}i^D, {bt}i^D = {b't?}lGjD и {a^^D^^b^^D следует {,a'i}ieJD<.D}b,l’}iGJD. Действительно, положим

Е = {Z ^ N | а. = а'^ F = {Z е N | Ь. = 6'}, q = {Z е N | а. < 6 J. По предположению все эти множества принадлежат D. Отсюда следует, что {Z е N | а^ ^ Ь'.} з Е П F Q G также при* натлежат D. Точно таким же образом обосновывается кор* ректность определений +D, -D и т. д.

Секрет успеха этой конструкции — в следующей теореме* которая справедлива для любой конструкции ультрастепени.

Теорема Скулема — Лося

Пусть А (хь ... , хп) — формула элементарного языка системы R со свободными переменными хх, ... , хп. Тогда для любого означивания этих переменных элемен- тами \a^t s JD, / = 1, ... , п, формула А ({«Ц, s JD, ..., ^a^i G N/B) справедлива в R^ тогда и только тогда, когда

{Z е N | Л (а|, а?, ... , а^ верно в Rj е О.

В частности, в R и R^ справедливы одни и те же элементарные теоремы.

Доказательство проводится, как обычно в таких случаях, методом индукции по логическому построению формулы Л(Х1, ..., хп).

Мы применяем сокращенное обозначение х для xv, ... , хп, at —для а\, ..., а" и а —для V°Ai®JD-

Если Л(х)—атомарная формула, то доказываемое утверждение верно в силу определения ультрастепени RN.

Пусть Л(х) имеет вид В(х)дС(х). Если А (а) верно в R^, то там верны также В (а) и С (а), а потому в силу предположения индукции множества В, = {/ е N | В (а^ верно в R) и Е2 = {z'е N |С (а^ верно в R) являются элементами множества D. Но тогда и множество Ех П Е2 = Е = = {z е N | В (at) л С (az) верно в R) является элементом D. Докажем обратную импликацию. Пусть EeD. Тогда в силу BsEiSN, ВеВгЕМ множества Вь В2 тоже принадлежат D. В силу предположения индукции в R^ верны В (а) ц С (а), а значит и их конъюнкция.

Пусть Д(х) имеет вид П5(х). Формула Л (а) верна в R^ тогда и только тогда, когда В^а) там неверна. По предположению индукции это имеет место тогда и только тогда, когда множество {Z^N|B(at) верно в R}=£ не принадлежит D. Так как D является ультрафильтром, множество N—Е принадлежит D как раз в этом случае. Но это множество можно представить и в виде N — Е = {Zg N| ~1В(а,)} верно в R}.

Пусть, наконец, Д(х) имеет вид ЗуВ(у, xY Пусть А (а) верно в Rd- Тогда в Rd имеется такой элемент b (который мы запишем в виде b = Vbi\isJDY что В (6, а) верно в R^. Отсюда по предположению индукции следует, что {Z е eN \B^bh aj верно в R}gD. Если теперь заметить, что {ZeN|B(6b а^ верно в R} ^ {Z е N | ЗуВ ^у, а^ верно в R}, то ясно, что и это последнее множество принадлежит D.

Докажем обратную импликацию. Пусть (Z е N | ЗуВ (у, а^ верно в К}еВ. Выберем последовательность {biYeN эле* ментов множества R таким образом, чтобы при каждом i^N формула В(Ьь а^ была верна в R, если для at вообще существует такой элемент bt; если же ”] В(6, а^ для любого 6, то выбираем bt произвольным образом. Для любой такой последовательности очевидным образом {Z е N \Вфь ^ верно в R} г {Z е N | ЗуВ (у. а^ верно в R}, и потому большее множество также принадлежит D. Отсюда следует, что В ({Ь^.^О, а) верни в Rd, а тем самым там верно и ЗуВ (у, а).

Итак, мы рассмотрели по существу все логические связки, так как В id С можно заменить на HBvC, ВмС —• на П(15л"]С) и VxB(x) —на 1 3* ПВ(х). □

Отметим еще, что структура R вложена в свою ультрастепень Rd особенно наглядным образом. Действительно, мы можем каждому а е R поставить в соответствие d = VaiYeN,^’ где ai = a для всех ZeN. Так определенное отображение множества R в Rd очевидным образом является мономорфизмом, и, кроме того, формула Л(аь ..., а^ верна в R тогда и только тогда, когда A (db ..., а^) верна в Rd- Поэтому отображение а*~^а структуры R в R^ называется элементарным вложением. Элементы структуры R, т. е. «обычные» вещественные числа содержатся в модели Rd; мы называем их стандартными элементами R^. Все остальные элементы называются нестандартными.

Бесконечно малый элемент структуры Rd:

{1, 1/2, 1/3, 1/4, 1/5, ...}/2) = е,

е < (1/п) для всех п. Действительно,

{/ е N I1// < \]п\ е D для каждого фиксированного п.

п • е < 1 для всех п. Действительно, {ZeN|n//< l}eZ) для каждого фиксированного п.

Бесконечно большой элемент структуры Rd:

{1, 2, 3, 4, ...}//) = со, со > /г для всех п е N.

Начиная с этого места мы применяем сокращение *R для обозначения ультрастепени Rd и *R — для обозначения множества Rd ее элементов. Кроме того, мы будем опускать нижний индекс D в обозначениях Ор, Ip, ^d, +d и т. д.

Пусть с ь—> с — элементарное вложение R в *R.

е *R называется бесконечно малым элементом, если а ^ 0 и | а | < с для всех с е R, с > 0;

ge*R называется бесконечно большим, если |д|>с для всех се R, с > 0;

cze*R называется конечным, если |а|< с для некоторого с е R, с > 0.

При этом |а| определяется соотношением ( а, если а ^ 0,

I а | = i( — а в противном случае.

Для любого конечного cz^*R мы определим его стандартную часть ° а как тот xeR, для которого разность х— а бесконечно мала или равна 0.

Чтобы обосновать последнее определение, нужно доказать существование и единственность °а.

Единственность. Пусть х, у е R, х#= у, причем х — а и у— а бесконечно малы. Но тогда и разность (х—а)— (у — а^ = = х — у = х-—у бесконечно мала, хотя х— y^R и |л — у\ > 0. Мы получили противоречие.

Существование. Если а=х для некоторого xeR, то все уже в порядке. В противном случае мы следующим образом

находим °а в виде дедекиндова сечения. Пусть Л, G определены соотношениями К = {х ^ R |х < а^, G = {х е R, х > о}. Тогда пара (Л, G) является дедекиндовым сечением и однозначно определяет некоторое вещественное число ^eR. Мы утверждаем, что Б — а бесконечно мало. Действительно, b является либо наибольшим элементом множества К, либо наименьшим элементом множества G. В первом случае имеем Б < а. Если бы разность Б — а не была бесконечно мала, то существовало бы число ^eR, такое, что е>0 и 15 — а\ = а — Б ^ ё, откуда Б+ё^а и тем самым Б-\-ё/2*<а. Поэтому число Б + ^/2 принадлежало бы множеству К вопреки предположению о том, что Ь — наибольший элемент множества К. В случае, когда Ь — наименьший элемент множества G, рассуждаем точно таким же образом.

Теперь мы переходим к обоснованию некоторой скромной части математического анализа с помощью введенных выше понятий. При этом иногда будет проводиться сравнение с параллельным построением в школьном курсе математики.

Предел, непрерывность и отношение дифференциалов

*Предел

Пусть /, а е R и f— функция *R->*R. Полагаем

lim f (х) = Z, если °f(a — y) = l для всех бесконечно х->а”

малых у > 0;

lim f^^L если °f (а + у) = I для всех бесконечно

малых у > 0;

lim / (х) = /, если °f (я + у) = I для всех бесконечно х~>у

малых у.

* Непрерывность

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

f Непрерывна в точке а, если °f (а + y) = °f (а) для всех бесконечно малых у.

*Производная

Пусть a, b е R и функция f определена на некотором открытом интервале, содержащем а.

Положим Г (а) = 6, если (ll^L+JL^ = у для всех бесконечно малых у.

В определении производной мы могли бы вслед за Лейбницем ввести бесконечно малые элементы как дифференциалы

dx вместо у,

df вместо f (а + dx) — f (а).

Тогда производная f4a) представится как отношение дифференциалов

Пример.

f(x) = x2, rw = ?

df = (х + dx)2 — х2 = 2х dx + (dx)2,

Применяя любой из двух намеченных способов, вы можете развить элементарное дифференциальное исчисление чрезвычайно изящным способом. Это относится не только к преобразованиям выражений. Доказательства основных теорем дифференциального исчисления, например теоремы Ролля, становятся в высшей степени наглядными. Поэтому можно с полной серьезностью ставить вопрос о том, не следует ли строить таким образом курс дифференциального и интегрального исчисления, т. е. не надо ли положить в основу структуру *R вместо R. Разумеется, при этом не надо воспроизводить построение *R описанным выше способом. Следует рассматривать *R как данное и квазиаксиоматически использовать несколько существенных свойств *R, как в конце концов делают и для R. Такая попытка сделана в книге [Keisler 1976].

Однако мы отложим такого рода педагогические вопросы в сторону и обратимся к еще не до конца решенному математическому вопросу: как связаны понятия «*предел», «*не- прерывность» и «*производная» с обычными понятиями?

В наше определение *предела и т. д. входит понятие функции. Сначала мы будем связывать с ним представление об определимой функции, а точнее — об определимости отношения f(x) = y формулой Л(х, у) элементарного языка, для которой в R имеет место утверждение

\jx3yA (х, у) л VxVytуу2 И (х, yj л А (х, у^. тзух = у^.

Тогда эта формула верна и в *IR, поэтому А(х, у) определяет и в расширенной структуре некоторую функцию, ко-

торую мы для простоты также будем обозначать через f. В этом смысле и следует понимать функции из определения *предела и т. д.

{Несколько дальше позволяет продвинуться следующая точка зрения. Вместо того чтобы исходить из структуры R, мы образуем ультрастепень структуры А элементарного анализа (см. § 2). Тогда для каждой функции f из А имеется расширенная функция f из *А, обладающая в точности теми же самыми свойствами, формулируемыми в языке системы А. Соответствующим образом можно было бы включить в эту конструкцию объекты еще более высоких типов, например функционалы; мы отсылаем читателя к обширной и активно растущей литературе по нестандартному анализу, например к статье [Robinson 1961] или книге [Davis 1977].}

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

Лемма 1. *lim f^ = l т. и т. т., когда limf(x) = Z, х->а~

Доказательство. (а) Пусть lim f(x) = t. Тогда, согласно х-^а-

обычному определению, для всякого ее R. е > 0, имеется бе R, б > 0, такое, что для всех у имеет место 0 < у < б лэ лэ | f (а — у') — 11 < е. Выберем е > 0, е е R, и найдем для него б > 0. Высказывание Vy (0 < у < блэ | f (а — у) — I1 < е верно в R, элементарно, а потому верно и в *R: Vy(0<y<6o If (а—у) — Z | < ё). Пусть теперь у бесконечно мало, 0 < у. Тогда в *R верно 0 < у < б, а потому и | f (а — у) — I1 < 5. Так как это рассуждение проведено для любого положительного е из R, то величина | f (а — у) — /1 бесконечно мала по определению. Поэтому °f (а — у) = /, а значит *lim f (x^L х->а~

(Ь) Для доказательства обратной импликации допустим, что °Цй— у) — 1 верно для всех бесконечно малых у > 0. Выберем бесконечно малый элемент 6 > 0. Тогда для любого е > 0, 8eR, и всех у, 0 < у < 6, верно \f(a—у)—7| <е, так как любой такой элемент у сам бесконечно мал. Это означает, что для любого ее R, е > 0, в *R верно высказывание Уу(0 < у < 6 =э |/(а — у)— Z | < е), а значит, и 3S > 0 >/У (0 < у < 6 =)| f(a — у) — I1 < е). Будучи элементарными утверждениями, они верны и в самом R: 36 > OVz/(O < у < 6

zd If (a — у) — /1 < e). Так как e > 0 в R было выбрано произвольно, мы проверили, что lim f (х) = /.

х->а~

Лемма 2. / Непрерывна в точке а тогда и только тогда, когда она непрерывна в точке а. □

Лемма 3. f имеет Производную b в точке а тогда и только тогда, когда ^а^ = Ь в обычном смысле. □

Доказательства этих лемм получаются непосредственным применением леммы 1.

ЛИТЕРАТУРА

Leibniz G. W. New Method for Maxima and Minima as well as Tangents which is neither by Fractional nor by Irrational Quantities, and a Remarkable Type of Calculus for this, 1646—1716. Английский перевод в кн: D. J. Struik: A Source Book in Mathematics, 1200—1800, S. 272— 280. — Cambridge, Mass.: Harvard University Press, 1969. [См. также: Лейбниц Г. Избранные отрывки из математических сочинений. — УМН 1948, т. 3, вып. 1(23), с. 165—204.]

Euler Р. Institutiones calculi differentials Opera Omnia, Ser. 1, Vol. X, S. 69—72. — St. Petersburg, 1755. Частичный английский перевод в кн.: D. J. Struik: A Source Book in Mathematics, 1200— 1800, p. 384—386.— Cambridge, Mass.: Harvard University Press, 1969. [См. также: Эйлер Л. Введение в анализ бесконечных. Т. 1, 2.— М.: Физматгиз, 1961.]

Berkeley G. The Analyst, or a Discourse Addressed to an Infidel Mathematician.— London, 1734. Отрывки в кн.: D. J. Struik: A Source Book in Mathematics, 1200—1800, p. 333—338. — Cambridge, Mass.: Harvard University Press, 1969.

Skolem Th. Ueber die Nicht-charakterisierbarkeit der Zahlenreihe mittels end- lich oder abzahlbarer unendlich vieler Aussagen mil ausschliefilich Zahlen- variablen. — Fund Math., v. 23, p. 150—161, 1934.

Los J. Quelques Remarques, Theoremes sur les Classes Definissables d’Al- gebres. In: Mathematical Interpretation of Formal Systems, p. 98—113.— Amsterdam: North-Holland, 1954.

Robinson A. Non Standard Analysis. — Koninklijke Nederlandse Akademie van Wetenschappen Proceedings, Series A, B. 64, S 432—440. 1961

Heisler H. J. Elementary Calculus. — Boston: Prindle, Weber & Schmidt Inc., 1976.

Davis M. Applied Nonstandard Analysis. — New York, 1977. [Имеется перевод: Девис M. Прикладной нестандартный анализ.—М.: Мир, 1980.]

§ 5. Аксиома выбора и континуум-гипотеза

Что такое вещественные числа? Теперь мы несколько лучше понимаем этот вопрос, поставленный в § 1. Очевидно, речь идет о разработке общей основы для математической деятельности, в особенности для доказательства теорем анализа. Опыт показывает, что эта деятельность имеет два противоположных аспекта. С одной стороны, то, что работающий математик (благоразумно избегая вдаваться в детали психологии) назвал бы «усмотрением» или «мышлением в содержательных понятиях», с другой, — математический фор-.

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

Очерчивание формальных границ, встретившееся нам в § 3, означает отступление в область возможных математических высказываний, которое, правда, позволяет нам считать все соответствующие вопросы решенными. До какой степени наше «усмотрение» поддерживает это отступление? Какова цена завоеванной таким образом однозначности? Очевидно, что она включает уменьшение выразительной силы формализма: понятие предела и отношение дифференциалов приходился, как уже отмечено, истолковывать как схемы, которые приходится вводить отдельно для каждой функции / (и допускаются только определимые функции). Это — больше, чем просто условность, связанная с формализмом; формализация неспособна охватить некоторые вещи, которые не только законны, но, по существу, необходимы. Число л трансцендентно и потому не определимо формулой Л(х), так как каждое число, определимое такой формулой, — алгебраическое. Не определима и функция «синус», так как любая определимая функция состоит из конечного числа кусков, являющихся алгебраическими функциями, а потому имеет лишь конечное число корней или тождественно равна 0. Множество натуральных чисел не определимо формулой А^ по той же причине.

Эта недостаточнсть выразительной силы соответствует той свободе, с которой математики представляют себе модели теории. Совершенно законно думать о R (что все мы кое-как и делаем), но можно и об *R (что могли бы делать классики анализа); формально описываемые математические результаты остаются теми же самыми, они лишь немного тощают.

Поэтому мы уже в § 2 предложили выйти за формальные рамки, сначала путем добавления функций в качестве новых сущностей. Что выразимо в расширенных рамках? Совпадает ли то, что выражено, с тем, что подразумевается, или снова есть нестандартные модели? Решает ли формализация все выразимые в расширенном языке вопросы, а если нет, то имеются ли интересные неразрешимые проблемы? С чего следует начать в данном случае?

Натуральные числа

N (.у) — сокращение для следующей формулы:

Vf [f (0) = 0 л Ух (0 < X к f (х) = о.=)

|(х+1) = 0).^/(^) = 0].

Аксиомы Пеано

(0 N^Y

N(x)^N(x + 1).

N (x) A N (у) л x + 1 = у + 1. zd x = y.

N (x) zd 0 ^ x + 1 •

Vx (Л (x) zd N (x)) л Л (0) л Vx (Л (x) zd Л (x + 1)). zd Vy (TV (у) лэ Л (y)).

Аксиомы Пеано выводимы в элементарном анализе. Это очевидно для (i), (ii) и (iii). Чтобы доказать (iv), заметим, что х < 0 лэ.ДУУ (х), так как функция

J 0 для х^О,'(x) = t 1 для х<0определима, удовлетворяет посылкам определения А (у), ноимеет значение f (х)=/= 0 для х < 0.

Доказательство аксиомы индукции (v). Пусть Л(х)— формула элементарного анализа, и пусть функция /д определена следующим образом:

J 0, если Л (х),^а(х)| 1, если -] Д

Существование этой функции следует из аксиом элементарного анализа. Допустим посылку импликации (v):

Vx (Л (х) ZD N (х)) А Л (0) A Vx (Л (х) лэ Л (х + 1))-

Заметим, что ^(0) = 0> так как допущено Л(0), и что

Vx (0 < X A fA (х) = 0. ZD fA (х + 1) = 0),

так как Vx (Л (х) zd Л (х + 1)).

Следовательно, в силу определения формулы N(y) должно иметь место ^y(N (у)=э /л(у) = 0), а значит, и Vy(A^(y)zo лэ Л (у)).

Многоместные функции

Мы расширяем язык, присоединяя фиксированный двухместный функциональный символ р вместе со следующим постулатом.

Аксиома спаривания:

[АГ (х) л N (у). зз N (р (х, z/))] Л

УМххМухМх^у^р^хХ1 yx)=pU2, У^=- Х!=х2л ух = у^.

Это дает возможность вводить многоместные функции, например, f(xi,x2, *з) вместо f (p(%i, р(х2, *з))) и т. д.

Теорема свертывания:

Мхх ... х„Э! уА (х,х„,у) о Э/Vxi ... хпА (х1хп,

Цхх, .... х„)).

Схема рекурсии;

4g4h {VX! ... х„+! [АГ (xj л ... л (х„+1).

^•^(g'Uiх„))л Nkh<xx, ..., х„+1))]

—* 3^хх ... хп+1 [АГ (х,) л ... Л N (х„+1).

=>fUiхп, 0) = g(Xb .... х„)

A f (хь ...» хп, хпц.х 4~ 1) ^ h (хп ..., хп1

fUl>Х„ + 1))].

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

Из полученных до сих пор теорем об элементарном анализе эрудированный логик легко получит, что данная аксиоматизация, если она вообще непротиворечива, нс является полной и не может быть пополнена эффективным образом. (Согласно Гёделю, это явление наблюдается уже в случае теории чисел.) В теории чисел естественные вопросы, не решаемые данными аксиомами, были найдены лишь в последние годы; в элементарном анализе это оказались гораздо менее скрытые, даже центральные ' вопросы — аксиома выбора и континуум-гипотеза.

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

Парадокс Банаха — Тарского

В усиленной форме, которую ему придал Робинсон, он звучит так.

Трехмерный шар 3 можно так разбить на шесть не- пересекающихся подмножеств

S-^UAIMIM U {0} U Ф}>

что из пары множеств

Л и 43 U {0}

можно с помощью вращения составить целый шар 3, и из трех множеств

Л2, Л4 И {Р}

снова можно с помощью вращения и переносов составить 3. Таким образом, из одного шара можно с помощью подходящих разрезаний и преобразований конгруэнтности сделать два шара первоначальной величины!

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

На вопросе о мощности континуума сломал зубы уже создатель теории множеств Кантор. Это — типичная ситуация, в которую попадают первооткрыватели: у них нет ощущения, какие проблемы трудны, а какие тривиальны. Гипотеза Кантора заключалась в том, что континуум имеет наименьшую несчетно бесконечную мощность. Положение континуум-гипотезы относительно современных аксиоматизаций теории множеств такое же, как у аксиомы выбора: это непротиворечивая (Гёдель) и независимая (Коэн) аксиома. Однако до сих пор найдено мало оснований для включения в рамки математики самой континуум-гипотезы или ее отрицания. Поэтому, в отличие от аксиомы выбора, каждое применение континуум-гипотезы в доказательстве какой-либо теоремы приходится выделять явно.

Для структуры А элементарного анализа можно записать континуум-гипотезу в особенно простом виде. Она просто выражает, что любое подмножество X множества R либо имеет мощность ^^о (т. с. имеется функция /, отображающая N на X), либо имеет мощность ^ мощности R (т. е. имеется функция g, отображающая X на R). Если мы понимаем X как множество тех xeR, для которых й(х) = 0, то она приобретает следующий вид.

Континуум-гипотеза

VA[3fVy(A(y) = O2

з 3x(N (x) Ai/ = f(x)))

v 3g^y3x mx) = o/\y = g (x))].

Так как теперь аксиому выбора и континуум-гипотезу можно сформулировать также и для элементарного анализа, то мы еще сформулируем в заключение следующие теоремы Гёделя и Коэна.

Теорема Гёделя о непротиворечивости

Любое формальное доказательство противоречия, которое получилось бы в результате присоединения аксиомы выбора и континуум-гипотезы к аксиомам элементарного анализа, можно эффективно преобразовать в доказательство противоречия из обычных аксиом.

Теорема Коэна о независимости

Любое формальное доказательство противоречия из аксиом элементарного анализа плюс аксиома выбора и отрицание континуум-гипотезы можно эффективно преобразовать в доказательство противоречия из исходных аксиом.

ЛИТЕРАТУРА

Hausdorff F. Grundziige der Mengenlehre, p. 399—403, 469—473, 1914.— New York. Chelsea (reprint 1949).

Robinson R. M. On the Decomposition of Spheres. — Fund. Math., v. 34, p. 246—260, 1947.

Godel К. What is Cantor’s Continuum Problem? In: P. 'Benacerraf and H. Putham. Philosophy of Mathematics, p. 258—273. — Englewood Cliffs: Prentice-Hall, 1964.

Godel K. Consistency Proof for the Generalized Continuum-Hypothesis. — Proc. Nat. Acad. Sci. USA, v. 25, p. 220—224, 1939.

Cohen P. The Independence of the Continuum Hypothesis I. II. — Proc. Nat. Acad. Sci. USA, v. 50, p. 1143—1148, 1963; v. 51, p. 105—110, 1964. [Имеется перевод: Коэн П. Теория множеств и континуум-гипотеза. — М.: Мир, 1969.]

Scott D. A Proof of the Independence of the Continuum Hypothesis, — Math. System Theory, v. 1, p. 89—111, 1967.

Глава II

ГЕОМЕТРИЯ

Пространство и математика

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

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

Чтобы служить целям измерения, евклидова геометрия должна представить в своей системе расстояний универсальную систему измерения величин (само собой разумеется, архимедовых величин!), т. е. вещественные числа. В этом свете проблема оснований геометрии рассматривалась различными геометрами, и поэтому она вполне сравнима с рассмотренной в гл. I проблемой оснований элементарной алгебры и анализа. В последующих разделах мы собираемся провестц

программу аксиоматизации, возникающую в результате такого подхода, и сопоставить результат с выработанным в гл. 1 критическим подходом и опытом, касающимся взаимозависимости между выразительностью языка и неполнотой систем аксиом, избегая, однако, той беспомощности, которая проявляется, например, в определении Евклида: «Точка — это то, что не имеет частей».

Здесь, однако, самое место остановиться на сомнительности намеченной выше программы по самой своей сути. Существует ли мыслительная необходимость постулировать для физического события независимый от него и присущий ему геометрический субстрат, т. е. является ли так называемое «пространство» физически необходимой гипотезой? И не следует ли, наоборот, как-то слить измерение с физикой, возможно, таким образом, что его вообще уже нельзя будет выделить обратно как отдельное подпонятие чисто «геометрического» характера? Современная физика рекомендует нам именно такой подход. Даже если целесообразность геометрического субстрата выдвигается в качестве физической гипотезы, нам следует упомянуть о геометрических сомнениях по поводу общности элементарно-геометрического подхода. Это — методологическая цель исследований так называемой проблемы пространства, которой геометрия, по существу, занималась последние 100 лет и на которой основано развитие дифференциальной геометрии. Здесь следует, прежде всего, назвать Римана, Гельмгольца и Ли. Мы укажем на чрезвычайно увлекательные статьи Римана «О гипотезах, лежащих в основании геометрии» [Riemann 1854] и Гельмгольца «О фактах, лежащих в основании геометрии». [Helmholtz 1868]. Обзор того, как развивали постановку вопроса Ли, Вейль и др., имеется в работе Фрейденталя [Freudenthal 1962]. Эта проблема жива и сегодня: какие следствия о структуре пространства вытекают из предположения о свободной подвижности конечных (инфинитезимальных) твердых тел? Проблему пространства можно также формулировать не дифференциально-геометрически, а топологически: каковы свойства топологического пространства, достаточные для характеризации евклидова пространства? Существуют ли такого рода свойства, которые можно назвать «наглядными»? Вопрос кажется очень трудным, см., например, работу Борсука [Borsuk 1959].

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

сиоматики. Гильберт четко считал, что аксиомы неявно определяют содержащиеся в них понятия. Чепуха, говорили «беотийцы», сделаем инверсию относительно единичного круга. Тогда аксиомы (инцидентности) все еще верны, а прямая — уже больше не прямая, а круг. Как же можно определить «прямую»? Несколько удачнее была критика со стороны Фреге. Ведь система аксиом — это что-то вроде системы уравнений, которую не удается решить. Если мы захотим ответить на вопрос, является ли нечто, например мои часы, точкой, то трудности возникнут уже с первой аксиомой, в которой говорится о двух точках. Поучительна пародия Фреге на гильбертовскую аксиоматизацию. Заявление: мы мыслим себе объекты, которые называем богами.

Аксиома 1. Любой бог всемогущ.

Аксиома 2. Существует хотя бы один бог.

Центральный пункт аксиоматизации затрагивается этой пародией: «Мы мыслим себе...» — геометрия становится чистой математикой.

ЛИТЕРАТУРА

Riemann В. Ueber die Hypothesen, welche der Geometric zu Grundle liegen, 1854. Переиздано под редакцией и с комментариями Г. Вейля в сб.: Das Kontinuum und 3 Monographien.— New York, Chelsea Publishing Company. [Имеется перевод: Риман Б. О гипотезах, лежащих в основании геометрии. — В кн.: Риман Б. Сочинения. — М.: ГИТТЛ, 1948, с. 279—293, а также в сб.: Об основаниях геометрии М.-Л.: ГИТТЛ, 1956, с. 309—341.]

Von Helmholzt Н. Ueber die Thatsachen, die der Geometrie zum Grunde liegen, 1868. In: Wissensch. Abhandlungen, B. 2, p. 618—639, 1883.— Leipzig; Barth.

Freudenthal H. Im Umkreis der sogenannten Raumprobleme. In: Bar-Hillel et al. Essays on the Foudations of Mathematics, p. 322—327. — Amsterdam, North-Holland, 1962.

Borsuk K. Grundlagen der Geometrie vom Standpunkte der allgemeinen To- pologie aus. In: Henkin, Suppes & Tarski. The Axiomatic Method with Special Reference to Geometry and Physics, S. 174—187. — Amsterdam: Horth-Holland, 1959.

Аксиоматизация посредством координатизации

После того как мы вынудили евклидову геометрию использовать в качестве системы расстояний поле R вещественных чисел, проще всего понимать ее как двумерное векторное пространство Е над R. Расстояние определяется тогда через скалярное произведение равенством

IIX, уII = VU—

для любых х.уеЕ.

Основные геометрические понятия — точка, прямая, круг, угол, конгруэнтность и т. д. нужно теперь определить в терминах векторного пространства Е. Затем нужно установить существенные свойства этих понятий и связи между ними и соединить их в единую систему основных геометрических фактов — аксиом — таким образом, чтобы в совокупности они снова характеризовали векторное пространство Е. Это и есть в достаточно расплывчатых выражениях та программа аксиоматизации элементарной геометрии, которую мы намерены здесь провести.

Какие понятия и отношения на Е следует записать в «геометрические»? Мы договоримся, что это будут те отношения, которые сохраняются при изометрических, т. е. сохраняющих расстояния, отображениях пространства Е. Например, образ круга при отображении /: Е-^Е всегда является кругом, если / — изометрия, т. с. равенство

IIX, у 11 = II /М, !Ш\ верно для всех х,у Е.

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

R^En есть ^-местное геометрическое отношение, если для любой изометрии / пространства Е имеет место

<Х1, х„)еR = (/(xj, fMeR.

Класс С подмножеств множества Е называется геометрическим, если {/(х)| хЕо^еС для любой изометрии / и любого множества ае С.

В этом смысле обычные основные понятия элементарной геометрии — прямые, круги, треугольники и т. д. являются геометрическими классами, а такие отношения, как инцидентность и конгруэнтность, являются геометрическими (на точках).

Нашу программу аксиоматизации можно точнее сформулировать следующим образом. Выбрав конечное число геометрических классов и геометрических отношений на этих классах, мы ищем такую систему аксиом для этих элементов и отношений, для которой из того,что некоторая элементарная теорема верна для принятого в Е определения основных понятий, вытекает, что она выводима из принятых аксиом, и, обратно, выводимость влечет истинность. (Здесь, как и раньше, мы называем высказывание элементарным, если оно выразимо в языке первой ступени с рассматриваемыми от-

ношениями на рассматриваемых элементах.) Наш подход к отысканию такой системы аксиом основан на следующих соображениях. (1) Точки линейного (одномерного) подпространства пространства Е однозначным образом соответствуют элементам основного поля пространства Е, т. е. вещественным числам. Операции поля можно, таким образом, выполнить с помощью простых геометрических конструкций: откладывания отрезков и использования теорем пропорциональности. Легко представить основные геометрические понятия и их свойства таким образом, чтобы эти конструкции были формально определимы, а свойства операций поля — формально доказуемы. (2) Пойе, введенное таким образом на одной прямой, будет затем применено для координатизации всей евклидовой плоскости и будет показано, что полученное таким образом векторное пространство изоморфно исходному векторному пространству Е. (3) После этого точный анализ доказательств выявляет, наконец, использованные свойства геометрических отношений и тем самым дает аксиоматизацию.

Мы хотим провести эту программу аксиоматизации таким образом, чтобы получить, по существу, известную гильбертову систему аксиом (для евклидовой плоскости). Этот выбор, разумеется, совершенно произволен. Его можно оправдать лишь тем, что он представляет исторический интерес, и доступностью литературы.

Таким образом, мы начинаем с того, что выбираем в качестве геометрических основных элементов

прямые — переменные, обозначаемые через х, у, г, ..., g, /, ..., а, b, с, ...,

точки — переменные, обозначаемые через X, У, Z, ..., Р, Q,...,A,B,C,....

В качестве геометрического отношения мы сначала включаем в словарь только инцидентность, для которой употребляется запись Р ^1. Мы принимаем нумерацию (но нс вид) гильбертовых аксиом

Аксиомы инцидентности и аксиома параллельности

It & 12: А #= В =) 31 а (А е а к В е а);

13:УаЗД35(Д ¥=Вл Asa ^ Bed)

л 3АЗВЗС П За (А е а л В е а л С е а)-.

Определение отношения а//Ь\

ЗА (А е а л А е b => а = Ь)

IV*:VaVA П /1 е а з 3! 6(<4 е 6 л а/Ь).

Из аксиом li — 13 следует существование фигуры, занимающей в дальнейшем центральное место. Она состоит из двух прямых g, g\ пересекающихся в точке 0, и отличных от 0 точек Е и Е\ лежащих соответственно на этих прямых. Мы введем теперь операции поля на прямой g геометрически, т. е. определим их через инцидентность, причем точка Е бу- дет представлять единицу для умножения, а точка 0 — нуль для сложения. Мы используем в дальнейшем обычные геометрические разговорные выражения, такие, как: «пересекаются», «лежит на», «проходит через» и т. д. На чертежах мы помещаем засечки на прямых, чтобы обозначить пучки параллельных прямых; gXh означает, что прямые g и h пересекаются.

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

Лемма. Если h^ g и hXg, то из hf //h следует h'Xg.

Сложение.

Вопрос о корректности определения сложения и умножения, а также о выполнении аксиом поля сводится к истинности некоторых теорем о пересечениях. Важнейшей из тех, что нам потребуются, будет теорема Дезарга, которую мы вначале присоединим к числу аксиом,

Теорема Дезарга

D: Если у двух треугольников соответственные стороны параллельны, то прямые, соединяющие соответственные вершины, либо пересекаются в одной точке, либо сами параллельны. Обратно, если два треугольника расположены таким образа^, что прямые, соединяющие соответственные вершины, проходят через одну точку или параллельны друг другу и при этом две пары соответственных сторон параллельны, то и третьи стороны параллельны между собой.

Из теоремы Дезарга непосредственно вытекает полезное замечание: в определении суммы В + А можно было проводить прямую g" не через Е', а через любую другую точку,

Теперь мы приведем выводы аксиом поля. Они состоят в основном из многократных применений теоремы Дезарга. На чертежах мы указываем это с помощью подходящей штриховки перспективных треугольников.

Коммутативность сложения

Ввиду теоремы Дезарга D для заштрихованных треугольников все точки, обозначенные кружком, лежат на одной прямой. Из-за перспективности треугольников, обведенных жирным контуром, с центром Р прямая RS проходит через В + А.

Ассоциативность сложения

О АВ А+В СВ+С А*(В^С)

В силу теоремы D для треугольников, обведенных жирным контуром, прямые, помеченные волной, параллельны. Из теоремы D для заштрихованных треугольников следует, что Л + (В + С) = (Д + В)+С.

Для доказательства коммутативности умножения нам нужна еще одна теорема о пересечениях, которую мы опять присоединим к числу аксиом. Это — теорема Паппа и Паскаля, обычно называемая просто теоремой Паскаля.

Теорема Паскаля

Р: Пусть на двух прямых расположены точки 1, 2, 3 и Г, 2', 3' соответственно таким образом, что среди соединяющих их прямых 12' и 1'2 параллельны друг другу и 2^ и 2'3 параллельны друг другу. Тогда и прямые 13' и ГЗ также параллельны друг другу.

Вообще-то теорема Дезарга следует из теоремы Паскаля. Полное доказательство состоит в рассмотрении многочисленных частных случаев, и мы позволим себе не приводить его.

Коммутативность умножения

Мы помечаем точки на прямых g и g' указанным выше образом и получаем с помощью теоремы Паскаля Р, что А-В = В-А.

Закон дистрибутивности

Для получения закона дистрибутивности мы дважды применяем теорему D.

Доказательство существования нуля (точка 0), единицы (точка f), противоположного и обратного элемента оказывается тривиальным упражнением. Таким образом, мы доказали, наконец, аксиомы поля. Чтобы ввести упорядочение

на этом поле, мы должны ухватиться за какое-то геометрическое понятие. Естественно выбрать отношение

АВС; Точка В лежит между точками А и С и отлична от обеих.

Это отношение непосредственно служит для введения отношения упорядочения на построенном поле. Мы основываем его на более простом свойстве положительности.

Определение

Д>0:=Л#=0лП АОЕ.

С помощью понятия положительности аксиомы порядка для поля формулируются следующим образом:

П (0 > 0); А > 0 v — А > 0 v А = 0;

A>0^B>0.=).A-VB>0^A•B>0.

Их следует вывести из подходящих аксиом для отношения «лежать между». Эти последние выглядят у Гильберта следующим образом.

Аксиомы упорядочения

1^: АВС =>. СВ А кЭа^А^ак В^акС ^а) гА^ВгхАФСкВ^С;

П2: А=АВ^ЭС АВС;

П3: АВС => П АСВ л П ВАС;

П4: 1 Эх(Л е х Г В е х л С е х) л

А ф a N В ф а ГС ф aN D ^ a n ADB. id. ЭЕ(Е ее а л AEC) v ЭР (F е а л BFC) (аксиома Паша).

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

Аксиома полноты

V: Пусть М и N — два непустых множества точек на прямой g, и пусть имеется точка С, такая, что для всех А^М и B^N верно САВ. Тогда имеется точка D, такая, что для всех А е М и В ^ N, отличных от D, верно ADB.

Из аксиомы V моментально следует, что поле, построенное на прямой g, полно. Тем самым доведена до конца задача (1) нашей программы аксиоматизации.

Для выполнения задачи (2) мы должны теперь использовать поле, построенное на прямой g, для координатизации всей плоскости. Для этого нужно сначала построить поле также и на прямой g'. Мы считаем, что это сделано в точности тем же способом, что и для g, лишь Е и Е' меняются

ролями. При этом выясняется, что поля, построенные на пря-

3 Э. Энгелер

Порядок

ОБА = ОБ'А' в силу аксиом группы II, особенно аксиомы Паша П4.

Каждой точке Р мы можем теперь сопоставить две координаты— вещественные числа Хи Ус помощью следующего определения:

Наконец, плоскость становится векторным пространством V, если определить скалярное произведение двух точек Р и Q следующим образом. Если Хь У1— координаты точки Р, а Х2, У2 — координаты точки Q, то полагаем: P-Q; = Xi-X2 + У1 • У2, где сложение и умножение — операции, введенные на осях координат.

Пока что наша координатизация несколько произвольна, так как у нас была полная свобода при выборе осей координат и единичных точек. Это выражается математически в том, что осуществляемое при помощи координат отображение (X, У)—>(Х У) плоскости на себя не является в общем случае изометрией. (При этом X, У обозначают координаты некоторой точки Р относительно осей g и g', а X, У — координаты той же точки относительно осей g и g'.) Для достижения изометричности не хватает возможности выразить требование, чтобы оси координат были взаимно перпендикулярны, а расстояния ОЕ и ОБ' были равны друг другу. С этой целью вводятся конгруэнтность отрезков:

AB^CD: отрезок АВ конгруэнтен отрезку CD и конгруэнтность углов:

ABC s EFG:

угол с вершиной В конгруэнтен углу с вершиной F.

Для этих новых геометрических понятий мы следующим образом формулируем аксиомы гильбертовой группы III.

Аксиомы конгруэнтности

П^: A^B^C^D. zd3E(CDEnAB« DEY

Ш2: AB « EF nCD « EF. zd AB « CD", 1113: AB ~ A'B' NBC» B'C' A ABC nA'B'C'.zdAC ~ A'C':

-\Зa(Aea^BeaNC ea)

A ~|3a(.4' Ей лй'е a aC'ga). zd

ЗС'За [A' e а д В' e а А Д 3D (D e aN C*DC') NABCZA'B'C'

A VC" ((1SC (E e a л C*EC") л ABC 5 A'B'C") zd (с" =c'v b'c"c' v b'c'C"yy

AB » A'B' nAC ~ A'C' А ВАС ~ B'A'C'. zd ABC-A'B'C';

: AB»CDtdC^D;

: A Ф В zd AB ~ BA;

: ABC 2 A'B'C' zd ~) За (A' e а А В' e а л C' e a);

;AjBiCi ~ A3B3C3 Л A2B2C2Z АзВзСз-zdAiBiCi — A2B2C2;

:H3a (A e a N В e a kC e a) zd ABC $CBA;

;"\3akAs а к В e a nC e. a) n (BA' А л BA A').

=> ABC ~ A'BC.

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

Пусть на евклидовой плоскости £ выбраны две прямые g и g', пересекающиеся в некоторой точке 0, а также точки Е и Е\ лежащие соответственно на g и g\ причем g перпендикулярна g' и ОЕ ^ ОЕ'. Тогда векторное пространство, построенное из точек плоскости Е указанным выше способом, изоморфно Е.

ЛИТЕРАТУРА

Artin Е. Geometric Algebra, Кар. II, S. 51 И. — New York, Interscience, 1957. [Имеется перевод: Артин Э. Геометрическая алгебра. —М.: Наука, 1969.]

Veblen О., Young J. W. Projective Geometry, Vol. I, Кар. VI, S. 141—168.— New York: Blaisdell.

Hilbert D. Grundlagen der Geometric, . Auflage, § 24—27, 32. — Stuttgart: Teubner, 1930. [Имеется перевод: Гильберт Д. Основания геометрии.— М.-Л, ГИТТЛ, 1948.]

Schwabhauser W. Ueber die Vollstandigkeit der elementaren Euklidischen Geometric. Zeitschrift fiir math. — Logik und Grundlagen der Mathematik, B. 2, S. 137—165, 1956.

Вопросы теории науки и методыэлементарной геометрии

Аксиома полноты V для евклидовой геометрии на плоскости снова ставит нас перед проблемой, уже рассматривавшейся в первой главе: в какдм смысле надо понимать участвующие там множества М и Я? Иными словами, как нам адекватно выразить содержание аксиомы V в нашем формальном языке? И снова мы выбираем тот же выход, что и раньше: мы отождествляем множества с экстенсионалами предикатов, следовательно, в данном случае — с предикатами в языке первого порядка для элементарной геометрии с введенными в § 2 исходными понятиями. Полученную таким образом элементаризированную аксиому полноты называют схемой Тарского.

Ут: Для любой пары формул ЯД-) и Н^^ ЗСМАМВ <НХ (Л) д Я2 (5). о АВС)

=3 ЗДУЛVB (Л ^ D л В ^ D л Н{ (Л) А Я2 (5) о ADB).

Из Ут непосредственно следует, что построенное на прямой g упорядоченное поле удовлетворяет (элементарной) аксиоме полноты из теории вещественных чисел (гл. I, § 2) Полнота и разрешимость этой последней теории переносятся

теперь с помощью конструкции из § 2 настоящей главы на элементарную евклидову геометрию. Мы разъясним это, сопоставляя друг с другом геометрию и линейную алгебру, что прояснит связи, порождаемые координатизацией, также и с формальной стороны. Для этого мы выбираем формулировки соответствующих языков, где одинаково обозначаются операции и отношения, которые являются геометрическими (соответственно алгебраическими) исходными понятиями, но определимы в линейной алгебре (соответственно евклидовой геометрии). В большинстве случаев мы не будем выписывать определения во всех подробностях.

Язык геометрии

Язык линейной алгебры

Р, Q, R> • • .переменные для точек

Р, Q, R,--- переменные для векторов

0, Е, Е' выделенные точки

0нулевой вектор

Е, Е'ортонормиро-

ванный базис

/, т, ппеременные

для прямых

/, т, ппеременные

для линейных подпространств

g, g'выделенные

прямые

g, g'натянутые на

Е, Е' линейные подпространства

еотношение ин

цидентности

еотношение

«быть элементом»

«конгруэнтность

отрезков

АВ ~ CD --(А-ВМА-В) =AC-DHC-D)

PQRотношение „ле

жать между"

PQR

2конгруэнтность

углов

PQR-UVW := ...

х, у, z, .. .переменныедля точек на прямой g

x, у, z, ... переменные для элементов основного поля

P-Q = x\= ...

Р • Qскалярное про

изведение

x-Vy=z;= ...

+сложение

в поле

— у=2:= ...

—вычитание

в поле

х • y = z:= ...

умножение в поле

y-1 = z:= ...

обращение в поле

х = 0 х = 0 х — 1 := х = Е х > 0 := ...

0нуль

1единица

<отношение

порядка

Мы видим, что любую формулу расширенного определениями языка геометрии можно воспринимать как формулу расширенного определениями языка линейной алгебры. Тем самым различие между геометрией и алгеброй заключается в большей степени в выделении тех фактов, которые мы хотим считать аксиомами. Ради наглядности мы приводим их еще раз.

Аксиомы геометрии; Г

Аксиомы линейной алгебры: Л

I, II, III, IV*, Vt, D, Р,

Аксиомы для вещественно замкнутых полей (с переменными X, у, ...),

плюс:

плюс:

(g ± g' л 0Е ~ 0Е' л 0 е g ^0 е g' А Е е g ^ Ez g g'

обычные аксиомы для векторных пространств, базис Е, Е'; инцидентность на линейных подпространствах.

Метатеорема

Для любой из формул F расширенного языка выводимость F из Г эквивалентна выводимости F из Л.

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

о полноте и разрешимости системы аксиом Г для евклидовой геометрии на плоскости. Оба этих метатеоретических свойства были подробно установлены в гл. I для аксиоматики вещественно замкнутых полей. Этот результат чрезвычайно просто переносится на аксиоматику Л линейной алгебры, намеченную выше: подробности получаются сами собой. Но из полноты и разрешимости системы Л вытекает, как мы сейчас покажем, следующее утверждение.

Полнота и разрешимость элементарной евклидовой геометрии на плоскости

Для любого предложения F в языке элементарной геометрии одно из предложений Р, ЛР выводимо из аксиом Г; вопрос о выводимости данного предложения эффективно разрешим.

Для доказательства рассмотрим произвольную формулу F элементарной геометрии. Будем мыслить се как формулу расширенного определениями языка линейной алгебры. Тогда из полноты и разрешимости системы Л следует, что либо F, либо "ЛР выводимо из аксиом Л, и мы можем эффективно решить, какое из этих двух предложений подходит. По метатеореме то же верно для Г.

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

Поэтому при изучении оснований геометрии очень рано занялись вопросом о выборе исходных геометрических понятий: какие из них, по возможности простые и в меньшем числе, следует поставить в самое начало?

Во-первых, легко видеть, что достаточно обойтись одним сортом вещей, например только точками. Прямую можно ввести как пару отличных друг от друга точек. Формально это излагается с помощью перевода, который сопоставляет любому предложению, содержащему переменные для прямых, эквивалентное предложение, куда они не входят:

3aF (я) = ЗАjBЛ2 (Л 1Л2 л FY

Здесь F' получается из F^a^ заменой каждой атомарной формулы В (а) на

В=== Ay V В = А^ V ВАуА2 v АуВА^ V АуА^В.

Формула а = Ь заменяется на

Ay е b л Л2 е Ь.

На следующем шаге можно устранить и конгруэнтность углов, так как в силу первого признака конгруэнтности треугольников имеет место

ABC 2 А*В*С*. = . ЗА'ЗС' (А'В* ~ АВ к А'С' ~ ЛС A В*С' ~ ВС л 1В*А'А*^А' = А*^В*А*А'Н (в*с'с* v с' = с* v b*g*c^y

Таким образом, евклидову геометрию можно построить, исходя только из точек и отношений «лежать между» и конгруэнтности отрезков. Соответствующую систему аксиом предъявил Тарский [Tarski 1959]. Он вводит такие сокращения:

рЛВС вместо АВС \/А = Bw В = С и

6ABCD вместо АВ CD V (Л = В А С = DY

Легко еще уменьшить список основных понятий, заметив, что рЛВС можно определить через б. Пользуясь тем, что уже нет различных сортов переменных, мы будем в дальнейшем для упрощения записи применять малые буквы в качестве переменных для точек.

Мы полагаем по определению

ху ^ уг := Vzz \6yuuz =) Ву (bxxwy а ЬиууйД.

Геометрически xy^yz означает, что расстояние между точками х и у не превосходит расстояния между у и 2,

Действительно,

II х, УII ^ II У» ^ II = Зи (byuuz л Vy (bvyyu id П бхииу)

что проясняет следующий чертеж:

Теперь отношение [3— модифицированное отношение «лежать между» — можно выразить следующим образом:

$xyz := V^^их ^. ху Auz^zy. td и =у).

Мы закрепим это следующим рисунком и ссылкой на школьную геометрию:

Следовательно, геометрия на плоскости может обойтись единственным четырехместным предикатом 6. Чтобы провести редукцию еще дальше, заметим, что в определении предикатов р и ^ предикат 6 использован только в сочетании bxyyz, т. е. с одинаковыми средними переменными. Это отношение, достаточность которого обнаружил еще Пьери в 1908 г.,

nxyz :== ^xyyz.

Действительно, сам предикат 6 можно тоже свести к предикату л. Для этого р и < определяются указанным выше образом (но с помощью символа л), а затем полагают

coll xyz := ^xyz М $yxz V ^xzy,sym xyz := Mu (coll хуи Л nxyu, = л = xM u = z\

Эти определения выражают соответственно, что х, у, г коллинеарны и что х и г расположены симметрично относительно у. Тогда в евклидовой геометрии очевидным образом справедлива теорема, позволяющая определить 6 следующим образом:

Ъхуис := ВгВ/ (sym хги Л sym yrt Л utwo\

Следующий чертеж иллюстрирует содержание этой теоремы.

Дальнейшие сведения найдены Бернайсом, Скоттом [Scott 1956] и Хенкиным [Henkin 1962]:

Mxyz\ угол с вершиной у прямой;

п' xyz: треугольник xyz равносторонний;

Vxyz: треугольник xyz прямоугольный.

Как далеко можно здесь пойти? В частности, какими средствами можно доказать, что некоторые отношения или типы отношений недостаточны для того, чтобы построить плоскую геометрию? Вот один пример.

Теорема

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

Идея доказательства. Мы построим некоторую модель геометрии и отображение этой модели в себя, которое яи-

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

Подготовительный шаг. Пусть А— подполе поля С комплексных чисел. Базис Хамеля для С с коэффициентами из А— это такое множество В^ С, что

любой г ^ С представим в виде конечной суммы

Е О/ • bi, где at е Л, bt г В;

(и) если У, at ■ bt=0, то at = 0 для всех I.

Для любого поля А имеется такой базис Хамеля. Действительно, рассмотрим вполне-упорядочение поля комплексных чисел С = {со, ^ь ^2, • • •, Са, • • }•

Будем добавлять элемент са к В в точности тогда, когда са не представим в виде конечной суммы элементов ср е В, Р < а, с коэффициентами из А. В рамках этой конструкции (с помощью так называемой трансфинитной рекурсии) можно довольно свободно распоряжаться несколькими первыми элементами множества В, например взять &0 = 1, Ь\— вещественное число ^А, Ь2— произвольное комплексное число ^А. Мы используем это обстоятельство ниже. Построенное множество В — базис. Действительно, пусть сеС. Тогда с = са для некоторого а. Если са е В, то все уже в порядке, в противном случае по построению множества В существует представление са = X ^i * ble

Допустим теперь, что X ai • bi = 0 и at v^ 0 для одного из аь Пусть са — последний (в нашем вполне-упорядочении поля С) из элементов 6/, для которых aj Ф 0. Тогда са^В, но он представим в виде линейной комбинации предшествующих элементов базиса. Это дает искомое противоречие. В заключение заметим еще, что представление элементов поля Cj линейными формами однозначно (с точностью до порядка слагаемых): это сразу следует из (ii).

Доказательство теоремы. Допустим, что у нас есть несколько таких операций р,, /=1,2, ..., п; их символы мы будем записывать между аргументами:

xpty = 2.

Эти операции должны сохраняться при отображениях подобия евклидовой плоскости на себя, так как это Верно

для л, а операции по предположению определимы через л. Теперь рассмотрим эту плоскость как поле С комплексных чисел. Тогда из инвариантности операций р, относительно переносов следует, что

XPi.y = Z. = Ax — y)PiO = z — у.

Введем сокращение

а. (х):= хрД

Из инвариантности о, относительно поворотов и растяже- ний следует, что для всех с е С.

Ut W = У- = -^ (с * *) = с • у, т. е. oz (с-х) = с-оДх) для всех с^ С. Если мы еще положим $/ = 07(1), то а совпадает с умножением на sr

Ui (х) = Oi(X • 1) = X • Ui (1) — Si • X.

Иными словами, для любой операции pz- имеется sze.C, такое, что

xpty = Si (х — у) + у.

Обозначим теперь через Л поле Q(sb ..., s„), где Q — поле (комплексных) рациональных чисел, и пусть В — базис Хамеля для С с коэффициентами из Л, такой, что 1,с, d^B, с — вещественное число, d— комплексное число. Пусть Т— линейное преобразование поля ,С, определяемое формулами

T^ = d; T(d) — c\ T(bi) — bi для всех остальных bi^B\

Т сохраняет все операции рг

т (xpty) = Т (Si -(х —у) + у) =

= Si (Г (х) - Т (у)) + Т(у) = Т (х) ptT (у).

В противоположность этому Т не сохраняет отношение л. Действительно, рассмотрим точки 0, 1, J на комплексной плоскости и (однозначно определенную) окружность, проходящую через 0, 1, и d. Обозначим ее центр через и.

Мы видим, что л0м1лл1ш/. Напротив, лТ (0) Т (и) Г(1) л лТ ^ Т (и) Т (d) не имеет места, так как иначе по определению Т было бы верно лОГ (w) 1 л лОТ (zz) с; Последнее означает, однако, что 0, 1, с лежат на одной окружности с центром Г (и), что противоречит нашим допущениям; □

Ситуация меняется, если в качестве исходных элементов геометрии рассматриваются прямые, а не точки.

Теорема

На евклидовой плоскости можно определить некоторую двуместную операцию над прямыми, такую, что элементарная евклидова геометрия на плоскости имеет полную аксиоматизацию с этой операцией в качестве единственного исходного понятия.

Набросок доказательства. Интуитивно мы рассматриваем точки как пары взаимно перпендикулярных прямых. Обещанная двуместная операция на прямых — это зеркальное отражение.

а*Ь = с

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

а | Ь; =. а • b = b л а Ь.

Точки —это пары прямых ^a,by такие, что a_L6. Запишем отношение «точка ^а, Ь) лежит на прямой с»;

(а, 6) е с; =а • (Ь • с) = с.

Это определение поясняет следующий чертеж:

Равенство точек:

(а, 6) = (а', //):= VекаАЬ-с^ = с. = .а' • (Ь' • с) = с\ Наконец, можно определить введенное Пьери отношение л:

Л (Уь Уг) кх\, х2) (zb z^:= 30363с [(X], х2) е а л (у„ у2) е а

Л (хн х2) е6л (гр 22)е6а (хр х2) е с L(c • a^ = b Л (с • г/р с • у^ = (гр г2)].

Эту ситуацию проясняет следующий эскиз:

Таким образом, операция а-Ь = с может быть положена в основу элементарной евклидовой геометрии на плоскости. Явную полную аксиоматику можно было бы получить путем переформулировки аксиом I—VT применительно к этому редуцированному словарю. Мы этого не сделали, да такой метод и не соответствует ситуации. Намного уместнее было бы постепенное добавление естественных для данной операции требований, возникающих, например, при проведении программы координатизации. Здесь мы находимся совсем не на целине; методологически сюда примыкает другой подход к обоснованию геометрии, а именно теоретико-групповой (ср., например, [Bachmann 1959]).

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

резка АВ и CD соизмеримы, и пишут АВ ~ CD, если АВ можно поделить на m частей, a CD — на п частей так, что все эти части конгруэнтны друг другу. Числовые меры m и п дают меры обоих отрезков относительно одной и той же меры этой получившейся части. Очевидно, что АВ ~ CD — геометрическое отношение на четверках точек. Однако оно неэлементарно.

Мы докажем это следующим образом с помощью нестандартных моделей. Пусть 7<(Л, 5, С, Z))— элементарная формула, которая эквивалентна формуле АВ ~ CD во всех моделях аксиом Г. В стандартной модели Е имеет место утверждение

4ABCDE3F. СОЕ л DFE л К (Л, 5, С, F),

т. е. любое продолжение отрезка CD отрезком DE содержит точку F, такую, что CF ~ АВ. Если К — элементарная формула, то это предложение должно иметь место и в нестандартной модели аксиом Г. Однако там оно нс имеет места, например, если отрезок АВ конечен, a CD бесконечен.

Разумеется, язык элементарной геометрии можно обогащать точно так же, как был расширен в гл. I язык вещественных чисел. Мы не будем здесь делать этого (однако см. [Tarski 1959]).

ЛИТЕРАТУРА

Beth Е., Tarski A. Equilaterality as the Only Primitive Notion of Euclidean Geometry. — Proc. Koninklijke Nederlandse Akademie van Wetenschappen, Series A, В 59, S. 462—467, 156.

Scott D. A. Symmetric Primitive Notion for Euclidean Geometry. — Proc. Koninklijke Nederlandse Akademie van Wetenstchappen, Series A, Band 59, S. 456—461, 1956.

Bernays P. Die Mannigfaltigkeit der Direktiven fur die Gestaltung geometri- scher Axiomensysteme. In: Henkin, Suppes & Tarski. The Axiomatic Method p. 1—15. — Amsterdam: North-Holland, 1959.

Tarski A. What is Elementary Geometry? In: Henkin, Suppes & Tarski. The . Axiomatic Method, p. 16—29. — Amsterdam: NortbHolland, 1959.

Scott D. Dimension in Elementary Euclidean Geometry: In: Henkin, Suppes & Tarski. The Axiomatic Method, p. 53—67. — Amsterdam: North-Holland, 1959.

Robinson R. Binary Relations as Primitive Notions in Elementary Geometry. In: Henkin, Suppes & Tarski. The Axiomatic Method, p. 68—85.— Amsterdam: North-Holland, 1959.

Royden H. L. Remarks on Primitive Notions for Elementary Euclidean and Non-Euclidean Plane Geometry. In: Henkin, Suppes & Tarski. The Axiomatic Method, p. 86—96. — Amsterdam; North-Holland, 1959.

Schwabhauser W., Szczerba L. W. Relatons on Lines as Primitive Notions for Euclidean Geometry. — Fund. Math., v. 82, p. 347—355, 1975.

Henkin L. Symmetric Euclidean Relations. — Proc. Koninklijke Nederlandse Akademie van Wetenschappen, Ser. A, B. 65, S. 549—553, 1962.

Pieri M. La geometria elementare istituita sulle nozioni di ‘punto’ e ‘sfera’.—

Memorie di Matematica е di Fisica della Societa Italiane delle Scienze, Ser. 3, v. 15, p. 345—450, 1908.

Bachmann F. Aufbau der Geometric aus dem Spiegelungsbegriff. — Berlin: Springer-Verlag, 1959.

Геометрические построения

Традиционное изложение теории геометрических построений начинается с перечисления так называемых конструктивных средств — линейка, циркуль, измеритель, линейка с делениями, данная кривая и т. п. и переходит к выводу теорем о границах и возможностях этих вспомогательных средств. Наиболее известны утверждения типа теорем невозможности (трисекция угла, удвоение куба и т. д.) и теоремы о взаимозаменяемости или избыточности конструктивных средств (построение с помощью одного циркуля), причем для доказательства первых применяются прежде всего алгебраические методы (теория Галуа), а для доказательства вторых — остроумные геометрические конструкции. Изложение теории геометрических конструкций, которое приводится в книгах по алгебре, вполне достаточно для алгебраических целей, однако для исследований в области оснований нужно уточнить исходные понятия. Хорошую службу в этой связи может сослужить круг понятий языков программирования высокого уровня. Я буду здесь предполагать некоторое знакомство с ними.

Исходные конструктивные операции (т. е. построения) представляются в языках программирования с помощью присваиваний. Например, мы пишем

к=Е^Р> Q).

Это присваивание берет две точки, обозначенные через Р и Q, строит связывающую их прямую и обозначает ее через /. К присваиваниям добавляются разрешающие операции, которые сопоставляют некоторое истинностное значение данным значениям переменных; примером является решение вопроса о том, имеет ли место PQR. Они встречаются в «структурированных» языках программирования в контекстах

if PQR then ... else ..., т. e. если PQR, то ...» иначе ...;

while ~\PQR do ..., т. e. пока ~\PQR делать ...

Во многих изложениях этой теории, особенно в алгебраических, о разрешающих операциях просто забывают! Таким образом, если мы предполагаем, что задан паскалеподобный

язык программирования, то для определения класса объектов, которые могут быть построены с помощью алгоритмов, достаточно задать набор средств построения, перечислив список допустимых переменных, констант, присваиваний и разрешающих операций. Вот один из простейших наборов такого рода, описывающий построения с помощью одной линейки.

Аффинные построения (с помощью одной линейки)

Переменные;

Р, Q, R, ... — точки, /, т, м, ... — прямые.

Константы;

О, Е, Е' — начало координат и точки на осях.

Присваивания;

§Mh,§Mh,. l\=L(P, Q) —прямая, соединяющая Р и Q, если P¥=Q,. l\=L(P, Q) —прямая, соединяющая Р и Q, если P¥=Q,Q;=PVg> А)— точка пересечения прямых g и А, если

§Mh,

§Mh,

. l\=L(P, Q) —прямая, соединяющая Р и Q, если P¥=Q,

. l\=L(P, Q) —прямая, соединяющая Р и Q, если P¥=Q,

/:=L(P, g) — прямая, параллельная g и проходящая через точку Р, если Р Ф g.

Разрешающие операции;

g\\h Pegg\\h PegP = Q, g=h — равенство,

g\\h Peg

g\\h Peg

— параллельность, — инцидентность.

Эти конструктивные средства (т. е. средства построения) позволяют нам конструировать новые фигуры (т. с. сопоставления прямых и точек некоторым переменным) из данных фигур. Их, например, достаточно для реализации операций геометрического сложения и умножения из § 2. Соответствующая программа для сложения выглядит следующим образом:

begin if Л = 0 then G;=B else

begin g:=L(0,£);

g';=L№; g":=UE',gY h:—ЦЕ'.A);

if В = 0 then G := A else

begin г.= ЦВ,§'У

" F:^PU,g"y,к;=ЦР,кУ,G.= P(K,g)end;

end;

end.

Из программируемости операций поля вытекает следующее утверждение. Множество координат конструируемых точек евклидовой! плоскости всегда есть поле, содержащее поле Q рациональных чисел. Если разрешены только указанные выше средства построения, то это поле — в точности Q (так как координаты точек пересечения прямых с рациональными координатами снова рациональны и т. д.). Если же задана некоторая исходная фигура, то наше поле получается из Q добавлением координат элементов этой исходной фигуры. Мы получили следующее утверждение.

Теорема 1а. Точка Р или прямая g могут быть построены, исходя из данной фигуры, с помощью одной линейки тогда и только тогда, когда их координаты принадлежат расширению поля рациональных чисел координатами исходной фигуры.

Этой алгебраической характеризации мы противопоставим другую, имеющую более аксиоматическую направленность, и зададим вопрос: какова связь между доказуемостью существования точки или прямой и возможностью геометрического построения? Разумеется, все точки и прямые, существование которых утверждается в аксиомах I, Р, D и IV*, могут быть построены. Это утверждение можно с помощью индукции по длине вывода распространить на все предложения вида

ЗРА^Р^ 3gB^

с бескванторными Л(.) и S(.), выводимые из этих аксиом. Обратно, каждому шагу геометрического построения соответствует некоторое экзистенциальное утверждение такого вида, выводимое из аксиом I, D, Р, IV*, и мы имеем следующий результат.

Теорема 1 Ь. Формула вида ЗРА (Р) или 3gB(g) с бескванторными Л(.), S(.) выводима из аксиом I, D, Р, IV* тогда и только тогда, когда удовлетворяющая этой формуле точка или прямая может быть построена одной линейкой.

Только что доказанная теорема вызывает вопрос, какие же

конструктивные средства соответствуют в этом смысле системе аксиом I, II, III, IV*. Мы находим их, просматривая требования существования, содержащиеся в аксиомах, и обнаруживаем вслед за Гильбертом, что это — построения с помощью линейки и эталона длины.

Пифагоровы построения (линейка и эталон)

В дополнение к аффинным конструкциям здесь разрешаются:

Р := Е (Л, В; С, D) — для А ^ В и С ф D построить точку Р, лежащую на CD и такую, что CDP Г АВ^ DP.

PQR— распознавание отношения «ле

жать между».

Теоремы 1а и 1Ь можно передоказать и для этого случая. Вместо поля рациональных чисел в соответствующих теоремах появляется понятие пифагорова упорядоченного поля, т. е. упорядоченного поля, которое вместе с а и b содержит д/^2 + ^2* Доказательства в основном содержатся в § 36, 37 книги Гильберта.

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

Теорема 2b. Формула вида ЗРА(Р) или 3gB^ с бескванторными Л(.), В(.) выводима из I, II, III, IV* тогда и только тогда, когда удовлетворяющая этой формуле точка или прямая может быть построена с помощью линейки и эталона.

Классические или «платоновские» конструктивные средства— циркуль и линейка — соответствуют несколько иному расширению аффинных средств построения.

Евклидовы построения (циркуль и линейка)

К аффинным средствам построения добавляются

Р г (Z; А, В)—- точка Р лежит внутри

окружности с центром Z и радиусом АВ для А =# В,

PX,P2;=P(Z; А, В; С, D) —если Се (Z; А,В)иС#=О, то PY, Р2 — №е точки пересечения прямой CD с окружностью (Z; А, В).

Чтобы сформулировать соответствующие предложения За и ЗЬ, нам нужны еще два понятия. Во-первых, евклидово упорядоченное поле — это упорядоченное поле, содержащее вместе с любым положительным элементом а также и квадратный корень ^а. Очевидно, что квадратный корень ^южно построить с помощью циркуля и линейки. Это — известное построение среднего пропорционального

а : х = х : 1,

которое получается из известных соотношений для прямоугольного треугольника:

Во-вторых, аксиома К пересечения прямой с окружностью, утверждающая, что прямая, проходящая через точку, лежащую внутри окружности, всегда имеет с ней точку пересечения (а тогда и две точки пересечения).

Теорема За. Точка или прямая может быть построена с помощью циркуля и линейки из данной исходной фигуры тогда и только тогда, когда ее координаты принадлежат евклидово упорядоченному полю над полем рациональных чисел, которое получается из последнего путем добавления координат исходной фигуры.

Теорема ЗЬ. Формула вида ЗРА^ или 3gB(g) с бескванторными Л(.), В(.) выводима из аксиом I, II, III, IV* и К тогда и только тогда, когда удовлетворяющая этой формуле точка или прямая может быть построена с помощью циркуля и линейки.

После того, что уже сказано выше, мы можем не заниматься деталями доказательства. Интересно заметить, что

здесь используется лишь частный случай аксиомы V (т. е. Vt), а именно аксиома К пересечения окружности с прямой.

Из существования пифагоровых полей, нс являющихся евклидовыми, следует, что К действительно является новым требованием. Число ^S-^S — S содержится в любом ев- клидовом поле над Q, но нс в любом пифагоровом.

Вообще аксиома полноты V, а особенно вытекающая из нес аксиома Архимеда, играет особую роль в теории геометрических построений. Можно, например, попытаться сравнить пифагоровы конструкции с предложенными Кюршаком (см. [Hilbert 1930], § 36) построениями с помощью линейки и единичного отрезка.

Линейка и единичный отрезок

Переменные;

P,Q, R, ... - Константы;

■ точки.

0, Е, Е', ... -

■ координатный треугольник.

Разрешающие средства*.

А = В;

равенство,

ABCD;

имеет место одно из двух: 1) А ф В, С ^ D и точка пересечения Р прямых АВ и CD либо совпадает с А, В, С или D, либо такова, что АРВ или CPD; 2) А^В, C = D и АСВ.

Присваивания;

Р;=ЩА, В):

при А #= В точка Р — это лежащая на АВ точка, для которой АВР л BP ~ 0Е.

P;=KA,B\C,DY

если ABCD и С #= D, то Р — точка пересечения прямых АВ и CD.

Эти вспомогательные средства, которые, вероятно, минимальны, достаточны, как можно убедиться, для построения решений всех задач, разрешимых с помощью линейки и эталона. В частности, мы выделим одну конструкцию — построение точки пересечения прямых, заданных парами точек А, В и С, D*.

begin

while 4ABCD do

begin D:=U(C,Dy, C\ = U<D^ end;

P\ = I<A,B\ C,D)

end.

Мы описали эти конструктивные средства столь подробно потому, что они дают не совсем то, что было обещано. Хотя все элементарные задачи на построение с помощью циркуля и линейки разрешимы, при их решении делается молчаливое допущение, выходящее за рамки аксиом I—IV* и даже аксиом I—VT. Дело в том, что общая программа нахождения точки пересечения не обязана давать точку пересечения в любой модели аксиом I—V! Действительно, рассмотрим нестандартную модель аксиом I—Ут, где есть бесконечно малые элементы, и в ней две прямые, пересекающиеся под бесконечно малым углом. Тогда применяемый в программе архимедовский принцип многократного откладывания единичного отрезка не поможет нам достичь ситуации ABCD; хотя точка пересечения существует, она не может быть построена.

Рассмотрим, наконец, конструктивные средства, соответствующие геометрии, обсуждавшейся в § 3 и основанной на понятии прямой и единственной двуместной операции.

Пифагоровы построения («перегибание листа бумаги»)

Переменные*.

I, tn, п, g, h, ... — прямые..

Константы*.

х, у, и—- прямые ОЕ, ОЕ' и ЕЕ'.

Присваивания*.

I := j_ (g, hy.если g jf h, то I — прямая, орто

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

lx, l2:= L(g, hy. в случае g J^h — биссектриса, в случае g||h — параллельная на середине расстояния.

I :=L(gi, g2; hv Н2У если gx И g^ ^i И h2 и точки пересечения различны, то / — прямая, соединяющая эти точки пересечения.-

Разрешающие операции*.

g = h:равенство,

(аь а2У) (61,62) (^1, с2у. ах и cz2 пересекаются в некоторой точке Д, Ьх и 62 —в точке В, сх и с2 — в точке С и имеет место АВС.

Мы считаем, что прямая задана перегибанием листа бумаги, и убеждаемся, что исходные конструкции действительно можно осуществить с помощью перегибания бумаги, в частности наложения линий перегиба друг на друга!

Теорема. С помощью перегибания листа бумаги можно осуществить в точности те же конструкции, что и с помощью линейки и эталона.

Доказательство. Мы должны показать, как можно промоделировать исходные конструкции одного набора построений на евклидовой плоскости с помощью другого набора построений.

(а) Моделирование построений с помощью линейки и эталона

l*=L(P, g), где Р— точка пересечения прямых рх, р2 и P^g.

Воспользуемся тем, что точки А, В, С, «оо» находятся в гармоническом положении:

Последовательность построений соответствует нумерации прямых.

P^h, где Р— точка пересечения прямых pi, р2, имеет место тогда и только тогда, когда JL (A, pi) = JL (А, р2).

P = Q, где Р — точка пересечения прямых рь р2, а Q — точка пересечения прямых рь р2, имеет место тогда и только тогда, когда Р е qx и Р е р2.

g\\h при g^h имеет место тогда и только тогда, когда Д_(й, x)=_L(g, 1 ^х^.

Если Л, В, С — точки пересечения соответственно прямых ах, а2; b\,b2\ Сь с2, то АВС имеет место тогда и только тогда, когда Е (Л, В; С, В) = А А Е (С, В; А, В) = С, где Е уже построено выше.

(Ь) Моделирование построений с помощью перегибания бумаги

Прямая 1, проходящая через точку Л, проводится с помощью точек О, Е или Е' таким образом, что она отлична от g и h. Последовательность оставшихся построений указана с помощью нумерации; отрезки АВ, AC, AD и AG конгруэнтны ОЕ.

1;=Е^ЛУ

Первый случай: g )Y h;

Отрезки АВ и АС конгруэнтны ОЕ. Второй случай: g\\h:

ЛИТЕРАТУРА

Engeler Е. Remarks on the Theory of Geometrical Constructions. In* C. Karp. The Syntax and Semantics of Infinitary Languages, S. 64—76, Lecture Notes in Mathematics, No. 72.— Berlin: Springer-Verlag, 1967,

Engeler Е. On the Solvability of Algorithmic Problem^, In: Rose & Shepherd- son. Logic Colloquium’73, p. 231—251. — Amsterdam: North-Holland, 1975.

Schreiber P. Theorie der geometrischen Konstruktionen. — Berlin: Verlag VEB, 1975.

Seeland H. Algorithmische Theorien und konstruktive Geometrie. — Stuttgart: Hochschul-Verlag, 1978.

Hilbert D. Grundlagen der Geometrie, 7 Auflage. — Stuttgart: Teubner, 1930. [Имеется перевод: Гильберт Д. Основания геометрии. М.-Л.: ГИТТЛ, 1948.]

Глава IIIАЛГОРИТМИКА

Принято, чтобы в последней главе автор мог заняться своим хобби. Я поступлю так же, но так как это — третья глава довольно тонкой книги, требуется еще какое-то обоснование.

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

Что такое вычислительное предписание?

Алгоритмика начинается с понятия функции, точнее, понятия вычислимой функции.

Разумеется, можно известным образом свести понятие функции к понятию множества*, функция из Л в В — это подмножество F ^ АХ В, обладающее свойством

ухе А31у^В.<х, у) ер,

В соответствии с этим реляционным определением функция расположена перед нами как единое целое во всем своем протяжении или экстенсионале. Однако это идеализированное теоретико-множественное понимание не вполне соответствует такому обращению с понятием функции, которое начинает с понятия вычисления: функция — это вычислительное предписание, которое в применении к аргументу выдает вполне определенное значение. В школе эти вычислительные предписания* принимают главным образом вид формул, точнее, функциональных выражений, таких, как

(х + 2)(х-2) или

х2 — 4.

На множестве Q оба этих вычислительных предписания fi и f2 дают одни и те же значения; fi в применении к хе Q всегда дает то же, что f2 в применении к х.

Мы пишем

f * х

вместо «f в применении к х». Таким образом, fi=^f2, хотя fi*x = f2*x для произвольного х. Два этих вычислительных предписания отличаются не только по внешнему виду, но и в столь важном аспекте, как сложность: f\ требует больше шагов вычисления, чем f2. Таким образом, в случае вычислительных предписаний наш интерес направлен не на экстен- сионал функции, совокупность ее значений, а скорее на ее интенсионал. Например, смысл функционального выражения в алгоритмике состоит в его сущности как предписания для исполнения одной или нескольких вычислительных операций.

Наша цель — обосновать алгоритмику как теорию оперирования с вычислительными предписаниями и над ними. Аксиоматическое обоснование алгоритмики, которое мы предпримем, лучше всего сравнить с аксиоматизацией теории групп. В математике мы часто встречаем разнообразные предметные области, представляющие собой группы. Точно так же мы, очевидно, встречаем многочисленные замкнутые в себе совокупности вычислительных предписаний, например, геометрические построения, разнообразные языки программирования, предписания о формальном оперировании с алгебраическими или логическими выражениями и т. д. В то время как теория групп работает с понятием умножения элементов группы, в аксиоматической алгоритмике основной операцией является применение функции к аргументу или аппликация f*a. Теория должна прежде всего выявить общие черты таких совокупностей вычислительных предписа-

ний, и цель дальнейших рассмотрений — представить их читателю.

Итак, исходный пункт — понятие функции, понимаемой как вычислительное предписание. Очевидно, что вычислительные предписания могут быть аргументами вычислительных предписаний или переходить из одной роли в другую. Теперь мы делаем большой скачок в неизвестное: мы мыслим вычислительные предписания собранными в одну-един- ственную неструктурированную совокупность. Совсем нс такая точка зрения принята в анализе, где функции из R в R отличаются от функционалов из RR в R и от функционалов более высокого типа, скажем из RR в RR и т. д. Предусмотренное нами слияние типов родственно точке зрения, принятой в теории множеств, где между множествами также нет никаких различий в уровне.

Как известно, в теории множеств упорядоченная пара, состоящая из двух множеств х и у, определяется как множество {{%}, {%, у}} и оказывается, таким образом, элементом множества-степени того множества, скажем R, из которого происходят х и у. В силу экстенсионального понимания функции любая функция из R в R снова оказывается тогда множеством — элементом множества-степени множества определенных выше пар. Поэтому вещественные числа, так же как и функции и функционалы, оказываются просто некоторыми множествами. Именно таким образом теории множеств удается образовать на основе одного-единственного понятия «х есть элемент совокупности у» чрезвычайно многообразно структурированную совокупность математических понятий. Этот методический опыт будет теперь с пользой применен к рассматриваемой совокупности объектов. Бестипо- вое понимание совокупности вычислительных предписаний делает возможным столь же экономный выбор исходных понятий при аксиоматизации, как и в аксиоматической теории множеств. Например, нам не нужно различать одноместные и многоместные вычислительные предписания. Вычислительное предписание F(x,y) с двумя параметрами мы можем понимать как вычислительное предписание /, которое в применении к х выдаст вычислительное предписание (f«), значение которого в точке у равно F^x.yY Эта идея восходит к Фреге и была впервые систематически применена Шейнфин- келем. Он следующим образом иллюстрирует эту идею с помощью функции х — у. Если рассматривать это выражение как вычислительное предписание для одного только у, то оно имеет вид «образовать разность между х и следующей величиной»; мы записываем это вычислительное предписание в виде ^х—). Упомянутое выше вычислительное предписание / должно было бы в применении к х давать это (х—),

Тогда, очевидно,

(f * х) * у = (х —) * у = X — у.

Ясно, что эта идея обобщается и на многоместные функции, т. с. ^(хь^, • хп^ понимается как ((...(f«i)* х2) ... ^Хп) для подходящего f.

Соглашение. Для упрощения записи мы часто будем опускать знак аппликации *, а также некоторые пары скобок, подразумевая группировку влево:

(fxyz) означает (((/* х) * у) * 2).

Предписание «применить вычислительное предписание / к результату применения вычислительного предписания g» само является вычислительным предписанием, которое называется композицией и образует из f и g вычислительное предписание (f°g). Оно действует на аргумент х следующим образом:

(f ° s') * X = f * (g * х\

Этот способ комбинирования f и g нс зависит от каких- либо специальных свойств применяемых функций и их значений. Он сам является вычислительным предписанием и потому должен принадлежать нашей объектной области. Иными словами, мы должны мыслить себе объект В, удовлетворяющий равенству

Bfgx = fgx

для любых f, g, х. Выражение

sin (а + tg (6)) + tg (sin (a + b))

оказывается частным случаем вычислительного предписания F(sin, tg, +, a, by которое определенным образом комбинирует функции sin, tg, +, а также числовые значения а, Ь. Способ комбинирования снова нс зависит от специальных свойств применяемых функций и значений. Будучи вычислительным предписанием (обозначим его через f), оно само должно принадлежать предметной области. Поясним это требование. Приведенное выше выражение использует два одноместных функциональных знака sin, tg и один двуместный функциональный знак +, который мы с помощью описанного выше метода заменим одноместным знаком Ф,

ф ху есть х + у.

После этого приведенное выше выражение запишется с помощью операции аппликации в виде

ф (sin (ф л (tg 6))) (tg (sin (ф ab^,

и мы потребуем существования объекта Д такого, что

f sin tg ф ab — ф (sin (ф a (tg 6))) (tg (sin (ф ab))Y

и вообще

fxyzuv = z (х (zu (yv))) (у (x (2^v)))

для произвольных объектов х, у, г. и, и. Тем самым мы требуем, чтобы в вычислительном предписании / овеществлялось само комбинирование sin, tg и т. д., а не свойства этих объектов. Мы говорим также, что «/ получается в результате функциональной абстракции».

Общие черты этих примеров таковы. Некоторые объекты — вычислительные предписания — рассматриваются как данные. Они комбинируются друг с другом исключительно с помощью аппликации:

f * (g * х) или z * (х * (z * и) * (у * и)) * (у * (х * ((z * и) * v))).

Затем мы требуем существования некоторого объекта

В, соответственно /,

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

Теперь мы выдвинем неограниченную выполнимость этой функциональной абстракции в качестве аксиоматического требования к предметной области.

Комбинаторные алгебры

Пусть А =<Л, *, сь ..., ст> — алгебраическая структура с непустым основным множеством Л, выделенными в нем элементами сь с2) ..., ст, т^О, и двуместной операцией *. Пусть /(xi, ..., хп^ — терм в Л, т. е. пусть / построен из констант, обозначающих выделенные элементы, и переменных хь ..., хп с помощью скобок и знака операции *. Говорят, что элемент / множества Л представляет терм / в Л, если для любого выбора элементов ац ..., ап из Л

faxa2 ... an = t(ab а2> ... ап\

Алгебра Л комбинаторно полна, если любой терм / представим в Л. В этом случае Л называется комбинаторной алгеброй. Она называется нетривиальной, если Л содержит более одного элемента.

Таким образом, комбинация, заданная термом /, всегда представляется в комбинаторной алгебре (хотя бы одним) объектом. Ввиду их происхождения мы называем такие объекты комбинаторами.

Шейнфинкель [Schdnfinkel 1924] и независимо от него Карри [Curry 1930] поставили привлекательный в математическом отношении вопрос: нельзя ли составить все такие комбинации из небольшого их количества. Ответ оказался утвердительным.

Достаточно комбинаторов S и К

Пусть Л = (Л, *, си ..., с^ — алгебраическая структура, где имеется два элемента S и К> тождественно по х, у, z ^ А удовлетворяющие следующим уравнениям:

(S) Sxyz = хх (yz\

(К) Кху = х.

Тогда Л — комбинаторная алгебра. (Обратно, в любой комбинаторной алгебре очевидным образом всегда имеются элементы S и К, удовлетворяющие этим уравнениям.)

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

Лемма. Для любого п и любого терма tn(x\, ..., х^, построенного из S, К и хь ..., хп, имеется терм tn~\^X\, ..., Хл-i), построенный из S, К и хь ..., Хп-х, такой, что

tn—x(%h •••* ^п-* 1) * ^п ^п^Х» •••^п)'

Доказательство. Если /„ есть один из термов 3, К или Xi для I ^ п, то в качестве tn_x берем К1п» Тогда имеет место tn_xxn = №J ^п = tn. Если tn составной, то 1п = tntn> и мы, применяя предложение индукции, получаем 1п = 1п__ххп и 1п = 1п-хХп. Берем теперь Stn-xC-\ в качестве 1п_х и проверяем наше равенство:

tn— \Хп Stn—Xtn—\Xntn—\Хп ^tn—\Xn^ == tntn ^^ tn*

Остается еще случай t ~ хп. Здесь нам нужен комбинатор /, такой, что

(I)1х = х.

Такой комбинатор можно составить из 3, К различными способами. Легко проверить, что годятся SKK (Восковиц) или 3К (КК) (Бернайс). □

Теперь комбинаторная полнота легко получается путем многократного применения леммы:

Ш, xn> = tn_xkxX) .хп„х)хп =

tn — 2^ 1» • • • > ^п — 2) ^п — \^п ^^ • • • ==:: 4Л^2 • * * ^п*

Читатель может заинтересоваться тем, как комбинаторы, приведенные выше в качестве примеров, составляются из 3 и К* Например,

В = 5^К.

Как и в случае /, здесь возможны многочисленные варианты. Другая привлекательная задача — поиск алгоритмов, механизирующих предыдущую задачу.

ЛИТЕРАТУРА

Curry Н В. Grundlagen der kombinatorischen Log\k.— Amer. 3. Math., v.52, p. 509—536, 789—834, 1930; а также написанная с соавторами Combinatory Logic, v. I, II. — Amsterdam: North-Holland, 1958, 1972.

Frege G. Begriffschrift, Halle a. S., 1879 (в четности, § 9). 2. Auflage.— Hildesheim: G. Olms Verlag, 1977.

Schonfinkel M. Ueber die Bausteine der mathematischen Logik. — Math. Ann., B. 92, S. 305—316, 1924. (В приложении, написанном Беманом, указана ошибка, найденная автором после завершения работы.)

Quine W. v. О. On the building blocks of mathematical logic (комментарий к переводу предыдущей работы Шейнфинкеля). In: van Hejenoort, ed. From Frege to Godel. — Cambridge, Mass.: Harvard University Press, 1967.

4 Э. Энгелер

Существование комбинаторных алгебр:комбинаторная логика

Если читатель попытается создать удобный в обращении пример комбинаторной алгебры, то через некоторое время он согласится со мной, что при отказе от различия в типах в значительной степени пропадает математическая интуиция. В действительности многие математики сделали на этом пути шаг от возможного к противоречивому. Первоначальным намерением основателей (Шейнфинкель, Карри и Чёрч) была не только аксиоматизация понятия аппликации для общего понятия функции, но и функциональное обоснование всей логики и математики вообще. В частности, Карри и Чёрч первоначально построили системы, которые с помощью казавшихся разумными предложений присоединяли к комбинаторной алгебре также логические законы и части математики. Эти расширенные системы оказались противоречивыми [Kleene, Rosser 1935]. Карри считает, что это проявление существа дела. Он сравнивает исходные соображения с системой Фреге и указывает: «Мы работаем с объектами столь большой общности, что нам изменяет интуиция. Мы исследуем ничью землю, лежащую между надежным и заведомо противоречивым».

К центральному вопросу о существовании нетривиальных комбинаторных алгебр можно подойти, с разных сторон. Исторически первым был теоретико-доказательственный подход. Ему следовали как Чёрч, так и Карри под влиянием целей и стереотипов мышления программы Гильберта (предусматривавшей доказательство непротиворечивости теории чисел и анализа). Мы сначала обрисуем этот подход, а затем обратимся к другому, алгебраическому.

Теоретико-доказательственный подход рассматривает математическую теорию комбинаторных алгебр как формальнодедуктивную дисциплину. Таким образом, он исходит из системы аксиом и правил вывода, и вопрос о существовании таких алгебр заменяется вопросом о непротиворечивости формальной системы; комбинаторная алгебра превращается в комбинаторную логику.

Комбинаторная логика

Подразумеваемая структура;

Д = (Д, *, S, К).

Язык*.

Термы, построенные из атомарных термов, т. е. из переменных х, у, г, ... и констант S, К с помощью двуместной операции *.

Формулы: равенства термов.

Аксиомы*.

1 = 1 для атомарных термов /,

£/1^з =: ^з (Уз)> Kt\t2 = t\ Для произвольных термов tb ^2> 4*

Правила вывода;

^1 = ^21 = ^2^1^2^1 — ^2 /г — ^3

/^3 = ^2^3 ’/3^1 = /3/2 *^2 " ^1/1 = /3

Доказуемость;

Последовательность равенств аь а2, а3, ..., аЛ называется доказательством, если для любого i = = 1,2, ..., п равенство аг- либо является аксиомой, либо имеются /, к < /, такие, что at получается из а/ и ад по одному из правил вывода. В этом случае равенство ап называется доказуемым.

Так как язык комбинаторной логики, очевидно, чрезвычайно ограничен, в нем нет обычного понятия противоречивости, т. е. выводимости некоторого высказывания А вместе с его отрицаниеим ПЛ. Однако в обычной логике из Л и ПЛ можно вывести любую формулу. Мы возведем этот факт в ранг определения и скажем вообще, что логическая си стема противоречива, если в ней можно вывести все фор мулы соответствующего языка. Тогда непротиворечивость комбинаторной логики будет установлена, если мы сможем показать, что невозможна последовательность равенств ab a2, ..., ая, которая является доказательством и в которой ап есть равенство K = S.

Самое важное в теоретико-доказательственном подходе как раз то, что он освобождает нас от содержательной компоненты в проблеме существования. Мы ставим вопрос чисто формально, т. е. в терминах конечных совокупностей формул: имеется ли последовательность равенств а, обладающая тем или иным свойством? И в нашем случае для ответа на этот вопрос оказывается достаточно простых вспомогательных средств и высказываний о формальных манипуляциях с доказательствами ab ..., ап, см., в частности, приводимую ниже лемму 4. Эти манипуляции мы проведем

с помощью некоторого исчисления редукций, которое интересно и в других отношениях (мы еще вернемся к этому В §5).

Исчисление редукций исходит из замечания, что аксиомы для S и К обладают некоторой естественной ассимметрией: их левую часть можно рассматривать как аргумент, а правую— как результат некоторого упрощающего преобразования или редукции. Последовательное применение таких редукций будет здесь представлено с помощью выводов в некоторой системе аксиом и правил вывода, которая оказывается вполне естественной.

Исчисления редукций

Язык:

Термы такие же, как в комбинаторной логике.

Формулы: высказывания о редуцируемости t\ ^ /2.

Аксиомы:

t для атомарных термов,

Sixth's ^ ЛМ^з), термов.

Правила вывода:

/1^3 ^^2^3 'У1 ^ ^2

Доказуемость:

KUs ^ 11 Для произвольных

^3

Определяется аналогично тому, как это сделано в комбинаторной логике.

Бросается в глаза, что редукции можно применить только к термам, у которых в самой левой внешней позиции стоит S или К. Более общим является понятие конверсии. Если t содержит подтерм вида Shtsts (соответственно вида №1/2) и I' получается из t заменой этого подтерма на /1/3 (/2/3) (соответственно на /1), то мы говорим, что / конвертируется в 1\ Еще более общее понятие одновременной конверсии оказывается более удобным для нас в техническом отношении. Мы пишем /||->/', если в / имеется один или несколько неналегающих подтермов выделенного вида 5^/2^з или Kt\t^ таких, что их одновременная замена на бМ^з) или соответственно на /1 дает терм I'. Это понятие тоже можно сформулировать в виде исчисления.

Исчисление конверсий

Язык*.

Термы комбинаторной логики.

Формулы: 1\\->1'.

Аксиомы*.

/||->/ для атомарных /, SWall-^i^W, WiM-^i Для произвольных tt.

Правило вывода*.

/11|->/1/2||->/2

^2 11"^ ЧЧ

Доказуемость*.

По аналогии с предыдущим.

Очевидно, что Z Ц—^ Zz доказуемо в исчислении конверсий тогда и только тогда, когда Zz получается из / с помощью одной одновременной конверсии. В частности, для любого / выводима конверсия /||->/.

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

Лемма 1. t^f выводимо в исчислении редукций тогда и только тогда, когда найдется последовательность Zo, Zi, • ••> tn, такая, что терм Zo совпадает с t, терм tn — с I' и любое из сооотношений //1|—> ^z+i доказуемо в исчислении конверсий.

Доказательство. Если соотношение t^f доказуемо, то оно либо является аксиомой (но тогда и tW>t' — аксиома), либо получается по правилу вывода. Если мы предположим, что утверждение леммы справедливо для посылок правила вывода, то получим его и для заключения. Пусть, например, последовательность Sj ||-> s2||-> s3||-> ... Ц-* Sn соответствует посылке /1 ^ /2 первого правила вывода. Тогда последовательность 5^3 ||—► S2Z3 ||~> 83(3 ||—> . *. ||—> бДз является искомой для заключения этого правила. Аналогично поступаем и для остальных правил вывода.

Докажем обратную импликацию. Пусть соотношения

^i IH k IF* • • • IH ^п доказуемы в исчислении конверсий. Чтобы построить доказательство /i ^ tn, достаточно в силу транзитивности найти доказательство каждого из соотношений ti ^ ^+ь Итак, пусть доказуемо /|h>1'. Если это аксиома, то снова все в порядке. Если / Ц—> f получается по правилу конверсии, то мы перепишем его в виде Z1/211—> 6/2 и снова рассуждаем по индукции. По предположению индукции из доказуемости посылок ZJI-*^ и ^IH/' слеДУет доказуемость и L^t' Отсюда мы получаем LL^t'.L и Z^O^^X> а

значит, в силу транзитивности также и t\h^ Ms- □

Лемма 2. Если а\\-*пг и а\\^п доказуемы в исчислении конверсий, то по этим доказательствам можно эффективно построить г, такой, что доказуемы m\\-+z и nW-^z.

Доказательство. Пусть сначала а — атомарный терм. Тогда а\\~*пг и а\\-^п — аксиомы, так что а, пг и п совпадают.

Пусть теперь терм а составной, т. е. имеет вид а'а". Снова применим индукцию по длине доказательства.

Если обе формулы а\\-*пг и а IH п — аксиомы, то или обе они начинаются с S или обе с К, так что пг и п снова совпадают, и мы можем взять пг в качестве г.

Если только одна из этих формул, например п|Нт, является аксиомой, то рассмотрим случай, когда а имеет вид Sucw (случай Кис рассматривается аналогично). Тогда пг есть uw^cwY Вторая из рассматриваемых формул, aW-^n, получилась посредством правила конверсии из другой доказуемой формулы. В рассматриваемом случае это правило может иметь только вид Sucw \\->n'w', и заключительная часть доказательства имеет следующий вид. (Мы придали доказательству более наглядную древовидную форму, хотя по определению оно является просто последовательностью формул.)

SIHS uW-^u'

Su |Н / с IH с'

Sue |H n' w IH w'

Sucw IF* n'w'

Таким образом, l есть Su' и n' есть Su'c\ и мы получаем доказательство формулы Sucw Ц-> Su'c'w' в исчислении конверсий. Терм п имеет, таким образом, вид Su'c'w'. Обе формулы Sucw ||->iz^ (utiy) и Su'c'w' ||—>u'w'^c'w'^— аксиомы,

и uw^ow^ \\-^u'w'(u'w') следует из и\\-^и', п||->п' и ш||->иу'.

Так получается диаграмма

Suuw ||-> Su'u'w'Suuw ||-> Su'u'w'т. е.т. е.uw^uw) ||-> u'w' (v'w')uw^uw) ||-> u'w' (v'w')а т mа т mII-»- пТЦ-> гII-»- пТЦ-> г

Suuw ||-> Su'u'w'

Suuw ||-> Su'u'w'

т. е.

т. е.

uw^uw) ||-> u'w' (v'w')

uw^uw) ||-> u'w' (v'w')

а т m

а т m

II-»- п

Т

Ц-> г

II-»- п

Т

Ц-> г

Пусть, наконец, а||->/п и а||"»побе доказаны с помощью одновременной конверсии, т. е. заключительные части доказательств имеют вид

а' ||-> m' a" ||-> nV а' ||-> п' а" ||-> п"а'а” ||-> m'т" И а'а" ||-> п'п"

Применяем предложение индукции отдельно к а' и а". Тогда найдутся 2Z и г", такие, что т' ||->2Z, п' ||->2Z и mzz ||~>2ZZ, nzz ||->2Z/. С помощью конверсии получаем m'm" ||->2Z2ZZ и n'n" \\->z'z". Следовательно, в качестве z можно взять z'z". □

Лемму 2 можно непосредственно перенести на исчисление редукций.

Лемма 3. Если а^ т и а*^ п выводимы в исчислении редукций, то найдется г, такой, что m^z ип^г.

IH а, \\->пгТ ТС Ц 11-*^ТIH а, \\->пгТ ТС Ц 11-*^ТДоказательство. По лемме 1 у нас есть верхняя и левая части следующей диаграммы:

IH а, \\->пг

Т Т

С Ц 11-*^

Т

IH а, \\->пг

Т Т

С Ц 11-*^

Т

а ||—> <^i 11->о2||-> ...

т т

61 И“* ^11 11“* ^12

III

^2 11“* ^21 П“* ^22

т

т bi II-» Сл т т п IHd! ||-> ...

Т ■ Си II-» ег Т Т II-» dj\\ -> 2

Многократно применяя лемму 2, можно дополнить обе стороны диаграммы указанным образом, после чего лемма получается дополнительным применением леммы 1 к правой и нижней сторонам этой диаграммы. □

Лемма 4. По каждому доказательству равенства m = n в комбинаторной логике можно эффективно построить терм z, такой, что в исчислении редукций доказуемы т>г и п^г.

Доказательство. Если пг = п — аксиома комбинаторной логики, то либо пг совпадает с п и является атомарным термом (тогда можно взять пг в качестве 2), либо мы имеем дело с одной из двух «настоящих» аксиом. Рассмотрим, например, аксиому Sabc = ас {be). Но тогда выводимы как Sabc ^ ас{Ьс), так и ac{bc) ^ ас{Ьс); последняя доказывается многократным применением двух первых правил вывода, исходя из аксиом и ^ и для атомарных и.

В случае когда равенство пг = п — результат применения некоторого правила вывода, мы рассмотрим соответствующие случаи. Пусть m имеет вид ab, п — вид ас и рассматриваемое правило — вид

Ь = с

ab = ас *

По предположению индукции для посылки существует терм 2', такой, что b ^ z' и с ^ z'. Тогда в исчислении редукций мы получаем ab ^ az' и ас^ az', и можно взять az' в качестве z. Для второго правила вывода рассмотрение проводится аналогично. Третье правило имеет вид

m = а а = п

m = а

По предположению индукции существуют и и и, такие, что пг ^ и, а^ и, а^ v, п^ v. Теперь применение леммы 3 ка^^иа^и дает существование z, такого, что u^z и d^z. Из транзитивности отношения ^ окончательно получаем m z и п z. □

Теорема. S = K недоказуемо в комбинаторной логике.

Доказательство. Если бы S = K было доказуемо, мы получили бы по лемме 4 терм z, для которого были бы доказуемы S^z и К^г. По лемме 1 можно было бы перевести S и К в z серией конверсий, что очевидным образом невозможно. □

(Приведенное выше доказательство принадлежит по существу Захосу.)

ЛИТЕРАТУРА

Church A., Rosser J. В. Some properties of conversion. — Trans. Amer. Math. Soc., v. 39, p. 472—482, 1936.

Curry H. B. Recent advances in combinatory logic. — Bull. Soc. Math. Belgique, v. 20, p. 288—298 (cm. p. 296—297), 1968.

Engeler E. Zum logischen Werk von Paul Bernays. — Dialectica, B. 32, S. 191—200, 1978.

Kleene S. C., Rosser J. B. The inconsistency of certain formal logics. — Ann. of Math., v. 36, p. 630—636, 1935.

Zachos E. Kombinatorische Logik und S-Terme. — Dissertation ETH Zurich, 1978.

Конкретные комбинаторные алгебры

Сначала я должен извиниться за слово «конкретный». Конкретность описываемых ниже моделей сравнима с конкретностью поля вещественных чисел, построенных в виде дедекиндовых сечений. Таким образом, они конкретны относительно принятого без размышлений субстрата наивной теории множеств. Однако они все же конкретны в той же степени, что и объекты классической математики вообще.

Исходя из этой точки зрения, мы уже создали в предыдущем параграфе предпосылки для конкретизации модели комбинаторной логики — комбинаторной алгебры. Для этого множество термов комбинаторной логики разбивается на классы эквивалентности с помощью понятия доказуемости. Термы t и I' эквивалентны, если можно доказать равенство / = f. Эта эквивалентность является даже конгруэнтностью относительно операции *: если доказуемы tv=fx и t^ = fy то, как легко видеть, доказуемо и /1*/2 = ^*^- ^ак мы ПРИ* ходим к модели из термов.

Эта модель нетривиальна — ведь доказательство непротиворечивости показывает, что S и К лежат в различных классах конгруэнтности.

Модель из термов

Т = термы комбинаторной логики,

/ ~ f т. и т. т., когда 1 = 1' доказуемо. Пусть

t = V\t~t'y

Заметим, что tx ~ t'v /2 ~ /2 влечет /, * /2 ^ /, * /' (конгруэнтность).

Для Л = {71 / g 7"}, где 7i*72 = /1*/2> система А = =ЦА, *, 5, К) является комбинаторной алгеброй. Она называется моделью из термов.

У читателя может возникнуть аналогия между этой конструкцией и построением поля рациональных чисел из натуральных чисел. Там мы образуем классы эквивалентности троек <а,Ь,с>^№ с помощью следующего отношения: <а, Ь, с) ~<а\ V, с'), если можно доказать ас' + Ь'с = а'с + Ьс'. Однако здесь имеется качественное различие. Вычисление, приводящее к доказательству (или опровержению) данного числового равенства, всегда заканчивается за небольшое количество шагов. Поэтому мы готовы называть конкретным построенное таким образом множество Q. Напротив, вопрос о доказуемости равенства 1 = 1' в комбинаторной логике несравненно более труден; как мы увидим, он алгоритмически неразрешим. Элементы ?, из которых состоит модель, не являются алгоритмически отграниченными. Вопрос: как с этой точки зрения выглядит конструкция модели из термов по сравнению с моделью вещественных чисел как дедекиндовых сечений?

При теоретико-множественном восприятии математических структур такое переплетение построения модели и понятия доказательства кажется, мягко говоря, несколько необычным. Однако прошло сорок лет, прежде чем появились первые теоретико-множественные конструкции моделей комбинаторной логики — конструкции Скотта и Плоткина (ср. Barendregt 1977). Теперь имеется еще одна упрощенная и, как мы покажем, универсальная конструкция моделей. Она и будет изложена ниже.

Мы попытаемся реализовать элементы комбинаторной алгебры в виде множеств. График F функции f из множеств в множества снова является множеством, а именно множеством пар {a, /(а)>. Применение функции Д понимаемой как график, к аргументу а, понимаемому как множество {я}, принимает вид следующей операции над множествами: FA {а} = {6 |3х ^=ДаУ^ Ь) е ру

Эта операция А определена для произвольных множеств М, N из теории множеств: М AN = {у| Эх е N. (х, у) е М}. Однако с помощью этой операции мы не сможем сделать никакой комбинаторной алгебры из теории множеств. Мы применим следующую операцию:

М * N = {у | Эх е N.(x, у)^ М ^x конечен}.

Применять в этой конструкции всю теорию множеств, видимо, слишком избыточно, и окажется, что мы строим множества, множества множеств и т. д. лишь в той мере, в какой это в действительности требуется ниже при доказательстве комбинаторной полноты. Эти рассмотрения приводят к следующей кбнетрукции. Чтобы выявить функциональные связи, мы пишем V^yY вместо <х, у). Кроме того, мы при-

меняем в дальнейшем малые греческие буквы а, р, ... для обозначения конечных множеств.

Графиковые модели

Пусть А^0. Определим G^A^ рекурсивными соотношениями .

Go (Л)-Л;

Сп+1(Д) = С„(Д)и{(а-*^)|а = О„(Д)}, а конечно, угОп (Д).

Пусть G (Д) = U Gn (Д), и пусть В — множество-сте- п >0 пень множества G(A).

Положим М * N = {у | За £ ^.(а -> у) е М),

^ = {М-^(0->у))1уес(Д)},

5 = {{т->({гь .... rrt)->s)}->({*!-► Пап —> гп} —*

-> (а -> s)) | п > 0,Г!гпеВ,

т (J U ^i = О' — 5, о конечно}.

Тогда 6 = (В, *, S, К) — комбинаторная алгебра.

Нам нужно, во-первых, показать, что В — действительно комбинаторная алгебра, и, во-вторых, что наша конструкция действительно имеет обещанный универсальный характер. Последнее вытекает из следующего предложения.

Теорема о вложении. Пусть Л =<Л, •> — алгебраическая структура с двуместной операцией •. Тогда Л можно изоморфно вложить в В =<В, *>.

Доказательство. Вложение /: А-^В составлено из отображений /V. А-^В следующим образом: 1^ = U Ма).

Здесь для a. G Л полагаем/о («) = {«},f^(«) = fn(a)U{({a'}-*6)la' gA- befn(a-a')}.

Отображение f инъективно, так как fWft А=ДаУ Кроме того, имеет место f(a)*f(b) = f(a)‘f(b). Действительно,

f № * f (6) = {z/1 Ba с f (6),(a ->y) s f (a)}

= U {y|3asf(6).(a->y)ef/+1(a)}

0<i

= и Ky\Wb}-^y}efmta}}

= U VtiXy^h (а ■ b)} — f (а ■ b). □ o<z

Чтобы доказать, что В— комбинаторная алгебра, нужна механическая проверка. Итак, пусть М, L, N — произвольные подмножества множества 6(Л). Тогда имеем

£MAr = {s|3asM3p sM.(0^(a^s))<=£}

= {s | {s} c ^.({s} -^ (0 -> s)) e K} = M.

ML (NL) = {s 13p s NL.^p ^s)^ ML}

= {s|3n>03rb .... rne С(Л)3<ть ..., on^L.

({/b • • •, fn} -> s) e ML A (a, -> rj, ..., (azl -* r„) e N} = {s 13n ^ 03rb ..., rn e G (Л) 3ab ..., a„ s L3t G L. (T-*({rir^^s^e/WAfff^r!)(<r„-* r„) e W}. SMNL = {s 13o c £3n s N3e s M.(e -* (4 -> (a -^ s))) e 3}

= {s 13<r s L3n^03r,г„еС(Л)Зг, o-j ..., QnsL.

(T->({nrn}->s}}e M

(tfi -* П)(crn -> rn) e vV А <т = т U U "J

= {s I Эм > ОЗп, ..., rn e G (Л) 3т, ab ..., on c L. (т->({гь .... rn} -> s)) г M ^ (oj -> rj, .... (o„ -> rn) e N}.

S^K: ({a}->(0->a))^S.

Тем самым мы получили следующее утверждение.

Теорема существования. В — комбинаторная алгебра. □

В качестве полезной иллюстрации комбинаторной полноты мы рассмотрим типично алгебраическую проблему, а именно: разрешимость уравнений в комбинаторной алгебре, точнее — вопрос об уравнениях вида

F-Х = Х.

Явное нахождение такой неподвижной точки означает получение решения X в виде комбинации F и исходных комбинаторов 3 и К. Но тогда можно искать такое представление в виде YF. Это делается с помощью следующей конструкции, Пусть р — комбинатор, удовлетворяющий равенству

Dxy — x(yy).

Он существует в силу комбинаторной полноты. Пусть У — комбинатор с определяющим равенством

Yx = Dx(Dx).

Неподвижная точка комбинатора F, т. е. решение уравнения FX = X, может быть теперь получена в виде YF. Действительно,

YF = DF фР) = F (ФР) (DF)) = F фр\

Теорема. YF — наименьшая неподвижная точка комбинатора F в графиковой модели.

Доказательство. Мы уже доказали, что YF — неподвижная точка. Пусть X — еще какая-нибудь неподвижная точка. Нужно показать, что YF, рассматриваемое как подмножество множества G (Л), содержится в X. Пусть М = DF, так что YF = ММ.

YF = ММ г X следует из того факта, что аа s X для всех конечных а г М. Действительно, если а е ММ, то существует а£М, такое, что (а-*а)е М. Но тогда имеется конечное р, такое, что а е РР; можно взять p = a|J{a->a}-

Пусть а — произвольное конечное подмножество множества М. Так как М Ё G (Л) = (J Gn (Л), то а есть подмно- п

жество множества Сл(Л) для некоторого минимального п. Следовательно, мы можем воспользоваться индукцией по п. Если а^С0(Л) = Л, то а-а = 0 ^Х. Пусть уже доказано, что аа ^ X для всех а гМ, ос ^ Gn-\ (Л), и пусть р £ Gn (Л), р $ Gn_x (Л), р ^ М, а^ рр. Нужно показать, что а еХ. Так как а е рр, то имеется у s= Р, такое, что (у-^а)^р. Отсюда следует, что у^ С«-1(Л) и тем самым уу^Х по предположению индукции. Так как (у —> а)е р М, то а е Му = ^(уу) по определению множества М. Кроме того, из p^q^G(A) вообще следует Fp^Fq. Так как уу г X, то, в частности, F(yy)^ FX = X и тем самым а ^ F^^^Х. откуда а^Х. □

В графиковой модели наименьшую неподвижную точку можно найти не только описанным выше явным способом, но и с помощью следующей привлекательной теоретико-множественной конструкции. Легко показать, что она равна

и^0,п

где F^I, Fn*x = BFnF, т. е. F°0 = 0, FnU0=FnF0.

ЛИТЕРАТУРА

Barendregt Н. Р. The type free lambda calculus. In: J. Barwise. Handbook of Mathematical Logic, p. 1091 —1132. — Amsterdam: North-Holland, 1977. [Имеется перевод: Справочная книга по математической" логике. Т. 4. — М.: Наука, 1984.]

Engeler Е. Algebras and Combinators. — Algebra Universalis v. 13, p. 389—

Meyer A. What is a Model of the Lambda Calculus? — Report MIT/LCS/TM- 171 (соотв. TM-201), 1980 (1981).

Ламбда-исчисление

Напомним еще раз, что означает «комбинаторная алгебра»: для любого терма Цхххп) в В имеется элемент Г, такой, что для любых Л4Ь ..., Мп^ В

ТМХ ...Мп = ЦМх, Мп\

Таким образом, вычислительное предписание / конкретизируется в объекте Т. Переход от терма / к объекту Т в приложениях отражает существо дела. При этом возникают некоторые неудобства из-за того,что одному и тому же / может соответствовать несколько совершенно различных Т. Вот простой пример. Мы использовали в свое время комбинатор / со свойством IN — N для всех N. В В имеются по меньшей мере два таких /:

/0 = {({а} -> я) | я е G (Л)} и 1Х = {(а —> а) | а е а г G (Л)},

а на самом деле много, много больше (какие?). Выход, если он возможен, состоит в предъявлении конструкции, однозначно сопоставляющей каждому М элемент М из В, дающий ту же самую аппликацию к произвольному N: MN=MN. Разумеется, мы хотели бы осуществить эту конструкцию снова в виде комбинатора L. Это приводит к определению А-алгебр.

А-алгебры

L-алгебра — это структура

В = (В, *, S, К, L)

с двуместной операцией * и элементами S, К» L, удовлетворяющими следующим условиям:

Кху = х,

Sxyz = xz (уг).

Lxy = xy,

^y.xxy = X^ ZD Lxx = Lx2.

В графиковой моделе определим L в виде подмножества множества 6 (Л).

Лемма. Полагая L = {{а -> 6} -> (р -> 6) | а ^ 0 г G (Л), b е е G (Л)} для конечных а, (3, мы превращаем графиковую модель в L-алгебру.

Доказательство. Если b е MN, то имеется а^ N, такое, что (а~> b^^ М. Тогда (а-> 6)е LM, а значит, и b^LMN. Обратно, если b^LMN, то (P~>&)eLA4 для некоторого Р с N, т. е. (а->6)еЛ4 для некоторого а ^ Р, а потому b г MN. Отсюда следует LMN = MN для всех М и N.

Для доказательства последнего требования из определения L-алгебры допустим, что LMX^ ЬМ2, например (а->&)е LMx"n ^a-^b)^ LM2. Из (a->b)elX следует существование некоторого р ^ а, такого, что (р->6)еЛ11. Для этого Р верно 6еЛ11Р. Так как, с другой стороны, (a->b)^LM2, то невозможно у Е а, такое, что ^~^Ь)еМ2) в частности (Р~>&)^ТИ2, и, следовательно, 6^Л12р. Поэтому неверно, что MXN = M2N для всех N. □

Как мы только что видели, в L-алгебре можно конкретизировать любое вычислительное предписание /(х) в однозначно определенный объект Ы\ для которого верно LTx = /(х) при всех х. В силу комбинаторной полноты Т можно построить в виде выражения, составленного из S и К. Однако этот способ построения и особенно его описание оказывается довольно громоздким; с другой стороны, само понятие функциональной абстракции столь важно, что буквально вынуждает ввести короткий и выразительный метод записи. В отличие от теоретико-множественной абстракции, т. с. перехода от свойства Е^х) к его экстенсионалу {х|£(х)}, функциональная абстракция пока еще не проникла в повседневную математику, хотя она могла бы внести большой вклад в прояснение понятий.

Для иллюстрации ламбда-записи, вводимой ниже, мы приведем два примера из повседневной практики математиков.

Что значит «функция Зх2+1»? Если кто-то хочет быть точным, он вводит по этому поводу функциональный символ, например Д и говорит: «функция Д R -> R, определенная со-

отношением f(x) = Зх2 + 1». При этом очевидно, что переменную х можно здесь, не меняя смысла, заменить на другую переменную у, так что х— связанная переменная. Ламбда-запись устраняет произвольность в выборе / в качестве функционального символа. Она предлагает вместо / выражение «Хх.Зх2 + 1». Поэтому значение выражения (Хх.Зх2 + 1)2 равно 13. Таким образом, ламбда-запись преодолевает нерегулярность обозначений при обычном функциональном способе выражения.

Пусть Р— оператор, т. е. сопоставление функций функциями. У малообразованного математика можно встретить обороты вроде «пусть Цх) — функция, и положим g(x) = Р(^х^». Это в общем случае ведет к недоразумениям. Например, что такое P(f(x— 1))? То ли это P(f) (х— 1), то ли P^g^x), гДе g^ = Нх~ 1)? А это не 0ДН0 и то же, как показывает следующий пример. Пусть Р определен соотношением

{

О для х < О,

/ (х) в противном случае.

Тогда

(0 для х < 1,

Р^П^х- 1) = < п п

( /(х—1) в противном случае,

(0 для х^О,

Р (§") to = ) 5 / IX

( /(х—1) в противном случае.

Математики, не получившие формалистической выучки, вводят в нужных случаях символы и соглашения, устраняющие такие недоразумения; стоит только вспомнить о введении оператора дифференцирования! И снова ламбда-запись дает равномерный и экономный метод достижения той же цели.

Здесь мы займемся одним и только одним полезным приложением ламбда-записи — в качестве способа обозначения терма LT, который строится для /(х), чтобы гарантировать равенство LTx = t^ для всех х. Этот терм будет также обозначаться через кх.ЦхУ

Определение. Пусть /(xi, ..., х^х)— терм комбинаторной логики, построенный из S, К, L и переменных хь ... ,хп, х. Пусть Т— терм, который построен из S, К, L и хь ..., хп, согласно лемме из § 1, и для которого верно Т*х = Цхх, ..., х^, х) для всех хь ..., хп. Тогда ХхДхх, ..,, хт х) обозначает терм LT,

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

Принятая нами обратная последовательность — рассмотрение ламбда-алгебр до ламбда-исчисления — была избрана по педагогическим причинам. (См. также введение к § 2.)

Соглашение. Для термов tx, /2 и переменной х обозначим через ^ |£2 результат замены всех свободных вхождений переменной х в fi на /2. При этом следует сделать переименования переменных, чтобы свободные вхождения переменных в /2 не попали в область действия X по тем же переменным в Л.

Исчисление ламбда-конверсии

Язык*.

Термы строятся из атомарных термов, менных и, возможно, констант, с помощью операции * и ламбда-абстракции: если х — переменная, то ^ХхЛ) — снова терм.

Формулы — это равенства термов.

Аксиомы:

1 = 1 для атомарных термов,

Xx.t = Quj.t |0 (переименование), (ЛхЛх) /2 = 1х £2 (0-редукция).

Правила вывода:

/1 ~ /2Л = /2Л = /2

т. е. пере- двуместной / — терм и

ЦЦ ~ Vd*3*1 ” ^3^2^2 == t\

t\ = /2^2 ^ ^3Л " ^2

/1 = /3’ Xx.tx = Xx.t2 *

Доказуемость:

Определяется так же, как в комбинаторной

логике.

Теорема. Любая L-алгебра является моделью исчисления ламбда-конверсии. Иными словами, в L-алгебре можно опре-

делить операцию ламбда-абстракции таким образом, что аксиомы верны, а правила вывода сохраняют истинность равенств.

Доказательство. Мы устроили все наилучшим образом. Действительно, пусть В = (В, *, S, К, L) есть L-алгебра. Истинность равенства 1Х = /2 в В означает, что при любой оценке переменных элементами множества В значение терма /1 — то же, что и значение терма /2. Под «значением» мы понимаем результат, получаемый, согласно построению терма, с помощью операции аппликации * или ламбда-абстракции (т. е. LT^ в соответствии с их определениями в В-ал- гебре. После этого указания доказательство сводится к простой проверке. Например, доказательство для аксиомы (3-редукции состоит в следующей индукции по построению терма tx.

Если /1 есть переменная х, то Т по определению есть SKK И ^x.tx = LT = L(SKKY Поэтому ^x.tx^ t2 = L (SKK) /2 = = /2 = х|£. Если tx — переменная, отличная от х, или S, К, L, то Т определяется как Ktx и имеет место (Xx.tx^ = L(Ktx)t2 = — Ktxt2 = txVx. Если, наконец, данный терм — составной, т. е. имеет вид 6-/2, то соответствующий Т определяется как STXT2, где Тх и Т2 можно найти по предположению индукции. Тогда

(*Кх.1х1^ (з = L (STХТ2) /3 = STхТ21з = Т1/3 (Г2/з)

= (LTX^ (LT2^ = tx £ • /2£ = (tx * /2) 1^.

Из правил вывода рассмотрим только последнее. Пусть истинно tx = /2, т. е. tx (х) = t2 (х) выполнено для произвольных оценок переменной х элементами множества В. Пусть Тх и Г2 снова определены таким образом, что tx(x) = Tx-x, t2(x) = T2*x. Тогда Bi-x = B2-x для всех х, и потому в нашей В-алгебре истинно LTxx = LT2x для всех х из В. Тогда Xx.tx = Хх./2 тоже верно в В по определению ламбда-абстракции. □

Читателя может заинтересовать тот факт, что константы S, К, L не обязательны для построения исчисления ламбда- конверсии, хотя мы и допустили их использование. В действительности легко можно определить элементы с соответствующими комбинаторными свойствами с помощью ламбда-термов. Например, S можно представить термом Хх.Ху.Кг.хг^гУ Кроме того, определение В-алгебры, в котором одна из аксиом есть импликация, а нс равенство, может

показаться несколько неизящным. В действительности недавние исследования позволили дать аксиоматику, состоящую только из равенств (ср. [Barendregt 1981], гл. 7).

ЛИТЕРАТУРА

Barendregt Н. Р. The Lambda Calculus, its Syntax and Semantics, Studies in Logic, 103. — Amsterdam, North-Holland, 1981. [Имеется перевод: Барендрегт X. Ламбда-исчисление, его синтаксис и семантика.—М.: Мир, 1985.]

Church A. The Calculi of Lambda-Conversion. — Princeton, NJ: Princeton University Press, 1941.

Scott D. S. Lambda calculus: some models, some philosophy. In: Barwise et al. The Kleene Symposium, Studies in Logic, 101, p. 381—421. — Amsterdam: North-Holland, 1980.

Scott D. S. Relating theories of the X-calculus. In: Seldin et al.: To H. B. Curry; Essays on Combinatory Logic, Lambda Calculus and Formalism, p. 403—450. — New York: Academic Press, 1980.

Вычислимость и комбинаторы

В этом параграфе мы кратко коснемся связей комбинаторной алгебры и логики с теорией рекурсии. Они будут свидетельствовать о том, что понятия комбинаторной алгебры действительно служат цели, для которой они были введены. Мы исходим из мысли уточнить понятие «вычислительного предписания» с помощью объектов некоторой алгебраической структуры. С другой стороны, оно, как известно, дается и понятием частично рекурсивной функции — это тезис Чёрча. Поэтому остается показать, что каждая частично рекурсивная функция соответствует некоторому комбинатору, который в применении к подходящим объектам-числам дает то же самое.

Во-первых, мы воспользуемся возможностью с самого начала явно встроить объекты-числа в конструкцию графиковой модели 6, а именно выберем N в качестве исходного множества А. Каждому натуральному числу п мы можем сопоставить в качестве представителя элемент {п} модели В. Мы используем сокращение п для {п}. Кроме того, исходным функциям теории рекурсии

функции следования N: N(n) = nA-^ ^^N,

нулевой функции Z: Z^ = Q, n^N, мы сопоставим определенные подмножества множества G(N), а именно

N = {W -> n + 1 | n е N},

Z = {{n}~>0|neN}.

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

UT: U?U\, ..., nm) = nt, l<i<meN.

Для функций U? имеется комбинатор UT> для которого верно определяющее равенство

U i X1Х2 • • • Хщ — Х[.

Выбранные таким образом объекты комбинаторной логики представляют соответствующие числовые функции очевидным образом:

Nn = m т. и т. т., когда N(n) = m,

U^n^ ... rtm = к т. и т. т, когда U? (пъ ..., пт) = 6,

и аналогично для Z. В общем случае поступаем так.

Определение. Частичная функция f; Nn->N называется представимой в В, если в В существует объект F, такой, что Fkxk2 ... kn = m верно в В тогда и только тогда, когда /(6Ь 62, . ., кп) определено и равно ш. В этом случае говорят, что F представляет f.

Теорема. В определенной выше графиковой модели представима любая частично рекурсивная функция.

Доказательство. Мъ\ используем определение множества частично рекурсивных функций как замыкания исходных функций Z, N, U? с помощью схем композиции, примитивной рекурсии и ц-схемы.

Представимость исходных частично рекурсивных функций встроена в В так же, как и объекты-числа.

Замкнутость относительно композиции:

Пусть f (хь . . ., Х„) = A (gl (х,, ..., Х„), . . ., gm (хь ..., х„)), где Н представляет h и при каждом i объект Gt представляет функцию gx. В силу комбинаторной полноты существует F, такой, что Fxx ... хп — Н (G^! ... х^ (G^Xj ... хп). Убедимся, что F представляет f. Имеем Fkx ... kn — = Н (Gxkx ... k_n) ... (Gmky ... An)). Это (в случае когда все gxKkxАп) определены) равно

Hgx(kxkn) ... gm(kx, ..., kn) =

A tei (A,kn), ..., gm(kxkn)) при выполнении соответствующих условий.

Замкнутость относительно примитивной рекурсии: Для наглядности ограничимся одноместными функциями. Итак, пусть

/(п) = если а = 0, то к, иначе g(f(n — 1), п — 1), где g представлена объектом G. Мы намерены применить комбинатор неподвижной точки У, но проведем некоторую подготовку. Сюда относятся построение функции предшествования и разрешающей функции, соответствующей операции если .то иначе. Полагаем

У = {{n + l}_>neN},

откуда сразу видно, что Vn = k т. и т. т., когда п > 0 и к = п — 1. Для построения разрешающей функции нам нужен объект Zero, такой, что

{

М, если х = 0,

N, если x = n+J для некоторого

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

Zero = {{0} -> х | х ее £} U {{^-М} —> х\х ее KL п е N}.

Действительно, в этом случае ZeroO = K и Zeron-V I = KL откуда ZeroOMN=KMN=M и Zeron+1MN=KJ MN=IN=N. Применяя объекты V и Zero, мы можем переписать примитивную рекурсию в виде уравнения для неподвижной точки. В силу комбинаторной полноты находим R, такой, что

R^x = Zeroxk (G (/ (Ух)) (Ух)).

Искомый представитель функции / — это неподвижная точка Rf = f, которую дает YR. И действительно, YR решает уравнения рекурсии:

у/?о = 5 № ° = ZeI°— <9 та @ (уо)) = к = /(0), YRn+X = R(YR)n+\ = Zeron-yVk (G((У Я)(Уп+ I))(№))

= 5 та = Gf^n=g(L(^ =f(^+i).

To, что У/? является к тому же наименьшей неподвижной точкой, гарантирует нам, что он представляет искомое решение рекурсивных уравнений.

Замкнутость относительно р-схемьп

Пусть f (х) — цу [^(х, у) = 0], и пусть g представлена объектом G. Как известно, / можно следующим образом ввести с помощью если ...., то ..., иначе

/г(х, у)= если g^x, у^ = 0, то у, иначе h^x, у + 1);

Цх) = цХ1 0).

В соответствии с этим мы рассматриваем

Rhxy = Zero (Gxy) у ^Нх (Ny^, Н = YR, Fx = НхО.

Чтобы проверить, что F представляет /, делаем следующие вычисления:

Fn = ^° = (YR) п0_= R (YR) n0 = RHnO

Г 0, если g(n, 0) =0,

= Zero(Gn0)0(Hnl)=<

- vНп\ в противном случае.

Далее, вычисление значения Нп1 происходит так:

f 1, если g(n, 1) = 0, Нп\ = RHn\ =Zero(GnV) 1 (Нп2) = s

нп2 в противном случае.

И так далее для //м2, НпЗ, ... . Таким образом, во всех случаях будет найдено истинное значение Fn. Если же ни одно из вычисляемых выражений Gn£ не дает числового значения, то, как и задумано, Fn не получает значения, но ведь в этом случае /(м) не определено. □

Итак, мы показали, что в некоторой комбинаторной алгебре все вычислимые функции могут быть представлены объектами. В действительности это возможно во всех комбинаторных алгебрах. Чтобы показать это, достаточно определить в любой комбинаторной алгебре объекты-числа 0, 1,2, ... и заменить специальные конструкции, использованные для ^, Z, V, Zero, на комбинаторы, имеющиеся во всех таких алгебрах.

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

Определимые числовые функции

Частичная функция /: Nn->N называется определимой» если имеется терм F комбинаторной логики, такой, что

Fkx ... kn = m выводимо т. и т. тм когда f Цгъ ..., к^ определено и равно т.

Теперь мы проведем намеченные выше обобщения в рамках формального подхода, то есть определим комбинаторы п (п^ N), N, Z, V и Zero. Тогда получится следующее утверж^ дение.

Теорема. Любая частично рекурсивная функция определима в комбинаторной логике.

Для упрощения приводимых ниже определений мы будем пользоваться ламбда-обозначениями для определенных комбинаторов: ХхДх") будет обозначать построенный в § 1 из S и К терм 7, такой, что 7х = /(х) для всех х. Введем еще обозначение

Xxyz.t для XxAy.Xz.t»

так что

^Ххуг.Цх» у, z)) MN L = t (Mt N, L)

и аналогично для любого числа связанных переменных.

Упорядоченная пара

Р :=Хио.Хх.хии

(спаривание)

Р0:=Хи.иК

(первая компонента)

Рх :=Хи.и(КП

(вторая компонента)

Сокращения: Рау

= \и, v], Рои = (и)о> Pxu = ^v

Лемма. Комбинаторы Р, Р^ Рх определяют • спаривание^ т. е.

Yu, у]0 —w, \и> ^h

Доказательство. Проведем вычисления.

[zz, v]0 = Ро (P^v) = (Хх.хис) К = Кис = и,

Vu, v]! = Р! (Рис) = (Хх.хис) (КП ис = 1с = с.

Натуральные числа

Определим с помощью рекурсии комбинаторы 0, 1, 2, ..., которые будут определять натуральные числа:

0:= Л £:=[0,! = \п, ^].

Различны ли комбинаторы, сопоставленные различным натуральным числам? С формальной точки зрения различие может означать только доказуемость соотношения п^т. Однако это бессмысленно, так как это соотношение вообще не является формулой комбинаторной логики и тем более не может быть доказуемо. В § 2 в похожих обстоятельствах (верно ли S = КН мы приняли точку зрения, что нужно лишь установить недоказуемость равенства. Затем в § 3 это соглашение было положено в основу построения модели из термов, когда доказуемо равные термы были собраны в один класс эквивалентности. При установлении недоказуемости равенства S = К существенны были лемма 1 и лемма 4, согласно которым равенство п = m доказуемо в точности тогда, когда m и п могут быть редуцированы к одному и тому же 2 с помощью конверсий. Так как S и К, очевидно, уже не конвертируемы дальше, то равенство S = K не может быть доказуемо.

Определение. Говорят, что терм / комбинаторной логики находится в нормальной форме, если его нельзя редуцировать дальше в исчислении конверсий.

Следствие. Если /1 и /2 синтаксически различны и находятся в нормальной форме, то 1\ = /2 недоказуемо в комбинаторной логике. □

Лемма. Любой комбинатор п при п е N находится в нормальной форме.

Теперь сцена готова, и мы вводим следующее определение.

Теоретико-числовые комбинаторы

Z :=Лх.О,

У:=и.[х, /<], V := ХхАА,, Zero-.= Xx\xWKI)K.

Соответствующие обоснования проводятся легко:

Zn = (А,х.О) п — 0.

Nn = (Лх.[х, КА)п = \п, ^] = п + I.

у (Nn) = (Хх.(х)о) (W = (Wo

= ((Хх.\х, КД ) п)0 = [п, £]о = п.

Zejo0 = ^x\x\ (KI) W = (0)1 (KI) К

= 2 ^0 WD ^L ^П wn к = (кп (кп к=iк=к.

Zero (Nn) = (Хх.(х\ (KI) К) Vi, К]

= h, KL (KI) К = К (КП К = KL

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

В заключение этого параграфа мы еще рассмотрим вкратце вопрос о разрешимости в комбинаторной логике.

Проблема остановки в комбинаторной логике

Здесь рассматривается вопрос о том, имеет ли нормальную форму данный терм / комбинаторной логики. [Что эквивалентно вопросу о том, останавливается ли процесс редукции данного терма. — ПеревД Этот вопрос неразрешим, если невозможен комбинатор Н,

такой, что

( 0, если / имеет нормальную форму,

Hl = 2

" I 1 в противном случае.

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

Теорема. Проблема остановки в комбинаторной логике неразрешима.

Доказательство. Допустим, что такой комбинатор Н существует. Мы используем его, чтобы построить комбинатор D, такой, что

^ Г К (tf), если (//) имеет нормальную форму,

[ S в противном случае.

Он строится очевидным образом:

D := M.Zero (Н (//)) (К (//)) S,

и терм Dt имеет нормальную форму для любого I, значит, имеет ее и терм DD. Но, согласно определению D, комбинатор DD равен в этом случае нормальной форме K(DD), отличной от DD. Это дает противоречие. □

ЛИТЕРАТУРА

Hermes Н. Aufzahlbarkeit, Entscheidbarkeit, Berechenbarkeit; Einfiihrung in die Theorie der rekursiven Funktionen. — Berlin, Springer-Verlag, 1961.

Kleene S. C. X-definability and recursiveness. — Duke Math. J., 2, 344—353, 1936.

Артин 24, 25, 36

■Архимед 9, 18, 19, 85

Зенон 20

Кавальери 19, 37

Банах 52

Беркли 32

Бернайс 13, 16, 74, 97

Бет 75

Бойаи 56

Борсук 56

Восковиц 97

Брауэр 35, 36

Буль 13

Кантор 13, 52

Карри 96, 98

Коллинз 34

Коши 38

Коэн 25, 52, 53

Крайзель 25, 36

Кривин 25

Кэли 33

Кюршак 85

Валлис 20

Ван дер Варден 25, 33

Вейерштрасс 25, 38

Вейль 56

Виет 20

Левенгейм 38

Лейбниц 12, 13, 37, 42

Ленгдорф 22

Ли 56

Лось 42

Галилей 19, 20

Гаусс 56

Гёдель 13, 51—53

Мальцев А. И. 38

Гельмгольц 56

Гильберт 9, 13, 36, 64, 67, 83, 87

Ньютон 37, 55

Гонсет 55

Падоа 75

Папп 62

Дедекинд 7—9, 13

Дезарг 60, 61

Декарт 21

Демокрит 20

Паскаль 62

Паш 64

Пеано 10, 13, 50

Пирс 13

Плоткин 106

Понселе 32, 33

Евдокс 18, 20

Евклид 18

Ершов Ю. Л. 22

Протагор 20

Пьери 73, 78

Рабин 34

Зайденберг 31, 32

Захос 104

Рассел 13—15

Риман 50

Робинсон 36, 38

Розенблум 32

Ролль 25

Хамель 75

Хенкин 74

Цермелло 15

Скотт 74, 106

Скулем 38, 39, 42

Спиноза 13

Цорн 39

Чёрч 13, 98, 112, 122

Тарский 22, 32, 34—36, 33, 52, 67, 72

Шейнфинкель 93, 96, 98

Шрёдер 13

Шрейер 24, 25

Штурм 23, 24

Уайтхед 13, 14

Шюттег 33

Эйлер 32, 33, 37

Фишер 34

Фреге 13—15, 93, 98

Фрейденталь 56

Якоби 33

Аксиома Архимеда 9, 18, 45

— выбора 21, 51, 52

— Паша 64

— пересечения прямой с окружностью 84

— полноты 16, 21, 65, 68

— свертывания 21

Аксиомы геометрии 70

— инцидентности 59

— конгруэнтности 67

— линейной алгебры 70

— параллельности 59

— Пеано 10, 50

— порядка 16, 18, 64

Алгебра комбинаторная 96, 110

— комбинаторно полная 96

L-агебра НО

Аппликация 92

Арифметизация континуума по Дедекинду 7

Архимедова система величин 17

Аффинные построения 81

Базис Хамеля 75

Бесконечно большой элемент 44

— малый элемент 44

Категоричность системы аксиом 9

Комбинатор 96

Комбинаторная алгебра 96, НО

— логика 98

Комбинаторно полная алгебра 96

Композиция 94

Конверсия 100

— одновременная 100

Континуум-гипотеза 52, 53

Ламбда-запись 111

Лемма Цорна 39

Логика высказываний 14

— классов 14

Метод Падоа 75

Модель из термов 105

Нормальная форма терма 120

Определимая частичная функция 119

Геометрический класс 58

Геометрическое отношение 58

Евклидово упорядоченное поле 84

Евклидовы построения 83

Идеальное исчисление Фреге 15

Интенсионал 92

Исчисление конверсий 101

— ламбда-конверсий 113

— предикатов 14

— редукций 100

Парадокс Банаха — Тарского 52

— Рассела 15

Пифагорово упорядоченное поле 83

Пифагоровы построения 83, 86

Полнота системы аксиом 71

Представимая частичная функция 116

Представимый терм 95

Присваивание 80

Проблема Гильберта 17-я 36

— остановки 122

— Понселе 32

— Эйлера 32

Противоречивая логическая система 99

Прямая степень 39

Разрешающие операции 80

Разрешимость системы аксиом 71

Стандартная часть 44

Стандартный элемент 43

Степень бескванторной формулы

26

Схема Тарского 67

— рекурсии 51

Теорема Брауэра 35

— Гёделя о непротиворечивости

50

— Дезарга 61

— Коэна о независимости 53

— о вложении 107

— Паппа 62

Паскаля 62

— свертывания 51

— Скулема — Лося 42

— существования 108

Тарского 32, 35

Фишера — Рабина 34

Штурма 23, 24

обобщенная 24

Теория отношений 14

Функция 91

Экстенсионал 14, 92

Экстенсиональность 20

Элементарная теория вещественных чисел 16, 22

вещественно замкнутых полей 24

Элементарное вложение 43

Элементарный анализ 20

ОГЛАВЛЕНИЕ

Предисловиепереводчика . 5

Предисловие 6

Глава I.Континуум7

Что такое вещественные числа?7

Язык как часть математики12

Элементарнаятеориявещественныхчисел22

Нестандартный анализ37

Аксиома выбораиконтинуум-гипотеза48

ГлаваII.Геометрия55

Пространство и математика55

Аксиоматизация посредствомкоординатизации . . . 57

Вопросы теории науки и методы элементарной геометрии 68

Геометрические построения80

ГлаваIII.Алгоритмика91

Что такое вычислительное предписание?91

Существование комбинаторных алгебр: комбинаторная логика98

Конкретныекомбинаторные алгебры105

Ламбда-исчисление*НО

Вычислимостьикомбинаторы115

Именной указатель . . 123

Предметный указатель ,, , . 125

УВАЖАЕМЫЙ ЧИТАТЕЛЬ!

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

129820, Москва, И-НО, ГСП,1-й Рижский пер., д. 2,издательство «Мир».

Учебное издание

Эрвин Э н г е л е р

МЕТАМАТЕМАТИКА

ЭЛЕМЕНТАРНОЙ МАТЕМАТИКИ

Научный редактор Г. М. ЦукерманМл. научный редактор Л. А. Королева

Художник А. В. Шипов

Художественный редактор В. И. Шаповалов Технический редактор И. И. Володина

Корректор Т. П. Берлизова

И Б № 5937

Сдано в набор 07.04.86. Подписано к печати 14.11.86. Формат 60X 90V16. Бумага кн.-журн. сыкт. Печать высокая. Гарнитура литературная. Объем 4,0 бум. л. Усл. печ. л. 8,0. Усл. кр.-отт. 8,25. Уч.-изд. л. 6,43. Изд. № 1/4567. Тираж 14 000 экз. Зак. 178. Цена 50 коп.

ИЗДАТЕЛЬСТВО «МИР» 129820, ГСП, Москва,И-110, 1-й Рижский пер., 2

Ленинградская типография № 2 головное предприятие ордена Трудового Красного Знамени Ленинградского объединения «Техническая книга» им. Евгении Соколовой Со- юзполиграфпрома при Государственном комитете СССР по делам издательств, полиграфии и книжной торговли. 198052, г. Ленинград, Л-52, Измайловский проспект, 29.

5 0 коп

МЕТАМАТЕМАТИКА ЭЛЕМЕНТАРНОЙ МАТЕМАТИКИ

Hochschu I text

E. Engeler

Metamathematikder Elementarmathematik

Mit 29 Abbildungen

Springer-Verlag

Berlin Heidelberg New York 1983

Э.ЭНГЕЛЕР

МЕТАМАТЕМАТИКАЭЛЕМЕНТАРНОЙМАТЕМАТИКИ

Перевод с немецкогоГ. Е. Минца

под редакциейА. О. Слисенко

MQCKBA «МИР» 1987

ББК 22.10

Э62

УДК 510.6

Энгелер Э.

Э62 Метаматематика элементарной математики: Пер. с нем. — М.: Мир. 1987. - 128 с.

Книга швейцарского математика вышла в серии учебников для высшей школы издательства «Шпрингер». Она рассчитана на лиц, желающих получить общее представление о современных взглядах на основания математики и о некоторых разделах математической логики. В ней коротко описываются проблемы обоснования теории вещественных чисел, аксиоматика геометрии, понятие алгоритма. В частности, многих читателей заинтересуют обсуждение проблем геометрических построений ограниченными средствами, а также изложение разрешающего алгоритма для элементарной алгебры и геометрии.

Для читателей, интересующихся основаниями математики.

11—87, ч. 111—87, ч. 1ББК 22.10ББК 22.101702020000—122

11—87, ч. 1

11—87, ч. 1

ББК 22.10

ББК 22.10

9041(01)—87

Редакция литературы по математическим наукам

© by Springer-Verlag Berlin Heidelberg 1983.

All Rights Reserved. Authorized translation from German language edition published by Springer-Verlag Berlin Heidelberg New York Tokyo.

© перевод на русский язык, «Мир», 1987