Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 99
Текст из файла (страница 99)
Мы говорим, что в выражении зев(р) (или (йу((й)) переменная х относится к квантору йр (или соответственно к (р) и что она связывается этим квантором. Выражение 6(у) мы будем называть областью действия соответствующего кван- тора. Относительно самих кванторов всеобщности злу и существования Лр мы говорим, что они относятся к переменной р. Кван- торы, относящиеся к одной и той же связанной переменной, мы называем одноименными. При построении сложных выражений, отправляясь от более простых, мы, как обычно, употребляем скобки. В целях экономии скобок мы пользуемся следующими соглашениями: выражения вида ) Я, 'У~Я(р) и (ТЯ(р) в скобки не заключаются; конъюнкции и дизъюнкцин в качестве членов импликаций и эквивалентностей разрешается в скобки не заключать; конъюнкцию в качестве первого члена какой-либо другой конъюнкции, а также дизъюикцню в качестве первого члена какой-либо другой дизъюнкции разрешается не заключать в скобки, так что многочлеиные конъюнкции и дизъюнкции могут строиться без скобок.
Среди выражений, которые могут быть построены из переменных и символов исчисления предикатов, формулы характеризуются следующим образом: Элементарными формулами являются либо формульные переменные без аргументов, либо формульные переменные со свободными индивидными переменными в качестве аргументов. Формулы исчисления предикатов — это либо элементарные формулы, либо выражения, получающиеся из элементарных формул в результате описанного выше применения к ним символов исчисления предикатов. Таким образом, формулы мы получаем согласно следующему рекурсивному определению: Всякая элементарная формула является формулой.
Если Я— формула, то выражение ) Я тоже является формулой. Если Я и 8 суть формулы, то выражения Яйб, Я ')/ З, Я-ь6 и Я 3 тоже являются формулами. Если 6(с) — формула, содержащая свободную переменную с, но не содержащая связанной переменной р, то выражения Урй(у) и ЗХЯ(р) тоже являются формулами').
') Во всех атнх построениях предполагается, что обязательно употребляются скобки, являющиеся необходимыми для выделення составных частей, Формула исчисления предикатов, ие содержащая вхождений иидивидных переменных, называется формулой исчисления высказываний. Тождественно истинные, или, как мы иногда для краткости говорим, тождественные формулы исчисления высказываний, среди прочих формул характеризуются при помощи следующей процедуры вычисления их значений. Связки исчисления высказываний мы определяем как и с т и н н о с т н ы е функции (т. е. как функции, заданные в области из двух значений «истина» и «ложь», обозначаемых буквами И и Л) при помощи следующих равенств: ~И= Л, 1Л=И, ИЬИ=И, ИйЛ=Л, ЛЙИ =Л, ЛЙЛ=Л; РЦ«(= (() Роз ) у) Р- У= ~Р)уу, Р-У=(рйУ)М()Рй~)У) (для произвольных Р и д, принимающих значения И и Л). Тогда тождественно истинные формулы исчисления высказываний характеризуются тем, что они принимают значение «истина» при любом распр спределении истинностных значений по всем входящим в эти формулы формульным переменным.
Чтобы определить понятие вывода в исчислении предикатов, мы должны сначала описать операцию подстановки, а также операцию переименования связанных переменных. Подстановка в формулу Я вместо свободной индинидной переменной н заключается в том, что эта переменная всюду, где она встречается в Я, заменяется одной и той же свободиои индивидной переменной й; в этом случае мы говорим, что в формулу Я вместо перемениои а подставляется переменная й.
Переименование какой-либо связанной иидивидн< й переменной р в формуле Я заключается в том, что эта переменная всюду в области вия относящегося к ней квантора и в самом этом кванторе заменяется одной и той же отличной от иее связанной д дин ивиной переменной р, так что выражение УрЯ (р) (или =(рр((у)), являющееся формулои или составной частью какой-либо другой формулы, при этом преобразуется в»((рр((й) (в 396(р) соответственно). В этом случае мы говорим, что переменная р нереи меновываетоя в области действия относящегося к ней квантора в переменную р. Подстановка вместо Формудьной переменной 6 без аргументов в какую-либо формулу 6 заключается в том, что зта переменная всюду, где она встречается в формуле Я, заменяется одной и той же формулой 5.
В этом случае мы говорим, что в фора необязательные скобки могут быть опушены. Так, например, если %, 6 я ц — формулы, то выражения (П 6)-ь(г, (И й 5)-1- П н И й 6-~ 6 тоже являются форыуланн, а «н арена как аыраженне д 6-+В формулой не валяется. приложении мулу р( вместо формульной переменной Е подставляется формула 6. Подстановка вместо формульной переменной с одним или несколькими аргументами производится с помощью так называемой именной формы. Именной формой какой-либо формульной переменной, имеющей аргументы, называется элементарная формула, состоящая из той же самой формульной переменной с попарно различными свободными индивидными переменными в роли аргументов; зти переменные в рассматриваемой ситуации мы называем аргументными переменными данной именной формы.
Вариантом данной именной формы мы называем всякое выражение, получающееся из этой именной формы в результате замены каждой ее аргументной переменной какой-либо свободной или связанной индивидной переменной, а под заменителем для данной именной формы мы понимаем любую формулу, в которой встречаются все аргументные переменные данной именной формы' ). Для задания подстановки в данную формулу вместо данной формульной переменной с аргументами нужно для какой-либо именной формы этой формульной переменной указать некоторый заменитель.
Выполнение подстановки в этом случае заключается в том, что всюду, где в данной формуле встречается какой-либо вариант рассматриваемой именной формы, этот вариант заменяется тем выражением, которое получается из указанного заменителя при помощи тех же самых замен, в результате которых этот вариант получается из рассматриваемой именной формы. 3 а м е ч а н и е. Для того чтобы в результате подстановки вместо формульной переменной (с аргументами или без них) или переименования связанной переменной в какой-либо формуле снова получилась формула, необходимо, чтобы в получающемся выражении никакой квантор не оказывался в области действия другого одноименного квантора, или — как мы говорим короче— чтобы не возникало коллизий между связанными переменными.
Кроме подстановок и переименований, в выводах исчисления предикатов для перехода от одной формулы к другой используются также следующие схемы (а) и (р): Схема (а) состоит в переходе от какой-либо формулы 6-ч Е(а), в которой Е(а) не содержит переменной х, к формуле р(-+ АЗ (х), т) В иарвовачальном изложении исчисления ирехннатов (т. 1, ги.
Щ термины вариант и заменитель на вводились. Внарвыа онн поваляются в данном тома на с. 29К чистов исчислянив пвидикатои а схема (р) состоит в переходе от формулы 5(а)-ьЯ, в которой 6(и) не содержит переменной х к формуле ЗхЗ (х) -~- с(; при этом в о и бе х схемах переменная а не должна входить ни в 'Л.
ни в 8(х). и х в схе- . И чительная роль переменных а и х в с пения и авил подстановки и переименования, т схем (а) и (р) мы можем получить соответствующие им про е схемы, в которых вместо переменной а будет фигурировать произвольная свооодиая, а вместо и связанная переменная. в х схем (а) и (р) В известной мере обращениями этих двух сх м являются следующие две основные формулы: 'и хА (х) -ь А (а) А (а) -ь ВхА (х).
е е в качестве схемы исчисления высказываний И, наконец, еще в качестве нас имеется схема заключен и я, е еление вывода можно сформулировать следующим Теперь определение вывода нии предикатов мы о выводом в исчислении п ( следовательно, конечную) ь м л исчисления предикатов, в которой явно п едъявленную и, последовательность формул исчис следующих случаев: а ой фо м лы имеет место один из еле для каждо,„р у тождественно истинной формулои 1. Эта формула является тождес ваний или одной из формул (а и исчисления высказываний м ла не является первой рмулой " рассматривае- 2.
Эта формула ется из непосредственно предб езультате некоторой подстае овательности и получаетс формульной переменной, либо ей ей фо мулы ли о в р ия какой-либо связанной переменной ин ивидной или ор в езультате переименования какой-ли Р пения одной из схем (а) и либо в результате применения д 3. Эта формула ие является ни первой, ни второ' осле овательности и получается из двух непо- рассматриваемой по д ф о схеме заключения. средственно ттредп ую еств щнх ей ормул п 4. Эта формула совпадает с одно и ат иваемой последовательности. формул рассматр й которого является формула И, Вывод, последней формуло кот в ! Формулы вывода, удовлетворяющие и о м лами этого вывода. ак так исходными форму олучены ни из каких пред- характерт уют тэ ся тем, что они не получе нн в результате повторения, щентвующнх формул этого вывода 463 ПРИЛОЖЕНИЕ ни в результате подстановки либо переименования, ни в резуль.