Гильберт, Бернайс - Основания математики. Теория доказательств (Гильберт Д. - Основания математики и прочие работы), страница 14

Таким образом, прн разрешении экзистенциальных аксиом нашей системы аксиом геометрии мы можеь. обойтись введением индивидных символов а, Р и у и функциональных знаков ф(а, Ь, с, 4 и $(а, Ь, с, д). В результате получается следующая система, состоящая из аксиом в разрешенном виде: Аксиомы равенства а а, а=Ь-«(а=с †«Ь=с), а = Ь -«(бг (а, с, г() «бг (Ь, с, д)), а Ь - (Ъч (с, д, а) — Ъч (с, г(, Ь)), =Ь вЂ” Ь. Аксиомы соединения бг('а, а, Ь), бг(а, Ь, с)-«бг(Ь, а, с) йбг (а, с, Ь), бг(а, Ь, с)йбг(а, Ь, д) йачьЬ-«бг(а, с, д), )бг(а, Р, у), Аксиомы порядка Ъч (а, Ь, с) -«бг (а, Ь, с), )Ъч(а, Ь, Ь), Ъч(а, Ь, с)- Ъч(а, с, Ь)й 1Ъч(Ь, а, с), )бг(а, Ь, с)йЪч(р, а, Ь)й)бг(су, а, Ь)й 1бг(с, р, д)-« (бг(р, с, $(р, д, а, с)) йЪч($(р, д, а, с)), а, с)) Ч' (бг(р, а, $(р, а, Ь, с)) йЪч(Ц(р, а, Ь, с), Ь, с)).

Аксиомы конгрузнтности аЬ ии Ьа й аа Вм ЬЬ, аЬ = райсдэмра-«аЬ вЂ” сд, а~Ьйсчьд-«Ъч(с, д, ф(а, Ь, с, 4)йаЬ=ф(а, Ь, с, д), бг(а, Ь, с)й 1Ъч(а, Ь, с)йаЬ ас-«Ь=с, Ъч(Ь, а, с) йЪЕ(д, р, г)йаЬ= рсйЬс=аг- ас=рг, 1бг(а, Ь, с) й )бг(р, д, г)йЪч(Ь, а„г() йЪч(д, р, з) й аЬ ма рс й Ьс — аг й ас = рг й Ьд = аз -«сд Ви гз. Аксиома о иараллельных )бг(а, Ь, с)-«(бг(д, е, $(а, Ь, д, е)) йбг(а, Ь, ь(а, Ь, а, е))) ~~ (бг(д, е, 8(а, с, г(, е)) йбг (а, с, $(а, с, а, е))). Замечание. Нам нет надобности формулировать аксиомы равенства для функциональных знаков ф(а, Ь„с, 4 и $(а, Ь,с, г(), так как символьным решением соответствующих экзистенциальных аксиом мы будем пользоваться лишь как вспомогательным средством для установления непротиворечивости рассматриваемой снстемы геометрических аксиом в ее первоначальном виде прн условии использования рассуждений, формализуемых с помощью средств исчисления предикатов н е-аксиомы. Но для этого доста- 3* 69 ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕННЫХ ДОКАЗАТЕЛЬСТВА НЕПРОТИВОРЕЧИВОСТИ )гл.

1 точно рассматривать введенную нами систему аксиом, так как все аксиомы нашей первоначальной системы ') могут быть выведены из нее средствами исчисления предикатов. Теперь, для того чтобы извлечь из нп-теоремы непротиворечивость сформулированной системы аксиом, нам достаточно задать истинностные значения для постоянных элементарных формул таким образом, чтобы наши аксиомы оказались при этом Верифицируемыми. Нужное определение нам дает аналитическая геометрия. В качестве числовой области для наших целей достаточно будет взять совокупность чисел, получающихся из единицы в результате применения четырех элементарных арифметических действий и операции извлечения квадратного корня из положительного числа. Действия над числами нз втой области, которую мы обозначим посредством Я, выполняются финитным образом. Используя комплексные числа, мы можем разработать некоторый сокращенный способ записи различных отношений аналитической геометрии. Для этого координаты а и Ь данной точки плоскости мы будем объединять в комплексное число а+ И.

Таким образом, в дальнейшем мы будем иметь дело только с такими комплексными числами а+И, у которых и и Ь суть числа из Я. Область этих комплексных чисел мы обозначим посредством яе. В дальнейшем мы будем применять ряд общеупотребительных обозначений, связанных с комплексными числами. Если с — число а+И, то 3(г) будет обозначать число Ь (мнимую часть г), )с! будет обозначать число р'аа+Ь» (абоолютную величину с), а с будет обозначать сопряженное а с число а — И; число с будет называться действительным, если Ь=О, и положительным, если 6 = О и а положительно.

Определяя истинностные значения постоянных элементарных формул, мы должны помнить, что каждая постоянная элементарная формула имеет один из следующих четырех видов: а=Ь, Ог(а, Ь, с), Ещ(а, Ь, с), ВЬьмьсд, где а, Ь, с и д — постоянные термы, и что каждый постоянный ') Впрочем, добавление восьми аксипм равенства, соответствующих восьми аргументам функциональных знаков ф(а, Ь, с, й) и 1(а, Ь, е, а), в том духе, как формула и= Ь - Ф (а, р, д, г) Ф (Ь, Р, а, г) соответствует первому аргументу р(а, Ь, с, ьв, не составило бы никакпгп труда. В свмом деле, легко видеть, что арифметическое истолкование, с помощью кпп»рого мы праводим наше доказательство, дает для тернов ф (а, Ь, Ч ь) м ц(а, Ь, с, Ь) с постоянными аргументами некоторое однозначное определение нх истинностных значений.

См. далее с, 69. терм либо совпадает с одним из индивидных символов а, ан и у, либо строится из ннх с помощью функциональных знаков ф и $. В соответствии со сказанным, мы получим распределение истинностных значений для постоянных элементарных формул, указав способ сопоставления каждому постоянному терму некоторого числа из области Я*, а также указав для каждой из элементарных формул а =Ь, Ог(а, Ь, с), Хти(а, Ь, с), аЬ~сь некоторое арифметическое высказывание, истинность или ложность которого для чисел из Яе, сопоставляемых данным термам и, Ь, с н Ь, будет определять, какое истинностное значение— «истина» или <ложь» — получает рассматриваемая элементарная формула. Символам се, б и у мы сопоставим комплексные числа О, 1 и 1, а функции ф и й для любых значений аргументов 1, (,щ и и из Я" определим следующим образом:  а+: (щ — и), если щчьп, )г — И гр (1, 1, т, и) щ, если щ=п; 3(Е 1) (а — и) — 3(м а) (г — О 3((1 — 1) (ш — а)) если (1 — 1) (щ — и) не является действительным числом, т, если 1=1, щ~п, в остальных случаях.

$(1, 1, щ, и)= Пояснения. При щ~п терм ~р(1, 1, а, и) изображает собой точку, которая лежит на продолжении отрезка, ведущего от и к щ, на расстоянии ~1 — 1! от точки щ. Если число (1 — 1) (щ — и) не является действительным, то 1Ф1, щ~ и и направление отрезка, ведущего от 1 к 1, не совпадает ни с направлением отрезка, ведущего от щ к и, ни с направлением противоположного ему отрезка. В этом случае $ (1, 1, щ, и) изображает точку пересечения прямой, проходящей через 1 и 1, и прямой, проходящей через щ и и. Далее, каждому постоянному терму мы однозначно сопоставим некоторое число нз Я', )(ля чего сначала каждый встречающийся в данном терме индивидный символ мы заменим соответствующим ему комплексным числом, а затем функциональные знаки, аргументами которых уже оказались комплексные числа, будем заменять приписанными им для этих значений аргументов значениями ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕННЫХ 1гл.

з из Яа до тех пор, пока не будут удалены все функциональные знаки и не останется результирующее значение из яа. Теперь мы сопоставим элементарным формулам «=Ь, Ог(«, Ь, с), Уча(«, Ь, г). «Ь=сь соответствующие им арифметические высказывания. Пусть 1, 1, пз и и суть комплексные числа, соотнесенные термам «, Ь, с и ь соответственно в силу предыдущих соглашений. Тогда: Формула «= Ь будет считаться истинной или ложной в зависимости от того, имеет или не имеет место арифметическое равенство 1=1 между числами 1 и 1 из (га. Формула Ог(«, Ь, с) будет считаться истинной или ложной в зависимости от того, является или не является действительным комплексное число (1 — 1). (ш — и).

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

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