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

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 41)

1ао — !аз. 189 теОРемА эРБРАнл 166 а.символ и логичгскип оогмхлизм (гл гц как для этого символа будут иметься только собственные аксиомы, он может быть полностью уравнен с остальными предикатными символами, и тогда мы получим некий формализм гэ без знака равенства. В соответствующем формализме Р' будут содержаться одновременно два символа; = и 1д.

Для символа == у нас будут иметься аксиомы ()з) и (Яз), а для символа 1б — некоторые собственные аксиомы, которые будут внесены в список аксиом л~,*, ..., 31„*. Поэтому и в случае таких формализованных систем аксиом с функциональными знаками, когда равенство либо вообще отсутствует, либо фигурирует в сочетании с одними лишь собственными аксиомами, исследование выводимости формул сводится к исследованию выводимости в некоторых специальных системах аксиом без функциональных знаков'). Рассмотренное здесь сведение теоретико-доказательственного исследования систем аксиом с функциональными знаками к исследованию систем без функциональных знаков имеет большое принципиальное значение, так как для систем аксиом первой ступени без функциональных знаков исследование выводимости какой- либо формулы, как мы уже знаем, сводится к выяснению вопроса о выводимости некоторой формулы в чистом исчислении предикатов.

Еще раз вкратце напомним, как происходит это сведение. Во-первых, исследование выводимости произвольной формулы из формализма рассматриваемой системы аксиом сводится к исследованию выводимости некоторой формулы без формульных переменных'). В выводе формулы такого рода аксиома равенства (Лз) может быть заменена некоторыми собственными аксиомами, так что мы должны будем иметь дело с выводимостью формулы только из собственных аксиом (средствами исчисления предикатов). А теперь пусть 11 — подлежащая выводу формула, и пусть 3(ы ..., 3(и — формулы, получающиеся из наших собственных аксиом путем замены свободных переменных связанными, Тогда исследуемая нами выводимость будет равносильна выводимости формулы 3(зй".йу(з-'"б средбтвами одного только исчисления предикатов.

В силу нашего предположения в этой формуле не встречаются никакие другие символы, кроме индивидных и предикатных, и поэтому ее выводимость равносильна выводимости формулы чистого исчисления предикатов, которая получается из нее в результате замены упо- ') Разумеется, здссь мы нс учитываем случай, когда систина аксиом содсржит аксиому (Лз), но нс содержит аксиомы (Л,), и в ной невозможно вывести зту аксиому. Однако в применениях теоретической логики этот случай сдва ли интересен. ") См. относишисси н этому вопросу замечания на с.

