Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 102
Текст из файла (страница 102)
Пг) ыть выве ены рекурсивные равенства дл ф я функции Так, в случае рекурсивных равенств ф (а, О) = а (а), ф (а, и') = Ь (а, п, ф (а, и)) это выглядит следующим образом. Термам а(с) и Ь(с й, т ветствуют некоторые формулы Я(с Ь) и 6'с й и ф в (2) соответствует некоторая формула а,, о соответствие имеет место в том смысле то указанные рекурсивные определения п исое еи я присоедин ть с стеме (~), ми формулами следующие эквивалентности: Я (с, й) я (с) = Й, 6(с, й, т, Ь) Ь(с, й, т)=Ь, Е(а, Ь, Й) ф(а, Ь)=й. В самой системе (Х) будут выводимы формулы Е(а, О, с) Я(а, с), Е(а, и, Ь) (Е(а, и', с) 6(а, и, Ь, с)), соответствующие рекурсивным равенствам для функ ункции ф. 1) См, в связи с этим г.
1, с. 499 — 510. Дедуктивный формализм мы называем непротиворечивым, если не существует таких двух формул Я и ) Я, которые можно было бы вывести средствами этого формализма. Опираясь на тождественную формулу Аз-() А-РВ), из пары формул Я и ) Я можно вывести любую формулу рассматриваемого формализма. Поэтому для установления непротиворечивости любого формализма, включающего в себя наше исчисление высказываний, достаточно показать, что в рассматриваемом формализме ие выводима какая-нибудь специально подобранная формула этого формализма. 9 3. Теоремы об исчислении предикатов Приведем еще ряд понятий и фактов'), относящихся к исчислению предикатов и к таким дедуктивным формализмам, которые получаются из него, как только что было описано в 6 2, путем добавления каких-либо индивидных и предикатных символов, функциональных знаков, а также тех или иных аксиом').
(1-правило сюда не включается.) 1. Формула Я называется переводимой в формулу 6, если выводима эквивалентность Я З или — что сводится к тому же самому — если выводимы обе импликации Я-з-З и 6 — РЯ. 2. Любая формула переводима в некоторую п редва ренн ую формулу, у которой все входящие в иее кванторы стоят в начале, а области их действия простираются до конца этой формулы. 3.
Формула Я называется дедуктивно равной форм у л е 6, если при включении в число исходных формулы Я становится выводимой формула З, а при включении в число исходных формулы 6 становится выводимой формула Я, или, короче, если из Я выводима формула 6, а нз 6 выводима формула Я. 4. Всякая формула Я дедуктивно равна любой такой формуле З, которая получается из Я, если каждую входящую в нее свободную индивидиую переменную заменить какой-нибудь соответствуюгцей ей ранее еще не встречавшейся связанной переменной, а относящиеся к введенным связанным переменным кванторы всеобщности в произвольном порядке записать в начале формулы, распространив тем самым области их действия до самого конца формулы.
Эта операция, преобразующая формулу Я в дедуктивно равную ей формулу 6, называется заменой свободных переменных связанными; обратная операция зачеркивания стоящих перед формулой кванторов всеобщности и замены отно- ') См, в связи с этим т. 1, с. 173, 182 в 185, 191 †2, 250, 275 †2, 286 — 288 456 459 з) В дальнейших формулировках мы не всегда будем оговаривать то, что мм ограничиваемся рассмотрением таких формализмов, ПРИЛОЖЕНИЕ сящихся к ним связанных переменных ранее не встречавшимися свободными переменными называется соответственно з а м е н о й связанных переменных свободными.
5. Всякая формула дедуктивно равна некоторой сколемовской нормальной форме, т. е. такой предваренной формуле, в кванторной приставке которой никакой квантор всеобщности не предшествует никакому квантору существования'). 6. Имеет место следующая Дедукцно ни а я теорема. Если формула 3 выводится из некоторой формулы й пикам образом, что никакая фигурирую- и)ая в Я свободная переменная при ятом не затрагивается, т. е. не используется ни в одной производимой вместо нее подстановке, а также не фигурирует в качестве выделенной переменной какой- либо из схем (а) и (Р), то формула 6 — ь6 может быть выведена без использования формулы Я. Ч.
Аксиома равенства (ля), т. е. формула а Ь-ь(А (а)-+-А (Ь)), при выводе формул, не содержащих формульных переменных, может быть ааменена конечным списком собственных аксиом вида а=Ь-ь(Р(а)-+ 4)(Ь)) а Ь-ь((а) ((Ь), где )р' — предикатный символ, а ( — функциональный знак рассматриваемого формализма, причем, кроме явно указанного аргумента, они могут содержать и какие-нибудь другие аргументы, отличные от а и Ь. Формулу такого вида мы называем специальной формулой равенства, соответствующей (или относящейся к) указанному аргументу рассматриваемого предикатного символа или функционального знака. [Этим предикатным символом или соответственно функциональным знаком и указанием интересующего нас аргумента такая формула определяется однозначно с точностью до обозначения свободных переменных, стоящих на месте остальных аргументов, если таковые имеются.] В число формул вида а-Ь-ь(4)(а)- 4)(Ь)), ь) Эту чтеоретиио-доиааательствеииуюь сиолемовеиую иормальиую форму следует отличать ет двойствеииой ей (т.
е. получающейся ив иее в результата иамеиеиии ролей иваиторов всеобшиости и существования) чтеоретиио-модельиой сиолемовсиой иормальиой форммэ (см. е. 233 этого тома), СЧИСЛЕНИЕ ПРЕДИКАТОВ БЕЗ ПРАВИЛА ПОДСТ АНОВКИ 473 исч в частности, включается и формула а=Ь-ь-(а=с-ьЬ с). 8. Всякий вывод допускает разложение на нити. Если, мы напишем над начиная с заключительной формулы вывода, аждой ~рормулой, по " ф " лучающейся из какой-либо предшествующей ф результате повторения, подстановки ей в выводе чормулы в „ (а) и ф), эту самую пе еименования либо по одной из схем а и , эт фо м л , а над каждой результирующей р- предшествующую „рмулу, — обе формулы, из которых м лой какой-либо схемы заключения — е оиа получается по этой схеме, причем с соблюдением следующего порядка: й Š— 3 то получим то, что мы на называем фигурой разложения дан- ного вывода. етствия между формулами получивВзаи мио однозначного соотв иг ы и о мулами самого вывода, вообще шеися таким образом фигуры и фор говоря, нет.
Более того, одна и та же ч рмула выв ия может стоять во многих местах, в фигуре разложения не стоят а исходными формулами в и ы з фо лы (здесь имеет место ветвлеы заключения стоят две ч рмулы зд й " формулой стоит по одной формуле. х); над любо другой Последовательность формул из даннон й, не являющейся заключительной формулой в формулой, не я й фигуре непосредственно под следует формула, стоящая в это ней, называе тся нитью доказательства. азложения вывода на нити 9. С помощью этой процедуры ра етном выводе можно все подстановки п ерелюбом "онкрсгио схо ные формулы, т. о й котором подстановки можно построит ь такой друго вывод, в ф ли в такие формулы, производятс я только в исходные формулы и ых в ез льтате одной или несколь- которь'е получаются из исходнь|х в Реву х г за д угом подстановок.
азумеется, и ( ) (Р) вместо переменной а нужно допуст стить чтобы в схемах а и обо ые индивидные переменные. могли фигурировать другие сво дные й 4. Исчисление предпкатов без правила подстановки Возможность переноса подстановок в исходные формулы открывает пе ед нами возможнос ность обходит" ся без использования правила . Эт жно добиться, допустив в качестве исходи подстановки. Этого можно д и формул не только прежние исходные формулы рассматрив 475 474 исчисление пгедиклтов вез ПРьвилл подстановки ПРИЛОЖЕНИЯ формализма, но еще и формулы, получающиеся из них в результате одной или нескольких следующих друг за другом подстановок, а кроме того, ликвидировав выделенную роль переменной а в схемах (сс) и ф) В частности, таким образом удается полностью исключить формульные переменные из выводов формул, не содержащих формульных переменных, так что формально-дедуктивное рассмотрение аксиоматических теорий вполне может производиться без привлечения 4аормульных переменных.
При таком способе изложения правило, позволяющее брать в качестве исходных формул любые тождественно истинные формулы исчисления высказываний, расширяется: в качестве исходных формул допускаются любые формулы, получающиеся из тождественно истинных формул исчисления высказываний в результате каких-либо подстаиовок. Функции основных формул (а) и (Ь) в этом случае выполняют схемы формул Чхй (х) -«Я (1) Я (1) -« =ЬЯ (х), где 1 обозначает некоторый терм, а место аксиом занимают схемы аксиом, в которых прежние свободные индивидные переменные заменены обозначениями произвольных термов, а прежние формульные переменные заменены обозначениями произвольных формул.
Так, например, вместо аксиом равенства у нас появляются схемы аксиом и с = 6 -« (Я (с) -« Я (6)), где с, 6 и 1 обозначают произвольные терлсы. Тем не менее здесь имеется возможность сохранить в аксиомах свободные индивидные переменные (и, в частности, избежать замены собственных аксиом соответствующими схемами) без того, чтобы потребовалось добавлять правило подстановки. Действительно, с помощью схемы формул Чхй(х)-«Я(1) и схемы (а) в ее модифицированном виде Я -« 6 (с) Я вЂ” «Чхб(х)' где с — произвольная, не входящая ни в Я, ни в 5(х) свободная индивидная переменная, правило подстановки вместо свободных индивидных переменных мы получаем в качестве производного и авила.
о означает, и . Эт ает что из формулы й(а) со свободной пере- о- пр пенной а для произв извольного терма 1 может быть выведена ф р- м ла о (1). Это достигается следующим образом. ачала случай, когда й (а) не содержит перемен- Рассмотрим сначала уч ", ной х. Мы возьмем какую-нибудь выводимую формулу ~,н р- нс, о мулу вида Ю-«С), в которую не входит переменная а. Образованная с помощью этой ю этой формулы формула Я (а)-«(ф — «й(а)) м лы, так как она ожет быть взята в качестве исходной формулы, так к к может пол ается в результате подст о становки из тождественно истинной о м лы А-«(В-«А)). Вместе с формулой й(а) она при помощи для квантора всеобщности дает нам формулу М,х,-« .
формулы вместе с выводимой формулой сл) двух- к атиым применением схемы заключения дают вам форму у (). и формула й (а) содержит переменную х, начала перейдем от этой формулы к иекоторо „ормуле переименовывая х в какую-ни удь друг в формуле Я(а) связанную переменную; затем из а т что указанным способом мы получим формулу, а последней путем п „ ереимеиования появившейся вместо х перемен- ной получим формулу Я (1). сх мы, вп очем, П разило переименования связанных переменных мы, р м л для лать производным, если в схемах фор у ной х.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
