ИСЧИСЛЕНИЕ ПРЕДИКАТОВ

Время: 25-02-2013, 11:42 Просмотров: 1019 Автор: antonin
    
ИСЧИСЛЕНИЕ ПРЕДИКАТОВ
В основе исчисления предикатов лежит язык логики пре-
дикатов. В остальном оно является расширением исчисления
высказываний.
Аксиоматическую систему исчисления предикатов мы по-
лучим, добавив к перечисленным выше схемам аксиомати-
ческого исчисления высказываний (имея в виду, конечно,
переход к языку логики предикатов) следующие четыре схе-
мы и одно правило:
1. Vx А{х) з A(t) — схема Уи.
2. A(t) з 3 хА{х) — схема Эв.
3. VJC (Вз С{х)) D(BDVX С(Х)) — схема введения V в кон-
секвент.
4. V* [С{х) з В) з {Зх С{х) з В) — схема введения 3 в анте-
цедент.
A{t) — результат правильной подстановки терма t вместо
х в А(х)\ В — не содержит х свободно.
Правило VB (правило введения квантора общности, иное
A[t)
название: правило обобщения): ——г (из А непосредственно
VХ/\
выводимо VxA).
Формально мы сохраняем прежнее определение вывода и
доказательства (ясно, что, по существу, изменение состоит в
том, что теперь могут использоваться новые аксиомы и но-
вое правило), однако, если мы хотим, чтобы отношение фор-
мальной выводимости было аналогом семантического поня-
тия следования, необходимо ограничить применение VB: оно
может применяться к некоторой формуле А[х) для обобще-
ния лишь по таким переменным х, которые не содержатся
свободно в допущениях, от которых зависит эта формула.
Чтобы смысл этого ограничения был ясным, мы должны
определить понятие зависимости некоторой формулы выво-
да от допущений (гипотез). Везде в дальнейшем будем иметь
в виду выводы с анализом (то есть обоснованием каждого
его шага ссылками либо на принадлежность формулы этого
шага к множеству взятых гипотез или аксиом системы, либо
152
на формулы, из которых она получатся, и используемые при
этом правила).
Формула В данного вывода зависит от некоторого допу-
щения А, если и только если: а) она есть само допущение А;
б) получается из некоторых формул по правилам системы
(из С ID В и С по т. р. или из С по \/в), какая-нибудь из кото-
рых зависит от А. Более простым образом понятие зависимо-
сти разъясняется в описываемой далее системе натурального
вывода, значительно проще осуществляются там сами выво-
ды и доказательства.
НАТУРАЛЬНАЯ СИСТЕМА ИСЧИСЛЕНИЯ ПРЕДИКАТОВ
Постулатами системы (исходными правилами) являются
все правила натуральной системы исчисления высказываний
и правила для кванторов. Как и раньше, мы используем по-
нятие зависимости формул в выводах от имеющихся в выво-
дах допущений; точнее говоря, это понятие, определенное
ранее для исчисления высказываний, расширяется в форму-
лировках правил для кванторов.
Правила вывода для выражений с кванторами:
1
В других системах — без характеристик зависимости — это правило
г,Л(*)нд
формулируется в виде явно непрямого: г Здг Aix\ кд , оно позволяет вместо
вывода В из допущений Г, Зх Ах заключать о наличии нужной здесь выво-
димости на основании вспомогательного вывода, представляющего выводи-
мость Г, А(х) ь В, что значительно проще. Ситуация здесь аналогична той,
что связана с правилом vH.
153
Понятие вывода и доказательства остаются формально
теми же, которые были сформулированы в исчислении вы-
сказываний, разница лишь в том, что при ссылке на правила
вывода теперь имеются в виду и вновь введенные правила
для выражений с кванторами. К числу указанных в предыду-
щем параграфе эвристических принципов введения допуще-
ний может быть добавлен еще один.
Если в выводе получена формула Э*А(х) и нужно вывес-
ти В, не выводимую непосредственно из имеющихся фор-
мул, вводим допущение А{х), применяя способ рассуждения
согласно Зи.
Рассмотрим несколько примеров выводов.
Схема доказательства формул вида: -i 3 хА{х) г> Ух -. А(х):
+ 1. -пЗхА(лг) [1].
+ 2. А[х) [2].
3. 3 хА{х) [21 — из 2, Зв.
4. -.А(*) [1] — из 1, 3, -,в.
5. Чх-,А(х) [1] — из 4, VB.
6. -,3xA{x)z>Vx-^A{x) [-] — из5,зв.
Схемы доказательств рассмотренных в аксиоматической
системе аксиом «введения V в консеквент» и «введения 3 в
антецедент»:
Предполагается, что А не содержит х свободно.
+ 1. \fx{Az>B{x)) [1].
4- 2. А 12].
З.А=>ВД — из 1, VH.
4. В[х) [1, 2] — из Зи2, зи.
5. \/хВ{х) [\, 2) — из 4, VB.
6. AZDVJCB(X) jl] — из5,=>в.
7. Vx (AIDB(x)) D(ADV^ B{X)) [-] — из 6, зв.
+ 1. Ух(ВДзА) [1].
+ 2. ЗхВ{х) [2].
+ 3. В[х) [3].
4. В(х)эА[1]— из 1, VH.
5. А [1, 3] — из 3, 4, ZDB.
6. А [1, 2] — из 5, Зи.
7. 3XB(X)ZDA [1] — из б, z>B.
8. VJC (В{Х) з А) з (3 х В{х) => А) — из 7, зв.
154
Сформулированное здесь исчисление, как и приведенная
выше аксиоматическая система исчисления предикатов,
представляет собой адекватную формализацию понятий ло-
гического следования и закона логики. Это значит, что для
них справедливы теоремы:
Г \= В е. т. е. Г к В и м А е. т. е. \-А.
В заключение параграфа в дополнение к ранее сформу-
лированным эквивалентностям языка логики высказываний
приведем схемы наиболее важных законов логики, относя-
щихся к языку логики предикатов, которые читатель может
использовать также в качестве упражнений для выводов и
доказательств:
I. Взаимовыразимость кванторов:
I. \/хА(х)~-,Зх-^А(х). 2. 3xA(x)~-,Vx-nA(x).
II. Законы образования контрадикторной противополож-
ности:
1. -, VxA(x) ~ Зх-,А(х). 2. -1 ЗхА{х) ~ Vx-,A(x).
III. Законы пронесения кванторов:
1. ((VxA(x) & V* Ј(;»:)) ~ Vx (А(х) &S(x))).
2. ((ЗхА(х) v ЗхВ(х)) ~ Зх (А(х) vB(x))).
3. (Зх (А(х) & В(х)) => (ЗхА(х) & Зх В(х))).
4. ((УхА(х) v VxB(x)) э V^: (A(x)vB(x))).
5. (Vx (i4vB(i)) ~ (A v VJC 5(^))), если х не свободна в А.
6. (Зх (А & Ј(.*)) ~ (А&Зх В(х))), если * не свободна в А.
7. (V* (А(х) о Ј(*)) з (ЧхА(х) з V^: 5(x))).
IV. Перестановка кванторов
V. Исключение квантора общности и введение квантора
существования.
1. Vx A(x) ID A(t). 2. A(t) з Зх А(х).
В обоих случаях A(t) есть результат правильной подста-
новки терма t вместо х в Л(х).
155
VI. Законы устранения вырожденных кванторов.
1. Vx А ~ А. 2. Зх А ~ А, где А не содержит х свободно.
VII. Связь кванторов V и 3 .
Vx А(х) -> Зх А{х).
Ясно, что приведенные эквивалентности также могут
быть использованы в рассуждениях посредством эквивалент-
ных преобразований (см. § 10).
Пример эквивалентных преобразований формулы
\/х {Р{х) z> -, Q(x)) з -• Зх [Р{х) & Q(x)).
с использованием некоторых из указанных в этом и пред-
ыдущем параграфе схем эквивалентностей:
Vx(P(x) ZD -,О(л)) з -, Зх(Р(х) & Q{x)) =
= -,\/х (Р{х) з -,Q(x)) v -,3*(Р(я)&0(*)) ^
s Зх -, (Р(х) з -, О(х)) v -, Вл: (Р(л) & О(х)) =
= Зх (Р(х) & -, -10(л)) v -п Зх (Р(х) & О(х)) =
= ЗХ (Р(Х) & О(Х)) V -, ЗХ (Р(Х) & О(Х)) г
= Зх (Р[х) & О(х)) v Vx -, (Р(х) & О(х)) г
= Зх (Р(х) & ОД) v Vx (-, Р{х) v -, О(х)).
• Упражнение
Укажите эквивалентности, применяемые на каждом шаге
преобразований в вышеприведенном примере.
Разработанный в современной символической логике ме-
тод построения логических исчислений является важнейшим
ее результатом. Его теоретическая и практическая значи-
мость состоит в том, что благодаря ему возникает возмож-
ность доказательства любой формулы, представляющей за-
кон логики, из бесконечного множества таких формул, а
также осуществлять соответствующий вывод для любого слу-
чая — опять-таки из бесконечного множества случаев — от-
156
ношения логического следования. В основе логических ис-
числений, как мы видели, лежат специальные логические
языки. Наряду с рассмотренными выше возможностями ис-
пользования этих языков для решения многих логических
вопросов, и в первую очередь для точного определения ос-
новных понятий логики (логическое следование и закон ло-
гики), следует заметить, что в этих языках имеются, по су-
ществу, точные понятия логической формы и логического
содержания мыслей, которые мы используем в дальнейшем.
Упражнения
Постройте доказательства следующих формул:
а) -,Vx A(x) з Зх ->А(х);
б) Vx (A(x) =>В(х)) з (\/х А(х) з Vx B(x));
в) Зх А{х) з -I Vx -»А(х);
г) Зх -I А(х) з -1 Vx А(х);
д) Ух \/у А(х, у) з Vy \/x А(х, у).

| распечатать

Другие новости по теме:

Другие новости по теме: