Глава 5. Классическая логика предикатов

ческой логики предикатов, называется упорядоченная пара M = (U,f), где U — непустое множество; f — функция такая, что f (pⁿ)e {l,0} при n = О, f (pⁿ)s Uⁿ при n > 0; если f(y)= a, то as U.

Необходимые неформальные объяснения, касаю­щиеся определения 5.7 М-модели, кратко могут быть изложены в следующих ситуациях.

Непустое множество U представляет собой предмет­ный универсум интерпретации: U = {«ц,«ц,...,«ц,...J. Предметный универсум индивидов может быть сколь угодно большим и ограничен лишь требованием непустоты. Каждой индивидной константе a., i > 1, КЛП-языка ставится в соответствие индивид «Ц из универсума U, определенного на М-модели.

Для интерпретации предикатных символов КЛП-язы­ка в структуру М-модели вводится функция припи­сывания f, которая каждому n-местному предикат­ному символу Р" ставит в соответствие предикат Р в качестве приписанного значения для f(Pⁿ). Если Р" — пропозициональный символ, то есть n = 0, то Р^ е {l>0}, где 1 и О соответственно предикаты «истин­но» и «ложно». Если Р^п — предикатный символ, то есть n > О, то Р" с U" • Функция f каждой свободной предметной переменной у приписывает в качестве ее значения индивид из универсума U, то есть f (y)e U.

Определение 5.8. Пусть А — произвольная форму­ла КЛП-языка со свободными переменными у,, ..., у_п. Тогда ее истинностное значение при заданном при­писывании f(yi)=^i» •••» НУп)= |4i определяется в М-модели рекурсивно следующими условиями.

6. Логика 161

Логика

1 . А = Р°. Значение f(A) определено М-моделью.

2. А = Р(у,, ..., У„)- А = 1, если и только если

^aj_,...,a,,Je f(Pⁿj. в противном случае А = 0.

3. А = — iB. А = 1, если и только если В = 0.

4. А = В л С. А = 1, если и только если В = 1 и С = 1 .

5. A=BvC. A = 1, если и только если В = 1%*б = 1.

ЧПЧ

6. А = В — > С. А = 1, если и только если В = 0-и С = 1 .

7. А = VxB(x, yj, . . . ,-у_п ) . А = 1 , если и только если В(у, у,, — , У_п) = 1 при каждом приписываемом f та-

ком, что f*(y)e U, f^l(yi)=ai, ..., f¹6'n)=^n •

8. A = 3xB(x,y₁,...,y_n). А = 1, если и только если В(У> У,, •••, У_п) = 1 при некотором приписании f, таком, что f'(y)eU, f¹(yi)=a_i,...,f¹(yn)=?n.

Определение 5.9. Формула А (у,, ..., у_п) называет­ся М-истинной, если и только если А = 1 при любом

приписывании f. Обозначается: Mh=A(y₁,...,y_n).

Определение 5.10. Формула А (у,, ..., у_п) называ­ется логически истинной в классической логике пре-

дикатов, если и только если Mb=&yi,...,y_n для каж­дой М-модели, определенной на структуре М = (U, f } .

В определениях 5.7-5.10 достаточно прозрачно уточняются основные семантические понятия клас­сической логики предикатов — понятия модели, ис­тинности в модели и логической истинности. Важно, что эти определения существенно опираются в своей идеологии на философскую классическую концепции истины, а поэтому сами приобретают образ класси­ческой теории моделей. Однако развитые таким об­разом теоретико-модельные понятия при всех их

162

Глава 5. Классическая логика предикатов

достоинствах философской и логической ясности имеют существенный недостаток, на который не пе­рестают обращать внимание исследователи.

В определениях модели и универсума интерпре­тации делаются сильные допущения, в соответствии с которыми предметный универсум не ограничен и может быть бесконечно большим. Этот факт делает невозможным прямое решение проблем М-истинно-сти и логической истинности эффективным образом. Поэтому для решения этих проблем приходится ис­кать косвенные методы доказательства.

Одним из таких косвенных методов установле­ния логической истинности формул КЛП-языка яв­ляется метод «безуспешного» поиска М-контрмоде-ли, опровергающей М-истинность искомой формулы. Суть дела сводится к следующей схеме косвенного доказательства. Вместо прямого доказательства ло­гической истинности формулы делается допущение, что формула может быть М-ложной и, поэтому, иметь опровергающую ее М-контрмодель. Если попытка построить такую М-контрмодель оказывается безус­пешной и приводит к противоречию в рассуждении, то это дает основания для утверждения логической истинности искомой формулы. Ясно, что здесь исполь­зуется известный уже метод рассуждения от против­ного или сведения доказательства к противоречию.

Пример 1. Доказать методом поиска М-контр-мо-дели: 1= 3x(A(x)v b(x))-> (3xA(x)v ЗхВ(х)). Символ н= означает: «логически истинно».

Доказательство. Допустим, что данная форму­ла не является логически истинной. Тогда для нее имеется М-контрмодель, в которой по КЛВ (1) |3x(A(x)v В(х))]= 1 и (2) (3xA(x)v ЗхВ(х)] = О . Из (1) по

