Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 52
Текст из файла (страница 52)
Вместо функций Ф„..., Ф« возьмем функции Ф,*, ..., Ф1*. 3. Вместо собственного имени для индивида из У вЂ” некоторый анак для целого класса индивидов. Но это означает, что формула Я выполнил~а в некоторой и- элементной индивидпой области и что, следовательно, формула )Я не является п-тождественной. Но п ( 21, а ранее мы показали, что всякая (п + 1)-тождественная формула является также и птождественной.
Поскольку формула ) Я не является и-тождественной, то отсюда следует, что она не может быть также и 2»- тождественной. Следовательно, формула Я выполнима в некоторой 2~-элементной индивидной области. Конечно, это рассмотрение не удовлетворяет требованиям припятой нами методики. Но мы можем уточнить его до финитного рассуждения, выдержанного в духе теории доказательств. В самом деле, теорема, которую мы только что сформулировали и доказали нефинитным образом, допускает следующую, более сильную формулировку: Если формула одноместного исчисления предикатое содержит не более 1 формульпых переменных с аргументом и является 2~-тождеетеепной, то опа еыеодима.
Правда, доказательство этой теоремы, получающееся пере- осмысливанием предыдущего рассмотрения в духе теории доказательств, оказывается довольно трудным, и поэтому мы проведем его здесь только для простейшего случая 1 =- 1. Не умаляя общности, мы можем ограничиться в этом докааательстве рассмотрением только таких формул, которые не содержат свободных индивидных переменных. Действительно, любая формула со свободными нндивидными переменными дедуктивно равна формуле, получающейся из нее связыванием по правилу (е) ") всех свободных индивидных переменных путем простановки перед формулой соответствующих кванторов всеобщности. Положив 1 = 1, мы будем иметь дело с 2'-тождественной, т.
е. с 2-тождественной формулой одноместного исчисления предикатов, в которую входит только одна формульная переменная с аргументом. Ксан обоаначить эту формульную переменную символом Р, то рассматриваемая формула после разложения ее в примарные формулы и после исключения тех примарпых формул, в которые переменная Р входит более одного рава»), окажется построенной из прнмарных формул Чх Р(х), чх )Р(х), Вх Р(х), Зх ~Р(х), а также нз формульных переменных без аргументов. Обозначим эту формулу символом Я(Р). Пусть Я*(Р, а) означает формулу, которая получится из Я (Р), если чх Р(х) и Эх Р(х) заменить посредством Р (а), а »«х -) р (х) и Дх чр (х) — посредством 1Р(а); пусть, кроме того, Я««(Р, а, Ь) означает формулу, которая получится нз Я (Р), если 7х Р (х) заменить посредством Р!(а) А Р (Ь), чх ~Р(х) — посредством ~Р(а)А ~Р(Ь), зх Р (х) — посредством Р (а) )( Р (Ь), Зх )Р(х) — посредством )Р(а) )/ ~Р(Ь).
Наше и едположенне, что формула Я (Р) является 2-тождественной, а тем самым и 1-тождественной, означает, что формулы Я*(Р, а) и Я *(Р, а, Ь) получаются в результате подстановки из некоторых тождественных формул исчисления высказываний. Нам требуется доказать, что при этом предположении формула Я (Р) оказывается выводимой. Таким образом, речь идет о том, чтобы вывести формулу Я ( ) из Я* (Р, а) и Я** (Р, а, Ь). Это может быть проделано следующим образом. ') с . . )т«. ») Си. с, 232. ИСЧИСЛЕНИЕ ПРЕДИКАТОВ С РАВЕНСТВОМ [гл, т РЕШЕНИЕ ПРОБЧЕМЫ РАЗРЕШИМОСТИ Как легко убедиться, обе формулы 1ех(Р(х) Р(а)) -+.
(Я (Р) Я*(Р, а)), Чх((Р(х) Р(а)) ~! (Р(х) Р(Ь))) -э- (Я (Р) Я*~(Р, а,, Ь)) выводимы. Первая из них в сочетании с Я* (Р, а) дает чх (Р (х) -+- Р (а)) -~- Я (Р); ив второй в сочетании с ЯЯ* (Р, а, Ь) мы получаем 1зх((Р(х) Р(а)) ~/(Р(х) Р(Ь)))-э-Я(Р). Используя выводимые формулы ~х Р (х) -~- 'Фх (Р (х) Р (а)) и 7х ~1Р(х) -~. Рх(Р(х) Р(а)), мы из формулы ч х (Р (х) Р (а)) — ~ Я (Р) по правилу силлогизма получим формулы Ух Р (х) -~ Я (Р) 7х 1Р(х) — ~- Я (Р). Далее, из формулы чх((Р(х) Р(а)) ~/ (Р(х) Р(Ь)))-~ Я(Р) мы с помощью выводимой формулы Р(а)А 1Р(Ь) — ~ 7х((Р(х) Р(а)) ~/ (Р(х) Р(Ь))) получим формулу Р (а) А ~Р (Ь) — ~ Я (Р); из нее, выполнив соответствующие преобразования, получим Р (а) — э ( 1Р (Ь) — ~ Я (Р)), а отсюда двукратным применением схемы (р) и путем элементарных преобразований получим Зхр(х) АЭх 1Р(х) — ~ Я (Р).
Но тем самым мы оказываемся у поставленной цели; действительно, последняя формула вместе с двумя ранее полученными АР(х) -э- Я (Р) и 7х .1 Р (х) -э Я (Р) дает 7хР(х) ~„! 7х 1Р(х) ~/ (Зхр(х) АЗх 1Р(х)) -~ Я (Р); посылка этой нмпликации является выводимой формулой, так что с помощью схемы заключения мы получим В этом выводе идея предыдущего содержательного доказательства находит свое отражение в применении формулы Р(а) А'ЧР(Ь) ч- чх((Р(х) Р(а)) ~/ (Р(х) Р(Ь))). Действительно, при содержательном истолковании эта формула выражает ту мысль, что если мы рассматриваем всего лишь одну- единственную логическую функцию, то в смысле упомянутого выше разбиения на классы таких классов окажется самое большее два.' При с = 2 вместо атой формулы будет фигурировать формула Р (а) & () (а) & Р (Ь) & "1 (! (Ь) А ~ Р (с) А ~) (с) А 1Р (д) А "1 0 (д) — эЧх(((Р (х) Р(а)) А (Ч (х) Ч (а))) ~/ ((Р (х) Р (Ь)) ~/ (() (х) Ч'(Ь))) ~/ ((Р (х) Р (с)) А ф (х) () (с))) ~/ ((Р (х) Р (д)) А (() (х) (Э (сК)))).
Здесь вместо двух переменных а и Ъ у нас будут четыре переменные а, Ь, с и д. Аналогично, в общем случае приходится ввести 21 свободных индивидных переменных. Получающаяся таким образом теорема о том, что 2~-тождественная формула одноместного исчисления предикатов, содержащая не более г формульных переменных с аргументом, является выводимой, также дает нам способ для распознавания выводимости произвольной заданной формулы одноместного исчисления предикатов.
В качестве непосредственного следствия из этой теоремы вытекает, что каждая формула одноместного исчисления предикатов, тоя~дественная в конечном, является также и выводимой. Мы докажем также теорему о том, что всякая формула одномесшноео исчисления предикатов либо выполнима в конечном, либо опровержима. Действительно, пусть Я вЂ” произвольная формула одноместного исчисления предикатов, и пусть с' — число различных встречающихся в ней формульных переменных; тогда либо Л 2 -выполнима, либо Ч Я 2 -тождественна. В первом случае 1 Я выполнима в конечном, во втором случае формула Ч Я выводима и, значит, Я оказывается опровержимой. РЕШЕНИЕ ПРОВЛЕМЫ РАЗРЕШИМОСТИ 250 ИСЧИСЛЕНИЕ ПРЕДИКАТОВ С РАВЕНСТВОМ !ГЛ У. 251 1 21 3. Нормальная форма формулы расширенного одноместного исчисления предикатов на основе дедуктивного равенства. Теоремы о полноте, только что установленные нами для одноместного исчисления предикатов, могут быть распространены и на расширенное одноместное исчисление прсдикатов.
Для формул этого исчисления также справедливо утверждение о том, что всякая формула, тождественная в конечном, может быть выведена по правилам этого формализма и что всякая формула либо выполнима в конечном, либо опровержима. Проблема разрешимости для этого формалнэма также полностью решается. Этн результаты вытекают нэ следующей теоремы: Всякая формула расширенного одноместного исчислсния прсдикатов дсдуктивно равна некоторой' другой формуле, которая либо сама является количественной формулой, либо оказывается составленной из количсствснных формул с помощью связок исчислсния в иска зыва ни й.
Эта теорема, сводящая теорию расширенного одноместного исчисления предикатов к всецело элементарным рассмотрениям, первоначально была найдена Девенгеймом, а затем более простым способом была доказана Сколемом. Неэависимо от исследований Левеыгейма и Сколема к тому же самому результату пришел Беман '). Докааательство следует методу, предложенному Беманом ').
Мы будем существенным образом опираться ыа доказанную ранее теорему о рааложении формулы расширенного одноместного исчисления предикатов в примарные формулы. Далее, мы будем пользоваться теоремой иэ гл. 1У, которая говорит о том, что формула переходит в дедуктивно равную, если одну или несколько входящих в эту формулу свободных индивидных ыеременпых заменить связанными переменными и поставить перед формулой соответствующие кванторы всеобщности, или если, наоборот, отбросить один нлн несколько стоящих перед атой формулой кванторов всеобщности, а соответствующие им переменные заменить ранее не встречавшимися свободными индивидными переменными '). Эту операцию перехода от свободных переменных к связанным и обратно мы будем кратко наэывать «заменой» (Апя1апясЬ) свободных переменных связанными и соответственно связанных переменных свободными. ') С 5 к я и Ь е ! ш Ь.
ОЬег МО61!«1кЬя!1«п !ш В«1я!!«ЬА)ЬВ1.— Ма1Ь. Апп.. 1915, 76; 8 Ь о ! е ш Т. СВ1«гяис1шпхвп 6Ь«г 6!е Ахгопкя к)яя К1аяяяпЬя)ЬВ1» ппк! йЬяг Ргьк)пЬ!Ак!опя- ши! БппипапьпяргоЫяпкя, ме1сЬ« Еяя~зяяя К1аяяяп «оп Апяяябяп Ьв1гяйяп,— УЫяпвхаряяя1»Ьаря!я 3ЬТ!!кяг 1, МакЬ.-)ЧА1. К1., 1919. М 3, 1 1; В я Ь кп а и и Н.
Веыгяде хпг А16яЬгя к!ег Ьоа!Ь, !п»Ьяяопйеге кита Еп!яссе!к!ВпуяргоЫяш.— МякЬ. Апп., 1922, 86, 26 314. к) См. Я 20 м 21 только что цвтпровяппого сочппякпя Вямява. Я) См. гл, 1У, с. 193. Пусть теперь дана формула расширенного одноместного исчи- сления преднкатов. Как было покааано вькше '), рядом преобра- зований ее можно перевести в некоторую формулу, составленную с помощью свяэок исчисления выскаэываний иа формул следую- щих шести типов: 1. Формульные переменные беэ аргументов. 2.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
