Relations of logical consequence in composition nominative logics

Semantic properties of composition nominative logics of partial single-valued, total and partial ambiguous predicates of propositional, renominative and quantifier levels are studied. Relations of logical consequence for pairs and sets of formulas, and relations of logical equivalence are investigat...

Ausführliche Beschreibung

Gespeichert in:

Bibliographische Detailangaben
Datum:	2025
1. Verfasser:	Shkilnyak, S.S.
Format:	Artikel
Sprache:	Ukrainian
Veröffentlicht:	PROBLEMS IN PROGRAMMING 2025
Schlagworte:	UDC 681.3.06
Online Zugang:	https://pp.isofts.kiev.ua/index.php/ojs1/article/view/844
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!
Назва журналу:	Problems in programming
Завантажити файл:

Institution

Problems in programming

id	pp_isofts_kiev_ua-article-844
record_format	ojs
resource_txt_mv	ppisoftskievua/ff/a0eb24f75b0c647c7b4f424f80f546ff.pdf
spelling	pp_isofts_kiev_ua-article-8442025-09-08T13:41:18Z Relations of logical consequence in composition nominative logics Отношения логического следования в композиционно-номинативных логиках Відношення логічного наслідку в композиційно-номінативних логіках Shkilnyak, S.S. UDC 681.3.06 УДК 681.3. УДК 681.3.06 Semantic properties of composition nominative logics of partial single-valued, total and partial ambiguous predicates of propositional, renominative and quantifier levels are studied. Relations of logical consequence for pairs and sets of formulas, and relations of logical equivalence are investigated.Prombles in programming 2010; 1: 15-38 Исследуются семантические свойства композиционно-номинативных логик частичиых однозначних, тотальных и частичиых неоднозначных предикатов пропозиционального, реноминативного и кванторного уровней. Изучаются отношения логического следствия для пар и множеств формул, отношения логической эквивалентности.Prombles in programming 2010; 1: 15-38 Досліджуються семантичні властивості композиційно-номінативних логік часткових однозначних, тотальних та часткових неоднозначних предикатів пропозиційного, реномінативного та кванторного рівнів. Вивчаються відношення логічного наслідку для пар та множин формул, відношення логічної еквівалентності.Prombles in programming 2010; 1: 15-38 PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2025-09-08 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/844 PROBLEMS IN PROGRAMMING; No 1 (2010); 15-38 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 1 (2010); 15-38 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 1 (2010); 15-38 1727-4907 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/844/895 Copyright (c) 2025 PROBLEMS IN PROGRAMMING
institution	Problems in programming
baseUrl_str	https://pp.isofts.kiev.ua/index.php/ojs1/oai
datestamp_date	2025-09-08T13:41:18Z
collection	OJS
language	Ukrainian
topic	UDC 681.3.06
spellingShingle	UDC 681.3.06 Shkilnyak, S.S. Relations of logical consequence in composition nominative logics
topic_facet	UDC 681.3.06 УДК 681.3. УДК 681.3.06
format	Article
author	Shkilnyak, S.S.
author_facet	Shkilnyak, S.S.
author_sort	Shkilnyak, S.S.
title	Relations of logical consequence in composition nominative logics
title_short	Relations of logical consequence in composition nominative logics
title_full	Relations of logical consequence in composition nominative logics
title_fullStr	Relations of logical consequence in composition nominative logics
title_full_unstemmed	Relations of logical consequence in composition nominative logics
title_sort	relations of logical consequence in composition nominative logics
title_alt	Отношения логического следования в композиционно-номинативных логиках Відношення логічного наслідку в композиційно-номінативних логіках
description	Semantic properties of composition nominative logics of partial single-valued, total and partial ambiguous predicates of propositional, renominative and quantifier levels are studied. Relations of logical consequence for pairs and sets of formulas, and relations of logical equivalence are investigated.Prombles in programming 2010; 1: 15-38
publisher	PROBLEMS IN PROGRAMMING
publishDate	2025
url	https://pp.isofts.kiev.ua/index.php/ojs1/article/view/844
work_keys_str_mv	AT shkilnyakss relationsoflogicalconsequenceincompositionnominativelogics AT shkilnyakss otnošeniâlogičeskogosledovaniâvkompozicionnonominativnyhlogikah AT shkilnyakss vídnošennâlogíčnogonaslídkuvkompozicíjnonomínativnihlogíkah
first_indexed	2025-09-17T09:25:26Z
last_indexed	2025-09-17T09:25:26Z
_version_	1850413047454105600
fulltext	Теоретичні та методологічні основи програмування 15 УДК 681.3.06 С.С. Шкільняк ВІДНОШЕННЯ ЛОГІЧНОГО НАСЛІДКУ В КОМПОЗИЦІЙНО-НОМІНАТИВНИХ ЛОГІКАХ Досліджуються семантичні властивості композиційно-номінативних логік часткових однозначних, то- тальних та часткових неоднозначних предикатів пропозиційного, реномінативного та кванторного рів- нів. Вивчаються відношення логічного наслідку для пар та множин формул, відношення логічної екві- валентності. Розвиток інформаційних технологій в наш час зумовлює розширення сфери за- стосування математичної логіки. Це ро- бить актуальною проблему побудови та дослідження адекватних логічних форма- лізмів, орієнтованих на розв’язання широ- кого спектра задач програмування та моде- лювання. Таку побудову природно вести на базі інтегрованого інтенсіонально-екстенсіо- нального підходу [1]. Логіки, збудовані [2] на основі зазначеного підходу, названі ком- позиційно-номінативними. Дана робота присвячена досліджен- ню семантичних властивостей композицій- но-номінативних логік (КНЛ). Основна увага приділяється вивченню поняття ло- гічного слідування, яке належить до най- фундаментальніших понять логіки. Логіч- не слідування можна формалізувати за допомогою відношення логічного наслід- ку. Будуючи різні семантики, таких від- ношень можна ввести багато. Нестандартні семантики для пропозиційної логіки та різноманітні відношення логічного нас- лідку запропоновані в [3], їх побудова базується на постулатах частковості предикатів і симетричності істинності та хибності. В роботі [4] на основі інтегро- ваного інтенсіонально-екстенсіонального підходу та ідей роботи [3] запропоновані семантики для композиційно-номінатив- них логік, дано визначення композицій через області істинності та хибності преди- катів, для таких логік введені відношення логічного наслідку. В даній роботі продов- жується дослідження семантик для компо- зиційно-номінативних логік часткових од- нозначних, тотальних неоднозначних та часткових неоднозначних предикатів про- позиційного, реномінативного та квантор- ного рівнів. Вивчаються відношення логіч- ного наслідку в таких логіках. У різних семантиках ці відношення мають різні властивості, зокрема, в класичній логіці усі вони збігаються. Зазначені відношення логічного наслідку індукують відповідні відношення еквівалентності, вони поши- рюються на множини формул. Поняття, які тут не визначаються, будемо тлумачити в сенсі [2]. 1. Основні поняття та визначення Основним поняттям логіки з семан- тичного погляду є поняття предиката. У загальному випадку під предика- том на множині D розумітимемо довільну часткову функцію вигляду P : D → { T, F}. Предикати можуть бути однознач- ними чи неоднозначними, тотальними чи частковими. Логіка тотальних однознач- них предикатів – це класична логіка. Логі- ки однозначних часткових предикатів до- сліджені в [2], це логіки з неокласичною семантикою. Логіки тотальних неоднозна- чних предикатів природно назвати (див також [3]) логіками з пересиченою семан- тикою. Логіки часткових неоднозначних предикатів назвемо логіками із загальною семантикою (в [3] – логіки з релевантною семантикою). Областю істинності та областю хи- бності предиката Р на D назвемо множини T(P) = P–1(T) = {d∈D \| T∈P(d)} та F(P) = P–1(F) = {d∈D \| F∈P(d)}. Якщо предикат Р – однозначний, то T(P)∩F(P) = ∅. © С.С. Шкільняк, 2010 ISSN 1727-4907. Проблеми програмування. 2010. № 1 Теоретичні та методологічні основи програмування 16 Якщо предикат Р – тотальний, то T(P)∪F(P) = D. Предикат P на D тотально істинний, якщо T(P) = D. Предикат P на D тотально хибний, якщо F(P) = D. Предикат P на D неспростовний, або частково істинний, якщо F(P) = ∅. Зрозуміло, що кожний неспростов- ний предикат є однозначним. Предикат P на D виконуваний, як- що T(P) ≠ ∅. Предикат P на D тотожно істинний, якщо T(P) = D та F(P) = ∅. Предикат P на D тотожно хибний, якщо T(P) = ∅ та F(P) = D. Для однозначних предикатів пише- мо P(a) ≅ Q(b), якщо із P(а)↓ та Q(b)↓ ви- пливає P(a) = Q(b). V-іменною множиною (V-ІМ) над A назвемо [2] довільну однозначну функцію δ : V→ A. V-ІМ подаватимемо у вигляді [v1aa1,...,vnaan,...]. Тут vі∈V, aі∈A, vі ≠ vj при і ≠ j. Множину всіх V-ІМ над A познача- тимемо VA. Для V-ІМ вводимо [2] операції: ║Х –звуження за множиною Х, ∇ – накладки, rv x – реномінації. Замість δ║(V\{ х}) писатимемо δ║-х. Предикат вигляду P : VA→{ T, F} назвемо V-квазіарним предикатом на А. Множину V-квазіарних предикатів на A позначимо PrА. Ім'я x∈V неістотне для однозначного V-квазіарного предиката P, якщо для дові- льних d∈VA та a, b∈A маємо P(d∇xaa) ≅ P(d∇xab). Ім'я x∈V строго неістотне для V- квазіарного предиката P, якщо для довіль- них d∈VA, a∈A маємо P(d∇xaa) = P(d║-х). Предикат P : VA→{T, F} назвемо ек- вітонним, якщо для довільних d, d'∈VA із d ⊆ d' випливає P(d) ⊆ P(d'). Еквітонність предиката означає, що прийняте ним значення не зникає при роз- ширенні даних. Для однозначних частко- вих предикатів таке збереження прийнято- го значення при розширенні даних нефор- мально може трактуватися як те, що “ін- формативність” предиката не може змен- шуватися при збільшенні “інформативнос- ті” вхідних даних. Для тотальних неодно- значних предикатів ситуація протилежна: при розширенні вхідних даних “інформа- тивність” предиката може тільки зменшу- ватися, тому в класі тотальних неоднозна- чних предикатів поняття еквітонності не зовсім адекватне. Дуальним до еквітонності є поняття антиеквітонності. Предикат P : VA→{ T, F} назвемо ан- тиеквітонним, якщо для довільних d, d'∈VA із d ⊆ d' випливає P(d) ⊇ P(d'). Якщо P антиеквітонний, то P(∅) складається з усіх значень, які предикат може приймати на D, тобто P(∅) = EP . В класі однозначних предикатів антиекві- тонними можуть бути лише майже конста- нтні предикати, тобто такі, що P(d) ≅ T для всіх d∈VA або P(d) ≅ F для всіх d∈VA. От- же, в класі однозначних предикатів понят- тя антиеквітонності малозмістовне. Вод- ночас для тотальних неоднозначних пре- дикатів поняття антиеквітонності цілком адекватне, адже для них антиеквітонність неформально означає, що “інформатив- ність” предиката не може зменшуватися при збільшенні “інформативності” вхідних даних. 2. Композиції пропозиційного, реномінативного та кванторного рівнів Композиції визначають універсаль- ні методи побудови предикатів, вони є яд- ром логіки певного типу. Згідно компози- ційно-номінативного підходу [5] компози- ції уточнюємо як функції (операції) над іменованими предикатами. Hа пропозиційному рівні предика- ти трактуються як абстрактні, тобто як фу- нкції вигляду Р : D →{ T, F}, де D – абстра- ктна множина. Фінітарні композиції пропозиційно- го рівня називають логiчними зв’язками. Основними логічними зв’язками є 1-арна композиція заперечення ¬¬¬¬ та бінар- ні композиції диз’юнкція ∨∨∨∨, кон’юнкція & , Теоретичні та методологічні основи програмування 17 імплікація →→→→, еквіваленція ↔↔↔↔, роздільна диз’юнкція ⊕⊕⊕⊕. Предикати ¬¬¬¬(P), ∨∨∨∨(P, Q) →→→→(P, Q), & (P, Q) ↔↔↔↔(P, Q) та ⊕⊕⊕⊕(P, Q) далі познача- тимемо ¬¬¬¬P, P∨∨∨∨Q, P→→→→Q, P& Q, P↔↔↔↔Q, P⊕⊕⊕⊕Q. Зазначені предикати задамо через їх області істинності та хибності так. T(¬¬¬¬P) = F(P); F(¬¬¬¬P) = T(P). T(P∨∨∨∨Q) = T(P)∪T(Q); F(P∨∨∨∨Q) = F(P)∩F(Q). T(P& Q) = T(P)∩T(Q); F(P& Q) = F(P)∪F(Q). T(P→→→→Q) = F(P)∪T(Q); F(P→→→→Q) = T(P)∩F(Q). T(P↔↔↔↔Q) = (T(P)∩T(Q))∪(F(P)∩F(Q)); F(P↔↔↔↔Q) = (T(P)∩F(Q))∪(F(P)∩T(Q)). T(P⊕⊕⊕⊕Q) = (T(P)∩F(Q))∪(F(P)∩T(Q)); F(P⊕⊕⊕⊕Q) = (T(P)∩T(Q))∪(F(P)∩F(Q)). До основних властивостей логічних зв’язок належать (див [2]): – комутативність ∨∨∨∨, & та ↔↔↔↔, ⊕⊕⊕⊕; – асоціативність ∨∨∨∨ та & ; – дистрибутивність ∨∨∨∨ щодо & та & щодо ∨∨∨∨; – ідемпотентність ∨∨∨∨ та & ; – закони контрапозиції, зняття по- двійного заперечення, де Моргана. Композиції ¬¬¬¬ та ∨∨∨∨ називають базо- вими пропозиційними композиціями. Композиції →→→→, & , ↔↔↔↔ та ⊕⊕⊕⊕ є похід- ними, вони виражаються через ¬¬¬¬ та ∨∨∨∨. Справді, композиції →→→→, ↔↔↔↔ та ⊕⊕⊕⊕ мо- жна звести до ¬¬¬¬, ∨∨∨∨ та & : P→→→→Q = ¬¬¬¬P∨∨∨∨Q; P↔↔↔↔Q = (P& Q)∨∨∨∨(¬¬¬¬Q& ¬¬¬¬P); P⊕⊕⊕⊕Q = (P& ¬¬¬¬Q)∨∨∨∨(¬¬¬¬P& Q). Далі використаємо закони де Мор- гана. Можна також виразити ↔↔↔↔ через ⊕⊕⊕⊕ та ⊕⊕⊕⊕ через ↔↔↔↔: ¬¬¬¬(P⊕⊕⊕⊕Q) = P↔↔↔↔Q та ¬¬¬¬(P↔↔↔↔Q) = P⊕⊕⊕⊕Q. Твердження 1. Вищенаведені влас- тивості справджуються для загального ви- падку логіки часткових неоднозначних предикатів. Наведені визначення P→→→→Q, P↔↔↔↔Q та P⊕⊕⊕⊕Q є природними для однозначних пре- дикатів. Для неоднозначних предикатів можливо T(P)∩F(P) ≠ ∅, звідки парадок- сальне F(P→→→→P) ≠ ∅. Твердження 2. Властивість P↔↔↔↔Q = = (P→→→→Q)& (Q→→→→P) справджується тільки для однозначних предикатів. Справді, маємо F((P→→→→Q)& (Q→→→→P)) = = (T(P)∩T(Q))∪(F(P)∩F(Q)) = F(P↔↔↔↔Q), T((P→→→→Q)& (Q→→→→P)) = T(P→→→→Q)∪T(Q→→→→P) = = (T(P)∩T(Q))∪(F(P)∩F(Q))∪(T(P)∩F(P))∪ ∪(T(Q)∩F(Q)) ≠ T(P↔↔↔↔Q) . Введемо зв’язку ↔↔↔↔Cm (повна екві- валенція), яка буде узгоджена з →→→→. Задамо ↔↔↔↔Cm так: T(P↔↔↔↔CmQ) = (F(P)∪T(Q))∩(F(Q)∪T(P)), F(P↔↔↔↔CmQ) = (T(P)∩F(Q))∪(F(P)∩T(Q)). Для логік однозначних предикатів зв’язки ↔↔↔↔ та ↔↔↔↔Cm збігаються. Введемо строгу еквіваленцію ↔↔↔↔s наступним чином: T(P ↔↔↔↔s Q) = (T(P)∩T(Q)∩F(P)∩F(Q))∪ ( ( ) ( ) ( ) ( ))T P T Q F P F Q∪ ∩ ∩ ∩ ∪ ( ( ) ( ) ( ) ( ))F P F Q T P T Q∪ ∩ ∩ ∩ ∪ ( ( ) ( ) ( ) ( ))T P T Q F P F Q∪ ∩ ∩ ∩ ; F(P ↔↔↔↔s Q) = ( ( ) ( )) ( ( ) ( ))T P T Q F P F Q= ∩ ∪ ∩ ∪ ( ( ) ( )) ( ( ) ( ))T Q T P F Q F P∪ ∩ ∪ ∩ . Звідси випливає, що для кожного d∈D при умові (P ↔↔↔↔s Q)(d) = T значення P(d) та Q(d) збігаються, тобто P(d) = Q(d). При (P ↔↔↔↔s Q)(d) = F маємо P(d) ≠ Q(d). Твердження 3. Для логік нетоталь- них чи неоднозначних предикатів строга еквіваленція ↔↔↔↔s незалежна від ¬¬¬¬ та ∨∨∨∨. Справді, при побудові похідних пропозиційних композицій із базових ¬¬¬¬ та ∨∨∨∨ області істинності й хибності утворених за їх допомогою предикатів будуються із використанням тільки ∪ та ∩. Для частко- вих предикатів операціями ∪ та ∩ із обла- стей істинності й хибності не завжди мож- на утворити всю D, а для неоднозначних предикатів – утворити ∅. Отже, доповнен- ня до областей істинності й хибності нето- тальних чи неоднозначних предикатів не можуть бути утворені із цих областей за допомогою ∪ та ∩. Теоретичні та методологічні основи програмування 18 На реномінативному рівні з'являю- ться композиції реномінації R v x : PrА → PrА. Дамо визначення предиката R v x (P) через його області істинності та хибності: T(R v x (P)) = rv x (T(P)); F(R v x (P)) = rv x (F(P)). Композиції ¬¬¬¬, ∨∨∨∨, R v x називають ба- зовими композиціями логік реномінатив- ного рівня. До основних властивостей компо- зицій R v x належать (див [2]): RT) R , , ( )z v z x P = R ( )v x P . R¬) R ( )v x P¬ = ¬¬¬¬R ( )v x P . R∨) R ( )v x P Q∨ = R ( )v x P ∨∨∨∨ R ( )v x Q . Аналогічно записуються властивос- ті R→, R&, R↔, R⊕. RR) R v x (R ( ))w y P = R ( )v w x y Po . RN) Нехай ім‘я у∈V неістотне для предиката Р. Тоді R , , ( )y v z x P ≅ R ( )v x P . RSN) Нехай ім‘я у∈V строго неісто- тне для предиката Р. Тоді R , , ( )y v z x P = R ( ).v x P Твердження 4. Вищенаведені влас- тивості справджуються для загального ви- падку логіки часткових неоднозначних предикатів. На кванторному рівні з'являються композиції квантифікації ∃∃∃∃x тa ∀∀∀∀x. Дамо визначення предикатів ∃∃∃∃xP і ∀∀∀∀xP через їх області істинності й хибності. T(∃∃∃∃xP) = {d∈VA \| Р(d∇xaa) = T для деякого a∈A}. F(∃∃∃∃xP) = {d∈VA \| Р(d∇xaa) = F для всіх a∈A}. T(∀∀∀∀xP) = {d∈VA \| Р(d∇xaa) = T для всіх a∈A}. F(∀∀∀∀xP) = {d∈VA \| Р(d∇xaa) = F для деякого a∈A}. Композиції ¬¬¬¬, ∨∨∨∨, R v x та ∃∃∃∃x назива- ють базовими композиціями логік кванто- рного рівня. До основних властивостей компо- зицій ∃∃∃∃x та ∀∀∀∀x належать (див [2]): 1) комутативність однотипних ква- нторів: ∃∃∃∃x∃∃∃∃уР = ∃∃∃∃у∃∃∃∃хР та ∀∀∀∀x∀∀∀∀уР = ∀∀∀∀у∀∀∀∀хР; 2) закони де Моргана для кванторів: ¬¬¬¬∃∃∃∃хР = ∀∀∀∀х¬¬¬¬Р та ¬¬¬¬∀∀∀∀хР = ∃∃∃∃х¬¬¬¬Р; 3) неістотність квантифікованих імен: ∃∃∃∃x∃∃∃∃хР = ∃∃∃∃хР; ∃∃∃∃x∀∀∀∀хР = ∀∀∀∀хР; ∀∀∀∀x∃∃∃∃хР = ∃∃∃∃хР; ∀∀∀∀x∀∀∀∀хР = ∀∀∀∀хР; 4) ∃∃∃∃хР ∨∨∨∨∃∃∃∃хQ = ∃∃∃∃х (Р∨∨∨∨Q) та ∀∀∀∀хР & ∀∀∀∀xQ = ∀∀∀∀х (Р& Q). Залучаючи до розгляду композицію реномінації, отримуємо також: NR) ∃∃∃∃yR , , ( )y v z x P = R , , ( )y v z x P та ∀∀∀∀yR , , ( )y v z x P = R , , ( )y v z x P при y∉{ ,z x }. R∃) ∃∃∃∃yR ( )v x P = R ( )v x yP∃ ; R∀) ∀∀∀∀yR ( )v x P = R ( )v x yP∀ . Для R∃ та R∀ умова: y∉{ ,v x }. Твердження 5. Вищенаведені влас- тивості справджуються для загального ви- падку логіки часткових неоднозначних предикатів. Теорема 1. Композиції ¬¬¬¬, ∨∨∨∨, R v x , ∃∃∃∃x зберігають еквітонність та антиеквітон- ність V-квазіарних предикатів. Доводимо для загального випадку ло- гіки часткових неоднозначних предикатів. Нехай d' ⊇ d, предикати Р та Q екві- тонні. Тоді маємо d∈T(P) ⇒ d'∈T(P) та d∈F(P) ⇒ d'∈F(P). Якщо d∈T(¬¬¬¬P), то d∈F(P), звідки за еквітонністю Р маємо d'∈F(P), а звідси d'∈T(¬¬¬¬P). Якщо d∈F(¬¬¬¬P), то d∈T(P), звід- ки за еквітонністю Р маємо d'∈T(P), а звід- си d'∈F(¬¬¬¬P). Отже, ¬¬¬¬Р еквітонний. Якщо d∈T(P∨∨∨∨Q), то d∈T(P)∪T(Q), звідки d∈T(P) або d∈T(Q). Якщо d∈T(P), то d'∈T(P), звідки d'∈T(P)∪T(Q), тому d'∈T(P∨∨∨∨Q); якщо d∈T(Q), то d'∈T(Q), зві- дки d'∈T(P)∪T(Q), тому d'∈T(P∨∨∨∨Q). Якщо d∈F(P∨∨∨∨Q), то d∈F(P)∩F(Q), звідки d∈F(P) та d∈F(Q). Але якщо d∈F(P), то d'∈F(P), якщо d∈F(Q), то d'∈F(Q), звідки d'∈F(P)∩F(Q), тому d'∈F(P∨∨∨∨Q). Отже, предикат P∨∨∨∨Q еквітонний. Якщо d∈T(R v x (P)), то r v x (d)∈T(P). Але d' ⊇ d ⇒ r v x (d') ⊇ r v x (d), звідки за екві- тонністю Р маємо r v x (d')∈T(P), а звідси Теоретичні та методологічні основи програмування 19 d'∈T(R v x P). Аналогічно d∈F(R v x (P)) ⇒ ⇒ d'∈F(R v x (P)). Отже, R v x (P) еквітонний. Якщо d∈T(∃∃∃∃x(Р)), то Р(d∇xaa) = T для деякого a∈A. Звідси d∇xaa∈T(Р). Із d' ⊇ d випливає d'∇xaa ⊇ d∇xaa, тому d'∇xaa∈T(Р) за еквітонністю предиката Р, звідки d'∈T(∃∃∃∃x(Р)). Якщо d∈F(∃∃∃∃x(Р)), то Р(d∇xaa) = F для всіх a∈A. Звідси d∇xaa∈F(Р) для всіх a∈A. Із d' ⊇ d випли- ває d'∇xaa ⊇ d∇xaa, тому за еквітонніс- тю Р для всіх a∈A маємо d'∇xaa∈F(Р), звідки d'∈F(∃∃∃∃x(Р)). Отже, предикат ∃∃∃∃x(Р) еквітонний. Доведення збереження антиекві- тонності аналогічне, тільки в доведенні треба поміняти місцями d та d'. Наслідок 1. Класи еквітонних та ан- тиеквітонних квазіарних предикатів за- мкнені щодо композицій ¬¬¬¬, ∨∨∨∨, →→→→, & , ↔↔↔↔, ⊕⊕⊕⊕, R v x , ∃∃∃∃x, ∀∀∀∀x. Наведені далі співвідношення вида- ються очевидними, але вони вірні далеко не завжди. T( x yR (Р)) ⊆ T(∃x(Р)) (TR∃) F(∃x(Р)) ⊆ F( x yR (Р)) (FR∃) T(∀x(Р)) ⊆ T( x yR (Р)) (TR∀) F( x yR (Р)) ⊆ F(∀x(Р)) (FR∀) Теорема 2. 1. Для нееквітонних пре- дикатів не справджуються всі чотири спів- відношення TR∃, FR∃, TR∀, FR∀. 2. Для еквітонних предикатів спра- вджуються TR∃ і FR∀ та не справджую- ться FR∃ і TR∀. 3. Для антиеквітонних предикатів справджуються FR∃ і TR∀ та не справ- джуються TR∃ і FR∀. Доводимо п. 1. Задамо предикат P так: { , якщо ( ),( ) , якщо ( ). F x im dP d T x im d ∈= ∉ При y∉im(δ) маємо δ(y)↑, звідки x yR (P)(δ) = P(δ∇xaδ(y)) = P(δ║-х) = T. При y∈im(η) маємо δ(η)↓, тому x yR (P)(η) = = η∇xaη(y)) = F. Звідси ∅ ⊂ T( x yR (Р)) ⊂ VA та ∅ ⊂ F( x yR (Р)) ⊂ VA. Проте для всіх d∈VA та a∈A маємо P(d∇xaa) = F, тому F(∃x(Р)) = VA та T(∃x(Р)) = ∅. Звідси неві- рно T( x yR (Р)) ⊆ T(∃x(Р)) та невірно F(∃x(Р)) ⊆ F( x yR (Р)). Задамо тепер предикат Р так: { , якщо ( ),( ) , якщо ( ). T x im dP d F x im d ∈= ∉ Тоді T(∀x(Р)) = VA, F(∀x(Р)) = ∅, ∅ ⊂ T( x yR (Р)) ⊂ VA та ∅ ⊂ F( x yR (Р)) ⊂ VA, Звідси невірно T(∀x(Р)) ⊆ T( x yR (Р)) та не- вірно F( x yR (Р)) ⊆ F(∀x(Р)). Доводимо п. 2. Нехай d∈T( x yR (Р)), тоді T∈( x yR (Р))(d), звідки T∈P(d∇xad(y)). Якщо d(y)↓a для деякого a∈A, то T∈P(d∇xaa), звідки T∈(∃x(P))(d). Якщо d(y)↑, то T∈P(d║-х), звідки за еквітонністю T∈P(d∇xaa) для всіх a∈A, тому T∈(∃x(P))(d). В обох випадках маємо T∈(∃x(P))(d), тому d∈T(∃x(P)). Отже, T( x yR (Р)) ⊆ T(∃x(Р)) вірне для довільних еквітонних предикатів. Нехай d∈F( x yR (Р)), тоді маємо F∈( x yR (Р))(d), звідки F∈P(d∇xad(y)). Як- що d(y)↓a для деякого a∈A, то F∈P(d∇xaa), звідки F∈(∀x(P))(d). Якщо d(y)↑, то F∈P(d║-х), звідки за еквітонніс- тю F∈P(d∇xaa) для всіх a∈A, тому F∈(∀x(P))(d). В обох випадках F∈(∀x(P))(d), тому d∈F(∀x(P)). Отже, F( x yR (Р)) ⊆ F(∀x(Р)) вірне для довільних еквітонних предикатів. Задамо предикат P так: { , якщо ( ),( ) невизначене, якщо ( ). F x im dP d x im d ∈= ∉ Тоді маємо F(∀x(Р)) = F(∃x(Р)) = VA, T( x yR (Р)) = ∅, T(∃x(Р)) = T(∀x(Р)) = ∅, ∅ ⊂ F( x yR (Р)) ⊂ VA. Отже, для нетотальних однозначних еквітонних предикатів F(∃x(Р)) ⊆ F( x yR (Р)) невірне. Теоретичні та методологічні основи програмування 20 Задамо тепер предикат P так: {{ , }, якщо ( ),( ) { }, якщо ( ). T F x im dP d T x im d ∈= ∉ Тоді маємо ∅ ⊂ F( x yR (Р)) ⊂ VA, T( x yR (Р)) = T(∃x(Р)) = T(∀x(Р)) = F(∀x(Р)) = = F(∃x(Р)) = VA, Тому для тотальних неод- нозначних еквітонних предикатів F(∃x(Р)) ⊆ F( x yR (Р)) невірне. Задамо предикат P так: { , якщо ( ),( ) невизначене, якщо ( ). T x im dP d x im d ∈= ∉ Тоді маємо T(∀x(Р)) = T(∀x(Р)) = VA, F( x yR (Р)) = ∅, F(∃x(Р)) = F(∀x(Р)) = ∅, ∅ ⊂ T( x yR (Р)) ⊂ VA. Отже, для нетотальних однозначних еквітонних предикатів T(∀x(Р)) ⊆ T( x yR (Р)) невірне. Тепер задамо предикат P так: {{ , }, якщо ( ),( ) { }, якщо ( ). T F x im dP d F x im d ∈= ∉ Тоді маємо ∅ ⊂ T( x yR (Р)) ⊂ VA, F( x yR (Р)) = F(∃x(Р)) = F(∀x(Р)) = T(∀x(Р)) = = T(∃x(Р)) = VA, Тому для тотальних неод- нозначних еквітонних предикатів T(∀x(Р)) ⊆ T( x yR (Р)) невірне. Доводимо п. 3. Нехай d∈T(∀x(Р)), тоді d∇xaa∈T(P) для всіх a∈A, тобто T∈Р(d∇xaa) для всіх a∈A. Якщо d(y)↓a для деякого a∈A, то T∈P(d∇xad(y)), звід- ки d∈T( x yR (Р)). Якщо d(y)↑, то маємо ( )x yr d = d║-х ⊂ d∇xaa для всіх a∈A, звідки за антиеквітонністю T∈P(d║-х) = x yR (Р)(d), тобто d∈T( x yR (Р)). Отже, для антиеквітон- них предикатів завжди T(∀x(Р)) ⊆ T( x yR (Р)). Нехай d∈F(∃x(Р)), тоді d∇xaa∈F(P) для всіх a∈A, тобто F∈Р(d∇xaa) для всіх a∈A. Якщо d(y)↓a для деякого a∈A, то F∈P(d∇xad(y)), звідки d∈F( x yR (Р)). Якщо d(y)↑, то ( )x yr d = d║-х ⊂ d∇xaa для всіх a∈A, звідки за антиеквітонністю маємо F∈P(d║-х) = x yR (Р)(d), тобто d∈F( x yR (Р)). Отже, F(∃x(Р)) ⊆ F( x yR (Р)) вірне для дові- льних антиеквітонних предикатів. Задамо предикат P так: { , якщо ( ),( ) невизначене, якщо ( ). F x im dP d x im d ∉= ∈ Тоді маємо ∅ ⊂ F( x yR (Р)) ⊂ VA, T( x yR (Р)) = T(∃x(Р)) = T(∀x(Р)) = F(∀x(Р)) = = F(∃x(Р)) = ∅. Отже, для нетотальних од- нозначних антиеквітонних предикатів F( x yR (Р)) ⊆ F(∀x(Р)) невірне. Задамо тепер предикат P так: {{ , }, якщо ( ),( ) { }, якщо ( ). T F x im dP d T x im d ∉= ∈ Тоді маємо F(∃x(Р)) = F(∀x(Р)) = ∅, ∅ ⊂ F( x yR (Р)) ⊂ VA, T(∃x(Р)) = T(∀x(Р)) = VA, T( x yR (Р)) = VA. Тому для тотальних неод- нозначних антиеквітонних предикатів F( x yR (Р)) ⊆ F(∀x(Р)) невірне. Задамо предикат P так: { , якщо ( ),( ) невизначене, якщо ( ). T x im dP d x im d ∈= ∉ Тоді маємо ∅ ⊂ T( x yR (Р)) ⊂ VA, F( x yR (Р)) = F(∃x(Р)) = F(∀x(Р)) = F(∀x(Р)) = = F(∀x(Р)) = ∅, Отже, для нетотальних однозначних антиеквітонних предикатів T( x yR (Р)) ⊆ T(∀x(Р)) невірне. Тепер задамо предикат P так: {{ , }, якщо ( ),( ) { }, якщо ( ). T F x im dP d F x im d ∉= ∈ Тоді маємо T(∀x(Р)) = T(∃x(Р)) = ∅, F(∃x(Р)) = F(∀x(Р)) = VA, F( x yR (Р)) = VA ∅ ⊂ T( x yR (Р)) ⊂ VA, Тому для тотальних не- однозначних антиеквітонних предикатів T( x yR (Р)) ⊆ T(∀x(Р)) теж невірне. Наслідок 2. 1) для нееквітонних пре- дикатів не справджуються всі 4 співвідно- шення T(Р) ⊆ T(∃x(Р)), F(∃x(Р)) ⊆ F(Р), T(∀x(Р)) ⊆ T(Р), F(Р) ⊆ F(∀x(Р)); 2) для еквітонних предикатів справ- джуються T(Р) ⊆ T(∃x(Р)) і F(Р) ⊆ F(∀x(Р)) Теоретичні та методологічні основи програмування 21 та не справджуються F(∃x(Р)) ⊆ F(Р) і T(∀x(Р)) ⊆ T(Р); 3) для антиеквітонних предикатів справджуються F(∃x(Р)) ⊆ F(Р) і T(∀x(Р)) ⊆ T(Р) та не справджуються T(Р) ⊆ T(∃x(Р)) і F(Р) ⊆ F(∀x(Р)). 3. Семантичні властивості пропозиційного рівня Семантичними моделями пропози- ційної логіки (ПЛ) є об’єкти вигляду (А, Pr, C) – композиційні предикатні сис- теми пропозиційного рівня. Тут Pr – мно- жина абстрактних предикатів на А, C – множина пропозиційних композицій над Pr, визначена множиною базових компо- зицій {¬¬¬¬, ∨∨∨∨}. При зафіксованій множині C система (А, Pr, C) однозначно визначаєть- ся об'єктом (А, Pr) – алгебраїчною систе- мою з абстрактними предикатами (ААС). Побудова композиційної системи визначає мову пропозиційної логіки. Алфавiт мови: символи логічних зв’язок ¬ і ∨ та множина Ps пропозиційних символів. Визначення множини Fр пропози- ційних формул (ПФ): 1) кожний А∈Ps є ПФ; такі ПФ на- звемо атомарними; 2) якщо Φ та Ψ є ПФ, то ¬Φ та ∨ΦΨ є ПФ. Інтерпретуємо мову ПЛ на семан- тичних моделях ПЛ. Конкретна інтерпре- тація мови визначається АС (A, Pr) та ви- діленням базових предикатів на A, яке за- даємо за допомогою тотального однознач- ного відображення I : Ps → Pr. Тому моде- лями мови ПЛ вважаємо [2] ААС із виді- леними базовими предикатами. Будемо їх позначати A = (A, I). Відображення інтерпретації формул J : Fр → Pr визначаємо за допомогою I так: 1) J(В) = I(В) для кожного В∈Ps; 2) нехай J(Φ) = P та J(Ψ) = Q; тоді J(¬Φ) = ¬¬¬¬P, J(∨ΦΨ) = P∨∨∨∨Q. Предикат J(Φ) – значення формули Φ при інтерпретації на A = (A, I), – позна- чаємо ΦA. Формула Φ тотально істинна при інтерпретації на A = (A, I), або A-істинна, якщо ΦA – тотально істинний предикат. Це позначаємо A \|≡ Φ. Формула Φ тотально iстинна, якщо Φ тотально істинна при кожній інтерпре- тації. Це позначаємо \|≡ Φ. Формула Φ частково істинна при інтерпретації на A = (A, I), або A-неспро- стовна, якщо ΦA – частково істинний (не- спростовний) предикат. Це позначаємо A \|= Φ. Формула Φ частково iстинна, або неспростовна, якщо Φ частково iстинна при кожній інтерпретації. Це позначаємо \|= Φ. Подібним чином можна дати визна- чення виконуваної на A, виконуваної, то- тожно істинної та тотожно хибної на A, тотожно істинної та тотожно хибної фор- мули. АС B = (A, IB) назвемо дуальною до A = (A, IA), якщо для кожного Φ∈Ps маємо ( ) ( )B AT FΦ = Φ та ( ) ( )B AF TΦ = Φ . Зрозуміло, що у цьому випадку ( ) ( )A BT FΦ = Φ та ( ) ( )A BF TΦ = Φ , тобто A = (A, IA) дуальна до B = (A, IB). Якщо A = (A, IA) – АС з частковими однозначними предикатами, то дуальна B = (A, IB) – АС з тотальними неоднознач- ними предикатами, та навпаки. Теорема 3. Нехай АС B = (A, IB) ду- альна до АС A = (A, IA). Тоді для кожної пропозиційної формули Φ маємо ( ) ( )B AT FΦ = Φ та ( ) ( )B AF TΦ = Φ . Доводимо індукцією згідно побудо- ви формули. Для атомарних Φ∈Ps маємо ( ) ( )B AT FΦ = Φ та ( ) ( )B AF TΦ = Φ згідно визначення дуальної АС. Нехай Φ має вигляд ¬Ψ. Тоді ( ) ( ) ( ) ( )B B B AT T F TΦ = ¬Ψ = Ψ = Ψ = ( ) ( ),A AF F= ¬Ψ = Φ ( ) ( )B BF FΦ = ¬Ψ = ( ) ( ) ( ) ( ).B A A AT F T T= Ψ = Ψ = ¬Ψ = Φ Нехай Φ має вигляд ∨ΨΞ. Тоді ( ) ( ) ( ) ( ) ( )B B B A AT T T F FΦ = Ψ ∪ Ξ = Ψ ∪ Ξ = Теоретичні та методологічні основи програмування 22 ( ) ( ) ( ) ( ),A A A A AF F F F= Ψ ∩ Ξ = Ψ ∨ Ξ = Φ ( ) ( ) ( ) ( ) ( )B B B A AF F F T TΦ = Ψ ∩ Ξ = Ψ ∩ Ξ = ( ) ( ) ( ) ( ).A A A A AT T T T= Ψ ∪ Ξ = Ψ ∨ Ξ = Φ Наслідок 3. Неокласична семантика та пересичена семантика дуальні. Це означає, що ΦA неспростовний на АС A з частковими однозначними пре- дикатами ⇔ ΦB тотально істинний на дуа- льній АС B з тотальними неоднозначними предикатами. За кожною АС з частковими одно- значними предикатами A = (A, IA) збудує- мо дуальну АС з тотальними неоднознач- ними предикатами B = (A, IB). Нехай ΦA неспростовний, тобто F(ΦA) = ∅. Тоді на дуальній АС B маємо ( ) ( )B AT FΦ = Φ = A, тобто ΦB тотально істинний. За кожною АС з тотальними неод- нозначними предикатами B = (A, IB) збуду- ємо дуальну АС з частковими однознач- ними предикатами A = (A, IA). Нехай ΦB тотально істинний, тобто T(ΦB) = A. Тоді на дуальній АС A ( ) ( ) ,A BF TΦ = Φ = ∅ тобто ΦA неспростовний. Традиційна інтерпретація ПФ да- ється за допомогою істиннісних оцінок. Iстиннiсна оцiнка мови ПЛ – це до- вільне тотальне однозначне відображення τ : Ps → { T, F}. Таке τ : Ps → { T, F} продовжимо до τ : Fр → { T, F}. Для цього покладемо τ(¬Φ) = T ⇔ τ(Φ) = F; τ(∨ΦΨ) = T ⇔ τ(Φ) = T або τ(Ψ) = T. Формула Φ тавтологiя, якщо τ(Φ) = T при кожній істиннісній оцінці τ мови ПЛ. З наведених визначень випливають наступні твердження. 1. Інтерпретація ПФ за допомогою істиннісних оцінок еквівалентна інтерпре- тації ПФ на АС з тотальними однозначни- ми предикатами. Тоді маємо: Φ неспростовна ⇔ ⇔ Φ тотально істинна ⇔ ⇔ Φ тавтологія. 2. При інтерпретації ПФ на АС з ча- стковими однозначними предикатами (нео- класична семантика) істинність трактуємо як неспростовність. Кожну ПФ можна про- інтерпретувати як нетотальний предикат тому множина тотально істинних формул порожня. Тоді маємо: Φ неспростовна ⇔ Φ тавтологія. 3. При інтерпретації ПФ на АС з то- тальними неоднозначними предикатами (пересичена семантика) істинність тракту- ємо як тотальну істинність. Кожну ПФ можна проінтерпретувати як предикат із непорожньою областю хибності, тому множина неспростовних формул порожня. У цьому випадку: Φ тотально істинна ⇔ Φ тавтологія. 4. При інтерпретації ПФ на АС з ча- стковими неоднозначними предикатами (загальна семантика) кожний ПС можна проінтерпретувати як нетотальний преди- кат із однаковими непорожніми областями істинності та хибності, звідки кожну ПФ можна проінтерпретувати як нетотальний предикат із непорожньою областю хибнос- ті, тому множини тотально істинних та не- спростовних формул порожні. 4. Відношення логічного наслідку На основі різних співвідношень між областями істинності та хибності предика- тів можна ввести багато відношень на множині формул. Задамо 5 “природних” відношень логічного наслідку. В різних семантиках ці відношення мають різні вла- стивості. Спочатку задамо відношення нас- лідку для двох формул при фіксованій ін- терпретації на АС A. 1. “Істиннісний” наслідок A\|=T : Φ A\|=T Ψ ⇔ T(ΦA) ⊆ T(ΨA). 2. “Хибнісний” наслідок A\|=F : Φ A\|=F Ψ ⇔ F(ΨA) ⊆ F(ΦA). 3. “Cильний” наслідок A\|=TF : Φ A\|=TF Ψ ⇔ ⇔ T(ΦA) ⊆ T(ΨA) та F(ΨA) ⊆ F(ΦA). 4. “Неспростовнісний” A\|=Cl : Φ A\|=Cl Ψ ⇔ T(ΦA)∩F(ΨA) = ∅. 5. “Насичений” A\|=Cm : Φ A\|=Cm Ψ ⇔ F(ΦA)∪T(ΨA) = A. Тепер визначаємо відповідні логічні наслідки для двох формул. Теоретичні та методологічні основи програмування 23 1. “ Істиннісний” логічний наслідок \|=T : Φ \|=T Ψ ⇔ Φ A\|=T Ψ для кожної A. 2. “Хибнісний” логічний наслідок \|=F : Φ \|=F Ψ ⇔ Φ A\|=F Ψ для кожної A. 3. “Cильний” логічний наслідок \|=TF : Φ \|=TF Ψ ⇔ Φ A\|=TF Ψ для кожної A. 4. “Неспростовнісний” логічний на- слідок \|=Cl : Φ \|=Cl Ψ ⇔ Φ A\|=Cl Ψ для ко- жної A. 5. “Насичений” логічний наслідок \|=Cm : Φ \|=Cm Ψ ⇔ Φ A\|=Cm Ψ для кожної A. Неспростовнісний логічний наслі- док будемо також називати неокласичним. Традиційним для пропозиційної ло- гіки є відношення тавтологічного наслідку. Ψ є тавтологічним наслідком [2] формули Φ (позначимо Φ \|=t Ψ), якщо Φ→Ψ – тавтологія. Нехай Φ \|= Ψ, де \|= – одне з відно- шень \|=Cl, \|=Cm, \|=T, \|=F, \|=TF. Тоді Φ A\|= Ψ мусить, зокрема, виконуватися для кожної класичної АС A з тотальними однозначни- ми предикатами, тому формула Φ→Ψ му- сить бути класичною тавтологією, тобто тоді Φ╞ Ψ. Введемо тепер відношення слабких наслідків. Формула Ψ є слабким логічним на- слідком [2] формули Φ, що позначимо Φ \|\|= Ψ, якщо для кожної A = (A, I) з умови A \|= Φ випливає A \|= Ψ. Формула Ψ є слабким тотальним наслідком формули Φ, що позначимо Φ \|\|≡ Ψ, якщо для кожної A = (A, I) з умови A \|≡ Φ випливає A \|≡ Ψ. Твердження 6. Відношення логіч- ного наслідку \|=T , \|=F , \|=TF , \|=Cl , \|=Cm , \|=t , \|\|=, \|≡ рефлексивні й транзитивні. Теорема 4. Нехай АС B = (A, IB) ду- альна до АС A = (A, IA). Тоді маємо 1) Φ A\|=T Ψ ⇔ Φ B\|=F Ψ та Φ A\|=F Ψ ⇔ Φ B\|=T Ψ; 2) Φ A\|=Cl Ψ ⇔ Φ B\|=Cm Ψ та Φ A\|=Cm Ψ ⇔ Φ B \|= Cl Ψ. Доводимо п. 1. Маємо Φ A\|=T Ψ ⇔ ⇔ T(ΦA) ⊆ T(ΨA) ⇔ ( ) ( )B BF FΦ ⊆ Ψ ⇔ ⇔ F(ΦB) ⊇ F(ΨB) ⇔ Φ B\|=F Ψ; Φ A\|=F Ψ ⇔ ⇔ F(ΦA) ⊇ F(ΨA) ⇔ ( ) ( )B BT TΦ ⊇ Ψ ⇔ ⇔ T(ΦB) ⊆ T(ΨB) ⇔ Φ B\|=T Ψ. Доводимо п. 2. Маємо Φ A\|=Cl Ψ ⇔ ⇔ T(ΦA)∩F(ΨA) = ∅ ⇔ ( ) ( )B BF TΦ ∩ Ψ = = ∅ ⇔ F(ΦB)∪T(ΨB) = A ⇔ Φ B\|=Cm Ψ; Φ A\|=Cm Ψ ⇔ F(ΦA)∪T(ΨA) = A ⇔ ⇔ ( ) ( )A AF TΦ ∩ Ψ = ∅ ⇔ T(ΦB)∩F(ΨB) = = ∅ ⇔ Φ B\|= Cl Ψ. Наслідок 4. У випадку загальної семантики Φ \|=T Ψ ⇔ Φ \|=F Ψ ⇔ \|=TF Ψ. Розглянемо тепер наслідки з поро- жньої множини формул. ∅ A\|=T Φ означає T(ΦA) = A, тобто A \|≡ Φ. ∅ A\|=F Φ означає F(ΦA) = ∅, тобто A \|= Φ. ∅ A\|=TF Φ означає T(ΦA) = A та F(ΦA) = ∅, тобто A \|≡ Φ та A \|= Φ. Інакше кажучи, ∅ A\|=TF Φ ⇔ ΦA то- тожно істинний. ∅ A\|=Cl Φ означає F(ΦA) = ∅, тобто A \|= Φ. ∅ A\|=Cm Φ означає T(ΦA) = A, тобто A \|≡ Φ. Звідси отримуємо: ∅ \|=T Φ означає, що для всіх A маємо ∅ A\|=T Φ, тобто \|≡ Φ. ∅ \|=F Φ означає, що для всіх A маємо ∅ A\|=F Φ, тобто \|= Φ. ∅ \|=TF Φ означає, що для всіх A маємо ∅ A\|=TF Φ, тобто \|≡ Φ та \|= Φ. Таким чином, ∅ \|=TF Φ справджу- ється тільки для тавтологій у класичній семантиці. ∅ \|=Cl Φ означає, що для всіх A маємо ∅ A\|=Cl Φ, тобто \|= Φ. ∅ \|=Cm Φ означає, що для всіх A маємо ∅ A\|=Cm Φ, тобто \|≡ Φ. ∅ \|=t Φ означає, що Φ – тавтологія. ∅ \|\|= Φ означає \|= Φ. ∅ \|\|≡ Φ означає \|≡ Φ. Розглянемо співвідношення між вве- деними відношеннями логічного наслідку. Неважко переконатись, що при ін- терпретації на АС з тотальними однознач- ними предикатами (класична семантика) усі вищевизначені логічні наслідки еквіва- лентні. Теоретичні та методологічні основи програмування 24 Для інших семантик справджуються наступні твердження. Теорема 5. Для випадку неокласич- ної семантики: 1) Φ \|=Cl Ψ ⇔ Φ \|=t Ψ; 2) Φ \|=T Ψ ⇔ Φ \|\|≡ Ψ; 3) Φ \|=F Ψ ⇔ Φ \|\|= Ψ. 4) Φ & (Φ→Ψ) \|=Cl Ψ (modus ponens); Φ \|=Cl Ψ ∨ Φ&¬Ψ; 5) Φ & (Φ→Ψ) \|=T Ψ; Φ \|≠T Ψ ∨ Φ&¬Ψ; 6) Φ & (Φ→Ψ) \|≠F Ψ; Φ \|=F Ψ ∨ Φ&¬Ψ; 7) Φ & (Φ→Ψ) \|≠TF Ψ; Φ \|≠TF Ψ ∨ Φ&¬Ψ. Теорема 6. Для випадку пересиче- ної семантики: 1) Φ \|=Cm Ψ ⇔ Φ \|=t Ψ; 2) Φ \|=T Ψ ⇔ Φ \|\|≡ Ψ; 3) Φ \|=F Ψ ⇔ Φ \|\|= Ψ; 4) Φ & (Φ→Ψ) \|=Cm Ψ; Φ \|=Cm Ψ ∨ Φ&¬Ψ; 5) Φ & (Φ→Ψ) \|≠T Ψ; Φ \|=T Ψ ∨ Φ&¬Ψ; 6) Φ & (Φ→Ψ) \|=F Ψ; Φ \|≠F Ψ ∨ Φ&¬Ψ; 7) Φ & (Φ→Ψ) \|≠TF Ψ; Φ \|≠TF Ψ ∨ Φ&¬Ψ. Теорема 7. Для випадку загальної семантики: 1) Φ \|=TF Ψ ⇔ Φ \|=T Ψ ⇔ Φ \|=F Ψ; 2) Φ \|=T Ψ ⇔ Φ \|\|≡ Ψ та Φ \|=F Ψ ⇔ Φ \|\|= Ψ; 3) Φ & (Φ→Ψ) \|≠ Ψ та Φ \|≠ Ψ ∨ Φ&¬Ψ. Тут \|= – одне з \|=T, \|=F, \|=TF . Аналогічні твердження щодо modus ponens і теореми дедукції (твердження “Φ & Ψ \|= ϑ ⇒ Ψ \|= Φ→ϑ”) для подібних семантик та відношень пропозиційної ло- гіки наведені в [3]. Зауважимо, що Φ \|= Ψ ∨ Φ&¬Ψ та “Φ & Ψ \|= ϑ ⇒ Ψ \|= Φ→ϑ” одночасно вико- нуються чи не виконуються для кожного із відношень \|=Cl, \|=Cm, \|=T, \|=F, \|=TF у відпо- відних семантиках. У певному розумінні “природним” для неокласичної семантики є наслідок \|=Cl , для пересиченої – наслідок \|=Cm , для загальної – наслідок \|=TF . Таким чином, отримуємо наступні співвідношення для множин формул, які перебувають у відповідних відношеннях. 1. Неокласична семантика (АС з не- тотальними однозначними предикатами): \|=TF ⊂ \|=T , \|=TF ⊂ \|=F , \|=T ⊂ \|=Cl , \|=F ⊂ \|=Cl ; \|=Cl = \|=t , \|=F = \|\|=, \|=T = \|\|≡. При інтерпретації формул як усюди невизначених предикатів \|=Cm не викону- ється для жодної пари формул, тому \|=Cm = ∅. 2. Пересичена семантика (АС з то- тальними неоднозначними предикатами): \|=TF ⊂ \|=T , \|=TF ⊂ \|=F , \|=T ⊂ \|=Cm , \|=F ⊂ \|=Cm ; \|=Cm = \|=t , \|=F = \|\|=, \|=T = \|\|≡. При інтерпретації формул як пре- дикатів із областями істинності та хибнос- ті, рівними А, відношення \|=Cl не викону- ється для жодної пари формул, тому \|=Cl = ∅. 3. Загальна семантика (АС з нетота- льними неоднозначними предикатами): \|=TF = \|=T = \|=F = \|\|= = \|\|≡ ⊂ \|=t . При цьому \|=Cl = ∅ та \|=Cm = ∅. Відношення логічного наслідку ін- дукують на множині формул відповідні відношення логічної еквівалентності. Такі відношення рефлексивні, транзитивні й си- метричні. Φ та Ψ Cl-еквiвалентнi в АС A (позначаємо Φ A∼Cl Ψ), якщо Φ A\|=Cl Ψ та Ψ A\|=Cl Φ. Φ та Ψ Cm-еквiвалентнi в АС A (позначаємо Φ A∼Cm Ψ), якщо Φ A\|=Cm Ψ та Ψ A\|=Cm Φ. Φ та Ψ T-еквiвалентнi в АС A (позначаємо Φ A∼T Ψ), якщо Φ A\|=T Ψ та Ψ A\|=T Φ. Φ та Ψ F-еквiвалентнi в АС A (позначаємо Φ A∼F Ψ), якщо Φ A\|=F Ψ та Ψ A\|=F Φ. Φ та Ψ TF-еквiвалентнi в АС A, або строго еквiвалентнi в АС A (позначаємо Φ A∼TF Ψ), якщо Φ A\|=TF Ψ та Ψ A\|=TF Φ. Звідси, зокрема, отримуємо: Φ A∼T Ψ ⇔ T(ΦA) = T(ΨA); Теоретичні та методологічні основи програмування 25 Φ A∼F Ψ ⇔ F(ΦA) = F(ΨA); Φ A∼TF Ψ ⇔ ⇔ T(ΦA) = T(ΨA) та F(ΦA) = F(ΨA). Φ та Ψ логiчно Cl-еквiвалентнi (позначаємо Φ ∼Cl Ψ), якщо Φ \|=Cl Ψ та Ψ \|=Cl Φ. Φ та Ψ логiчно Cm-еквiвалентнi (позначаємо Φ ∼Cm Ψ), якщо Φ \|=Cm Ψ та Ψ \|=Cm Φ. Φ та Ψ логiчно T-еквiвалентнi (позначаємо Φ ∼T Ψ), якщо Φ \|=T Ψ та Ψ \|=T Φ. Φ та Ψ логiчно F-еквiвалентнi (позначаємо Φ ∼F Ψ), якщо Φ \|=F Ψ та Ψ \|=F Φ. Φ та Ψ логiчно TF-еквiвалентнi, або логiчно строго еквiвалентнi (позначаємо Φ ∼TF Ψ), якщо Φ \|=TF Ψ та Ψ \|=TF Φ. Формули Φ та Ψ тавтологiчно еквiвалентнi (позначимо Φ ∼t Ψ), якщо Φ \|=t Ψ та Ψ \|=t Φ. Φ ∼TF Ψ означає: Φ та Ψ завжди ін- терпретуються як один і той же предикат. Справді, Φ ∼TF Ψ ⇔ Φ \|=TF Ψ та Ψ \|=TF Φ ⇔ ⇔ T(ΦA) = T(ΨA) та F(ΨA) = F(ΦA) для ко- жної АС A. Нехай Φ ∼ Ψ, де ∼ – одне з відно- шень ∼t, ∼Cl, ∼Cm, ∼T, ∼F, ∼TF. Тоді Φ A\|= Ψ та Ψ A\|= Φ мусить, зокрема, виконуватися для кожної класичної АС A з тотальними од- нозначними предикатами, тому Φ↔Ψ му- сить бути класичною тавтологією. При інтерпретації на АС з тоталь- ними однозначними предикатами (класич- на семантика) усі вищевизначені відно- шення логiчної еквівалентності збігаються. Вищенаведені основні властивості логічних зв’язок можна подати через логі- чну еквівалентність відповідних формул. Для кожної з цих властивостей формули у лівій та правій частинах задають один і той же предикат, тому такі формули логiчно строго еквівалентні. Логічні зв’язки ↔↔↔↔ та ↔↔↔↔Cm узго- джуються з відношеннями еквівалентності ∼Cl та ∼Cm . Твердження 7. 1) для неокласичної семантики Φ ∼Cl Ψ ⇔ \|= Φ↔Ψ ⇔ Φ↔Ψ та- втологія; 2) для пересиченої семантики Φ ∼Cm Ψ ⇔ \|≡ Φ↔CmΨ ⇔ Φ↔Ψ тавтологія. Логічна зв’язка ↔↔↔↔s узгоджується з відношенням ∼TF при умові розширення мови відповідним символом ↔s . У цьому випадку для всіх семантик справджується Твердження 8. Φ ∼TF Ψ ⇔ \|≡ Φ↔sΨ. Приклад 1. Для неокласичної се- мантики вірно Φ ∨ Ψ&¬Ψ ∼T Φ та невірно Φ ∨ Ψ&¬Ψ ∼F Φ. Для кожної АС A маємо T((Φ ∨ Ψ&¬Ψ)A) = T(ΦA)∪(T(ΨA)∩F(ΨA)) = = T(ΦA), проте для АС B такої, що T(ΨB) = F(ΨB) = ∅, маємо F((Φ ∨ Ψ&¬Ψ)B) = = F(ΦB)∩(F(ΨB)∪T(ΨB) = ∅. Приклад 2 Для пересиченої семан- тики вірно Φ ∨ Ψ&¬Ψ ∼F Φ та невірно Φ ∨ Ψ&¬Ψ ∼T Φ. Для кожної АС A маємо F((Φ ∨ Ψ&¬Ψ)A) = F(ΦA)∩(F(ΨA)∪T(ΨA)) = = F(ΦA); проте для АС B такої, що (T(ΨB)∩F(ΨB))\T(ΦB) ≠ ∅, вже маємо T((Φ ∨ Ψ&¬Ψ)B) = T(ΦB)∪(T(ΨB)∩F(ΨB)) ⊃ ⊃ T(ΦB). Приклад 3. Для неокласичної се- мантики вірно Φ&(Ψ∨¬Ψ) ∼F Φ та невірно Φ&(Ψ∨¬Ψ) ∼T Φ. Для кожної АС A маємо F((Φ&(Ψ∨¬Ψ))A) = F(ΦA)∪(F(ΨA)∩T(ΨA)) = F(ΦA), проте для АС B такої, що T(ΨB) = F(ΨB) = ∅, маємо T((Φ&(Ψ∨¬Ψ))B) = = T(ΦB)∩(T(ΨB)∪F(ΨB) = ∅. Приклад 4. Для пересиченої семан- тики вірно Φ&(Ψ∨¬Ψ) ∼T Φ та невірно Φ&(Ψ∨¬Ψ) ∼F Φ. Для кожної АС A маємо T((Φ&(Ψ∨¬Ψ)A) = T(ΦA)∩(T(ΨA)∪F(ΨA)) = = T(ΦA); проте для АС B такої, що (F(ΨB)∩T(ΨB))\F(ΦB) ≠ ∅, вже маємо F((Φ&(Ψ∨¬Ψ))B) = F(ΦB)∪(F(ΨB)∩T(ΨB)) ⊃ ⊃ F(ΦB). Для відношень ∼t, ∼Cl, ∼Cm та ∼TF справджується Теорема 8 (семантичної еквiвален- тностi). Нехай Φ' отримано з формули Φ замiною деяких входжень формул Φ1,..., Φn на Ψ1,..., Ψn вiдповiдно. Якщо Φ1 ∼ Ψ1, ..., Φn ∼ Ψn, то Φ ∼ Φ'. Теоретичні та методологічні основи програмування 26 Тут ∼ – одне з ∼t, ∼Cl, ∼Cm, ∼TF. Дове- дення – індукцією за побудовою формули. Для відношень ∼T та ∼F теорема 8, взагалі кажучи, невірна. Справді, як видно із прикладів 1– 4, можлива ситуація, коли Ξ ∼T Φ та невірно ¬Ξ ∼T ¬Φ, адже ¬Ξ ∼T ¬Φ ⇔ Ξ ∼F Φ; можливо також, що Ξ ∼F Φ та невірно ¬Ξ ∼F ¬Φ. Поширимо поняття логічного наслідку на довільні множини формул. Нехай ΓΓΓΓ ⊆ Fp та ∆∆∆∆ ⊆ Fp – деякі множини формул. ∆∆∆∆ є T-логічним наслідком ΓΓΓΓ в АС A (позначаємо ΓΓΓΓ A\|=T ∆∆∆∆), якщо ( ) ( )A AT T Φ∈Γ Ψ∈∆ Φ ⊆ ΨI U . ∆∆∆∆ є F-логічним наслідком ΓΓΓΓ в АС A (позначаємо ΓΓΓΓ A\|=F ∆∆∆∆), якщо ( ) ( )A AF F Ψ∈∆ Φ∈Γ Ψ ⊆ ΦI U . ∆∆∆∆ є TF-логічним наслідком ΓΓΓΓ в АС A (позначаємо ΓΓΓΓ A\|=TF ∆∆∆∆), якщо ( ) ( )A AT T Φ∈Γ Ψ∈∆ Φ ⊆ ΨI U та ( ) ( )A AF F Ψ∈∆ Φ∈Γ Ψ ⊆ ΦI U . ∆∆∆∆ є Cl-логічним наслідком ΓΓΓΓ в АС A (позначаємо ΓΓΓΓ A\|=Cl ∆∆∆∆), якщо ( ) ( )A AT F Φ∈Γ Ψ∈∆ Φ ∩ Ψ = ∅I I . ∆∆∆∆ є Cm-логічним наслідком ΓΓΓΓ в АС A (позначаємо ΓΓΓΓ A\|=Cm ∆∆∆∆), якщо ( ) ( )A AF T A Φ∈Γ Ψ∈∆ Φ ∪ Ψ =U U . Звідси отримуємо такі визначення: ∆∆∆∆ є T-логічним наслідком ΓΓΓΓ (позна- чаємо ΓΓΓΓ \|=T ∆∆∆∆), якщо ΓΓΓΓ A\|=T ∆∆∆∆ для кожної A. ∆∆∆∆ є F-логічним наслідком ΓΓΓΓ (позна- чаємо ΓΓΓΓ \|=F ∆∆∆∆), якщо ΓΓΓΓ A\|=F ∆∆∆∆ для кожної A. ∆∆∆∆ є TF-логічним наслідком ΓΓΓΓ (позначаємо ΓΓΓΓ \|=TF ∆∆∆∆), якщо ΓΓΓΓ A\|=TF ∆∆∆∆ для кожної A. ∆∆∆∆ є Cl-логічним наслідком ΓΓΓΓ (позна- чаємо ΓΓΓΓ \|=Cl ∆∆∆∆), якщо ΓΓΓΓ A\|=Cl ∆∆∆∆ для кожної A. ∆∆∆∆ є Cm-логічним наслідком ΓΓΓΓ (позна- чаємо ΓΓΓΓ \|=Cm ∆∆∆∆), якщо ΓΓΓΓ A\|=Cm ∆∆∆∆ для кожної A. ∆∆∆∆ є тавтологічним наслідком ΓΓΓΓ (позначаємо ΓΓΓΓ \|=t ∆∆∆∆), якщо для кожної іс- тиннісної оцінки τ : Fp→{ T, F} із того, що τ(Φ) = T для всіх Φ∈ΓΓΓΓ, випливає, що τ(Ψ) = T для деякої Ψ∈∆∆∆∆. Відношення логічного наслідку для множин формул рефлексивні, але не тран- зитивні. При інтерпретації на АС з тотальни- ми однозначними предикатами (класична семантика) усі наведені відношення логіч- ного наслідку для множин формул еквіва- лентні. При інтерпретації на АС з нетоталь- ними однозначними предикатами (неокла- сична семантика) можна розглядати \|=T , \|=F , \|=TF , \|=Cl , \|=t . При цьому \|=Cm = ∅. Для них маємо \|=TF ⊂ \|=T , \|=TF ⊂ \|=F , \|=T ⊂ \|=Cl , \|=F ⊂ \|=Cl , \|=Cl = \|=t . При інтерпретації на АС з тотальни- ми неоднозначними предикатами (переси- чена семантика) можна розглядати \|=T , \|=F , \|=TF , \|=Cm , \|=t . При цьому \|=Cl = ∅. Для них маємо \|=TF ⊂ \|=T , \|=TF ⊂ \|=F , \|=F ⊂ \|=Cm , \|=T ⊂ \|=Cm , \|=Cm = \|=t . При інтерпретації на АС з нетоталь- ними неоднозначними предикатами (зага- льна семантика) \|=TF = \|=T = \|=F ⊂ \|=t . При цьому \|=Cl = ∅ та \|=Cm = ∅. Для наступних властивостей \|= – це \|=T, \|=F, \|=TF, \|=Cl, \|=Cm . При цьому для нео- класичної семантики відпадає \|=Cm , для пересиченої відпадає \|=Cl , для загальної – \|=Cl та \|=Cm . U) Нехай ΓΓΓΓ \|= ∆∆∆∆ та ∆∆∆∆ ⊆ ΣΣΣΣ, тоді ΓΓΓΓ \|= ΣΣΣΣ; нехай ΓΓΓΓ \|= ∆∆∆∆ та ΓΓΓΓ ⊆ ΛΛΛΛ, тоді ΛΛΛΛ \|= ∆∆∆∆; С) Φ, ΓΓΓΓ \|= ∆∆∆∆, Φ; П1) ¬¬Φ, ΓΓΓΓ \|= ∆∆∆∆ ⇔ Φ, ΓΓΓΓ \|= ∆∆∆∆; П2) ΓΓΓΓ \|= ∆∆∆∆, ¬¬Φ ⇔ ΓΓΓΓ \|= ∆∆∆∆, Φ; П3) Φ∨Ψ, ΓΓΓΓ \|= ∆∆∆∆ ⇔ Φ, ΓΓΓΓ \|= ∆∆∆∆ та Ψ, ΓΓΓΓ \|= ∆∆∆∆; П4) ΓΓΓΓ \|= ∆∆∆∆, Φ∨Ψ ⇔ ΓΓΓΓ \|= ∆∆∆∆, Φ, Ψ; П5) ¬(Φ∨Ψ), ΓΓΓΓ \|= ∆∆∆∆ ⇔ ¬Φ, ¬Ψ, ΓΓΓΓ \|= ∆∆∆∆; П6) ΓΓΓΓ \|= ∆∆∆∆, ¬(Φ∨Ψ) ⇔ ΓΓΓΓ \|= ∆∆∆∆, ¬Φ та ΓΓΓΓ \|= ∆∆∆∆, ¬Ψ. Аналогічні до П3–П6 властивості можна записати для & та →. Для \|=Cl та \|=Cm також справджу- ються (тут \|= – це \|=Cl, \|=Cm ): П7) ¬Φ, ΓΓΓΓ \|= ∆∆∆∆ ⇔ ΓΓΓΓ \|= ∆∆∆∆, Φ; П8) ΓΓΓΓ \|= ∆∆∆∆, ¬Φ ⇔ Φ, ΓΓΓΓ \|= ∆∆∆∆. Проте ці властивості невірні для \|=T , \|=F та \|=TF, що засвідчує Теоретичні та методологічні основи програмування 27 Твердження 9. Для неокласичної семантики можливо: – ¬Φ, ΓΓΓΓ \|=T ∆∆∆∆ та ΓΓΓΓ \|≠≠≠≠T ∆∆∆∆, Φ; Φ, ΓΓΓΓ \|=T ∆∆∆∆ та ΓΓΓΓ \|≠≠≠≠T ∆∆∆∆, ¬Φ; – ΓΓΓΓ \|=F ∆∆∆∆, ¬Φ та Φ, ΓΓΓΓ \|≠≠≠≠F ∆∆∆∆; ΓΓΓΓ \|=F ∆∆∆∆, Φ та ¬Φ, ΓΓΓΓ \|≠≠≠≠F ∆∆∆∆. Для пересиченої семантики можливо: – ¬Φ, ΓΓΓΓ \|=F ∆∆∆∆ та ΓΓΓΓ \|≠≠≠≠F ∆∆∆∆, Φ; Φ, ΓΓΓΓ \|=F ∆∆∆∆ та ΓΓΓΓ \|≠≠≠≠F ∆∆∆∆, ¬Φ; – ΓΓΓΓ \|=T ∆∆∆∆, ¬Φ та Φ, ΓΓΓΓ \|≠≠≠≠T ∆∆∆∆; ΓΓΓΓ \|=T ∆∆∆∆, Φ та ¬Φ, ΓΓΓΓ \|≠≠≠≠T ∆∆∆∆. Твердження 10. У відповідних се- мантиках справджуються такі властивості: СL) Φ, ¬Φ, ΓΓΓΓ \|= ∆∆∆∆ (для неокласичної семантики \|= – це \|=T, \|=Cl ; для пересиченої – \|=F, \|=Cm ); СR) ΓΓΓΓ \|= ∆∆∆∆, Φ, ¬Φ (для неокласичної семантики \|= – це \|=F, \|=Cl ; для пересиченої – \|=T, \|=Cm ); СLR) Φ, ¬Φ, ΓΓΓΓ \|= ∆∆∆∆, Ψ, ¬Ψ (для неокласичної семантики \|= – це \|=T, \|=F, \|=TF, \|=Cl , для пересиченої – \|=T, \|=F, \|=TF, \|=Cm ). Для відношення \|=t справджуються всі вищенаведені властивості. Для відповідних семантик справ- джується Теорема 9 (заміни еквівалентних). Нехай Φ ∼TF Ψ. Тоді Φ, ΓΓΓΓ \|= ∆∆∆∆ ⇔ Ψ, ΓΓΓΓ \|= ∆∆∆∆ та ΓΓΓΓ \|= ∆∆∆∆, Φ ⇔ ⇔ ΓΓΓΓ \|= ∆∆∆∆, Ψ. Тут \|= – одне з \|=T, \|=F, \|=TF, \|=Cl, \|=Cm . Різновидностями теореми 9 є: Теорема 9_1. Нехай Φ ∼Cl Ψ. Тоді Φ, ΓΓΓΓ \|=Cl ∆∆∆∆ ⇔ Ψ, ΓΓΓΓ \|=Cl ∆∆∆∆ та ΓΓΓΓ \|=Cl ∆∆∆∆, Φ ⇔ ΓΓΓΓ \|=Cl ∆∆∆∆, Ψ. Теорема 9_2. Нехай Φ ∼Cm Ψ. Тоді Φ, ΓΓΓΓ \|=Cm ∆∆∆∆ ⇔ Ψ, ΓΓΓΓ \|=Cm ∆∆∆∆ та ΓΓΓΓ \|=Cm ∆∆∆∆, Φ ⇔ ΓΓΓΓ \|=Cm ∆∆∆∆, Ψ. Теорема 9_3. Нехай Φ ∼t Ψ. Тоді Φ, ΓΓΓΓ \|=t ∆∆∆∆ ⇔ Ψ, ΓΓΓΓ \|=t ∆∆∆∆ та ΓΓΓΓ \|=t ∆∆∆∆, Φ ⇔ ΓΓΓΓ \|=t ∆∆∆∆, Ψ. 5. Семантичні властивості логік номінативних рівнів Семантичними моделями компози- ційно-номінативних логік кванторного рі- вня (КНЛК) є композиційні системи квазі- арних предикатів (VA, PrA, C). Множина C задається множиною базових композицій { ¬¬¬¬, ∨∨∨∨, R v x , ∃∃∃∃x}. При зафіксованій C систе- ма (VA, PrA, C) однозначно визначається об'єктом вигляду (А, PrA) – неокласичною алгебраїчною системою [2]. Розгляд композиційних систем пе- редбачає наявність мови логіки, індукова- ної відповідними інтенсіональними моде- лями (рівнями розгляду). Це означає необ- хідність позначення базових предикатів, із яких за допомогою композицій будуються складніші предикати. Алфавiт мови КНЛК: символи базо- вих композицій, множина Ps предикатних символів (сигнатура мови), множина V предметних імен. Дамо визначення множини Fr фор- мул мови КНЛК (див. [2]): 1) кожний предикатний символ (ПС) є формулою; такі формули атомарні; 2) якшо Φ та Ψ – формули, то ¬Φ, ∨ФΨ, v xR Φ , ∃xΦ – формули. Конкретна інтерпретація мови ви- значається АС (A, PrA) та значеннями ПС на A, які задаємо за допомогою тотального однозначного відображення I : Ps → PrA. Тому моделями мови КНЛК вважаємо [2] АС з доданою сигнатурою вигляду ((A, PrA), I), які позначаємо (A, I). Відображення інтерпретації формул J : Fr→PrA визначається за допомогою I так: 1) J(р) = I(p) для кожного р∈Ps; 2) J(¬Φ) = ¬¬¬¬(J(Φ)); J(∨ΦΨ) = ∨∨∨∨(J(Φ), J(Ψ)); J ( )v xR Φ = R v x (J(Φ)); J(∃xΦ) = ∃∃∃∃x(J(Φ)). Предикат J(Φ) – значення формули Φ при інтерпретації на A = (A, I), – позна- чаємо ΦA. Для випадку КНЛ реномінативного рівня (РНЛ) у наведених визначеннях опускаємо пункти, пов’язані з кванторами. Визначення та позначення істинної на A, тотально істинної, частково істинної на A (A-неспростовної), частково істинної (неспростовної) формули аналогічні відпо- відним визначенням та позначенням, опи- саним в розділі 3 для випадку мови ПЛ. Теоретичні та методологічні основи програмування 28 Твердження 11. 1. При інтерпрета- ції на АС з частковими однозначними пре- дикатами (неокласична семантика) мно- жина тотально істинних формул порожня. 2. При інтерпретації на АС з тоталь- ними неоднозначними предикатами (пере- сичена семантика) множина неспростов- них формул порожня. 3. При інтерпретації на АС з частко- вими неоднозначними предикатами (зага- льна семантика) множини тотально істин- них та неспростовних формул порожні. Ім'я x∈V строго неістотне для фор- мули Φ, якщо для кожної A = (A, I) ім'я x строго неістотне для предиката ΦA. У випадку неокласичної семантики x∈V неістотне для формули Φ, якщо для кожної A = (A, I) ім'я x неістотне для ΦA. Теорема 10. 1. Нехай у∈V строго неістотне для Φ; тоді ∃xΦ ∼TF ∃у ( )x уR Φ . 2. Нехай у∈V неістотне для Φ; тоді ∃xΦ ∼Cl ∃у ( )x уR Φ . Для кожного р∈Ps множину синте- тично строго неістотних предметних імен задамо за допомогою тотальної функції ν : Ps→2V. Таку функцію продовжимо до ν : Fr→2V: ν(¬Φ) = ν(Ф); ν(∨ΦΨ) = ν(Φ)∩ν(Ψ); ν(∃xΦ) = ν(Φ)∪{ x}; 1 1 ,..., ,...,( )n n v v x xRν Φ = (ν(Φ)∪{ v1,...,vn}) ∩ ∩ (V\{ xi \| vi∉ν(Φ), i∈{1,…, n}}). Пару (Ps, ν) назвемо сигнатурою синтетичної строго неістотності. Тотальна строго неістотність імені x означає ( ) p Ps x p ∈ ∈ νI . Для КНЛК постулюємо нескінчен- ність множини VTs = ( ) p Ps p ∈ νI тотально строго неістотних імен. У випадку неокласичної семантики множину синтетично неістотних предмет- них імен задаємо [2] за допомогою функції µ : Ps→2V, яку продовжуємо до µ : Fr→2V. Для неокласичних логік постулюємо не- скінченність множини VT = ( ) p Ps p ∈ µI тота- льно неістотних імен. Успадкування властивостей пропо- зиційної логіки для КНЛК відбувається перенесенням понять і властивостей тавто- логії та відповідних логічних наслідків і еквівалентностей. Формула мови КНЛК пропозиційно нерозкладна, якщо вона атомарна або має вигляд ∃xΦ чи v xR Φ . Множину пропозицій- но нерозкладних формул позначимо Fr0. Iстиннiсна оцiнка мови КНЛК – до- вільне тотальне однозначне відображення τ : Fr0 → { T, F}. Таке відображення продовжимо до τ : Fr → {T, F}: τ(¬Φ) = T ⇔ τ(Φ) = F; τ(∨ΦΨ) = T ⇔ τ(Φ) = T або τ(Ψ) = T. Φ тавтологiя, якщо τ(Φ) = T при кожній істиннісній оцінці τ мови. У випадку неокласичної семантики кожна тавтологія – неспростовна формула. У випадку пересиченої семантики кожна тавтологія є тотально істинною фо- рмулою. Зворотні твердження невірні. На- приклад, формули вигляду x xRΦ ↔ Φ не- спростовні (неокласична семантика) чи то- тально істинні (пересичена семантика), але не тавтології. Визначення дуальної АС для РНЛ та КНЛК таке ж, як і для пропозиційної логіки. Теорема 11. Нехай АС B = (A, IB) дуальна до АС A = (A, IA). Тоді для кожної формули Φ: 1) ( ) ( ), ( ) ( )B A B AT F F TΦ = Φ Φ = Φ ; 2) ΦA еквітонний ⇒ ΦB антиекві- тонний; ΦA антиеквітонний ⇒ ΦB еквітон- ний. Доводимо п. 1 індукцією згідно по- будови формули аналогічно доведенню теореми 3, тільки у випадку РНЛ треба до- дати пункти побудови формули за допомо- гою v xR , у випадку КНЛК – за допомогою v xR та ∃x. Теоретичні та методологічні основи програмування 29 Нехай Φ має вигляд .v xR Ψ Тоді ( ) ( )v B x BT T RΦ = Ψ та ( ) ( ).v B x BF F RΦ = Ψ Маємо ( )v x Bd T R∈ Ψ ⇔ r ( )v x Bd T∈ Ψ ⇔ ⇔ r ( )v x Ad F∈ Ψ (припущення індукції) ⇔ ⇔ r ( )v x Ad F∉ Ψ ⇔ ( )v x Ad F R∉ Ψ ⇔ ⇔ ( )v x Ad F R∈ Ψ ⇔ ( ).Ad F∈ Φ Тепер ( )v x Bd F R∈ Ψ ⇔ r ( )v x Bd F∈ Ψ ⇔ ⇔ r ( )v x Ad T∈ Ψ (припущення індукції) ⇔ ⇔ r ( )v x Ad T∉ Ψ ⇔ ( )v x Ad T R∉ Ψ ⇔ ⇔ ( )v x Ad T R∈ Ψ ⇔ ( ).Ad T∈ Φ Таким чином, ( ) ( )B AT FΦ = Φ та ( ) ( ).B AF TΦ = Φ Нехай Φ має вигляд ∃xΨ. Тоді T(ΦB) = T(∃xΨB) та F(ΦB) = F(∃xΨB). Маємо d∈T(∃xΨB) ⇔ d∇xaa∈T(ΨB) для деякого a∈A ⇔ d∇xaa ( )AF∈ Ψ для деякого a∈A (припущення індукції) ⇔ ⇔ d∇xaa ( )AF∉ Ψ для деякого a∈A ⇔ ⇔ ( )Ad F x∉ ∃ Ψ ⇔ ( ).Ad F x∈ ∃ Ψ Тепер d∈F(∃xΨB) ⇔ d∇xaa∈F(ΨB) для всіх a∈A ⇔ d∇xaa ( )AT∈ Ψ для всіх a∈A (припущення індукції) ⇔ d∇xaa ( )AT∉ Ψ для всіх a∈A ⇔ ( )Ad T x∉ ∃ Ψ ⇔ ( ).Ad T x∈ ∃ Ψ Таким чином, ( ) ( )B AT FΦ = Φ та ( ) ( ).B AF TΦ = Φ Твердження п. 2 теореми безпосе- редньо випливає з визначень. Таким чином, неокласична семан- тика та пересичена семантика дуальні й у випадках КНЛ реномінативного та кванто- рного рівнів. Приклад 5. Для p∈Ps в A = (A, IA) з частковими однозначними предикатами задамо {невизначене, якщо ( ),( ) , якщо ( ).A x im dp d T x im d ∉= ∈ Звідси T(pA) = {d \| x∈im(d)}, F(pA) = ∅, предикат pA еквітонний. Для дуальної АС B = (A, IB) з тота- льними неоднозначними предикатами тоді T(pB) = VA, F(pB) = {d \| x∉im(d)}, звідки маємо антиеквітонний предикат pB : {{ , }, якщо ( ),( ) { }, якщо ( ).B T F x im dp d T x im d ∉= ∈ Приклад 6. Для q∈Ps в A = (A, IA) з тотальними неоднозначними предикатами задамо { { }, якщо ( ),( ) { , }, якщо ( ).A F x im dq d T F x im d ∉= ∈ Звідси T(qA) = {d \| x∈im(d)}, F(qA) = VA, предикат qA еквітонний. Для дуальної АС B = (A, IB) з част- ковими однозначними предикатами тоді T(qB) = ∅, F(qB) = {d \| x∉im(d)}, звідки отримуємо антиеквітонний qB : { , якщо ( ),( ) невизначене, якщо ( ).B F x im dq d x im d ∉= ∈ 6. Логічні наслідки в логіках номінативних рівнів На множині формул мови КНЛК введемо відношення логічних наслідків \|=T, \|=F, \|=TF, \|=Cl, \|=Cm, \|=t, \|\|= та \|\|≡ та відпо- відних еквівалентностей ∼T, ∼F, ∼TF, ∼Cl, ∼Cm, ∼t так, як це зроблено вище для пропо- зиційної логіки. Такі відношення логічних наслідків рефлексивні й транзитивні, відношення еквівалентності – рефлексивні, транзитивні й симетричні. Наслідки з порожньої множини формул задаємо аналогічно випадку ПЛ. ∅ A\|=F Φ, ∅ A\|=Cl Φ означають F(ΦA) = ∅, тобто A \|= Φ; ∅ A\|=T Φ, ∅ A\|=Cm Φ означають T(ΦA) = VA, тобто A \|≡ Φ; ∅ A\|=TF Φ означає T(ΦA) = VA та F(ΦA) = ∅, тобто ΦA тотожно істинний. ∅ \|=Cl Φ, ∅ \|=F Φ означають \|= Φ, тобто Φ неспростовна; ∅ \|=Cm Φ, ∅ \|=T Φ означають \|≡ Φ, тобто Φ тотально істинна; ∅ \|=TF Φ означає \|≡ Φ та \|= Φ, тобто Φ тотожно істинна. Відношення логічного наслідку \|=T, \|=F, \|=TF, \|=Cl, \|=Cm, \|=t для довільних мно- жин формул визначаємо аналогічно випад- ку пропозиційної логіки. Теорема 12. Для випадку неокласи- чної семантики: Теоретичні та методологічні основи програмування 30 1) Φ & (Φ→Ψ) \|\|≡ Ψ; невірно Φ \|\|≡ Ψ ∨ Φ&¬Ψ; ∀xΦ \|\|≡ ∃xΦ; Φ \|\|≡ ∀xΦ; 2) невірно Φ & (Φ→Ψ) \|\|= Ψ; Φ \|\|= Ψ ∨ Φ&¬Ψ; ∀xΦ \|\|= ∃xΦ; Φ \|\|= ∀xΦ; 3) Φ & (Φ→Ψ) \|=t Ψ; Φ \|=t Ψ ∨ Φ&¬Ψ; ∀xΦ \|≠t ∃xΦ; Φ \|≠t ∀xΦ; 4) Φ & (Φ→Ψ) \|=Cl Ψ; Φ \|=Cl Ψ ∨ Φ&¬Ψ; ∀xΦ \|=Cl ∃xΦ; Φ \|≠Cl ∀xΦ; 5) Φ & (Φ→Ψ) \|=T Ψ; Φ \|≠T Ψ ∨ Φ&¬Ψ; ∀xΦ \|=T ∃xΦ; Φ \|≠T ∀xΦ; 6) Φ & (Φ→Ψ) \|≠F Ψ; Φ \|=F Ψ ∨ Φ&¬Ψ; ∀xΦ \|=F ∃xΦ; Φ \|≠F ∀xΦ; 7) Φ & (Φ→Ψ) \|≠TF Ψ; Φ \|≠TF Ψ ∨ Φ&¬Ψ; ∀xΦ \|=TF ∃xΦ; Φ \|≠TF ∀xΦ. Теорема 13. Для випадку пересиче- ної семантики: 1) невірно Φ & (Φ→Ψ) \|\|≡ Ψ; Φ \|\|≡ Ψ ∨ Φ&¬Ψ; ∀xΦ \|\|≡ ∃xΦ; Φ \|\|≡ ∀xΦ; 2) Φ & (Φ→Ψ) \|\|= Ψ; невірно Φ \|\|= Ψ ∨ Φ&¬Ψ; ∀xΦ \|\|= ∃xΦ; Φ \|\|= ∀xΦ; 3) Φ & (Φ→Ψ) \|=t Ψ; Φ \|=t Ψ ∨ Φ&¬Ψ; ∀xΦ \|≠t ∃xΦ; Φ \|≠t ∀xΦ; 4) Φ & (Φ→Ψ) \|=Cm Ψ; Φ \|=Cm Ψ ∨ Φ&¬Ψ; ∀xΦ \|=Cm ∃xΦ; Φ \|≠Cm ∀xΦ; 5) Φ & (Φ→Ψ) \|≠T Ψ; Φ \|=T Ψ ∨ Φ&¬Ψ; ∀xΦ \|=T ∃xΦ; Φ \|≠T ∀xΦ; 6) Φ & (Φ→Ψ) \|=F Ψ; Φ \|≠F Ψ ∨ Φ&¬Ψ; ∀xΦ \|=F ∃xΦ; Φ \|≠F ∀xΦ; 7) Φ & (Φ→Ψ) \|≠TF Ψ; Φ \|≠TF Ψ ∨ Φ&¬Ψ; ∀xΦ \|=TF ∃xΦ; Φ \|≠TF ∀xΦ. Теорема 14. Для випадку загальної семантики: 1) Φ \|=TF Ψ ⇔ Φ \|=T Ψ ⇔ Φ \|=F Ψ; 2) Φ \|\|= Ψ ⇔ Φ \|\|≡ Ψ; 5) ∀xΦ \|\|≡ ∃xΦ; Φ \|\|≡ ∀xΦ; ∀xΦ \|\|= ∃xΦ; Φ \|\|= ∀xΦ; 3) Φ & (Φ→Ψ) \|=t Ψ; Φ \|=t Ψ ∨ Φ&¬Ψ; ∀xΦ \|≠t ∃xΦ; Φ \|≠t ∀xΦ; 4) Φ & (Φ→Ψ) \|≠ Ψ, Φ \|≠ Ψ ∨ Φ&¬Ψ, ∀xΦ \|= ∃xΦ; Φ \|≠ ∀xΦ (тут \|= – одне з \|=T, \|=F, \|=TF ). Твердження 12. 1. Для неокласич- ної семантики маємо Φ ∼Cl Ψ ⇔ \|= Φ↔Ψ. 2. Для пересиченої семантики має- мо Φ ∼Cm Ψ ⇔ \|≡ Φ↔CmΨ. 3. Для загальної семантики маємо Φ ∼TF Ψ ⇔ \|≡ Φ↔sΨ. Наведемо властивості формул, по- в'язані з композицією реномінації. Такі властивості, не пов’язані з кванторами, справджуються вже для логік реномінати- вного рівня. RT) , , ( )z v z xR P ∼TF R ( )v x P . Зокрема, R ( )z z P ∼TF Р. R¬) R ( )v x P¬ ∼TF ¬R ( )v x P . R∨) R ( )v x P Q∨ ∼TF R ( )v x P ∨ R ( )v x Q . Подібним чином записуємо власти- вості R&, R→, R↔ та R⊕. RR) Rv x (R ( ))w y P ∼TF R ( )v w x y Po . RSN) Нехай ім’я у строго неістотне для Р; тоді R , , ( )y v z x P ∼TF R ( )v x P . Для випадку неокласичної семанти- ки маємо (див. [2]): RN) Нехай ім’я у неістотне для Р; тоді R , , ( )y v z x P ∼Cl R ( )v x P . Залучаючи до реномінації квантори, отримуємо такі властивості: NR) ∃y , , ( )y v z xR Φ ∼TF , , ( )y v z xR Φ та ∀y , , ( )y v z xR Φ ∼TF , , ( )y v z xR Φ при y∉{ ,z x }. Зокрема, при y ≠ z маємо ∃y ( )y zR Φ ∼TF ( )y zR Φ та ∀y ( )y zR Φ ∼TF ( )y zR Φ . ∃R∃) ∃y ( )v xR Φ ∼TF , , ( )y v z xR y∃ Φ . R∀) ∀y ( )v xR Φ ∼TF , , ( )y v z xR y∀ Φ . Для ∃R∃ і ∀R∀ умова: y∉{ ,v x }. R∃) ( )v xR y∃ Φ ∼TF∃y ( )v xR Φ . R∀) ∀y ( )v xR Φ ∼TF ( )v xR y∀ Φ . Для R∃ і R∀ y∉{ ,v x }. R∃∃S) ( )v xR y∃ Φ ∼TF ( )v y x zzR∃ Φo . R∀∀S) ( )v xR y∀ Φ ∼TF ( )v y x zzR∀ Φo . Для R∃∃S і R∀∀S умова: y∈{ ,v x }, z∉ ( ( ))v xnm R x∃ Φ та z тотально строго неіс- тотне Для логік однозначних предикатів замість R∃∃S та R∀∀S маємо [2]: R∃∃) ( )v xR y∃ Φ ∼Cl ( )v y x zzR∃ Φo ; R∀∀) ( )v xR y∀ Φ ∼ Cl ( )v y x zzR∀ Φo . Теоретичні та методологічні основи програмування 31 Для R∃∃ і R∀∀ умова: y∈{ ,v x }, z тотально неістотне та z∉ ( ( ))v xnm R x∃ Φ . Наведемо тепер основні властивості композицій квантифікації. Q1) ∃x∃yΦ ∼TF ∃y∃xΦ та ∀x∀yΦ ∼TF ∀y∀xΦ. Q2) ¬∀xΦ ∼TF ∃x¬Φ та ¬∃xΦ ∼TF ∀x¬Φ. Q3) ∃xΦ ∼TF ∀x∃xΦ, ∃xΦ ∼TF ∃x∃xΦ; ∀xΦ ∼TF ∀x∀xΦ, ∀xΦ ∼TF ∃x∀xΦ. Q4) ∃xΦ∨∃xΨ ∼TF ∃x(Φ∨Ψ) та ∀xΦ&∀xΨ ∼TF ∀x(Φ&Ψ). Q5) ∃x(Φ&Ψ)\|=TF ∃xΦ&∃xΨ та ∀xΦ∨∀xΨ\|=TF ∀x(Φ∨Ψ). Q6) Якщо Φ \|=TF Ψ, то ∃xΦ \|=TF ∃xΨ та ∀xΦ \|=TF ∀xΨ. Q7) ∃y∀xΦ \|=TF ∀x∃yΦ; водночас не завжди ∀x∃yΦ\|=Cl ∃y∀xΦ (неокласична се- мантика), ∀x∃yΦ\|=Cm ∃y∀xΦ (пересичена семантика), не завжди ∀x∃yΦ\|=TF ∃y∀xΦ. Q8) Φ \|\|= ∃xΦ, Φ \|\|= ∀xΦ та Φ \|\|≡ ∃xΦ, Φ \|\|≡ ∀xΦ. Для логік часткових однозначних предикатів додаємо: Q9P) якщо \|= Φ, то \|= ∃xΦ, \|= ∀xΦ, \|= Φ ↔∃xΦ та \|= Φ ↔∀xΦ; Q10P) \|= ∃y∀xΦ→∀x∃yΦ, але не завжди \|= ∀x∃yΦ→∃y∀xΦ; Q11P) \|= ∀x (∀xΦ→Φ) та \|= ∃x (∀xΦ→Φ); \|= ∀x (Φ→∃xΦ) та \|= ∃x (Φ→∃xΦ). Для логік тотальних неоднозначних предикатів додаємо: Q9Т) якщо \|≡ Φ, то \|≡ ∃xΦ, \|≡ ∀xΦ, \|≡ Φ ↔Cm∃xΦ та \|≡ Φ ↔Cm∀xΦ; Q10Т) \|≡ ∃y∀xΦ→∀x∃yΦ, але не завжди \|≡ ∀x∃yΦ→∃y∀xΦ; Q11Т) \|≡ ∀x (∀xΦ→Φ) та \|≡ ∃x (∀xΦ→Φ); \|≡ ∀x (Φ→∃xΦ) та \|≡ ∃x (Φ→∃xΦ). Приклад 7. Існують АС A та фор- мула Φ такі: Φ A\|=TF ∀xΦ та ∃xΦ A\|≠Cl Φ, ∃xΦ A\|≠Cm Φ. Нехай Φ – це формула ∀x p → p для ПС p. Інтерпретуємо p на АС A так: { , якщо ( ),( ) , якщо ( ).A T x im dp d F x im d ∈= ∉ Тоді ∅ ⊂ T(pA) ⊂ VA, ∅ ⊂ F(pA) ⊂ VA, T(∀x pA) = VA, F(∀x pA) = ∅, T(∃x(∀x p → p)A) = VA, F(∃x(∀x p → p)A) = ∅, T(∀x(∀x p → p)A) = VA, F(∀x(∀x p → p)A) = ∅, ∅ ⊂ T((∀x p → p)A) ⊂ VA, ∅ ⊂ F((∀x p → p)A) ⊂ VA. Звідси Φ A\|=TF ∀xΦ, ∃xΦ A\|≠Cl Φ, ∃xΦ A\|≠Cm Φ. Теорема 15. Для загального випад- ку квазіарних предикатів у відповідних семантиках не завжди справджуються ( ) \| та \| ( ).x x z A A zR x x RΦ = ∃ Φ ∀ Φ = Φ Тут \|= – одне з \|=Cl, \|=Cm \|=T, \|=F, \|=TF. Візьмемо ПС p та q, проінтерпрету- ємо їх на певній АС A = (A, I) так: { , якщо ( ),( ) , якщо ( );A T x im dp d F x im d ∈= ∉ { , якщо ( ),( ) , якщо ( ).A F x im dq d T x im d ∈= ∉ Маємо ∅ ⊂ T ( )x z AR p ⊂ VA та ∅ ⊂ F ( )x z AR p ⊂ VA, T(∃x pA) = T(∀x pA) = VA та F(∃x pA) = F(∀x pA) = ∅. Звідси маємо ∀x p A\|≠Cl x zR p, ∀x p A\|≠Cm x zR p, ∀x p A\|≠T x zR p, ∀x p A\|≠F x zR p, ∀x p A\|≠TF x zR p. Маємо ∅ ⊂ T ( )x z AR q ⊂ VA та ∅ ⊂ F ( )x z AR q ⊂ VA, T(∃x qA) = T(∀x qA) = ∅ та F(∃x qA) = F(∀x qA) = VA. Звідси отриму- ємо x zR qA\|≠Cl ∃x q , x zR qA\|≠Cm ∃x q , x zR qA\|≠T ∃x q , x zR qA\|≠F ∃x q , x zR qA\|≠TF ∃x q . Наслідок 5. 1) існують АС A та фо- рмула Φ: Φ A\|≠Cl ∃xΦ та Φ A\|≠Cm ∃xΦ; 2) існують АС A та формула Φ: ∀xΦ A\|≠Cl Φ та ∀xΦ A\|≠Cm Φ; 3) існує формула Φ така: невірно ∀xΦ \|\|= Φ та невірно ∀xΦ \|\|≡ Φ. Щодо п. 3 зауважимо, що для АС A та ПС p з доведення теореми маємо A \|= ∀x p, A \|≡ ∀x p, A \|≠ p, невірно A \|≡ p; тому невірно ∀x p \|\|≡ p та невірно ∀x p \|\|= p. Із вищенаведених властивостей та прикладу 7 випливає: 1) у випадку неокласичної семанти- ки не завжди справджуються \|=∀xΦ→Φ, Теоретичні та методологічні основи програмування 32 ∀xΦ \|\|= Φ, \|= Φ→∃xΦ; для деяких формул Φ можливо: \|= Φ→∀xΦ та \|≠ ∃xΦ→Φ; 2) у випадку пересиченої семантики не завжди справджуються \|≡∀xΦ→Φ, ∀xΦ \|\|≡ Φ, \|≡ Φ→∃xΦ; для деяких формул Φ можливо: \|≡ Φ→∀xΦ та невірно \|≡ ∃xΦ→Φ. Із теореми 11 (про дуальну АС) для логік квазіарних предикатів у випадку за- гальної семантики отримуємо: Φ \|=T Ψ ⇔ ⇔ Φ \|=F Ψ ⇔ \|=TF Ψ. На основі розглянутих властивостей КНЛК отримуємо наступні співвідношен- ня для множин формул, які перебувають у відповідних відношеннях. 1. Неокласична семантика: \|=TF ⊂ \|=T , \|=TF ⊂ \|=F , \|=T ⊂ \|=Cl , \|=F ⊂ \|=Cl ; \|=t ⊂ \|=Cl , \|=F ⊂ \|\|=, \|=T ⊂ \|\|≡; =Cm = ∅; \|=t ⊄ \|=T , \|=t ⊄ \|=F , \|=TF ⊄ \|=t ; T ⊄ \|\|=, \|=F ⊄ \|\|≡, \|\|= ⊄ \|=Cl , \|\|≡ ⊄ \|=Cl . 2. Пересичена семантика: \|=TF ⊂ \|=T , \|=TF ⊂ \|=F , \|=T ⊂ \|=Cm , \|=F ⊂ \|=Cm ; \|=t ⊂ \|=Cm , \|=F ⊂ \|\|=, \|=T ⊂ \|\|≡; \|=Cl = ∅; \|=t ⊄ \|=T , \|=t ⊄ \|=F , \|=TF ⊄ \|=t ; T ⊄ \|\|=, \|=F ⊄ \|\|≡, \|\|= ⊄ \|=Cm , \|\|≡ ⊄ \|=Cm . 3. Загальна семантика: \|=TF = \|=T = \|=F ; \|=t ⊄ \|=TF , \|=TF ⊄ \|=t ; \|=TF ⊂ \|\|≡ = \|\|= ; \|=Cl = ∅ та \|=Cm = ∅. Для логік еквітонних та логік анти- еквітонних предикатів маємо також насту- пні властивості. Теорема 16. 1) для логік еквітонних та логік антиеквітонних предикатів у від- повідних семантиках завжди справджу- ються ( )x zR Φ A\|=Cl ∃xΦ, ∀xΦ A\|=Cl ( )x zR Φ , ( )x zR Φ A\|=Cm ∃xΦ, ∀xΦ A\|=Cm ( )x zR Φ ; 2) для логік еквітонних предикатів у відповідних семантиках завжди справджу- ються ( )x zR Φ A\|=T ∃xΦ, ∀xΦ A\|=F ( )x zR Φ та ∀xΦ \|\|= ( )x zR Φ , але вони не завжди вірні для логік антиеквітонних предикатів; 3) для логік антиеквітонних предика- тів у відповідних семантиках завжди справ- джуються ( )x zR Φ A\|=F ∃xΦ, ∀xΦ A\|=T ( )x zR Φ та ∀xΦ \|\|≡ ( )x zR Φ , але вони не завжди вірні для логік еквітонних предикатів; 4) для логік еквітонних та для логік антиеквітонних предикатів не завжди вірні ( )x zR Φ A\|=TF ∃xΦ та ∀xΦ A\|=TF ( )x zR Φ . Для доведення використовуємо тео- рему 2 та наведені далі приклади 8–15. Приклад 8. Для p∈Ps в A = (A, IA) з частковими однозначними предикатами задамо {невизначене, якщо ( ),( ) , якщо ( ).A x im dp d F x im d ∉= ∈ Такий pA – еквітонний. При цьому ∅ ⊂ F ( )x z AR p ⊂ VA, F(∃x pA) = F(∀x pA) = VA, T ( )x z AR p = T(∃x pA) = T(∀x pA) = ∅. Приклад 9. Для p∈Ps в A = (A, IA) з тотальними неоднозначними предикатами задамо { { }, якщо ( ),( ) { , }, якщо ( ).A T x im dp d T F x im d ∉= ∈ Такий pA – еквітонний. При цьому ∅ ⊂ F ( )x z AR p ⊂ VA, F(∃x pA) = F(∀x pA) = VA, T ( )x z AR p = T(∃x pA) = T(∀x pA) = VA. Приклад 10. Для p∈Ps в A = (A, IA) з частковими однозначними предикатами задамо {невизначене, якщо ( ),( ) , якщо ( ).A x im dp d T x im d ∉= ∈ Такий pA – еквітонний. При цьому ∅ ⊂ T ( )x z AR p ⊂ VA, T(∃x pA) = T(∀x pA) = VA, F ( )x z AR p = F(∃x pA) = F(∀x pA) = ∅. Приклад 11. Для p∈Ps в A = (A, IA) з тотальними неоднозначними предиката- ми задамо { { }, якщо ( ),( ) { , }, якщо ( ).A F x im dp d T F x im d ∉= ∈ Такий pA – еквітонний. При цьому ∅ ⊂ T ( )x z AR p ⊂ VA, T(∃x pA) = T(∀x pA) = VA, F ( )x z AR p = F(∃x pA) = F(∀x pA) = VA. Приклад 12. Для q∈Ps в A = (A, IA) з частковими однозначними предикатами задамо { , якщо ( ),( ) невизначене, якщо ( ).A F x im dq d x im d ∉= ∈ Такий qA – антиеквітонний. Маємо ∅ ⊂ F ( )x z AR q ⊂ VA, F(∃x qA) = F(∀x qA) = ∅, T ( )x z AR q = T(∃x qA) = T(∀x qA) = ∅. Теоретичні та методологічні основи програмування 33 Приклад 13. Для q∈Ps в A = (A, IA) з тотальними неоднозначними предиката- ми задамо {{ , }, якщо ( ),( ) { }, якщо ( ).A T F x im dq d T x im d ∉= ∈ Такий qA – антиеквітонний. Маємо ∅ ⊂ F ( )x z AR q ⊂ VA, F(∃x qA) = F(∀x qA) = ∅, T ( )x z AR q = T(∃x qA) = T(∀x qA) = VA. Приклад 14. Для q∈Ps в A = (A, IA) з частковими однозначними предикатами задамо { , якщо ( ),( ) невизначене, якщо ( ).A T x im dq d x im d ∉= ∈ Такий qA – антиеквітонний. Маємо ∅ ⊂ T ( )x z AR q ⊂ VA, T(∃x qA) = T(∀x qA) = ∅, F ( )x z AR q = F(∃x qA) = F(∀x qA) = ∅. Приклад 15. Для q∈Ps в A = (A, IA) з тотальними неоднозначними предиката- ми задамо {{ , }, якщо ( ),( ) { }, якщо ( ).A T F x im dq d F x im d ∉= ∈ Такий qA – антиеквітонний. Маємо ∅ ⊂ T ( )x z AR q ⊂ VA, T(∃x qA) = T(∀x qA) = ∅, F ( )x z AR q = F(∃x qA) = F(∀x qA) = VA. Наслідок 6. 1) для логік еквітонних предикатів у відповідних семантиках зав- жди Φ A\|=Cl ∃xΦ, ∀xΦ A\|=Cl Φ, Φ A\|=Cm ∃xΦ, ∀xΦ A\|=Cm Φ, Φ A\|=T ∃xΦ, ∀xΦ A\|=F Φ, ∀xΦ \|\|= Φ; завжди \|= ∀xΦ ⇔ \|=Φ; не зав- жди Φ A\|=F ∃xΦ, ∀xΦ A\|=T Φ, Φ A\|=TF ∃xΦ, ∀xΦ A\|=TF Φ та ∀xΦ \|\|≡ Φ; 2) для логік антиеквітонних преди- катів у відповідних семантиках завжди Φ A\|=Cl ∃xΦ, ∀xΦ A\|=Cl Φ, Φ A\|=Cm ∃xΦ, ∀xΦ A\|=Cm Φ, Φ A\|=F ∃xΦ, ∀xΦ A\|=T Φ, ∀xΦ \|\|≡ Φ; не завжди Φ A\|=T ∃xΦ, ∀xΦ A\|=F Φ, Φ A\|=TF ∃xΦ, ∀xΦ A\|=TF Φ та ∀xΦ \|\|= Φ. Наслідок 7. У випадках загальної семантики еквітонних предикатів та зага- льної семантики антиеквітонних предика- тів відношення \|=T , \|=F та \|=TF різні. Таким чином, у випадках загальної семантики еквітонних предикатів та зага- льної семантики антиеквітонних предика- тів отримуємо наступні співвідношення для множин формул, які перебувають у відповідних відношеннях: \|=TF ⊂ \|=T , \|=TF ⊂ \|=F ; \|=t ⊄ \|=TF , \|=TF ⊄ \|=t ; \|=T ⊂ \|\|≡ , \|=F ⊂ \|\|= ; \|=Cl = ∅, \|=Cm = ∅. Для логік квазіарних предикатів ре- номінативного та кванторного рівнів спра- вджуються теорема 8 (еквівалентності та теорема 9 (заміни еквівалентних). Розглянемо властивості відношень логічного наслідку для множин формул, пов‘язані з композицією реномінації. Такі властивості, не пов’язані з кванторами, справджуються вже для логік реномінати- вного рівня. При кожній інтерпретації пре- дикати, що є значеннями виділених фор- мул, збігаються, тому ці властивості спра- вджуються для \|=TF, вони вірні також для \|=T, \|=F, \|=Cl, \|=Cm. RT\|–) , , ( )z v z xR Φ , ΓΓΓΓ \|=TF ∆∆∆∆ ⇔ ⇔ ( )v xR Φ , ΓΓΓΓ \|=TF ∆∆∆∆. RT–\|) ΓΓΓΓ \|=TF ∆∆∆∆, , , ( )z v z xR Φ ⇔ ⇔ ΓΓΓΓ \|=TF ∆∆∆∆, ( )v xR Φ . RR\|–) ( ( )),v w x yR R Φ ΓΓΓΓ \|=TF ∆∆∆∆ ⇔ ⇔ ( ),v w x yR Φo ΓΓΓΓ \|=TF ∆∆∆∆. RR–\|) ΓΓΓΓ \|=TF ∆∆∆∆, ( ( ))v w x yR R Φ ⇔ ⇔ ΓΓΓΓ \|=TF ∆∆∆∆, ( )v w x yR Φo . R¬\|–) v xR (¬Φ), ΓΓΓΓ \|=TF ∆∆∆∆ ⇔ ⇔ ¬ v xR (Φ), \|=TF ∆∆∆∆. R¬–\|) ΓΓΓΓ \|=TF ∆∆∆∆, v xR (¬Φ) ⇔ ⇔ ΓΓΓΓ \|=TF ∆∆∆∆, ¬ v xR (Φ). R∨\|–) v xR (Φ∨Ψ), ΓΓΓΓ \|=TF ∆∆∆∆ ⇔ ⇔ v xR (Φ)∨ v xR (Ψ), ΓΓΓΓ \|=TF ∆∆∆∆. R∨–\|) ΓΓΓΓ \|=TF ∆∆∆∆, v xR (Φ∨Ψ) ⇔ ⇔ ΓΓΓΓ \|=TF ∆∆∆∆, v xR (Φ)∨ v xR (Ψ). Аналогічно записуються властивос- ті R→\|– , R→–\| , R&\|– , R&–\| . R∃\|–) ( ),v xR y∃ Φ ΓΓΓΓ \|=TF ∆∆∆∆ ⇔ ⇔ ( ),v xyR∃ Φ ΓΓΓΓ \|=TF ∆∆∆∆ за умови у∉{ ,v x }. R∃–\|) ΓΓΓΓ \|=TF ∆∆∆∆, ( )v xR y∃ Φ ⇔ ⇔ ΓΓΓΓ \|=TF ∆∆∆∆, ( )v xyR∃ Φ за умови у∉{ ,v x }. R∃∃S\|–) ( ),v xR y∃ Φ ΓΓΓΓ \|=TF ∆∆∆∆ ⇔ Теоретичні та методологічні основи програмування 34 ⇔ ( ),v y x zzR∃ Φo ΓΓΓΓ \|=TF ∆∆∆∆ за умови у∈{ ,v x }. R∃∃S–\|) ΓΓΓΓ \|=TF ∆∆∆∆, ( )v xR y∃ Φ ⇔ ⇔ ΓΓΓΓ \|=TF ∆∆∆∆, ( )v y x zzR∃ Φo за умови у∈{ ,v x }. Для R∃∃S\|– та R∃∃S–\| z тотально строго неістотне та z∉ ( ( ))v xnm R x∃ Φ . Аналогічно записуються власти- вості R∀\|– , R∀–\| , R∀∀S\|– , R∀∀S–\| . ΦNS\|–) , , ( ),y v z xR Φ ΓΓΓΓ \|=TF ∆∆∆∆ ⇔ ⇔ ( ),v xR Φ ΓΓΓΓ \|=TF ∆∆∆∆ за умови у∈ν(Φ). ΦNS–\|) ΓΓΓΓ \|=TF ∆∆∆∆, , , ( )y v z xR Φ ⇔ ⇔ ΓΓΓΓ \|=TF ∆∆∆∆, ( )v xR Φ за умови у∈ν(Φ). Для логік однозначних часткових предикатів також маємо відомі [2] власти- вості: R∃∃\|–) ( ),v xR y∃ Φ ΓΓΓΓ \|=Cl ∆∆∆∆ ⇔ ⇔ ( ),v y x zzR∃ Φo ΓΓΓΓ \|=Cl ∆∆∆∆; R∃∃–\|) ΓΓΓΓ \|=Cl ∆∆∆∆, ( )v xR y∃ Φ ⇔ ⇔ ΓΓΓΓ \|=Cl ∆∆∆∆, ( )v y x zzR∃ Φo . Для R∃∃\|– та R∃∃–\| умови: у∈{ ,v x }, z тотально неістотне та z∉ ( ( ))v xnm R x∃ Φ . Аналогічно записуються власти- вості R∀∀\|– , R∀∀–\| . ΦN\|–) , , ( ),y v z xR Φ ΓΓΓΓ \|=Cl ∆∆∆∆ ⇔ ⇔ ( ),v xR Φ ΓΓΓΓ \|=Cl ∆∆∆∆ за умови у∈µ(Φ). ΦN–\|) ΓΓΓΓ \|=Cl ∆∆∆∆, , , ( )y v z xR Φ ⇔ ⇔ ΓΓΓΓ \|=Cl ∆∆∆∆, ( )v xR Φ за умови у∈µ(Φ). Якщо Φ – це р∈Ps, властивості ΦN\|– і ΦN–\| записуємо як PsN\|– і PsN–\| . Розглянемо тепер властивості відно- шень \|=T, \|=F, \|=TF, \|=Cl, \|=Cm, пов'язані з елімінацією кванторів. Надалі ΓΓΓΓ та ∆∆∆∆ позначатимуть довіль- ні множини формул, A – довільну АС. Для спрощення запису при зафіксо- ваній A предикати вигляду ΦA будемо позначати Φ. У випадку ΓΓΓΓ A\|= ∆∆∆∆ будемо позначати ( )AT Φ∈Γ ΦI як T(ΓΓΓΓ), ( )AT Ψ∈∆ ΨU як T(∆∆∆∆), ( )AF Φ∈Γ ΦU як F(ΓΓΓΓ), ( )AF Ψ∈∆ ΨI як F(∆∆∆∆). Для загального випадку логік квазі- арних предикатів ( )x yR Φ \|= ( ),x yR xΦ ∃ Φ та , ( )x yx R∀ Φ Φ \|= ( )x yR Φ , де \|= – одне з \|=Cl, \|=Cm \|=T, \|=F, \|=TF. Враховуючи теорему 15, отримуємо, що із ΓΓΓΓ \|= ( ),x yR xΦ ∃ Φ не ви- пливає ΓΓΓΓ \|= ∃хΦ та із , ( )x yx R∀ Φ Φ \|= ∆∆∆∆ не випливає ∀хΦ \|= ∆∆∆∆ (тут \|= – одне з \|=Cl, \|=Cm \|=T, \|=F, \|=TF ). Отримали Наслідок 8. Для загального випадку квазіарних предикатів у відповідних се- мантиках: 1) із ΓΓΓΓ \|= ∆∆∆∆, ∃хΦ, ( )x yR Φ не випливає ΓΓΓΓ \|= ∆∆∆∆, ∃хΦ; 2) із , ( ),x yx R∀ Φ Φ ΓΓΓΓ \|= ∆∆∆∆ не випливає ∀хΦ,ΓΓΓΓ \|= ∆∆∆∆. Тут \|= – одне з \|=Cl, \|=Cm \|=T, \|=F, \|=TF . Дещо краща ситуація для логік екві- тонних та логік антиеквітонних предикатів. Теорема 17. 1) Для логік еквітон- них та логік антиеквітонних предикатів: а) ΓΓΓΓ A\|=Cl ∆∆∆∆, ∃хΦ, ( )x zR Φ ⇒ ⇒ ΓΓΓΓ A\|=Cl ∆∆∆∆, ∃хΦ та ΓΓΓΓ, ∀хΦ, ( )x zR Φ A\|=Cl ∆∆∆∆ ⇒ ⇒ ΓΓΓΓ, ∀хΦ A\|=Cl ∆∆∆∆; б) ΓΓΓΓ A\|=Cm ∆∆∆∆, ∃хΦ, ( )x zR Φ ⇒ ⇒ ΓΓΓΓ A\|=Cm ∆∆∆∆, ∃хΦ та ΓΓΓΓ, ∀хΦ, ( )x zR Φ A\|=Cm ∆∆∆∆ ⇒ ⇒ ΓΓΓΓ, ∀хΦ A\|=Cm ∆∆∆∆; 2) для логік еквітонних предикатів: а) ΓΓΓΓ A\|=T ∆∆∆∆, ∃хΦ, ( )x zR Φ ⇒ ⇒ ΓΓΓΓ A\|=T ∆∆∆∆, ∃хΦ, не завжди ΓΓΓΓ A\|=F ∆∆∆∆, ∃хΦ, ( )x zR Φ ⇒ ΓΓΓΓ A\|=F ∆∆∆∆, ∃хΦ; б) ΓΓΓΓ, ∀хΦ, ( )x zR Φ A\|=F ∆∆∆∆ ⇒ ⇒ ΓΓΓΓ, ∀хΦ A\|=F ∆∆∆∆, не завжди ΓΓΓΓ, ∀хΦ, ( )x zR Φ A\|=T ∆∆∆∆ ⇒ ΓΓΓΓ, ∀хΦ A\|=T ∆∆∆∆; 3) для логік антиеквітонних преди- катів: а) ΓΓΓΓ A\|=F ∆∆∆∆, ∃хΦ, ( )x zR Φ ⇒ ⇒ ΓΓΓΓ A\|=F ∆∆∆∆, ∃хΦ, не завжди ΓΓΓΓ A\|=T ∆∆∆∆, ∃хΦ, ( )x zR Φ ⇒ ΓΓΓΓ A\|=T ∆∆∆∆, ∃хΦ; б) ΓΓΓΓ, ∀хΦ, ( )x zR Φ A\|=T ∆∆∆∆ ⇒ ⇒ ΓΓΓΓ, ∀хΦ A\|=T ∆∆∆∆, не завжди ΓΓΓΓ, ∀хΦ, ( )x zR Φ A\|=F ∆∆∆∆ ⇒ ΓΓΓΓ, ∀хΦ A\|=F ∆∆∆∆. Теоретичні та методологічні основи програмування 35 Доводимо п. 1, а для логік еквітон- них предикатів. Покажемо, що з умови T(ΓΓΓΓ) ∩ F(∆∆∆∆) ∩ F( ( )x zR Φ ) ∩ F(∃хΦ) = ∅ ви- пливає T(ΓΓΓΓ) ∩ F(∆∆∆∆) ∩ F(∃хΦ) = ∅. Припустимо супротивне: існує d∈T(ΓΓΓΓ) ∩ F(∆∆∆∆) ∩ F(∃хΦ), (1) T(ΓΓΓΓ) ∩ F(∆∆∆∆) ∩ F( ( )x zR Φ ) ∩ F(∃хΦ) = ∅ (2). Звідси маємо d∈F(∃хΦ) та d∉F( ( )x zR Φ ), звідки отримуємо d∇xaa∈F(Φ) для всіх a∈A (3) та d∇xad(z)∉F(Φ). Із останнього при d(z)↓ маємо супе- речність із (3), тому d(z)↑, звідки d ⊂ d∇zaa для всіх a∈A. За еквітонністю тоді із (1) та із (3) для всіх a∈A отримуємо d∇zaa∈T(ΓΓΓΓ) ∩ F(∆∆∆∆) ∩ F(∃хΦ) та d∇xaa∇zaa∈F(Φ). Із останнього маємо d∇zaa∈F( ( )x zR Φ ), звідки отримуємо d∇zaa∈T(ΓΓΓΓ) ∩ F(∆∆∆∆) ∩ F( ( )x zR Φ ) ∩ F(∃хΦ), що суперечить (2). Доводимо п. 1, а для антиеквітонних предикатів. Згідно теореми 2 маємо F(∃xΦ) ⊆ F( ( )x zR Φ ), звідки отримуємо T(ΓΓΓΓ) ∩ F(∆∆∆∆) ∩ F( ( )x zR Φ ) ∩ F(∃хΦ) = ∅ ⇒ ⇒ T(ΓΓΓΓ) ∩ F(∆∆∆∆) ∩ F(∃хΦ) = ∅. Доводимо п. 1, б для еквітонних пре- дикатів. Згідно теореми 2 маємо T( ( )x zR Φ ) ⊆ T(∃xΦ), тому отримуємо F(ΓΓΓΓ) ∪ T(∆∆∆∆) ∪ T(∃хΦ) ∪ T( ( )x zR Φ ) = VA ⇒ ⇒F(ΓΓΓΓ) ∪ T(∆∆∆∆) ∪ T(∃хΦ) = VA. Доводимо п. 1, б для антиеквітонних предикатів. Покажемо, що з умови F(ΓΓΓΓ) ∪ T(∆∆∆∆) ∪ T(∃хΦ) ∪ T( ( )x zR Φ ) = VA ви- пливає F(ΓΓΓΓ) ∪ T(∆∆∆∆) ∪ T(∃хΦ) = VA. Припустимо супротивне: існує d∉F(ΓΓΓΓ) ∪ T(∆∆∆∆) ∪ T(∃хΦ), (4) F(ΓΓΓΓ) ∪ T(∆∆∆∆) ∪ T(∃хΦ) ∪ T( ( )x zR Φ ) = VA. (5) Звідси маємо d∉T(∃хΦ) та d∈T( ( )x zR Φ ), звідки отримуємо d∇xaa∉T(Φ) для всіх a∈A (6) та d∇xad(z)∈T(Φ). Із останнього при d(z)↓ маємо супе- речність із (6), тому d(z)↑, звідки отримує- мо d ⊂ d∇zaa для всіх a∈A. За антиекві- тонністю тоді із (4) та (6) для всіх a∈A ма- ємо d∇zaa∉F(ΓΓΓΓ) ∪ T(∆∆∆∆) ∪ T(∃хΦ), звідки d∇xaa∇zaa∉T(Φ). Із останнього маємо d∇zaa∉T( ( )x zR Φ ), що суперечить (5). Враховуючи властивості пропози- ційного рівня П7 та П8, із вищедоведених ΓΓΓΓ A\|=Cl ∆∆∆∆, ∃хΦ, ( )x zR Φ ⇒ ΓΓΓΓ A\|=Cl ∆∆∆∆, ∃хΦ та ΓΓΓΓ A\|=Cm ∆∆∆∆, ∃хΦ, ( )x zR Φ ⇒ ΓΓΓΓ A\|=Cm ∆∆∆∆, ∃хΦ має- мо ΓΓΓΓ, ∀хΦ, ( )x zR Φ A\|=Cl ∆∆∆∆ ⇒ ΓΓΓΓ, ∀хΦ A\|=Cl ∆∆∆∆ та ΓΓΓΓ, ∀хΦ, ( )x zR Φ A\|=Cm ∆∆∆∆ ⇒ ΓΓΓΓ, ∀хΦ A\|=Cm ∆∆∆∆. Доводимо п. 2. Згідно теореми 2 для еквітонних предикатів маємо T( ( )x zR Φ ) ⊆ T(∃xΦ) та F( ( )x zR Φ ) ⊆ ⊆ F(∀xΦ), тому T(ΓΓΓΓ) ⊆ T(∆∆∆∆) ∪ T(∃хΦ) ∪ T( ( )x zR Φ ) ⇒ ⇒ T(ΓΓΓΓ) ⊆ T(∆∆∆∆) ∪ T(∃хΦ) та F(∆∆∆∆) ⊆ F(∀xΦ) ∪ F( ( )x zR Φ ) ∪ F(ΓΓΓΓ) ⇒ ⇒ F(∆∆∆∆) ⊆ F(∀xΦ) ∪ F(ΓΓΓΓ). Доводимо п. 3. Для антиеквітонних предикатів маємо F(∃x(Φ)) ⊆ F( ( )x zR Φ ) та T(∀xΦ) ⊆ T( ( )x zR Φ ) згідно теореми 2, тому F( ( )x zR Φ ) ∩ F(∃x(Φ)) ∩ F(∆∆∆∆) ⊆ F(ΓΓΓΓ) ⇒ ⇒ F(∃x(Φ)) ∩ F(∆∆∆∆) ⊆ F(ΓΓΓΓ) та T(ΓΓΓΓ) ∩ T(∀xΦ) ∩ T( ( )x zR Φ ) ⊆ T(∆∆∆∆) ⇒ ⇒ T(ΓΓΓΓ) ∩ T(∀xΦ) ⊆ T(∆∆∆∆). Наслідок 9. Для логік еквітонних та логік антиеквітонних предикатів: а) не завжди ΓΓΓΓ A\|=TF ∆∆∆∆, ∃хΦ, ( )x zR Φ ⇒ ⇒ ΓΓΓΓ A\|=TF ∆∆∆∆, ∃хΦ; б) не завжди ΓΓΓΓ, ∀хΦ, ( )x zR Φ A\|=TF ∆∆∆∆ ⇒ ⇒ ΓΓΓΓ, ∀хΦ A\|=TF ∆∆∆∆. Враховуючи властивість пропозицій- ного рівня U, із теореми 17 отримуємо Наслідок 10. 1) для логік еквітонних та логік антиеквітонних предикатів: а) ΓΓΓΓ A\|=Cl ∆∆∆∆, ∃хΦ, ( )x zR Φ ⇔ ⇔ ΓΓΓΓ A\|=Cl ∆∆∆∆, ∃хΦ та ΓΓΓΓ, ∀хΦ, ( )x zR Φ A\|=Cl ∆∆∆∆ ⇔ ⇔ ΓΓΓΓ, ∀хΦ A\|=Cl ∆∆∆∆; б) ΓΓΓΓ A\|=Cm ∆∆∆∆, ∃хΦ, ( )x zR Φ ⇔ ⇔ ΓΓΓΓ A\|=Cm ∆∆∆∆, ∃хΦ та ΓΓΓΓ, ∀хΦ, ( )x zR Φ A\|=Cm ∆∆∆∆ ⇔ Теоретичні та методологічні основи програмування 36 ⇔ ΓΓΓΓ, ∀хΦ A\|=Cm ∆∆∆∆; 2) для логік еквітонних предикатів: а) ΓΓΓΓ A\|=T ∆∆∆∆, ∃хΦ, ( )x zR Φ ⇔ ⇔ ΓΓΓΓ A\|=T ∆∆∆∆, ∃хΦ; б) ΓΓΓΓ, ∀хΦ, ( )x zR Φ A\|=F ∆∆∆∆ ⇔ ⇔ ΓΓΓΓ, ∀хΦ A\|=F ∆∆∆∆; 3) для логік антиеквітонних предика- тів: а) ΓΓΓΓ A\|=F ∆∆∆∆, ∃хΦ, ( )x zR Φ ⇔ ⇔ ΓΓΓΓ A\|=F ∆∆∆∆, ∃хΦ; б) ΓΓΓΓ, ∀хΦ, ( )x zR Φ A\|=T ∆∆∆∆ ⇔ ⇔ ΓΓΓΓ, ∀хΦ A\|=T ∆∆∆∆. Для логік квазіарних предикатів у відповідних семантиках завжди ∃хΦ \|= ∃хΦ та ∀хΦ \|= ∀хΦ, де \|= – одне з \|=Cl, \|=Cm \|=T, \|=F, \|=TF. Враховуючи теорему 15, звідси Наслідок 11. Для загального випад- ку логік квазіарних предикатів у відповід- них семантиках не завжди ∃хΦ, ΓΓΓΓ \|= ∆∆∆∆ ⇒ ⇒ ( ),x zR Φ ΓΓΓΓ \|= ∆∆∆∆ та не завжди ΓΓΓΓ \|= ∀хΦ, ∆∆∆∆ ⇒ ⇒ ΓΓΓΓ \|= ( ),x zR Φ ∆∆∆∆ (тут \|= – одне з \|=Cl, \|=Cm \|=T, \|=F, \|=TF ). Теорема 18. 1) для логік еквітонних предикатів в неокласичній семантиці: а) ∃хΦ, ΓΓΓΓ A\|=Cl ∆∆∆∆ ⇒ ( ),x zR Φ ΓΓΓΓ A\|=Cl ∆∆∆∆ та ΓΓΓΓ A\|=Cl ∀хΦ, ∆∆∆∆ ⇒ ΓΓΓΓ A\|=Cl ( ),x zR Φ ∆∆∆∆; б) ∃хΦ, ΓΓΓΓ A\|=T ∆∆∆∆ ⇒ ( ),x zR Φ ΓΓΓΓ A\|=T ∆∆∆∆ та ΓΓΓΓ A\|=F ∀хΦ, ∆∆∆∆ ⇒ ΓΓΓΓ A\|=F ( ),x zR Φ ∆∆∆∆; в) не завжди ∃хΦ, ΓΓΓΓ \|=F ∆∆∆∆ ⇒ ( ),x yR Φ ΓΓΓΓ \|=F ∆∆∆∆, ∃хΦ, ΓΓΓΓ \|=TF ∆∆∆∆ ⇒ ( ),x yR Φ ΓΓΓΓ \|=TF ∆∆∆∆, ΓΓΓΓ A\|=T ∀хΦ, ∆∆∆∆ ⇒ ΓΓΓΓ A\|=T ( ),x zR Φ ∆∆∆∆, ΓΓΓΓ A\|=TF ∀хΦ, ∆∆∆∆ ⇒ ΓΓΓΓ A\|=TF ( ),x zR Φ ∆∆∆∆; 2) для логік антиеквітонних преди- катів в пересиченій семантиці: а) ∃хΦ, ΓΓΓΓ A\|=Cm ∆∆∆∆ ⇒ ( ),x zR Φ ΓΓΓΓ A\|=Cm ∆∆∆∆ та ΓΓΓΓ A\|=Cm ∀хΦ, ∆∆∆∆ ⇒ ΓΓΓΓ A\|=Cm ( ),x zR Φ ∆∆∆∆; б) ∃хΦ, ΓΓΓΓ A\|=F ∆∆∆∆ ⇒ ( ),x zR Φ ΓΓΓΓ A\|=F ∆∆∆∆ та ΓΓΓΓ A\|=T ∀хΦ, ∆∆∆∆ ⇒ ΓΓΓΓ A\|=T ( ),x zR Φ ∆∆∆∆; в) не завжди ∃хΦ, ΓΓΓΓ \|=T ∆∆∆∆ ⇒ ( ),x yR Φ ΓΓΓΓ \|=T ∆∆∆∆, ∃хΦ, ΓΓΓΓ \|=TF ∆∆∆∆ ⇒ ( ),x yR Φ ΓΓΓΓ \|=TF ∆∆∆∆, ΓΓΓΓ A\|=F ∀хΦ, ∆∆∆∆ ⇒ ΓΓΓΓ A\|=F ( ),x zR Φ ∆∆∆∆, ΓΓΓΓ A\|=TF ∀хΦ, ∆∆∆∆ ⇒ ΓΓΓΓ A\|=TF ( ),x zR Φ ∆∆∆∆. Теорема 18 доводиться на основі тео- реми 2 та прикладів 8–15. Теорема 19. Нехай z тотально стро- го неістотне та z∉пт(ΓΓΓΓ, ∆∆∆∆, Φ). Тоді 1) ( ),x zR Φ ΓΓΓΓ A\|= ∆∆∆∆ ⇒ ∃хΦ, ΓΓΓΓ A\|= ∆∆∆∆; 2) ΓΓΓΓ A\|= ( ),x zR Φ ∆∆∆∆ ⇒ ΓΓΓΓ A\|= ∀хΦ, ∆∆∆∆. Тут \|= – одне з \|=Cl, \|=Cm \|=T, \|=F, \|=TF. Доводимо п. 1 для \|=Cl . Покажемо, що із T(ΓΓΓΓ) ∩ T( ( )x zR Φ ) ∩ F(∆∆∆∆) = ∅ випли- ває T(ΓΓΓΓ) ∩ T(∃хΦ) ∩ F(∆∆∆∆) = ∅. Припустимо супротивне: існує d∈T(ΓΓΓΓ) ∩ T(∃хΦ) ∩ F(∆∆∆∆), проте T(ΓΓΓΓ) ∩ T( ( )x zR Φ ) ∩ F(∆∆∆∆) = ∅. Тоді маємо d∈T(∃хΦ), d∈T(ΓΓΓΓ) та d∈F(∆∆∆∆), із d∈T(∃хΦ) маємо d∇xaa∈T(Φ) для деякого a∈A. Але z тотально строго неістотне та z∉пт(ΓΓΓΓ, ∆∆∆∆, Φ), тому маємо d∇zaa∈T(ΓΓΓΓ), d∇zaa∈F(∆∆∆∆) та d∇xaa∇zaa∈T(Φ). Із ос- таннього отримуємо d∇zaa∈T( ( )x zR Φ ), тому d∇zaa∈T(ΓΓΓΓ) ∩ T( ( )x zR Φ ) ∩ F(∆∆∆∆), що суперечить T(ΓΓΓΓ) ∩ T( ( )x zR Φ ) ∩ F(∆∆∆∆) = ∅. Враховуючи властивості П7 та П8, п. 2 для \|=Cl випливає з п. 1. Доводимо п. 1 для \|=Cm . Покажемо, що з F(ΓΓΓΓ) ∪ F( ( )x zR Φ ) ∪ T(∆∆∆∆) = VA випливає F(ΓΓΓΓ) ∪ F(∃хΦ) ∪ T(∆∆∆∆) = VA. Припустимо су- противне: існує d∉F(ΓΓΓΓ) ∪ F(∃хΦ) ∪ T(∆∆∆∆), проте F(ΓΓΓΓ) ∪ F( ( )x zR Φ ) ∪ T(∆∆∆∆) = VA. Тоді d∉F(ΓΓΓΓ), d∉F(∃хΦ) та d∉T(∆∆∆∆), із d∉F(∃хΦ) маємо d∇xaa∉F(Φ) для деякого a∈A. Але z тотально строго неістотне і z∉пт(ΓΓΓΓ, ∆∆∆∆, Φ), тому маємо d∇zaa∉F(ΓΓΓΓ), d∇zaa∉T(∆∆∆∆), d∇xaa∇zaa∉F(Φ). Із останнього маємо d∇zaa∉F( ( )x zR Φ ), тому отримуємо d∇zaa∉F(ΓΓΓΓ) ∪ F( ( )x zR Φ ) ∪ T(∆∆∆∆), що супе- речить F(ΓΓΓΓ) ∪ F( ( )x zR Φ ) ∪ T(∆∆∆∆) = VA. Враховуючи властивості П7 та П8, п. 2 для \|=Cm випливає з п. 1. Доводимо п. 1 для \|=T . Покажемо, що із T(ΓΓΓΓ) ∩ T( ( )x zR Φ ) ⊆ T(∆∆∆∆) випливає T(ΓΓΓΓ) ∩ T(∃хΦ) ⊆ T(∆∆∆∆). Припустимо супроти- вне: деяке d∈T(ΓΓΓΓ), d∈T(∃хΦ), d∉T(∆∆∆∆), про- Теоретичні та методологічні основи програмування 37 те T(ΓΓΓΓ) ∩ T( ( )x zR Φ ) ⊆ T(∆∆∆∆). Із d∈T(∃хΦ) ма- ємо d∇xaa∈T(Φ) для деякого a∈A. Але z тотально строго неістотне та z∉пт(ΓΓΓΓ, ∆∆∆∆, Φ), тому звідси d∇zaa∈T(ΓΓΓΓ), d∇zaa∉T(∆∆∆∆) та d∇xaa∇zaa∈T(Φ). Із останнього маємо d∇zaa∈T( ( )x zR Φ ), тому d∇zaa∉T(∆∆∆∆) та d∇zaa∈T(ΓΓΓΓ) ∩ T( ( )x zR Φ ), що суперечить T(ΓΓΓΓ) ∩ T( ( )x zR Φ ) ⊆ T(∆∆∆∆). Доводимо п. 2 для \|=T . Покажемо, що із T(ΓΓΓΓ) ⊆ T( ( )x zR Φ ) ∪ T(∆∆∆∆) випливає T(ΓΓΓΓ) ⊆ T(∀хΦ) ∪ T(∆∆∆∆). Припустимо супро- тивне: деяке d∈T(ΓΓΓΓ), d∉T(∀хΦ), d∉T(∆∆∆∆), проте T(ΓΓΓΓ) ⊆ T( ( )x zR Φ ) ∪ T(∆∆∆∆). Із d∉T(∀хΦ) маємо d∇xaa∉T(Φ) для деякого a∈A. Але z тотально строго неістотне та z∉пт(ΓΓΓΓ, ∆∆∆∆, Φ), тому маємо d∇zaa∈T(ΓΓΓΓ), d∇zaa∉T(∆∆∆∆) та d∇xaa∇zaa∉T(Φ). Із останнього маємо d∇zaa∉T( ( )x zR Φ ), тому d∇zaa∈T(ΓΓΓΓ) та d∇zaa∉T( ( )x zR Φ ) ∪ T(∆∆∆∆), що суперечить T(ΓΓΓΓ) ⊆ T( ( )x zR Φ ) ∪ T(∆∆∆∆). Доводимо п. 1 для \|=F . Покажемо, що із F(∆∆∆∆) ⊆ F(ΓΓΓΓ) ∪ F( ( )x zR Φ ) випливає F(∆∆∆∆) ⊆ F(ΓΓΓΓ) ∪ F(∃хΦ). Припустимо супро- тивне: деяке d∈F(∆∆∆∆), d∉F(∃хΦ), d∉F(ΓΓΓΓ), проте F(∆∆∆∆) ⊆ F(ΓΓΓΓ) ∪ F( ( )x zR Φ ). Із d∉F(∃хΦ) маємо d∇xaa∉F(Φ) для деякого a∈A. Але z тотально строго неістотне та z∉пт(ΓΓΓΓ, ∆∆∆∆, Φ), тому маємо d∇zaa∈F(∆∆∆∆), d∇zaa∉F(ΓΓΓΓ) та d∇xaa∇zaa∉F(Φ). Із останнього маємо d∇zaa∉F( ( )x zR Φ ), тому d∇zaa∈F(∆∆∆∆) та d∇zaa∉F(ΓΓΓΓ) ∪ F( ( )x zR Φ ), що суперечить F(∆∆∆∆) ⊆ F(ΓΓΓΓ) ∪ F( ( )x zR Φ ). Доводимо п. 2 для \|=F . Покажемо, що із F( ( )x zR Φ ) ∩ F(∆∆∆∆) ⊆ F(ΓΓΓΓ) випливає F(∀хΦ) ∩ F(∆∆∆∆) ⊆ F(ΓΓΓΓ). Припустимо супро- тивне: деяке d∈F(∆∆∆∆), d∈F(∀хΦ), d∉F(ΓΓΓΓ), проте F( ( )x zR Φ ) ∩ F(∆∆∆∆) ⊆ F(ΓΓΓΓ). Із умови d∈F(∀хΦ) маємо d∇xaa∈F(Φ) для деяко- го a∈A. Але z тотально строго неістотне та z∉пт(ΓΓΓΓ, ∆∆∆∆, Φ), тому маємо d∇zaa∈F(∆∆∆∆), d∇zaa∉F(ΓΓΓΓ) та d∇xaa∇zaa∈F(Φ). Із останнього маємо d∇zaa∈F( ( )x zR Φ ), тому d∇zaa∉F(ΓΓΓΓ) та d∇zaa∈F( ( )x zR Φ ) ∩ F(∆∆∆∆), що суперечить F( ( )x zR Φ ) ∩ F(∆∆∆∆) ⊆ F(ΓΓΓΓ). Доводимо п. 1 для \|=TF . Для цього покажемо: із T(ΓΓΓΓ) ∩ T( ( )x zR Φ ) ⊆ T(∆∆∆∆) та F(∆∆∆∆) ⊆ F(ΓΓΓΓ) ∪ F( ( )x zR Φ ) випливають умови T(ΓΓΓΓ) ∩ T(∃хΦ) ⊆ T(∆∆∆∆), F(∆∆∆∆) ⊆ F(ΓΓΓΓ) ∪ F(∃хΦ). Нехай супротивне: T(ΓΓΓΓ) ∩ T( ( )x zR Φ ) ⊆ T(∆∆∆∆), F(∆∆∆∆) ⊆ F(ΓΓΓΓ) ∪ F( ( )x zR Φ ) та невірно T(ΓΓΓΓ) ∩ T(∃хΦ) ⊆ T(∆∆∆∆) або невірно F(∆∆∆∆) ⊆ F(ΓΓΓΓ) ∪ F(∃хΦ). У першому випадку доводимо так як для \|=T , а в другому – як для \|=F . Доводимо п. 2 для \|=TF . Для цього покажемо: із T(ΓΓΓΓ) ⊆ T( ( )x zR Φ ) ∪ T(∆∆∆∆) та F( ( )x zR Φ ) ∩ F(∆∆∆∆) ⊆ F(ΓΓΓΓ) (1) випливають T(ΓΓΓΓ) ⊆ T(∀хΦ) ∪ T(∆∆∆∆), F(∀хΦ) ∩ F(∆∆∆∆) ⊆ F(ΓΓΓΓ). Нехай супротивне: T(ΓΓΓΓ) ⊆ T( ( )x zR Φ ) ∪ T(∆∆∆∆), F( ( )x zR Φ ) ∩ F(∆∆∆∆) ⊆ F(ΓΓΓΓ) та невірно T(ΓΓΓΓ) ⊆ T(∀хΦ) ∪ T(∆∆∆∆) або невірно F(∀хΦ) ∩ F(∆∆∆∆) ⊆ F(ΓΓΓΓ). У першому випадку доводимо так як для \|=T , а в другому – як для \|=F . Із теорем 18 та 19 отримуємо Наслідок 12. Нехай z тотально неіс- тотне та z∉пт(ΓΓΓΓ, ∆∆∆∆, Φ). Тоді 1) для логік еквітонних предикатів: ∃хΦ, ΓΓΓΓ A\|=Cl ∆∆∆∆ ⇔ ( ),x zR Φ ΓΓΓΓ A\|=Cl ∆∆∆∆, ΓΓΓΓ A\|=Cl ∀хΦ, ∆∆∆∆ ⇔ ΓΓΓΓ A\|=Cl ( ),x zR Φ ∆∆∆∆, ∃хΦ, ΓΓΓΓ A\|=T ∆∆∆∆ ⇔ ( ),x zR Φ ΓΓΓΓ A\|=T ∆∆∆∆, ΓΓΓΓ A\|=F ∀хΦ, ∆∆∆∆ ⇔ ΓΓΓΓ A\|=F ( ),x zR Φ ∆∆∆∆; 2) для логік антиеквітонних преди- катів: ∃хΦ, ΓΓΓΓ A\|=Cm ∆∆∆∆ ⇔ ( ),x zR Φ ΓΓΓΓ A\|=Cm ∆∆∆∆, ΓΓΓΓ A\|=Cm ∀хΦ, ∆∆∆∆ ⇔ ΓΓΓΓ A\|=Cm ( ),x zR Φ ∆∆∆∆, ∃хΦ, ΓΓΓΓ A\|=F ∆∆∆∆ ⇔ ( ),x zR Φ ΓΓΓΓ A\|=F ∆∆∆∆, ΓΓΓΓ A\|=T ∀хΦ, ∆∆∆∆ ⇔ ΓΓΓΓ A\|=T ( ),x zR Φ ∆∆∆∆. Висновки У роботі вивчаються семантичні вла- стивості композиційно номінативних логік Теоретичні та методологічні основи програмування 38 часткових однозначних, тотальних та част- кових неоднозначних предикатів пропози- ційного, реномінативного та кванторного рівнів. Дається визначення композицій че- рез області істинності та хибності преди- катів, визначення еквітонних та антиекві- тонних предикатів. Для зазначених логік досліджуються відношення логічного нас- лідку для пар та множин формул, відпо- відні відношення логічної еквівалентності. 1. Нікітченко М.С., Шкільняк С.С. Інтенсіона- льно-орієнтований підхід до побудови логі- чних систем // Проблеми програмування. – 2007. – № 2. – C. 15–40. 2. Нікітченко М.С., Шкільняк С.С. Математи- чна логіка та теорія алгоритмів. – К., 2008. – 528 с. 3. Смирнова Е.Д. Логика и философия. – М., 1996. – 304 с. 4. Нікітченко М.С., Шкільняк С.С. Семантичні властивості композиційно-номінативних логік. – Міжнар. конф. "Теоретичні та при- кладні аспекти побудови програмних сис- тем". – TAAPSD'2009. Тези доповідей. – К., 2009. – С. 50–59. 5. Никитченко Н.С. Предикатные компози- ционно-номинативные системы // Пробле- мы программирования. – 1999. – № 2. – С. 3–19. Отримано 29.12.2009 Про автора: Шкільняк Степан Степанович, кандидат фізико-математичних наук, доцент кафедри теорії та технології програмування Київського національного університету імені Тараса Шевченка. Місце роботи автора: Київський національний університет імені Тараса Шевченка, 01601, Київ-601, вул. Володимирська, 60. Тел.: (044) 259-0519, (044) 522-0640 (д), e-mail: sssh@unicyb.kiev.ua

Relations of logical consequence in composition nominative logics

Institution

Ähnliche Einträge