6* 163

__ __ __Логика ___

условию 8 определения 5.8 следует (3) [А.(у) v В(у)] = 1 для некоторого, по крайней мере одного, приписыва­ния f такого, что f(y)e U. Случай (3) по условию 5 распадается на два подслучая: (4.1) [А(у)] = 1 или (4.2) [В(у)] = 1 при некотором заданном приписы­вании f.

С другой стороны, (2) по КЛВ влечет (5.1) [ЭхА(х)]=0, (6.1) [ЗхВ(х)]=0, (5.2) [ЗхА(х)]=Ои (6.2) [ЗхВ(х)] = 0, то есть ложность дизъюнкторов из (2) в обоих подслучаях. Но из (5.1) следует (7.1) [А(у)] = 0 при любом приписывании, в том числе и f, что противоречит (4.1). Из (6.2), в свою очередь, следует (7.2) [В(у)] = 0 при любом приписывании, в том числе и f, что противоречит (4.2).

Таким образом, доказано, что анализируемая в примере формула зх(а(х) v b(x)) -> (ЗхА(х) v ЭхВ(х)) не имеет М-контрмоделей и, поэтому, является логи­чески истинной. Доказательство завершено.

Пример 2. Доказать методом поиска М-контрмо-дели: -н (VxA(x) -> VxB(x)) -» Vx(A(x) -» b(x)). Сим­вол =н означает: «опровержимо».

Доказательство. Для доказательства опровер-жимости данной формулы следует найти для нее М-контрмодель, в которой: (1) [VxA(x) —> VxB(x)] = 1 и (2) [Vx(A(x)-*B(x))]=0.

Из (2) по условию 7 определения 5.8 следует, что имеет место (3) [А^) -» В(у_х)]= 0 для некоторого приписывания f¹ такого, что f¹(y₁)e U. (3), в свою очередь, по КЛВ влечет (4) [А(у_х)] = 1 и (5) [Щу^] = О при заданном приписывании f¹.

Случай (1) по условию 5 распадается на два под-случая: (6.1) [VxA(x)]=0 или (6.2) [VxB(x)] = l. Подслучай (6.2) закрывается, так как из него следу-

164

_____Глава 5. Классическая логика предикатов_____

ет по условию 7 (7.2) [В(у₁)] = 1 для любого припи­сывания, в том числе и приписывания f¹. Тогда (7.2) противоречит (5).

Подслучай (6.1) требует по условию 7 введения новой свободной переменной у₂, не встречающейся ранее в рассуждении, то есть (7.1) [А(у₂)] = О при новом приписывании f², отличающимся от f¹ только тем, что f¹^)^ f²(y₂) . Противоречия между (7.1) и (4) не возникает. Следовательно, данный подслу-чай и является М-контрмоделью, опровергающей ло­гическую истинность анализируемой формулы (VxA(x) -> VxB(x)) -» Vx(A(x) -> b(x)) . Доказатель­ство завершено.

Упражнения

5.6. Докажите логическую истинность в класси­ческой логике предикатов следующих фор­мул методом поиска М-контрмоделей.

1. h= -iVx-iACx) <-> ЗхА(х);

2. i= -,VxA(x) <-> Зх-.А(х);

3. h= Vx-,A(x) <-> -i3xA(x);

4. h= VxA(x) <-» -.3x-.A(x);

5. h= Ух(А(х)л В(х)) о (УхА(х)л VxB(x)); 6.1= (VxA(x) v VxB(x)) -> Vx(A(x) v B(x)); 7. И=Зх(А(х)л В(х)) -^ (ЗхА(х)л ЗхВ(х)); 165

________________Логика_______________ 8. l= 3x(A(x)v b(x))<-> (3xA(x)v ЭхВ(х)) .

5.7. Опровергните логическую истинность в клас­сической логике предикатов следующих фор­мул методом поиска М-контрмоделей.

1. -н Vx(A(x) v b(x)) -> (VxA(x) v VxB(x));

2. =н (ЗхА(х) л ЭхВ(х)) -» Зх(А(х) л b(x)) .

Изложенный выше метод поиска М-контрмоде-лей для установления логической истинности фор­мул КЛП-языка достаточно тяжел в изложении, так как многие его фрагменты выражены в форме рас­суждений на естественном языке. Это затрудняет ре­гулярную эффективность поиска нужной контрмо­дели и, практически, делает невозможным конструк­тивное ведение доказательства. Далее в данном разделе описывается метод модельных конструкций, который, как представляется, свободен от указанных недостатков.

Определение 5.11. Пусть А — произвольная фор­мула КЛП-языка в негативно-нормальной форме, В — подформула формулы А. Тогда последовательность формул < А, В^ ..., В_п> образует список Сп[А] фор­мул, если она построена по следующим правилам:

1. Если В = А, то ВеСп[А].

2. Если В = (С л D) и Be сп[а], то Се сп[а] иям-DeCn[A).

3. Если В = (С v D) и Be сп[а) , то Се сп[а) или DeCn[A).

166