37 — 33 и в т. 1, с. 466. мянутых индивидных символов какими-либо ранее не встречавшимися свободными индивидными переменными, а предиклтных символов — формульными переменными. Аналогичным образом можно показать, что непротиворечивость этой системы аксиом (в рамках способов рассуждений, формализуемых средствами исчисления предикатов) равносильна невыводимости формулы, получающейся из отрицания формулы а,й„.ай(и в результате упомянутых замен индивидных и предикатных символов соответствующими свободными переменными. Теперь, благодаря теореме о возможности замены функциональных знаков предикатными символами, эта редукция вопросов о выводимости тех или иных формул в различных аксиоматнческих системах и о непротиворечивости этих систем к вопросам о выводимости соответствующих формул в чистом исчислении предидикатов распространяется и на системы аксиом с функциональными знаками.

Но, с другой стороны, все-таки следует подчеркнуть, что при исследовании той или иной выводимости исключение функциональных знаков отнюдь не всегда бывает выгодным. Наоборот, исследуя выводимость в чистом исчислении предикатов, мы иногда бываем вынуждены ввести какие-либо функциональные знаки. После этих вводных рассуждений мы теперь возвратимся в основное русло нашего изложения. й 3.

Теорема Эрбрана Формулировка второй е-теоремы не исчерпывает всего содержания приведенного нами доказательства этой теоремы. И действительно, с помощью этого доказательства мы не только убедились в возможности исключать — при выполнении предположений, приведенных в формулировке второй е-теоремы, — з-символы из выводов любых не содержащих вхождений е-символа формул, но при этом мы выявили еще и некоторый специальный тип выводимости, и это имеет большое значение вне зависимости от того, чтб можег дать нам оперирование с е-символом. Чтобы этому материалу, изложенному в доказательстве, придать форму, удобную для применений, целесообразно освободить рассуждение, с помощью которого мы доказывали вторую е-теорему "), от использования сколемовской нормальной формы'). з) См.

с. 169 и далсс. ') Вместо этого мы могли бы отказаться от получении в конечном рсзультате снолсмовсиой нормальной формы дли рассматривасмоя формулы. Однако это нс привело бы нас к окольно-нибудь заметному упрощению. 191 ТЕОРЕМА ЗРВРАНА 4 э1 99О е-СИМВОЛ И ЛОГИЧЕСКИЙ ФОРМАЛИЗМ [ГЛ и! С этой целью мы должны будем еще раз вкратце повторить это рассуждение, причем вместо формулы 6 специального вида 3!',...39„)(В,...

УВ,Я(~, ..., 9) мы теперь возьмем произвольную предваренную формулу. Чтобы понять требующиеся в связи с этим модификации, нам будет достаточно рассмотреть какой-нибудь типичный пример. В качестве такового мы возьмем формулу 6, имеющую вид 3Яхчу3и3оЫг3вЯ(1, х, у, и, о, г, в). Условимся, что в 6 не входят никакие связанные переменные, кроме указанных, но будем считать, что, кроме переменных и логических символов, в нее могут входить еще и какие-нибудь дополнительные иидивндные, функциональные и предикатные символы. Пусть эта формула 6 выведена средствами исчисления предикатов, причем имеется вывод, в котором не используются никакие аксиомы, но, может быть, используются дополнительные индивидиые, функциональные или предикатные символы. Будем предполагать, что в 6 не входят функциональные знаки ~р, ф и Х.

л(ы выведем сначала формулу 6-«313и3о3вЯ(1, ~р(1), ф(1), и, о, Х(1, и, о), в). Это может быть сделано следующим образом. Будем исходить из выводимых формул (1) 3И(х1(уА(1, х, у)- 3(А((, <р(1), ф(1)) и (2) 313и3о»(гА(1, и, о, г)-».313и3оА(1, и, о, Х(1, и, о)), которые получаются использованием основной формулы (а) исчисле- ния предикатов вместе с подстановками и применениями правила (ь)'). Если в формулу (1) вместо именной формулы А(а, Ь, с), где а, Ь и с — три различные, не входящие в формулу 6 свободные пере- менные, подставить формулу 3и3о»ег3вЯ(а, Ь, с, и, о, г, в), то получится формула (3) 6-» 313и3о7г3вр!(1, ч (1), ф(1), и, о, г, в).

С другой стороны, если мы в формулу (2) подставим формулу 3вЯ(а, ч»(а), ф(а), Ь, с, Ь, в) вместо именной формы А(а, Ь, с, Ь), где Ь вЂ” какая-либо отличная от а, Ь и с и не входящая в формулу 6 свободная переменная, х) Сн. т, 1, с. 176, то получим формулу 313и3онг3в91(1, Ч»(1), »р(1), и, о, г, в) -«313и3о3вЯ(1, (р(1)»р(1), и, о, Х(1, и, о), в), которая вместе с формулой (Э) по правилу силлогизма дает искомую формулу (4) 6- 313и3о3вЯ(1, <р(1), »р(1), и, о, Х(1, и, о), в). Вывод этой формулы (4) совместно с заданным выводом формулы 6 даст нам вывод формулы (5) 313и3о3вЯ(1, ср(1), ф(1), и, о, Х(1, и, о), Го) средствами исчисления предикатов.

А теперь из этого вывода формулы (5) по обобщенной первой е-теоремех) мы получим вывод некоторой дизъюнкции, состоящей из членов вида »)((д, <р (д), ф (Ч), Г, д, Х (а, с, 6), 1), где Ч, Г, 6 и ! — некоторые термы, построенные нз свободных переменных, иидивидных символов н функциональных знаков, причем этот вывод будет производиться средствами элементарного исчисления со свободными переменными без использования каких бы то ни было аксиом. Поэтому данная дизъюнкция должна получаться подстановкой из некоторой тождественно истинной формулы исчисления высказываний, и, значит, она будет истинной в логике высказываний ').

К этому же самому результату можно прийти и путем следующего, в эвристическом отношении более привлекательного рассуждения '). Какова бы ни была формула П, по выводу формулы 6 всегда можно построить вывод импликацин ') 6-«1!. Возьмем в качестве !( какую-нибудь бескванторную формулу, отрицание которой является истинным в логике высказываний, т. е. получается подстановкой из некотопой тождественно истинной формулы исчисления высказываний ), — например, формулу вида Ч)6Г )"4), где »4) — какая-либо элементарная формула.

Сначала мы предположим, что формула 6 не содержит свободных переменных. Отрицание формулы 6 может быть преобразовано в формулу »йНх3у'Г(и но3г'Г(в ) Я(1, х, у, и, о, г, в), х) Си. с. 54 и далее. а) Сн. Приложение 1, с. 462. а) Идеи этого рассуждения восходит к Эрику Стеннусу, !92 е-СНМВОЛ И ЛОГИЧЕСКИН ЕОРМАЛИЗМ 1гллн ТЕОРЕМА ЭРБРАНА которую мы обозначим через 6т. Из этой формулы выводима формула И. К формуле ьхт мы применим процедуру символьного решения ').

Эта процедура — после того как будут выбраны какие-нибудь отличные друг от друга свободные переменные, например а, Ь, с и й, а также какие-нибудь одноместные функциональные знаки Ч» и »р и трехместный функциональный знак (функциональные знаки берутся из числа тех, которые в ьх ие встречаются), — даст иам бескванторную формулу 1 Я (а, »р(а), тР(а), Ь, с, Х (а, Ь, с), й), которую мы обозначим через 6е. От этой формулы можно средствами исчисления предикатов вернуться к формуле ~~„а потому из нее выводима и формула И. В этом выводе формулы И из формулы чха ни исходные фор. мулы, ни сама результирукбщая формула ие содержат связанных переменных. Поэтому применение теоремы об элементарном выводе, которую мы в свое время получили нз первой а-теоремы' ), позволяет нам заключить, что формула И может быть выведена из 6п средствами одного только элементарного исчисления со свободными переменными.

Кроме того, в таком выводе, разложив фигуру доказательства на нити, можно перенести подстановки в исходные формулы '). Тогда на месте исходной формулы 6п появятся епримеры» этой формулы, т. е. формулы, получающиеся из 6п в результате подстановок термов вместо свободных переменных. Онн имеют внд ) Я (Ч„ р (Ч,), Р (Ч,), „ б„ Х (Ч„ т„ б,). 1,) (1=1, ..., п). Мы сокращенно обозначим их через !Я„..., )Яп. Формула И выводима из этих формул средствами одного только исчисления высказываний, и поэтому в силу дедукционной теоремы формула ! Лт ет 3» 1Лп выводима без использования аксиом, средствами одного только исчисления высказываний, а тем самым оиа истинна в логике высказываний, Значит, то же самое верно и в отношении формулы ) И Я, !/ ... Ч 91„, а так как формула )И тоже истинна в логике высказываний, '! См.

Характеристики

Список файлов книги