Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 92
Текст из файла (страница 92)
а' ( Ь' и а = Ь-1- а' = Ь'. Третья иэ них есть (1 ) и с формулой (',); ервая получается иэ (1 ) в сочетан и э и а = Ь- ~(„.с Ь) а вторая получается иэ а = Ь-э- а «., Ь в результате подстановки. Тем самым в хаэенъегеровск (,) ожетбытьзамененаформуламн(1 ) а=Ь-Р 1( с.Ь) г ровском выводе и а = Ь-з- а ( Ь . С другой стороны, располагая формулой а ( Ь вЂ” ~- а'= Ь 1/ а' «. Ь, мы можем получить формулу а ~ Ь-Р а ( Ь )1' Ь ( а '), польвуясь схемой индукции и, кроме того, формулами О = О ((э) и («э), а также формулой Ф Э а=Ь-э-Ь«а (которая может быть получена иэ а = Ь-1- Ь = а ( Ь'). а = -1- = а и а = Ь-+. э Э) ДОПОЛНИТЕЛЬНОЕ РАССМОТРЕНИЕ АКСИОМ РАВЕНСТВА 461 Но, как бьгло замечено выше, используя формулы ()1), (1,), (1э), а чь Ь-~ а ( Ь 1/ Ь < а и добавив к ним формулу а = Ь-э- 1(а ( Ь), можно вывести (1,) и (1,).
Таким обраэом, в итоге получается, что в системе (В) аксиома (э' э) может быть эаменена формулами (11) и (1э), взятыми вместе с формулами а= Ь-1- Ц(а(Ь) и а=Ь-э а<Ь'. Здесь можно произвести еще одно упрощение, поскольку две последние формулы, с учетом наличия аксиомы (э1), делают ненужными аксиомы («л) и («.э). Итак, в конце концов вместо системы (В) получается следующая система аксиом: Теперь применим нашу теорему о второй аксиоме равенства (э' э) к системе (г,). В этой системе аксиом в качестве единственного предикатного символа (взятого в качестве основного знака) фигурирует знак равенства.
Однако, кроме штрих-символа, в ней имеются еще два математических функциональных анака: а + Ь и а Ь. Наша теорема в этом случае утверждает, что если интересоваться выводимостью формул, не содержащих формульных переменных, то формула ((э) монгет быть эаменена формулами (1,), (11) и следующими четырьмя формулами: Но последние четыре формулы с помощью формул ()1), (1,), (1,) и схемы индукции могут быть выведены нэ рекурсивных равенств для а + Ь и а.
Ь. Таким образом, при выводе арифметических формул, не содержащих формульных переменных, а также при исследовании вопроса о непротиворечивости, который сводится к вопросу о выводи- мости формулы О чь О, формулу (5 ) можно заменить двумя формулами (11) и (1 ). Формулу (1э), т. е. 1гл Уп РЕКУРСИВНЫЕ ОПРЕДЕЛЕЕДИЯ 5 5 Ополнительное РАссмотРение Акси Ом РАЕЕНСтвА 463 462 можно объединить в одну формулу а=Ь а'=Ь'. Если же мы, кроме того, заменим аксиому индукции равносильной ей ') схемой индукции, то получится система, состоящая из аксиом Ь=с), а = Ь->- (а = с->- а' ~ О, а=Ь а'= а+0 = а, а+Ь' =(а+ а 0=0, аЪ'=аЬ+ Ь)', ') См.
с. 326, д) См. с. 303 — 306. 5) См. с. 199. н схемы индукцдпд. Здесь как в аксиомах, так и в схеме индукции нет ни связанных, ни формульных переменных. Теперь при выводе арифметических формул мы вообще сможем избежать применения формульнмх переменных, ааменив все формулы исчисления предикатов схемами формул упоминавшимся в гл. Ъ'1 методом д), т. е. выполнив заранее в исходных формулах те подстановки вместо формульных переменных, которые должны были бы выполняться впоследствии, так что формульные переменные будут полностью исключены. Действуя таким обрааом, мы значительно ограничиваем наш формализм; разумеется, при этом мы ничего не выигрываем в части, касающейся установления его непротиворечивости; более того, такое ограничение формализма лишь частично предвосхищает результат операции возвратного переноса подстановок, который все равно имеется в нашем распоряжении в качестве начального шага в установлении непротиворечивости.
И все же для целого ряда рассмотрений полезно знать, что формализация арифметических доказательств может быть произведена столь ограниченными средствами. 3. Применение к проблеме разрешимости; устранимость аксиом равенства из выводов формул исчисления предикатов. Доказанная нами теорема о второй аксиоме равенства играет, в частности, важную роль в установлении взаимосвязи между аксиоматикой и проблемой разрешимости, Напомним рассуждение, которое мы проводили относительно этой взаимосвязи в гл. 1(г '). Мы рассматривали системы аксиом, такие что входящие в нх состав аксиомы жно ыло записать ть без функциональных знаков и ез р ых.
В таких системах при записи аксиом мож мульных переменных. так всякая об б и без свободных переменных, так как всякая воо ще о оитись впо авиа о муле, со свободными переменными дедуктивно р р. мула со зобо ных переменных связан- получающейся из нее путем замены сво од ными. Пусть Яд~ 1 Я1 без свободных переменных, изображающие рассмат— ч ормулы е иваемые нами аксиомы, и пусть иао раяд Ри ии и едложенне. Тогда условие, неоохоФор~ул~руемое этом теории пр димов и достаточное для того, чтобы лредлоя ение ыло мо иэ аксиом Я„..., ,..., Я при помощи докааательства, допускаюления п едикатов, заключает- щего формализацию в рамках исчис р о" о и лы, которая получается ся в выводимости той логическои р у иа формулы Я>8 ...
бди)->-6 е и е икатного символа некоторои заменой каждого входящего в нее пред то в). й,с тем же самым числом аргументов . формульной переменнои с словие в большинстве П едполагаемое в этом рассуждении условие в оль ре аксиом пап имер в системе рассматриваемых конкретных систем ак аксиом элемептарнои геом мет„ин (с исключением аксиом непрерыв, так как в этих системах ности, вообше говоря, не выполняется, так как этих м и е икатам обычно до авксиоматически введенным основным пр д ляется (содержательно понимаемое) отнош р ошенне авенства.
таких сл чаях мы можем действовать, как было замечено ранее ', двояб Д б б им аксиомы равенства к исчислению кима р з а ом. и о мы до авим в асши епном исчислении и едикатов и исследуем выводимость в расшир предикатов соответствующеи фор у, у пред и лы, пол чающейся из импликации Ядб, ... б Я1-.6 и о же мы равняем аксиомы в е Р вультате указанных замен, ли ми,...
Я, как мы это делали равенства в правах с аксиомами Яд,..., в арифметических системах. Однако у р вто ого из этих способов если интересоваться сведением проблемы доказуе(особенно, если н мости имеется тот недо- мост и в аксиоматике к проблеме разреши и ет формульная переменная. статок, что в аксиоме (15) фигурируе к тепе ь можно будет устранить, ааменив аксиому б формульных переменных.
рядом спец п иализи ованных аксиом ез впервую аксиому равенства Если мы добавим эти аксиомы, а такж д) Сдд гл )У с 171 РЕКУРСИВНЫЕ ОПРВДЕЛЕНИЯ 464 $»] дополнительнОВ РАссмотрение АксиОИ РАВенстВА 465 ИГЛ. ТП к нашей первоначальной системе, не включающей в себя аксиом равенства, то условия применимости предыдущего рассуждения будут выполнены, и поэтому докаауемость какого-либо предложения с помощью этих аксиом снова будет совпадать с выводимо- стью некоторой логической формулы в обычном исчислении предикатов ').
Вкратце поясним сказанное на примере системы сформулированных в гл. 1 аксиом») (включая и аксиому о параллельных) для основных предикатов Сг (х, у, и) (х, у, х лежат на одной прямой) Х»р (х, у, г) (х лежит между у и х), которые представляют собой аксиоматиэацию отношений сочетания и порядка для плоской геометрии, В основе рассмотрения будет лежать единственная предметная область — область «точек». Каждому из аргументов обоих основных предикатов Сг и Хч будет соответствовать некоторая специализация формулы (Уз). Ввиду симметричности этих предикатов, из шести получающихся таким образом формул мы можем взять только три, а именно — одну для Сг и две для Хсу.
К этим формулам мы добавим, кроме того, формулы (1») и (1,). Если мы заменим теперь свободные переменные связанными, а затем для равенства примем обозначение, аналогичное обоаначению основных предикатов Сг и Хсу, перейдя от употребления знака равенства к употреблению символа 14, то у вас получатся нять формул: )1х и (х, 'эсхилу'зз(1б(х, у)-е-(1й(х, г)-+-Ы(у, г))), 'чхс(ус(йуо(1с) (х, у)-е-(СТ(х, и, и)-+.Сг(у, и, Р))), МхМуМиМР(Ы(х, у)-е-(Усу(х, и, о)-+-Хчс(у, и, и))), МхМуМиМР(1Й(х, у) — з-(Я»г(и, и, х)-+ Х»в(и, Р, у))), которые необходимо будет добавить к прежним аксиомам, ириведенным в пп. 1, П и1П 9 1 гл. 1.
Если теперь обоаначить посредством й конъюнкцию всех аксиом, а посредством Я вЂ” формулу для какого-либо геометрического предложения, выразимого с помощью основных предикатов 1б, Сг и Х»в, то доказуемость этого предложения на основе наших аксиом будет равносильна выводимости в исчислении предикатов формулы, которая получит- с) В связи с этим см. проведенное с позиций теоретико-мивжвстввииой логики првдикатов исследование Л.
Кальмара (К а 1 ш з г Е. Есцв Ввевгяццз зцг Еасвсй»Ыавзвсйвог!в.— Ас»а ЕКЕ 8сй 8»взе4, 4929, 4, Аз 4). ») См. с. 28 и двявв. ся из формулы если мы всюду заменим в ней символ 1б формульной переменной А с двумя аргументами, а символы Сг и Хтс — формульными переменными В и С с тремя аргументами. Заметим, что этот метод исследования доказуемости сохраняет свою применимость и в том случае, когда речь идет о докаауемости предложений, наображаемых формулами ~~, содержащими формульные переменные.
В самом деле, в выводе такой формулы Я входящие в нее формульные переменные не долисны затрагиваться (каждая начиная с того места, где она впервые появляется среди формул, связанных с заключительной формулой вывода), т. е. По отношению к ним не должны производиться никакие подстановки. Таким образом, они ведут себя точно так же, как н предикатные символы. В силу этого выводимость формулы Я совпадает с выводимостью формулы, которая получится из Я, если мы каждую из входящих в $ формульных переменных заменим новым предикатным символом с тем же самым числом аргументов.
Для исследования этой выводимости, кроме уже добавленных вместо второй аксиомы равенства (1») специализаций этой аксиомы,мы должны будем добавить в качестве аксиом некоторые другие ее специализации для вновь вводимых предикатных символов. Из этого рассуждения мы можем извлечь еще одно важное следствие. Пусть Я вЂ” формула исчисления предикатов, выводимая с привлечением аксиом равенства. Как уже отмечалось, мы можем, не производя никаких других изменений, заменить в выводе этой формулы встречающиеся в ней формульные переменные предикатными символами с тем нсе самым числом аргументов.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
