Игошин Математическая логика и теория алгоритмов (1019110), страница 76
Текст из файла (страница 76)
Координатизация геометрического пространс т в а. Хорошо известна модель планиметрической части системы аксиом Гильберта, в которой точкой плоскости является упорядоченная пара (х, у) действительных чисел, а прямой линией— фактически алгебраическое уравнение первой степени. При ее создании геометрия строится из чисел. Задача координатизации состоит в обратном: построить числовую систему, исходя из геометрии (т.е.
из точек и прямых). Точнее, пусть имеется некоторая планиметрия, объектами которой являются элементы двух множеств — множества точек (обозначаются заглавными латинскими буквами) и множества прямых (обозначаются малыми латинскими буквами), для которых справедливы аксиомы Гильберта в их планиметрической части. (При этом основным отношением является отношение инцидентности (принадлежности): А а ! — точка А принадлежит прямой 1.) Требуется построить такое поле К, изоморфное полю Я вещественных чисел, чтобы точки в нашей геометрии задавались упорядоченными парами элементов (координатами) из К, а прямые — линейными алгебраическими уравнениями.
Из аксиом (1.1) — (1.3) первой группы аксиом системы аксиом Гильберта вытекает существование в нашей планиметрии фигуры, играющей важнейшую роль в процессе ее координатизации. Эта фигура состоит из двух прямых К, у', пересекающихся в точке Д, и двух отличных от Д точек Е и Е', лежащих соответственно на этих прямых.
Элементами поля К будут точки прямой К. Для точек этой прямой мы введем операции поля — сложение и умножение — геометрически, т.е. определим их через инцидентность, причем точка Е будет представлять единицу для умножения, а точка Д вЂ” нуль для сложения. Возможность использования этой фигуры для изображения конструкции сложения и умножения точек прямой основана на следующей лемме, которая легко выводится из аксиомы параллельности (ч').
Лемма 30.4. Если две различные прямые й и 8 пересекаются, то всякая прямая Б, параллельная Ь, также пересекается с К. Доказательство. Если допустить, что это не такдля некоторой прямой й', то через точку пересечения прямых й и К, не принадлежащую прямой й', проходит две различных прямых й и 303 я, не пересекающихся с Л', что противоречит аксиоме параллельности Евклида. П Теперь определяем сложение точек В и А прямой я с помощью следующих построений. В нашей фигуре е, е', О, Е, Е' проводим прямые: е": Е' е я", ~"~~ я; ВТ: В е ВТ, ВТ Па', ТЕ: Те Т1., ЧАЕ'. Тогда ВЕ = ОА, и, следовательно, ОВ+ ОА = ОВ+ ВЕ = ОЕ.
0 Е А В В+А 8 Аналогично определяется умножение точек В и А прямой я с помощью следующих построений. Проводим прямые ВВ'. В е ВВ', ВВ~~ЕЕ' и В'Е: В' в В'Ь, В'ЦЕ'А. Тогда из подобия треугольников ОАЕ'и ОЕВ'вытекает, что ОА:ОЬ= ОЕ:ОВ,т.е. ОЬ ОЕ= ОВ. ОА (ОŠ— единичный отрезок).
0 Е А В Можно показать, что так определяемые операции определены корректно и удовлетворяют всем аксиомам поля. Улорядочение в этом поле основывается на геометрическом отношении «междугк р(АВС) — точка В лежит между точками А и С. Сначала определяется понятие положительности: А > 0 «» А ~ 0 л -р(АОЕ). Затем, исходя из гильбертовых аксиом второй группы (аксиомы порядка), устанавливается выполнимость в построенном поле аксиом порядка: (О > 0); А > 0 ч — А > 0 ч А = 0; (А > 0 л В > 0) -> -» (А + В > 0 л А . В > 0). Наконец, чтобы наше упорядоченное поле было полным (всякое ограниченное сверху подмножество имело точную верхнюю грань), нужно, чтобы исходная геометрия удовлетворяла аксиоме непрерывности (или полноты).
Известны различные формы 304 таких аксиом, например Кантора, Дедекинда. Приведем еще одну формулировку. Аксиома полноты: пусть Ми Ф вЂ” два непустых множества точек иа прямой 8 и пусть имеется точка С, такая, что для всех А я М и В я Ф верно )г (САВ). Тогда имеется такая точка Р, что для всех А е Ми В я Ф, отличных от Р, верно 1г(АРВ). Из геометрической аксиомы полноты (непрерывности) немедленно следует, что поле, построенное на прямой я, полно. Это фактически завершает доказательство того, что построенное поле изоморфно полю А вещественных чисел.
Поле, построенное на прямой 8, можно использовать теперь, для координатизации всей плоскости. Для этого нужно сначала построить поле и на прямой 8' так же, как это сделано на прямой 8 (Е' — единичная точка на 8'). Построенные на 8' и 8 поля оказываются изоморфными: изоморфизм осуществляется проектированием параллельно прямой ЕЕ'. Теперь каждой точке Р плоскости мы можем сопоставить упорядоченную пару (Х, г ) точек (вещественных чисел), как показано на следукпцем рисунке. Остается выразить требование взаимной перпендикулярности осей координат 8 и 8' и равенства единичных отрезков ОЕ = ОЕ'. Это достигается с помощью гильбертовых аксиом П1 группы— аксиом конгруэнтности отрезков и углов.
Если Р(Хь )~) и Д(Хв );) — две точки плоскости со своими координатами, то точечное пространство упорядоченных пар (Х У) можно рассматривать над векторным пространством векторов РЦ (Х,— -Хп 1~ — У) в котором скалярное произведение определяется по формуле Р0 БТ = (Хг — ХНХ4 — Хз) + (1; — 1~)()4 — 1З).
В итоге точечное пространство упорядоченных пар (Х, У) оказывается изоморфно исходному евклидову точечному пространству Е над векторным пространством К С подробностями процесса координатизации можно познакомиться в [5.28, с. 57 — 68), (3.9, э 7Ц. Элементарная теория евклидовой планиметрии. Задача формализации аксиоматической геометрии, построенной, например, на базе системы аксиом Гильберта, снова ставит нас перед проблемой, уже возникавшей при формализации теорий 305 числовых систем: как адекватно выразить содержание аксиомы полноты (непрерывности), в формулировке которой участвуют множества М и гу, в нашем формальном языке первой ступени, как понимать участвующие там множества? Здесь мы снова выбираем тот же выход, что и при формализации теорий числовых систем: мы заменяем множества определяющими их предикатами (свойствами) в языке первого порядка для элементарной геометрии с исходными понятиями по системе Гильберта.
Получаемая таким образом в элементарной форме аксиома полноты (а точнее, схема аксиом, называемая схемой Тарского) может быть сформулирована следующим образом: для любых формул Р(.) и Д() имеем (ЗС)(1УА)(1УВ)(Р(А) л Д(В) -+ )г(АВС)) -+ (З.(2)('ггА)(ХгВ)(А ~ )) л л В ге Р л Р(А) л Ц(В) -+ )г(АРВ)). Из этой схемы Тарского непосредственно следует, что построенное на прямой я упорядоченное поле удовлетворяет (элементарной) аксиоме полноты из теории вещественных чисел, т.е. в конечном итоге является вещественно-замкнутым полем. Поскольку, как было отмечено выше, эта элементарная теория полна и разрешима, то теперь с помощью изложенной в предыдущем пункте процедуры координатизации эти свойства переносятся и на элементарную теорию евклидовой геометрии.
Таким образом, элементарная теория евклидовой геометрии на плоскости, построенная на основе планиметрических аксиом системы Гильберта, полна, т.е. для любого предложения Р в языке элементарной геометрии одно из предложений Рили Рвыводимо из этих аксиом; более того, вопрос о выводимости данного предложения эффективно разрешим. Это связано с тем, что всякую формулу в языке элементарной геометрии можно в силу осуществленной координатизации воспринимать (или перевести) в языке линейной алгебры, основывающейся на полной и разрешимой теории вещественно-замкнутых полей. Фактически это означает справедливость своего рода метатеоремы, утверждающей, что формула элементарной геометрии выводима из аксиом геометрии тогда и только тогда, когда она (или соответствующий ее перевод на язык линейной алгебры) выводима из аксиом линейной алгебры. Подробно это доказательство приведено в статье А.
Тарского'. О формальном математическом анализе. Это формальная аксиоматическая теория, специально предназначенная для формализации (точного описания доказательств) математического анализа. Таких теорий существует несколько: они характеризуются раз- ' ТапИ А. %ьаг Ь е!егпепгагу Веогпеггу? // Непа!о, Борреа, Таге!о. ТЬе ах1огпаг!е гпегвогг. Агпагегггапг, 1959. Р.
! б — 29. ЗОб личными подходами к формализации. При этом каждую из них стараются строить по возможности минимальной по своим дедуктивным и выразительным возможностям, но все же достаточной для формализации всего традиционного материала математического анализа. Наиболее распространенной из формальных теорий математического анализа является теория Гияьберта — Бернайса, Она строится следующим образом. К языку формальной арифметики, описанной в предыдущем пункте, добавляется новый вид переменных Х, У, У, ..., которые рассматриваются как пробегающие множества натуральных чисел. Добавляется новый вид атомарных формул: (г в Х) («г принадлежит множеству Х»). Логические аксиомы формальной арифметики (т.е.
аксиомы формализованного исчисления предикатов) и схема аксиом индукции естественно усиливаются таким образом, чтобы включать в себя формулы расширенного языка. Наконец, добавляется единственная новая схема аксиом — схема аксиом свертывания: (Эх)(чу)(у в Х <-+ А(у)), где А(у) — формула рассматриваемого языка, не содержащая свободно Х; у — переменная для натуральных чисел. Эта теория Гильберта — Бернайса, хотя в ней речь идет лишь о натуральных числах и о множествах натуральных чисел, достаточна для естественной формализации математического анализа.
Интересна проблема обоснования непротиворечивости этой теории. Согласно теореме Геделя о неполноте формальной арифметики для этого необходимо использовать средства, выходящие за пределы формального математического анализа. В 1962 г. К. Спектор доказал непротиворечивость этой теории с помощью остроумной модификации модели Геделя для интуиционистской арифметики, которая представляет собой некоторое далеко идущее расширение требований интуиционизма. Трудности в попытках доказательства непротиворечивости теории Гильберта — Бернайса связаны с той особенностью аксиомы свертывания этой теории, что в формуле А(у) этой аксиомы разрешается свободно использовать кванторы по множествам.
Таким образом, при выяснении принадлежности числа у определяемому в аксиоме множеству Х необходимо использовать наличие всех множеств натуральных чисел, в том числе и определяемого множества Х Можно сказать, что аксиома свертывания формального анализа выражает до некоторой степени необходимость актуального существования всех множеств натуральных чисел одновременно (только после этого в формуле могут использоваться кванторы по переменным, пробегающим множество таких множеств). Эта особенность встречается в ряде формальных теоретико-множественных теорий и называется ненредикативностью теории.
Так что фор- 307 мальный анализ Гильберта — Бернайса является непредикативной формальной теорией. Имеется эквивалентная формулировка анализа Гильберта — Бернайса, в которой вместо множеств натуральных чисел фигурируют функции, перерабатывающие натуральные числа в натуральные. Для такого вида функции к формальной арифметике добавляются переменные а, ~3, у, ...
и новый вид термов: ц(г) (»результат применения а к г»); логические аксиомы и схема аксиом индукции естественно распространяются на формулы нового языка, и, наконец, добавляется единственная новая схема аксиом, называемая аксиомой выбора анализа: (1Ух)(Лу)(А(х, у)) -э (За)(ЧхКА(х, а(х))). Эта аксиома утверждает, что если для всякого х найдется у, удовлетворяющий условию А(х, у), то существует функция и, выдающая по х соответствующий у. Ценность этой формулировки состоит в том, что после исключения из числа логических аксиом теории закона исключенного третьего полученная система удобна для формализации в ней интуиционистского (или конструктивного) формального математического анализа, который представляет собой переработку традиционного материала математического анализа в соответствии с требованиями программы интуиционизма (или соответственно конструктивной математики).
Для устранения непредикативности были предложены различные формальные аксиоматические теории предикативного (или разветвленного) анализа. Общий взгляд па процесс формализации математической теории. Ознакомившись с рядом формальных аксиоматических теорий, так или иначе связанных с основаниями школьного курса математики, подведем итог„дав краткую общую характеристику методу формализации. Суть этого метода состоит в следующем. Допустим, у нас имеется некоторая содержательная математическая теория Т, и нас интересует, является ли она непротиворечивой. Для выяснения этого вопроса данная теория Т, подвергается формализации. Для этого сначала формализуется точный логико-математический язык й, такой, что все интересуюшие нас утверждения теории Т, записываются в виде формул языка й (математика теории Т, соединяется с логикой).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
