Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 51
Текст из файла (страница 51)
Зх Лу Л (х, у). С помощью доказанной теоремы может быть разработан способ, позволяющий распознавать выводимость такие предваренных формул, у которых все квапторы всеобщности предптествуют всем кванторам существования. Действительно, по этой теореме для любой формулы указанного вида мы найдем число 1, обладающее тем свойством, что если данная формула $-тождественна, то она и выводима. С другой стороны, если формула выводима, то она должна быть также и $-тождественной. Таким образом, для решения вопроса о выводимости данной формулы нам достаточно будет выяснить вопрос о том, является ли она 1-тождественной.
Но ответ на этот вопрос может быть получен путем соответствующего перебора. Перед нами частный случай положительного решения проблемы разрешимости, причем это первый из тех упомянутых ') в л. трех частных случаев, когда это решение удается найти. г . 1Ч В качестве непосредственного следствия из доказанной нами теоремы далее получается, что всякая тождественная в конечном предваренная формула, у которой все кванторы всеобщности предшествуют всем кванторам существования, является выводимой.
2. Выводимость всякой тождественной в конечном формулы одноместного исчисления предикатов; доказательство с помощью прежней распознающей процедуры; теоретико-множественное доказательство и его финитное уточнение. Если мы теперь вернемся к одноместному исчислению предикатов, то без труда сможем доказать, что всякан тождественная в конечном формула этого исчисления является выводимой. Мы сначала покажем, что любая формула й) одноместного исчисления предикатов может быть переведена в некоторую конъюнкцию, состоящую из членов вида 'чубах ... 7иЛХЯ (х, у, г, ..., и), где Я (х, у, г,..., и) кванторов не содержит. Такое преобразование может быть получено на следующем пути.
Сперва мы применим к формуле 5 описанную в гл. 1Ч з) процедуру разложения в примарные формулы. В результате применения этой процедуры формула )В будет преобразована в такую формулу й)*, которая построена с помощью связок исчисления высказываний из составных частей следующих типов: 1. Элементарные формулы (формульные переменные с аргументом или без него). 2.
Формулы вида 'УХЯ (х). 3. Формулы вида ОХЯ (х). При этом выражения Я (х) не содержат, кроме х, никаких связанных переменные. (Полее точное знание структуры выражений Я (х) нам адесь совершенно не понадобится.) Приведем формулу Е1* к конъюнктивной нормальной форме относительно заданных составных частеи; одновременно преобразуем по правилу ().) отрицания выражений 7ХЯ (х) и ВхЯ (х), в результате чего выражение, начинающееся квантором всеобщности, перейдет в выражение, начинающееся квантором существования, н обратно.
Рассмотрим теперь какой-нибудь из членов полученной таким образом конъюнктивной нормальной формы. Он имеет вид 'УХЯ» (х) Ч ... Ч УхЯ„(х) Ч ЗХЯ1(х) Ч ... 'Ч' Зхб„(х) Ч 'В, ') Пм. гл. !Ч, с. $86. э] Пм. с. $88. 1ЕА 244 исчисление ЛРедикАТОВ с РАВВнстВОИ 1РЛ У Реп1нние ЛРОВлемы РлзРешимости $23 где никаких кванторов, кроме укааанных, больше нет, так что З, в частности, вообще не содержит связанных переменных. (Может случиться, что не окажется ни одного дизъюнктивного члена вида Зхб (х); но тогда можно будет специально ввести такой член, добавив дизъюнктивно Лх(А (х) дг 1А(х)), что представляет собой допустимое преобразование.) Формула укааанного вида, согласно правилу (О) 1), может быть переведена в формулу 'УхЯ1(х) 1/ ...
~( 'УхЯН (х) 1/ йх (61(х) ~/ ... '1/ бз(х)) Ч;4), а затем переименованием связанных переменных и применением правила (1) ') — в формулу чу72 ... Чи3х (Я, (у) ~/ Яз (з) 1/ ... ~/ Я з, (и) ~/ 61(х) 1( ° ° ° '»7 Яа(х) Ч 'А7) и, аначит, в формулу вида 'зузз ... 'зи3хЯ (х,1'у, г, ..., и), где нет никаких кванторов, кроме указанных. Тем самым требуемое преобразование выполнено.
Теперь доказываемая теорема может быть получена без труда. Действительно, пусть З вЂ” тождественная в конечном формула одноместного исчисления предикатов, а я' — конъюнкция, получаемая из З в результате укаэанного преобразования; тогда— поскольку совокупность формул, тождественных в конечном, дедуктивно замкнута — формула й также будет тождественной в конечном; то же самое можно сказать и о каждом члене этой конъюнкции, как это непосредственно видно иа определения тождественных в конечном формул. Но каждый конъюнктивный член и' имеет вид 1Уу ... »1изхЯ (х, у, ..., и), где Я (х, у,..., и) кванторов ие содержит.
А для всякой такой формулы мы доказали, что если она тождественна в конечном, то она выводима. Таким обрааом, Й есть конъюнкция выводимых формул и, значит, является выводимой формулой; и так как й получается преобразованием З, то выводима и сама З. Таким образом, всякая тождественная в конечном формула одноместного исчисления предикатов действительно оказывается выводимой.
1) Сн. с. 478. ») См. с. 479. Примененный в этом доказательстве метод преобрааования в то же самое время дает нам и способ, позволяющий для произвольной данной формулы одноместного исчисления предикатов выяснить, является она выводимой или нет. В самом деле, это преобразование ведет нас к конъюнкции, состоящей иа таких членов, выводимость которых (в силу ранее изложенного) может быть проверена; а всякая конъюнкция выводима тогда и только тогда, когда выводим каждый из ее членов. К способу проверки выводимости формул одноместного исчисления предикатов и к только что доказанной об этом исчислении теореме мы можем прийти и другим путем, на который нас приводит рассмотрение теоретико-множественной логики предикатов. С точки зрения теоретико-множественной логики предикатов возможность распознавания общезначимости формул одноместного исчисления предикатов проще всегс получается из следующей теоремы; 2 -тождественная формула одноместного исчисления предикатов, содержащая не более 1 различных формульных переменных с аргументом, является общлгначимой; или, что сводится к тому же самому: если формула одноместного исчисления предикатов, содержащая не более 1 различных формульных переменных с аргументом, выполнима, то она выполнима и в 21-элементной индивидной области.
Во второй ее формулировке зта теорема доказывается следующим образом. Пусть Я вЂ” рассматриваемая выполнимая формула. Она принимает значение «истина» при некоторой оценке для свободных переменных, складывающейся из 1. Вполне определенных истинностпых значений («истина» или «ложь»), приписываемых формульнымперемеияым без аргументов. 2. Вполне определенных логических функций от одного аргумента Ф» Ф»~ ° ° . ФВ подставляемых вместо формульных переменных с аргументом (эти функции относятся к вполне определенной индивидной области Х, и мы можем считать, что их имеется в точности 1).
3. Собственных имен индивидов из У, которые подставляются вместо свободных индивидных переменных. Индивиды из г' мы можем затем разбить на классы таким обрааом, чтобы два индивида — например, а и () — причислялись к одному классу тогда и только тогда, когда последовательность, состоящая из 1 значений Ф, (а), ..., Ф1(а), совпадает с последовательностью значений Ф, (р), ..., Фз (р). 2«т 246 исчисление пРедиклтов с РАвенством [Гл. ч «») Ркшкник пРОвлкмы РАзРкшимОсти Так как значениями функций Ф„..., Ф1 могут быть только два значения «истина» и «ложь», то в смысле определенного нами разбиения может быть самое большее 2~ различных классов. Пусть и — число этих классов, а У* — индивидная область, обрааованная этими классами.
Каждой из функций Ф, однозначным образом соотносится некоторая функция Ф,", определенная на инднвидной области г"» и принимающая на каждом из этих и классов то одноаначно определенное аначенне, которое Ф, принимает на индивидах из этого класса. Теперь легко рассудить — с помощью предваренной нормальной формы или с помощью разложения на элементарные формулы, — что формула Я будет принимать значение «истина» и в том случае, если рассматриваемая нами подстановка будет модифицирована таким образом, что: 1. Вместо индивидной области Х мы возьмем и-элементную область Х*. 2.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
