Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 50
Текст из файла (страница 50)
Этих вопросов мы уже касались в гл. зтг' т. 1, и нами было высказано обещание обсудить их более подробно '). Мы изложим здесь некоторые вопросы, связанные с теоретико- множественной трактовкой проблемы разрешимости. При этом мы сознательным образом откажемся от выполнения требований финитной точки зрения Напомним, чтб мы понимаем под в ы п о л н и м о от ь ю какой- либо формулы й чистого исчисления предикатов в теоретико-мно- жественной логике предикатов'). Выполнимость формулы 6 означает, что можно выбрать такую индивидную область з' и такие замены свободных иидивидных переменных формул й индивидами из з', формульных переменных без аргументов истинностными значениями и формульных переменных с аргументами логическими функциями с тем же самым числом аргументов, пробегающих область У, что при этих заменах формула й примет значение «истинак При этом вычисление значения $ производится с учетом истинностиых значений элементарных формул на основе понимания связок исчисления высказываний как истинностных функций и следующего толкования кваиторов: формула Чрг! (е) при указанных заменах принимает значение «истииа», если для каждого индивида а из рассматриваемой индивидной области формула р((а) имеет значение «истина», и значение «ложь» в противном случае; а формула :-)ер( (х) при этих заменах принимает значение «истина», если по крайней мере для одного индивида а рассматриваемой индивидной области формула гг((а) имеет значение «истина», и значение «ложь» в противном случае.
Систему замен, которая в указанном смысле сообщает формулейзначение«истина», мы назовем моделью*) формулы й с обл встык з', а логические функции, используемые в качестве замен, будем называть выполняющими логическими функциями. Тот факт, что выполнимая формула не может быть опровержимой, с использованием теоретико-множественных рассуждений ') См т 1 с 169 ') См. т. 1, с. 164 и далее. ') Авторы употреблигот термин «Ше Нг)йПнпк».— Приз. пер«а.
232 е.СИМВОЛ И ЛОГИЧЕСКИИ ФОРМАЛИЗМ 1ГЛ 1и пРименение к пРОБлеме РАзрешимости 2ЗЗ й н) немедленно вытекает из теоремы о том, что всякая выводимая формула исчисления предикатов является общезначимой'), т. е. из того, что она принимает значение «истина» при любой замене свободных нндивидных переменных элементами индивидной области г', формульных переменных без аргументов истннностными значениями, а формульных переменных с аргументами логическими функциями, аргументы которых пробегают /. В качестве следствия этой теоремы получается, что любые две переводимые друг в друга формулы либо обе выполнимы, либо обе невыполнимы. Следовательно, проблема изучения выполнимости произвольных формул исчисления предикатов сводится к проблеме изучения выполнимости предваренных формул, поскольку любая формула исчисления предикатов переводима в некоторую предваренную формулу.
Заметим также, что при изучении выполнимости формул исчисления предикатов формульные переменные без аргументов могут быть исключены. Действительно, легко убедиться, что формула 5 исчисления предикатов, содержащая формульную переменную 6 без аргументов, может быть преобразована в некоторую формулу вида (6х ~ 6) И6е 4 ) З), не содержащую никаких других формульных переменных без аргументов, кроме тех, которые входят в 5, и такую, что $, и Яе уже не содержат переменной 6. Эта формула выполнима или невыполнима одновременно с формулой 5; но, с другой стороны, она выполнима тогда и только тогда, когда выполнима формула ОхЧбе, которая переменной З уже не содержит.
Эту процедуру исключения формульной переменной без аргументов можно применить нужное число раз, и в результате у нас получится формула, не содержащая формульных переменных без аргументов и выполнимая или невыполнимая одновременно с формулой 5. При изучении вопроса о выполнимости какой-либо формулы свободные индивидные переменные тоже могут быть исключены, так как формула 5 со свободными индивидными переменными в отношении выполнимости ведет себя в точности так же, как любая из формул, получающихся из нее в результате замены свободных переменных связанными переменными с проставлением соответствующих кванторов суи(всоыования в начале формулы. Поэтому, изучая выполнимость, мы можем ограничиться рассмотрением таких предваренных формул, которые не содержат х) См.
т. 1е с. 168. ни формульных переменных без аргументов, ни свободных индивидных переменных. Дальнейшее сведение подобного рода заключается в построении такой нормальной формы из числа форм, найденных Сколемом, которая представляет собой двойственный эквивалент нормальной формы, названной нами с к о л е м о в с к о й. Эта т е оретико-модельная' ) сколемовская нормальная форма — как мы ее будем называть в отличие от теоретико доказательс т в е н н о й сколемовской нормальной формы ') — представляет собой такую предваренную формулу, у которой все кванторы всеобщности предшествуют всем кванторам существования. Процедура построения такой нормальной формы для заданной предваренной формулы и доказательство того, что в отношении выполнимости эти две формулы одинаковы, аналогичны дедуктивному переходу от предваренной формулы к дедуктивно равной ей сколемовской нормальной форме и доказательству этого дедуктивного равенства.
В случае выполнимости зто рассмотрение оказывается еще более простым, поскольку мы можем пользоваться рассуждениями, допустимыми с теоретико-множественной точки зрения. Мы проведем это рассмотрение на каком-либо типичном примере. Для этого мы возьмем формулу 5 вида ЧхЭихЭиеЧу,ЧуеЧуДОЧЕ,Чгел(х, и„и„у,, у„у„о, г„г,).
Для простоты будем считать, что в эту формулу не входят ни свободные нндивидные переменные, ни формульные переменные без аргументов, Пусть эта формула 5 выполнима в какой-либо индивидной области У. Введем для выполняющих логических функций какие- либо символы (например, занумерованные функциональные знаки ц1И 1ее, ...). Пусть в результате замены в выражении Е((х, и„и„у„у„у„о, гы г,) формульных переменных символами соответствующих логических функций получается выражение 6(х, и„и„у„у„у„о, зх, г,). Если мы обозначим через с))(а, Ь, с, й, (, т, л) логическую функцию, которая для любой системы значений аргументов из г' имеет то же самое истинностное значение, что и формула Чг,Чгяе((а, Ь, с, й, (, т, и, гы г,), ') В тех случаях, когда мы не будем опасаться недорззуменнй, прнлнгнтельное «теоретнко-модельный» мы будем опускать ') См.
т. 1, с. 203. 2Зл е с~м~ол и логичгсхггя воры»лизы примвнвние к п»овлвме»дз»вшимости е 5! !гл гп а через Ч'(а, 6, с) — логическую функцию, которая для любой системы значений аргументов из г имеет то же самое истинностное значение, что и формула Уу»УУ»УУДоУг»Уг»21(а, Ь, с, уь уь уз о, гь гз) то следующие три формулы: УхУигУи»УУ»УУ»УУ»Уо(г))(х иь из Уь Уь Уз ") Уг»Угвр!1(х, иь иь Уь Уь Уз о гь гз)) УхУи,Уи,(Ч" (х, иг, из)-~ЧУ»УУ<УУДпФ(х, иь иь Уь Уз У» о)) Ух3иДи»Чг(х, иь и,) относительно иидивидной области г' будут иметь значение <истина», и поэтому, если Ц и 2) суть формульные переменные, не входящие в формулу 5, то формула (!) УхУи»Уи»УУ»УУ»УУ»Уо(ц(х, иг, иь Уь Уь Уз ") ~г»Угад(х, иь и„уь у„, у„о, гь г,)) ЙУхУи»Уиз (й)(х иь из) 'Уу»Уу»Чу»~о(1(х, их, иь уь уь уз о))»г УхЗигшиз'<!(х, иь и,) будет выполнима в области 1.
С другой стороны, если эта формула выполнима, то — вследствие истинности второго и третьего членов конъюнкции — для любой системы выполняющих логических функций выражение УхшиДи»УУ»УУ»УУ»Згг)1(х, иь и„уь уь у», о) принимает значение «истнна», а тогда вследствие истинности первого члена конъюнкции и формула 5 принимает значеяие «истииа». Таким образом, всякая модель формулы !1 дает нам некоторую модель формулы (1) с той же самой индивидной областью и наоборот. Но формулу (1) легко можно преобразовать (и даже различными способами) в какую-либо теоретико-модельную сколемовскую нормальную форму, например, в формулу (2) УхУигУи»УУ»УУ»УУ»УоУг»Угз'Зшг шгп»огсз (( (х иь иь Уг Уь Ув о) +'<1(х иь из Уь Уь Уь " гь гз)) г< (6(х, иг, из) — \1 (х, их, из, уз, Уь уз, игх)) о. Ж(х, газ, игз)).
Тем самым мы совершили искомый переход от фо м лы ь к некото ой а рой равносильной ей по выполнимости сколемовской формулы ь нормальной форме. Заметим, что в рассмотренном случае равносильность (относительно выполнимости) произвольной формулы 5 исчисления предикатов некоторой сколемовской нормальной форме % мы установили в том сильном смысле, что по каждой модели формулы $ была построена соответствующая модель формулы Я с гной же самой индивидной областью, н наоборот. Такую равносильность двух формул мы будем кратко называть их м одел ь н ы м р а ве нотном'). Наряду с этим обнаруживается следующее соотношение двойственности между теоретико-модельной и теоретико-доказательственной сколемовскими нормальными формами: если мы возьмем отрицание формулы (2) и заменим введенные для получения этой нормальной формы формульные переменные 11 и 5 их отрицаниями — что будет означать переход к дедуктивно равной формуле, — то получится формула, которую можно будет преобразовать в теоретико-доказательственную сколемовскую нормальную форму формулы Л 5.
Отсюда на основании ранее доказанной теоремы о теоретико-доказательственной сколемовской нормальной форме, в частности, вытекает, что отрицание формулы (2) дедуктивно равно отрицанию формулы 5. И, вообще, этим способом получается, что отрицание любой теоретико-модельной сколемовской нормальной формы Ж какой-либо формулы 5 исчисления предикатов дедуктивно равно отрицанию 5. Поэтому любая такая нормальная форма % формулы 5 не только модельно равна !1, но и равносильна ей в отношении опуовержилгоспги.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
