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

1 т, 1, мы собрали в у 1 настоящей главы в аксиомы 1 — 4 группы 1 и акси) — 5 ру и) ..15). ')с ..)р. ез 1ГЛ 1 аЬ =сд ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕННЫХ Аксиомы конгруэнтности целесообразно взять в редакции Р. Л. Мура '), который для случая линейной конгруэитности в основном берет аксиомы Гильберта, ио не пользуется понятием конгруэитности углов.

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

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

Тот факт, что этой аксиомы о конгруэнтности треугольников достаточно для того, чтобы в сочетании и предшествующими з) См. его работу: Мао ге й. !.. яеы о1 гае1«1««1 Ьуро1Ьемм !аг Ееоте1гу — Тгзнз, А!пег, Млнн зос., !908, 9, р. 487 — 512. ') Аксиома о конгрузвтнаетн всех двойным точек дабзнлнетсл здесь н пелла Фармзльной палноеы, ДОКАВАтельстВА непРОтиВОРечиВОсти аксиомами линейной конг руэнтности и на основе подходящим образом сформулированного определения конгруэнтности углов, понятий б о л ь ш е и м е н ь ш е для отрезков и углов, а также понятий прямого. острого и тупого угла получить обычные теоремы элементарной геометрии, не зависящие от аксиомы о параллельных, впервые полностью показал Дорро'). Благодаря наличи!о в этой системе третьей, экзистенциальной аксиомы, аксиома ПЛ, которая выражает возможность продолжения любого отрезка, становится ненужной.

Поэтому мы ее опустим, чем заодно будет исключен и функциональный знак ер(а, Ь). Аксиома о параллельных в тильбертовской редакции гласит (если ограничиться плоской геометрией); «Через точку, лежащую вне прямой а, проходит, самое большее, одна прямая, не пересекающая а», Иначе это можно сформулировать так: «Из двух различных прямых, проходящих через точку Р, лежащую вне прямой а, по крайней мере одна имеет с прямой а общую точку». В последней формулировке мы можем опустить условие, требующее, чтобы Точка Р лежала вне прямой а. Тогда с помощью отношения Сзг эта аксиома запишется следующим образом: 1С»т(а, Ь, с)-ь Зх(ОТ (д, е„х) й(ОТ (а, Ь, х) )/ Ог(а, с, х))).

(П о я с н е н и е. Прямая, проходящая через 1( и е, — это заданная прямая '); а — это та произвольная точка, через которую проходят две различные прямые,— одна через 6, другая через с; утверждается, что по крайней мере одна из этих двух прямых имеет общую точку х с прямой, проходящей через е1 и е.) ') Смл !) ее гоп й !.. Сопсегн!ВК з зе1 а1 ше1«!ез! )зуро1Ьезез !ог йеоше1гу. — Апн. М«16., 2 Бег., !928, 29, р.

229 — 23!. Мур показал достаточность «Фармулнронзнных нм аксиом конгрузнтнестн только нрн условии добавления к ннм одной аксиомы ненрерынноетн, вместо которой, кзк он показал, дестзточно взять предлеженне о том, что каждый отрезок имеет среднюю течку. работе Дорро зта предложенне было доке»зла нз основе аксиом контру»к«- носта Мура. а- е; ) Это геометрическое истолкование является осмысленным лишь когда чь е; аднзко вследствие аксиомы бг (а, а, Ь) дзен»я нмплнкзннн ныполнкетсн ннрн4 «. ДОКАЗАТЕЛЬСТВА НЕПРОТИВОРЕЧИВОСТИ 64 ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕННЫХ !ГЛ, 1 Наконеп, мы еще должны добавить в виде собственных аксиом аксиомы равенства. Прежде всего мы возьмем аксиомы а=а а=Ь-ь-(а=с- Ь=с). Затем нужно взять аксиомы равенства, связанные с основными предикатами бг, 21ч и —= , С учетом числа аргументов этих .

предикатов здесь надо было бы написать десять формул. Однако ' вследствие аксиомы 1.1 бг(а, Ь, с)- бг(Ь, а, с)йбг(а, с, Ь) и непосредственно получающейся из 11.3 формулы 2чс(а, Ь, с)- 2ьч(а, с, Ь) нам нужно взять для бг и 21ч лишь формулыа) а=6- (бг(а, с, Й)- бг (Ь, с, Й)), а = 6 — ь (2тч (а, с, д) -ь.

