Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 15
Текст из файла (страница 15)
еОснования геометрина Гильберта, Добавление Ш, акрама 1ч', с. !б2 7.го издания (с, 232 русск. перев.), ДОКАЗАТЕЛЬСТВА НЕПРОТИВОРЕЧИВОСТИ мой Ьс, в то время как для любой точки Й, расположенной ~ежду р и д, прямая ад пересекает прямую Ьсв, Эта аксиома изображается формулой )Ог(а, Ь, с)-+.З.хЗу( 1ОТ(а, х, у) й ) Зг(ОТ(а, х, г) й Ог(Ь, с, х)) й) Зг(ОТ(а, у, г) йбг(Ь, с, г))й Уи(ХХР(и, х, у)-~ЗО(ОТ(а, и„о) йбг(Ь, с, о)))). Ее символьное решение может быть дано с помощью ранее использованного функционального знака $(а, Ь, с, с() и нового функционального знака )((а, Ь, с). Сопоставив кванторам существования Зх и =)у функции у(п, Ь, с) и )((а, с, Ь) и несколько усилив рассматриваемую аксиому, мы получим следующий ее разрешенный вид: ~ОТ(а, Ь, с)- 3ОТ(а, Х(а, Ь, с), Х(а, с, Ь))й ( 16г(а, у(а, Ь, с), д)'!/ )Ог(Ь, с, д))й (Еь (е, )((а, Ь, с), )((а, с, Ь))-ьбг(а, е, $(а, е, Ь, с)) й Ог(Ь, с, 5(4; е, Ь, с))). (Обратим внимание на то, что конъюнктивиый член, который сначала появляется вместо 1Зг(ОТ(а, у, г) йбг(Ь, с, г)), затем оказывается ненужным ').) Если мы возьмем данную аксиому вместо прежде рассматривавшейся аксиомы о параллельных, то получим систему аксиом плоской неевклидовой геометрии (без аксиом непрерывности).
Теперь мы получим финитное доказательство непротиворечивости этой системы, воспользовавшись восходящей к Феликсу Клейну проективной моделью. Для этого в нашем предыдущем распределении значений термов достаточно произвести следующие модификации и дополнения: 1. а) Вместо области !',1* комплексных чисел «+Ь1, у которых и Ь принадлежат 9, мы возьмем те числа из (гч, абсолютная величина которых меньше единицы. (Обозначим зту область через Я,*.) б) Символам а, р и у сопоставим числа О, 2 и (соответственно. в) Определение арифметических функций ограничим аргументами из области Я.
Впрочем, каи заметил Арнольд Шмидт, конъюнктивный член '|От ',а, у (а, Ь, с), Х (а, с, Ь)) в последней формуле можно заменить более простым членом Х(а, Ь, с) ~ Х(а, с, Ь). Действительно, модифицированная таким образом формула дедуктинно равна указанной в силу аксиом соединения, порядка и аксиом равенства, а также зкзистенцнальной (третьей) аксиомы ионгрувитносзн, нз которой, в частности, выводится формула ать Ь-ь Злсм Ьь а, Ь).
73 ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕННЫХ )гл. 1 4 41 ДОКАЗАТЕЛЬСТВА НЕПРОТИВОРЕЧИВОСТИ г) В определение функции й(1, 1, в, и) внесем следующее изменение: для тех четверок чисел 1, 1, в и и из (',)4*, для которых согласно предыдущему определению значение $(1, 1, в, и) имело абсолютную величину в1, значением $(1, 1, а, н) мы теперь будем считать число 1. 2. )((ы добавим определение функции )((1, 1, 4а), которую с использованием вспомогательной функции Ф 1, если 1=1, определим равенством )((1, в, и) = -'- (1+т(в, и)). Пояснение: При (чь( т(1, 1) изображает точку пересечения луча, идущего в направлении от 1 к 1, с окружностью единичного радиуса с центром в нулевой точке, а )((1, а, л) — середину отрезка, идущего из 1 в т(в, и).
Заметим, что хотя значение т(1, !) и не принадлежит (е44, значение у(1, в, п) принадлежит втой области. 3. Сопоставление постоянным элементарным формулам соответствующих им арифметических высказываний изменится только в части, касающейся формулы АЬвв!Ь. Именно, если термам я, Ь, с и Ь соотнесены числа 1, 1, в и и из Я;, то формула АЬ вЂ” сЬ будет считаться истинной или ложной в зависимости от того, истинно или ложно равенство (1 — т(1, 1))-(1 — т(1, !)) (в — т(п, в)) ° (и — т(а, и)) (1 — г(1, 1)) (1 — т(1, 1)) (в — т(в, и)) ° (и — т(п, а))' Что же касается установления верифицируемости этих аксиом на основе данного определения, то у всех аксиом, за исключением последней из группы аксиом конгруэнтности, оно получается прямой проверкой, а для рассмотрения оставшейся аксиомы конгруэнтности целесообразно воспользоваться некоторыми соображениями из области проективной аналитической геометрии.
Зги соображения будут иметь финитный характер, так как нам придется иметь дело лишь с точками, координаты которых суть числа из Я. Намеченные здесь доказательства непротиворечивости систем геометрических аксиом показывают, что мы вполне можем пользоваться идеями обычных доказательств непротиворечивости, производимых путем сведения к арифметике. Добавляется лишь одно финитное усиление, состоящее в том, что при рассмотрении данной арифметической модели мы ограничиваемся финитно-арифметическими рассуждениями (в наших примерах — рассуждениями, касающимися числовой области (е). При этом поначалу в доказательстве непротиворечивости возникает некоторый пробел, связанны й с тем, что наша финитно-арифметическая модель дает приемлем 7 интерпретацию только для аксиом теории, но не для рассуждени, ений, участвующих в доказательствах, Устранение этого пр е об ла в Дальнейшем как Раз и ДостигаетсЯ с помощью нашей нп-теоремы. Зтот прием был бы излишним, если бы мы располагали каким-либо финитным доказательством непротиворечивости для всей системы анализа в целом.
В рассмотренных нами случаях геометрических аксиом хватило бы даже финитного доказательства непротиворечивости для теории числовой обл с асти о включением в эту теорию принципа 1егВшп поп 4(а(пг. Однако проводившиеся нами до сих пор рассмотрения не содержат в себе такого доказательства даже для формализма аксиоматической арифметики').
В самом деле, вопрос о непротиворечивости этого формализма нашей нп-теоремой пока еще не решается Имеющие здесь место связи мы в дальнейшем рассмотрим самым присталь- А) См. т. 1, гл. ЧП, е. 454 ыли же Праловекае 1, ГЛАВА П ИРимеиение нп-теоРемы к АРиометикв 4 П ИССЛЕДОВАНИЕ АРИФМЕТИКИ ПРИ ПОМОЩИ СВЯЗАННЫХ С к-СИМВОЛОМ МЕТОДОВ ТЕОРИИ ДОКАЗАТЕЛЬСТВ $1.
Применение нп-теоремы к арифметике В главах УП и У(11 т. 1 мы рассмотрели два различных формализма арифметики: рекурсивную арифметику н формализм системы (Е) с добавлением к нему функции „А (х). Логич еский формализм, лежащий в основе рекурсивной а ифх. метики, п е й ариф- ными пе е р дставляет собой элементарное исчисление со своб переменными. К нему в качестве исходных формул добав- ляются аксиомы равенства и формула О'чм О, а в качестве схем— схема индукции и схема примитивной рекурсии. Средств этого формализма уже достаточно для того, чтобы с их помощью мо- жно было изобразить различные понятия, утверждения и дока- зательства элементарной арифметики.
С другой стороны, этот формализм еще допускает определенное финитное ноготков Но и без прямого обращения к этому истолкованию мы легко смогли доказать непротиворечивость этого формализма и даже установить, что всякая выводимая в нем формула, не с , не содержа- щая формульных переменных, при любой замене входящих в неэ свободных инднвндиых переменных цифрами после вычисле- ния значений соответствующих функций переходит в истинн формулу. Никаких трудностей в доказательстве не возникает и в том случае, если мы дополним данный формализм некоторыми есте- ственными обобщениями схем индукции и рекурсии в том виде, как они были рассмотрены нами в гл.
Ч11 т.1'). Другой формализм арифметики, рассмотренный нами в гл. Ч1П катов т. 1, был получен в результате объединения исчисле с аксиомами равенства (1,) и ()а), аксиомами Пеано') и ния преди- принимаемыми в качестве аксиом рекурсивными равенствами для сложения и умножения'). Получившуюся таким образом систему аксиом мы в свое время назвали системой (Е). К этому логи- ческому формализму мы затем присоединили ь-правило. С помощью ь-символа можно, жно, как мы это установили'), явно определить См. г. 1, с. 400 — 427, в См. т, 1, с.
272 — 273 н 325. а) Тем самым акснома (31) сгановнтсн нснудаой. а) См. т. 1, с. 481 н далее. нкцию раА(х), хаРактеРизУющУюсЯ формУлами (Рг) ЭхА(х)-РА(Ь А(х)). ()гз) А (а) -ь к,А (х) ~ а, (Рз) Чх ) А (х) -ь )г,А (х) = О. Мы показали, что с помощью этой функции могут быть изображены все те арифметические конструкции, которые опираются иа понятие наименьшего числа, обладающего заданным свойством.
Оказалось также, что если взять за основу функции сложения н умножения и воспользоваться функцией )ь„А (х), то схему примитивной рекурсии можно свести к явным определениям, причем таким образом, что на базе этих определений первоначальные рекурсивные равенства становятся выводимыми формулами'). То же самое верно н в отношении перекрестной рекурсии'). Что касается вопроса о непротиворечивости этого формализма, то нз теоремы об устранимости ь-правила а) вытекает, что для его решения достаточно рассмотреть данный формализм без ь-правила, т. е.
просто формализм системы (Е). В гл. Ч11 т. 1') мы осуществили другую редукцию, воспользовавшись теоремами о возможности замены общей аксиомы равенства ()а) соответствующими специальными аксиомами равенгтва и о заменимости аксиомы индукции соответствующей схемой. На этом пути мы пришли к системе аксиом а=а а=Ь-ь(а=с-РЬ=с)1 а'ФО, а=Ь а' Ь', а+О=а, а+Ь' (а+Ь)', аО* О аЬ=аЬ+а которая дополняется схемой индукции а(О) И (а) -~ щ (а') В (а) ") См. т. 1, с.
499 н далее. ') См. ъ 1, с. 509 — 5!О. Идею упоминаемого здесь доказательства, прннадлежащсго фон Найману, Р. Петер недавно неформальным образом прнмснила к общему случаю м н ого к р а т н ы х рекурсий, т. е. рекурсий, ведущихся по нескольким аргументам одновременно (см. ае работу: Р с ! е г й. Оьсг гие гпс1п1асье Пейпгыоп, — Ма!Ь. Апп. !936 113 № 4 4 5). Вто рассуждение Петер может быть полностью воспроизведено на языке теории доказательств. См. т.
1, с. 5!О н далее. См. т. 1! гл. 47П, а. 4$1 — 409. 76 исследование Арнэметики при помощи а.символа )гл. и (условие применимости этой схемы заключается в том, что переменная а должна встречаться в формуле 71(а) лишь на местах, указанных в качестве аргумента). Если в основу нашего рассмотрения положить исчисление предикатов,.то эта система аксиом, которую мы назовем системой (Е'), в отношении выводимости формул без формульных переменных (а значит, и в отношении арифметических выводов), а также в отношении непротиворечивости оказывается равносильной системе (Е).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
