Игошин Математическая логика и теория алгоритмов (1019110), страница 75
Текст из файла (страница 75)
Например, чтобы сказать, что множество вещественных чисел х, обладающих свойством Г(х), не пусто„мы пишем просто (Лх)(Г(х)); существование верхней грани выражается формулой (ЛЬ)(Чх)(Г(х) — > х < Ь) и т.д. Это и дает приведенную выше формальную запись аксиомы полноты. Вопрос о том, насколько мы при этом отдалились от первичной теоретико-множественной аксиомы полноты, — зто по существу, вопрос о том, каков класс множеств, определимых свойствами Г(х).
Таким образом, формальная (элементарная) теория вещественных чисел может быть построена на базе системы следующих аксиом: аксиомы ноля; аксиомы лорлдка: х < х, (х<улу<х)»х=у, (х<улу<г)-+х<г х<уму<х, к <у-» х+г <у+г (х<улг>0) »х.г<у.г; аксиома полноты (схема аксиом). Это означает, что система действительных чисел есть полное линейно упорядоченное поле. Иногда аксиому полноты формулируют в более ограниченном виде — не для произвольного свойства Р(х) действительных чисел х, а для конкретного свойства: а х'"+ а,х '+ ... + а,х+ а, = 0— быть корнем алгебраического многочлена. В этом случае аксиома полноты формулируется так: 299 (~'а а Ь, с) [Ь<слр (Ь) <Олр (с) >О-э(ЗгНЬ<г<сл лр (х)=0(, где р (х) = а х'"+ а,х '+ ...
+ а,х+ ав. Или же в этом случае аксиома полноты распалается на две части: (ЧхНВуНх = у~ м — х = у'-) (из каждого вещественного числа или противоположного ему числа можно извлечь квадратный корень); (~ао а| - аг ~Н3гНры,,(г) = 0) (каждый алгебраический многочлен нечетной степени имеет хотя бы один вещественный корень). Аксиомы поля и аксиомы порядка (т.е. аксиомы линейно упорядоченного поля) и аксиома полноты в одной из двух последних формулировок образуют систему аксиом элементарной теории так называемых вещественно-замкнутых нолей.
Разрешимость и абсолютная полнота элементарной теории вещественно-замкнутых полей. Приведенные в предыдущем пункте системы аксиом представляют собой попытки аксиоматизировать совокупность свойств, справедливых в системе действительных чисел. Считается, что самый большой успех аксиоматизации достигнут, если с ее помощью удается обосновать эффективную разрешающую процедуру, т.е. процедуру, которая для любого предложения 5, сформулированного на данном формальном языке, распознает за конечное число шагов его истинность в подразумеваемой структуре, в данном случае в системе действительных чисел.
В 1930-е гг. А.Тарский доказал, что для любого данного суждения о действительных числах, которое может быть выражено на формальном языке элементарной теории вещественно-замкнутых полей, либо само это суждение, либо его отрицание доказуемо в этой теории, т.е. выводимо из ее аксиом. Это означает, что элементарная теория вещественно-замкнутых полей абсолютно полна, а соответствующая система аксиом по существу определяет алгебраические свойства действительных чисел.
При этом разрешающая процедура (алгоритм) основана на так называемом методе элиминации (ликвндации) нванторов, который впервые применили Ленгфорд и Пресбургер в 1920-е гг. Этот метод оказался чрезвычайно эффективным и впоследствии нашел многочисленные применения для решения проблемы разрешимости в самых разных разделах математики (7.7[. Идея метода элиминации кванторов состоит в следующем. Вначале доказывается, что для любой формулы А (рассматриваемой теории первого порядка) вида (ВхНА,(х) л ... л А„(х)), где А;(х) — атомарная формула или отрицание атомарной формулы, найдется такая бескванторная формула В, что в данной теории доказуема (выводима) эквивалентность А <-~ В.
Основываясь на этом утверждении, к каждой замкнутой формуле (предложению) 5 300 данной теории может быть применена процедура элиминации кван- торов, которая состоит в следующем: 1) превратить самые внутренние кванторы этого предложения в кванторы существования, если они не таковы (пользоваться при этом законами де Моргана); 2) привести область действия каждого из этих кванторов к дизьюнктивной нормальной форме; 3) распределить кванторы существования по дизъюнктивным членам; 4) заменить все 3-формулы А эквивалентными им бескванторными формулами В на основании предыдущего утверждения; 5) если полученная формула все еше не является бескванторной, то повторить описанные шаги, начиная с п. 1; в противном случае рассматриваемое предложение В превратилось бы либо в истину, либо в ложь.
Таким образом, метод элиминации кванторов сводит логический вопрос о (раз)решении к математическому вопросу о критериях существования решения совершенно определенной задачи. Что касается теории вещественно-замкнутых полей, то решение обсуждаемой проблемы в ней основывается на классической теореме Штурма (доказанной еще в 1829 г.) и доставляющей средство определения числа (вещественных) корней алгебраического многочлена с целыми коэффициентами между двумя заданными границами, а также общего числа корней такого многочлена (см., например, [7.1, э 79[).
Теорема утверждает, что число корней между Ь и с (Ь < с) многочлена р(х) равно (без учета кратности) числу перемен знака в так называемом ряду Штурма этого многочлена. В удобной для элиминации кванторов форме эта теорема может быть сформулирована следующим образом: для каждого многочлена р(х, а„..., а„) с целыми коэффициентами имеется такая бескванторная формула В(а„..., а„, Ь, с), что эквивалентность (Зх)(Ь < х < с л р(х, а„..., а„) = О) ч-+ (Ь < с -э В(а„..., а„, Ь, с)) выводима из аксиом элементарной теории вещественно-замкнутых полей. Заслуга А. Тарского состоит в том, что он доказал зту теорему в следующем обобщенном виде: для любой бескванторной формулы А(х) найдется такая бескванторная формула В(Ь, с), что эквивалентность (Зх)(Ь < х < с л А(х)) ч-> (Ь < с — > В(Ь, с)) выводима из аксиом элементарной теории вещественно-замкнутых полей.
(Подробное доказательство этой обобщенной теоремы Штурма содержится в [5.28, с. 25 — 31],) С помощью этой теоремы уже легко обосновывается процедура элиминации кванторов для элементарной теории вещественно-замкнутых полей. В самом 301 деле, пусть А(х) — бескванторная формула с единственной свободной переменной х и мы хотим элиминировать (удалить) квантор Лх из формулы (Вх)(А(х)). Очевидно, что в любом линейно упорядоченном поле справедливо утверждение (эквивалентность) (Вх)(А(х)) <-э 1А(-1) ч А(1) ч (Вх)(-! < х < 1 л А(х)) ч (Вх)(-1 < < х < 0 л А(л ') ч Ях)(0 < х < ! л А(х '))).
Но ведь из этой формулы можно удалить кванторы на основании обобщенной теоремы Штурма. Итак, выводимость из аксиом вещественно-замкнутых полей разрешима, т.е. разрешима элементарная теория вещественно-замкнутых полей. Более того, эта теория полна, т.е. для любого данного суждения о действительных числах, которое может быть выражено на формальном языке формальной теории вещественно-замкнутых полей, либо само это суждение, либо его отрицание выводимо из аксиом этой теории.
Кроме того, А.Тарский показал„что теорема элементарной алгебры истинна в поле вещественных чисел тогда и только тогда, когда она верна во всех вещественно-замкнутых полях, т.е. выводима в элементарной теории вещественно-замкнутых полей. О формальиой геометрии. В вопросе о понятии математического пространства особенно остро проявляется проблема соотношения математики с окружающей действительностью. Математической наукой о физическом пространстве как раз и является геометрия. Ньютон считал, что основанием для геометрии является практика механики, и в действительности геометрия есть не что иное, как та часть механики в целом, которая точно устанавливает и обосновывает искусство измерения.
Следовательно, смысл геометрии заключается в подведении под искусство измерения прочного и достаточно обязательного базиса: необходимо, чтобы математические следствия основных допущений о физическом пространстве можно было проверить фактическим измерением в этом пространстве. Но установление соответствия между математической теорией и эфемерным реальным пространством не является математической задачей. С точки зрения математики задача формализации геометрии выглядит примерно следующим образом. Нужно принять некоторую математическую концепцию реального физического пространства.
Поскольку в качестве системы расстояний в евклидовой геометрии принимается поле Я вещественных чисел, геометрию проще всего понимать, например, по Вейлю — как точечное пространство Е над соответствующим векторным пространством !~ над полем Л. Теперь программу формализации (аксиоматизиции) можно сформулиРовать следующим образом. Выбрав конечное число первичных геометрических понятий (элементов) и отношений между ними, найти такую систему аксиом для этих элементов и отношений, 302 для которой из того, что некоторая элементарная теорема верна для принятого в Е определения основных понятий, вытекает, что она выводима из принятых аксиом, и, обратно, выводимость влечет истинность. (Здесь, как и обычно, мы называем высказывание элементарным, если оно выразимо в языке первой ступени с рассматриваемыми отношениями на рассматриваемых элементах.) Эта программа аксиоматизации реализуется посредством так называемой координатизации исходного геометрического пространства Е.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