2тч (Ь, с, б()), а = Ь-ь. (2ъ (с, 1(, а) -+. 24ч (с, с(, Ь)), вторая из которых снова оказывается излишней ввиду аксиомы 11.1 Ъч (а, Ь, с) -ь- бг (а, Ь, с) и выводимости формул 2ьч (а, Ь, с) - а Ф Ь й а чь с й Ь Ф с бг (а, Ь, с) й а Ф ЬйаФсйЬ чьс-~- 2ьч (а, Ь, с) 1/ 2тч (Ь, а, с) у' Ъч (с, а, Ь). Ввиду аксиом аЬ = — Ьа аЬ = рдйсб(= ра- аЬ =сб(, для предиката = — достаточно нзять одну следующую формулу," равенства: а=Ь- ас — Ьс. ч Теперь мы должны привести к разрешенному виду две появившиеся экзистенциальные аксиомы. Вместо аксиомы а~=Ьйсчьб( — мх(21ч(с, б(, х) йаЬ вЂ” сх), 1) См, т.

1, гл. ЧП, с. 4б4, Вв~дя функциональный знак ф(а, 6, с, б(), мы получим формулу а~Ьйс~б-~2чг(с, 41, ф(а, 6, с, д)) йаЬ=сф(а, 6, с, 4(). для того чтобы привести к разрешенному виду формулу, выражающую аксиому о параллельных, нам нужно было бы, согласно общему методу, ввести функциональный знак с пятью аргументами. Но здесь можно будет добиться некоторых упрощений. Ь(ы воспользуемся тем обстоятельством, что с помощью е-символа и явного определения может быть произведено символьное решение любой экзистенциальной формулы.

Для символьного решения формулы, выражающей аксиому о параллельных, нам в соответствии с общим методом нужно было бы ввести з-символ е (бг(д, е, х) й(бг (а, Ь, х) 11 бг(а, с, х))). Однако с равным успехом вместо него здесь может быть введен е-символ е (бг(а, Ь, х)йбг(с, б(, х)). Действительно, если ввести явное определение $(а, Ь, с, 11)=е (бг(а, Ь, х) йбг(с, с(, х)), то из нашей формулы для аксиомы о параллельных, взятой в сочетании с формулой 'Зх А (х) — ь. А (а А (х)), легко получится формула )бг (а, Ь, с)-ь (бг (б(, е, Ц(а, Ь, 41, е)) йбг(а, Ь, $(а, Ь, а(, е))) 1/ (бг(11, е, $(а, с, б(, е)) йбг(а, б, $(а, с, 11, е))), от которой с помощью средств исчисления предикатов можно снова вернуться к нашей формуле, выражающей аксиому о параллельных. Геометрически $ (а, 6, с, 11) изображает некоторую общую точку прямых аЬ и сб( (еслн таковая существует); в частности, в том случае, когда аЬ и сй суть две отличные друг от друга пересекающиеся прямые, $(а, Ь, с, 4() изображает точку пересечения этих прямых.

Эта геометрическая интерпретация заодно показывает, что с помощью функции $(а, 6, с, д) можно также осуществить символьное решение пятой аксиомы порядка, что позволит сэкономить функциональный знак ф(а, 6, с, 11, е). Эта аксиома утверждает, что если какая-либо прямая пересекает сторону аЬ треугольника аЬС в какой-нибудь точке, лежащей между а и 6, то тогда она проходит через какую-нибудь точку стороны (т, е. отрезка) аа 3 Д. Гнньберт, П. Вернабс-140 ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕННЫХ игл.

! ДОКАЗАТЕЛЬСТВА НЕПРОТИВОРЕЧИВОСТИ илн через какую-нибудь точку стороны Ьс. Это утверждение можно сформулировать еще н следующим образом: «Если точки а, Ь н а,. не лежат на одной прямой„точка р лежит между а и Ь, а пря-е мая рд отлична от прямой аЬ н не проходит через с, то сущест-' вует либо точка пересечения прямых.

Рд н ас, лежащая между:: а н с, либо точка пересечения прямых рд н Ьс, лежащая между' Ьн С помощью нашей символики это высказывание запишется ' посредством формулы (ьг) 1бг(а, Ь, с)йЪч(Р, а, Ь)й 3бг(д, а, Ь)й1бг(с, р, д) -«(бг(р, ч, з(р, д, а, с)) йЪч($(р, д, а, с), а, с)) ~у (бг (Р Ч Б(Р Ч Ь, с))йЪч($(р, у, Ь, с), Ь, с)).

Формула (еьг) дедуктивно равна первоначальной формуле для аксиомы П.б. Для установления этого факта надо воспользоваться в-формулой н определением функционального знака $(а, Ь, с, д). Действительно, если мы в первоначальной формуле '4хЧуЧЕЧиЧо( )бг(х, у, г)йЪК(и, х, у) й 1бг(о, х, у) й ~бг(е, и, о)-«Эв(бг(и, о, в)й(Ъч(в, х, е) ~/ Ъч(в, у, е))Ц заменим связанные переменные х, у, г, и, о свободными н произведем некоторые преобразования по правилам исчисления предикатов, то она перейдет в формулу )бг(а, Ь, с)йЪч(р, а, Ь)й'1бг(д, а, Ь)й 1бг(с, р, д) -«=(в(бг(р, а, в) йЪч(в, а, с)) Ч Зв(бг(р, а, в) йЪч(в, Ь, с)), а эта последняя может быть легко выведена нз формулы ($А) средствами исчисления преднкатов.

С другой стороны, формула ($г) может быть выведена нз нее с помощью формулы БЬ (бг (р, а, в) й Ъч (в, д, с)) й ~ бг (с, р, а) -«бг(р, а, $(р, а, 4, с)) й Ъч Я(р, с, д, с), д, с), которая, в свою очередь, получается на основе определения снмвола $(а, Ь, с, д) с использованием аксиом 1.1, 2, 3, 11.1, 2, 3, аксиом равенства и е-формулы.