Special relations of logical consequence in logics of quasi-ary predicates
We introduce and study X–Y-valued relations of logical consequence for first-order composition-nominative logics of partial single-valued, total multiple-valued and partial multiple-valued predicates. A number of properties of the defined relations is obtained, particularly the properties of quantif...
Gespeichert in:
| Datum: | 2025 |
|---|---|
| 1. Verfasser: | |
| Format: | Artikel |
| Sprache: | Ukrainian |
| Veröffentlicht: |
PROBLEMS IN PROGRAMMING
2025
|
| Schlagworte: | |
| Online Zugang: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/824 |
| 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-824 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/68/b4e6b99735b694d79413f5735a4b4c68.pdf |
| spelling |
pp_isofts_kiev_ua-article-8242025-09-02T15:42:07Z Special relations of logical consequence in logics of quasi-ary predicates Спеціальні відношення логічного наслідку в логіках квазіарних предикатів Shkilniak, S.S. UDC 004.42:510.69 УДК 004.42:510.69 We introduce and study X–Y-valued relations of logical consequence for first-order composition-nominative logics of partial single-valued, total multiple-valued and partial multiple-valued predicates. A number of properties of the defined relations is obtained, particularly the properties of quantifier elimination. Such properties will be the basis for construction of corresponding sequent calculi.Prombles in programming 2011; 4: 36-48 Для першопорядкових композиційно-номінативних логік часткових однозначних, тотальних неоднозначних та часткових неоднозначних квазіарних предикатів запропоновано і досліджено Х–Y-означені відношення логічного наслідку. Отримано низку властивостей цих відношень у різних семантиках, зокрема, властивості елімінації кванторів. Такі властивості ляжуть в основу побудови відповідних числень секвенційного типу.Prombles in programming 2011; 4: 36-48 PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2025-09-02 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/824 PROBLEMS IN PROGRAMMING; No 4 (2011); 36-48 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 4 (2011); 36-48 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 4 (2011); 36-48 1727-4907 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/824/876 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-02T15:42:07Z |
| collection |
OJS |
| language |
Ukrainian |
| topic |
UDC 004.42:510.69 |
| spellingShingle |
UDC 004.42:510.69 Shkilniak, S.S. Special relations of logical consequence in logics of quasi-ary predicates |
| topic_facet |
UDC 004.42:510.69 УДК 004.42:510.69 |
| format |
Article |
| author |
Shkilniak, S.S. |
| author_facet |
Shkilniak, S.S. |
| author_sort |
Shkilniak, S.S. |
| title |
Special relations of logical consequence in logics of quasi-ary predicates |
| title_short |
Special relations of logical consequence in logics of quasi-ary predicates |
| title_full |
Special relations of logical consequence in logics of quasi-ary predicates |
| title_fullStr |
Special relations of logical consequence in logics of quasi-ary predicates |
| title_full_unstemmed |
Special relations of logical consequence in logics of quasi-ary predicates |
| title_sort |
special relations of logical consequence in logics of quasi-ary predicates |
| title_alt |
Спеціальні відношення логічного наслідку в логіках квазіарних предикатів |
| description |
We introduce and study X–Y-valued relations of logical consequence for first-order composition-nominative logics of partial single-valued, total multiple-valued and partial multiple-valued predicates. A number of properties of the defined relations is obtained, particularly the properties of quantifier elimination. Such properties will be the basis for construction of corresponding sequent calculi.Prombles in programming 2011; 4: 36-48 |
| publisher |
PROBLEMS IN PROGRAMMING |
| publishDate |
2025 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/824 |
| work_keys_str_mv |
AT shkilniakss specialrelationsoflogicalconsequenceinlogicsofquasiarypredicates AT shkilniakss specíalʹnívídnošennâlogíčnogonaslídkuvlogíkahkvazíarnihpredikatív |
| first_indexed |
2025-09-17T09:24:25Z |
| last_indexed |
2025-09-17T09:24:25Z |
| _version_ |
1850410895759376384 |
| fulltext |
Теоретичні та методологічні основи програмування
36
УДК 004.42:510.69
С.С. Шкільняк
СПЕЦІАЛЬНІ ВІДНОШЕННЯ ЛОГІЧНОГО НАСЛІДКУ
В ЛОГІКАХ КВАЗІАРНИХ ПРЕДИКАТІВ
Для першопорядкових композиційно-номінативних логік часткових однозначних, тотальних неодно-
значних та часткових неоднозначних квазіарних предикатів запропоновано і досліджено Х–Y-означені
відношення логічного наслідку. Отримано низку властивостей цих відношень у різних семантиках, зок-
рема, властивості елімінації кванторів. Такі властивості ляжуть в основу побудови відповідних числень
секвенційного типу.
Вступ
Поняття логічного слідування нале-
жить до найфундаментальніших понять
логіки. Логічне слідування можна форма-
лізувати за допомогою відношення логіч-
ного наслідку. Будуючи різні семантики,
можна визначити багато таких відношень.
Нестандартні семантики для пропозицій-
ної логіки та різноманітні відношення логі-
чного наслідку запропоновані О.Д. Смир-
новою [1], їх побудова базується на пос-
тулатах частковості предикатів і симетрич-
ності істинності та хибності. В роботі [2]
подібні семантики та формалізації відно-
шення логічного наслідку узагальнені на
випадок композиційно-номінативних логік
часткових однозначних, тотальних неодно-
значних та часткових неоднозначних пре-
дикатів. Композиційно-номінативні логіки
(КНЛ) – це програмно-орієнтовані логічні
формалізми, будовані на основі компози-
ційно-номінативного підходу [3]. Зазначе-
ний підхід до побудови моделей програм
та орієнтованих на них логік виявився ве-
льми плідним, на його базі розроблено [4]
широкий спектр логічних формалізмів, що
знаходяться на різних рівнях абстрактності
та загальності. КНЛ базуються на загаль-
них класах часткових відображень, зада-
них на довільних наборах іменованих зна-
чень. Такі відображення названо квазіар-
ними.
У роботі [2] визначено відношення
логічного наслідку та досліджено семан-
тичні властивості КНЛ часткових однозна-
чних, тотальних неоднозначних і частко-
вих неоднозначних квазіарних предикатів
на пропозиційному, реномінативному та
кванторному рівнях. У різних семантиках
ці відношення мають різні властивості, зо-
крема, в класичній логіці усі вони збіга-
ються. Такі відношення логічного наслідку
індукують відповідні відношення еквіва-
лентності, вони поширюються на множини
формул.
Метою даної роботи є вивчення
спеціальних відношень логічного наслідку
для першопорядкових КНЛ квазіарних
предикатів. Для таких логік кванторного
рівня запропоновано і досліджено в різних
семантиках Х–Y-означені відношення логіч-
ного наслідку для пар та множин формул.
Поняття Х–Y-означеного відношення логіч-
ного наслідку для логік часткових однозна-
чних квазіарних предикатів введене в [5],
на цій основі для таких логік побудоване
числення секвенційного типу. В даній ро-
боті різні Х–Y-означені відношення логіч-
ного наслідку визначаються як для частко-
вих однозначних, так і для тотальних не-
однозначних та часткових неоднозначних
предикатів. Отримано низку властивостей
цих відношень, зокрема, властивості елімі-
нації кванторів. Такі властивості ляжуть в
основу побудови відповідних секвенційних
числень для КНЛ часткових однозначних,
тотальних неоднозначних та часткових не-
однозначних предикатів.
Поняття, які тут не визначаються,
тлумачимо в сенсі робіт [2, 4, 5].
Для полегшення читання наведемо
небхідні для подальшого викладу поняття
та визначення.
© C.С. Шкільняк, 2011
ISSN 1727-4907. Проблеми програмування. 2011. № 4
Теоретичні та методологічні основи програмування
37
1. Основні поняття та визначення
Під предикатом на множині D буде-
мо розуміти довільну (часткову неодно
значну, взагалі кажучи) функцію вигляду
P : D → {T, F}.
Предикати можуть бути однознач-
ними чи неоднозначними, тотальними чи
частковими. Логіка тотальних однознач-
них предикатів – це класична логіка. Логі-
ки однозначних часткових предикатів – це
логіки з неокласичною семантикою, логіки
тотальних неоднозначних предикатів – ло-
гіки з пересиченою семантикою. Логіки
часткових неоднозначних предикатів при-
родно назвати логіками із загальною се-
мантикою.
Областю істинності та областю хи-
бності предиката Р на 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) = ∅. Якщо Р – тотальний, то
T(P)∪F(P) = D.
Предикат P на D тотально істинний,
якщо T(P) = D.
Предикат P на D неспростовний,
або частково істинний, якщо F(P) = ∅.
Будемо писати P(d)↓, якщо значен-
ня P(d) визначене, тобто d∈T(P)∪F(P).
Пишемо P(d)↑, якщо P(d) невизна-
чене, тобто d∉T(P)∪F(P).
V-іменною множиною (V-ІМ) над A
назвемо [4] довільну однозначну функцію
δ : V→ A. V-ІМ будемо подавати у вигляді
[v1aa1,...,vnaan,...]; тут vі∈V, aі∈A, vі ≠ vj
при і ≠ j. Множину всіх V-ІМ над A позна-
чатимемо VA.
Для V-ІМ вводимо [4] функції
im(δ) = {v∈V | vaa∈δ для деякого a∈A} та
δ ||Х = {vaa∈δ | v∈X⊆V}; вводимо операції
накладки δ1∇δ2 = δ2∪ (δ1 ||(V \ im(δ2))) та ре-
номінації r 1
1
,...,
,...,
n
n
v v
x x (δ) = [v1aδ(x1),...,vnaδ(xn)] ∪
∪ (δ ||(V\{v1,...,vn})).
Замість δ║(V\{х}) писатимемо δ║-х.
Предикат вигляду P : VA→{T, F}
назвемо V-квазіарним предикатом на А.
Множину V-квазіарних предикатів
на A позначимо PrА.
Ім'я x∈V строго неістотне для V-ква-
зіарного предиката P, якщо для довільних
d∈VA, a∈A маємо P(d∇xaa) = P(d║-х).
Предикат P : VA→{T, F} монотонний,
якщо з умови d ⊆ d' випливає P(d) ⊆ P(d').
Для однозначних часткових преди-
катів монотонність називають еквітоністю.
Еквітоність предиката означає, що прийня-
те ним значення зберігається при розши-
ренні даних. Це можна трактувати як збе-
реження "інформативності" предиката при
збільшенні "інформативності" вхідних да-
них. Водночас для тотальних монотонних
предикатів при розширенні вхідних даних
"інформативність" може тільки зменшува-
тися, тому поняття еквітонності (монотон-
ності) не зовсім адекватне для тотальних
неоднозначних предикатів. Для таких пре-
дикатів адекватним є дуальне поняття ан-
титонності. У випадку предикатів антитон-
ність також названа [2] антиеквітонністю.
Предикат P : VA→{T, F} антитонний,
якщо з умови d ⊆ d' випливає P(d) ⊇ P(d').
В класі однозначних предикатів по-
няття антитонності малозмістовне.
Універсальні методи побудови пре-
дикатів визначають композиції, вони вис-
тупають ядром логіки певного типу. Згідно
композиційно-номінативного підходу [3],
композиції уточнюємо як функції (опера-
ції) над іменованими предикатами.
Hа пропозиційному рівні композиції
називають логiчними зв’язками.
Базовими пропозиційними компози-
ціями вважатимемо [4] ¬ та ∨.
Композиції →, &, ↔ є похідними,
вони виражаються через ¬ та ∨.
Предикати ¬(P) та ∨(P, Q) будемо
позначати ¬P, P∨Q. Задаємо їх так:
T(¬P) = F(P);
F(¬P) = T(P).
T(P∨Q) = T(P)∪T(Q);
F(P∨Q) = F(P)∩F(Q).
Базовими композиціями реноміна-
тивного рівня є [4] ¬, ∨ та реномінація
R v
x : PrА → PrА.
Предикат R v
x (P) визначаємо так:
T(R v
x (P)) = r v
x (T(P));
Теоретичні та методологічні основи програмування
38
F(R v
x (P)) = r v
x (F(P)).
Базовими композиціями кванторно-
го рівня є ¬, ∨, R v
x , ∃x.
Композиція ∀x є похідною: для ко-
жного предиката Р маємо ¬∀хР = ¬∃х¬Р.
Предикат ∃xP визначаємо так:
T(∃xP) = {d∈VA | T∈Р(d∇xaa) для
деякого a∈A}.
F(∃xP) = {d∈VA | F∈Р(d∇xaa) для
всіх a∈A}.
Композиції ¬, ∨, R v
x , ∃x зберігають
[2, 4] еквітонність та антитонність V-квазі-
арних предикатів.
Семантичними моделями компози-
ційно-номінативних логік кванторного рі-
вня (КНЛК) є [4] композиційні системи
квазіарних предикатів (VA, PrA, C), де C
задається множиною базових композицій
{¬, ∨, R v
x , ∃x}. Кожна така композиційна
система задає дві алгебри: неокласичну
алгебраїчну систему (АС) даних (A, PrA) та
композиційну алгебру предикатів (PrA, C).
Мова логіки індукується [4] відповідними
інтенсіональними моделями (рівнями роз-
гляду). Побудова композиційної системи
фактично визначає мову логіки: терми
композиційної алгебри предикатів тракту-
ємо як формули мови.
Опишемо мову КНЛК. Алфавiт мо-
ви: символи базових композицій
¬, ∨, ,v
xR ∃x, множина Ps предикатних си-
мволів (сигнатура мови), множина V пред-
метних імен.
Дамо визначення множини Fr фор-
мул мови КНЛК.
1. Кожний предикатний символ
(ПС) є формулою. Такі формули атомарні.
2. Якшо Φ та Ψ – формули, то ¬Φ,
∨ФΨ, v
xR Φ , ∃xΦ – формули.
Інтерпретуємо мову КНЛК на ком-
позиційних системах квазіарних предика-
тів кванторного рівня (VA, PrA, C). Відо-
браження інтерпретації формул J : Fr→PrA
визначається, згідно побудови формул із
простіших за допомогою символів базових
композицій, на основі тотального однозна-
чного відображення I : Ps → PrA, яке по-
значає символами Рs базові предикати:
– J(р) = I(p) для кожного р∈Ps;
– J(¬Φ) = ¬(J(Φ));
– J(∨ΦΨ) = ∨(J(Φ), J(Ψ));
– J ( )v
xR Φ = R v
x (J(Φ));
– J(∃xΦ) = ∃x(J(Φ)).
Відображення I прив'язує АС даних
(А, Pr) до мови КНЛК. Отримуємо АС з
доданою сигнатурою вигляду ((A, PrA), I),
яку позначаємо (A, I). Такі АС є інтегрова-
ними семантичними моделями, які пов'я-
зують мову КНЛК із АС даних. Будемо їх
називати моделями мови.
Предикат J(Φ) – значення формули
Φ при інтерпретації на A = (A, I), – позна-
чаємо ΦA.
Формула Φ частково істинна при ін-
терпретації на A = (A, I), або A-неспро-
стовна, якщо ΦA – частково істинний (не-
спростовний) предикат.
Це позначаємо A |= Φ.
Формула Φ частково iстинна, або
неспростовна, якщо Φ частково iстинна
при кожній інтерпретації.
Це позначаємо |= Φ.
Аналогічно визначаємо [4] тотально
істинні при інтерпретації на A та тотально
істинні формули.
Ім'я x∈V строго неістотне для фор-
мули Φ, якщо для кожної A = (A, I) ім'я x
строго неістотне для предиката ΦA.
Для виконання еквівалентних пере-
творень формул мови КНЛК необхідна [4]
наявність нескінченної множини тотально
(строго) неістотних імен.
Для кожного р∈Ps множину синте-
тично строго неістотних предметних імен
задамо за допомогою тотальної функції
ν : Ps→2V. Така функція природним чином
[4] продовжується до ν : Fr→2V. Тотальна
строго неістотність імені x означає, що
( )
p Ps
x p
∈
∈ νI .
АС B = (A, IB) назвемо [2] дуальною
до A = (A, IA), якщо для кожного Φ∈Ps ма-
ємо ( ) ( )B AT FΦ = Φ та ( ) ( )B AF TΦ = Φ .
Тоді A = (A, IA) дуальна до B = (A, IB).
Якщо A = (A, IA) – АС з частковими
однозначними предикатами, то дуальна
Теоретичні та методологічні основи програмування
39
B = (A, IB) – АС з тотальними неоднознач-
ними предикатами, та навпаки.
Нехай A = (A, IA) та B = (A, IB) дуа-
льні. Тоді [2] для кожної формули Φ:
1) ( ) ( )B AT FΦ = Φ та ( ) ( )B AF TΦ = Φ ;
2) ΦA еквітонний ⇒ ΦB антитонний та
ΦA антитонний ⇒ ΦB еквітонний.
Таким чином, неокласична семан-
тика та пересичена семантика дуальні. Це
означає, що ΦA неспростовний на АС A із
частковими однозначними предикатами
(неокласична семантика) ⇔ ΦB тотально
істинний на дуальній АС B із тотальними
неоднозначними предикатами (пересичена
семантика).
2. Х–Y-означені відношення
логічного наслідку
У випадку формалізації за допомо-
гою секвенційних числень відношень |=T ,
|=F , |=TF в різних семантиках, а також від-
ношення |=Cl для логік нееквітонних пре-
дикатів (дуально: відношення |=Cm для ло-
гік неантитонних предикатів) необхідно
врахувати ту обставину, що значення пре-
диката P(d) може бути різним залежно від
того, входить чи не входить до d компоне-
нта з певним предметним іменем. Ця об-
ставина має принциповий характер, вона
веде (див. [2]) до неможливості елімінації
кванторів у випадках відношень |=T , |=F ,
|=TF, а також відношення |=Cl для логік не-
еквітонних предикатів (відношення |=Cm
для логік неантитонних предикатів).
Таким чином, при інтерпретаціях
формул на моделях мови необхідно явно
виділяти множини означених та неозначе-
них імен для даних, до яких застосовують-
ся предикати. Тому в [5] введено поняття
Х–Y-означених іменних множин, Х–Y-озна-
чених областей істинності й хибності ква-
зіарного предиката. Для логік однозначних
часткових предикатів в [5] введено понят-
тя Х–Y-означених відношень логічного на-
слідку (для випадку Cl-відношень).
Х–Y-означені іменні множини.
Множини Х, Y називають диз’юнктними,
якщо Х ∩ Y = ∅.
Для довільних диз’юнктних Х, Y ⊆ V
множину Х–Y-означених V-ІМ задамо так:
V, Х–YA = {d∈VA | Х ⊆ im(d) та
Y ∩ im(d) = ∅}.
Х–Y-означеність полягає в наступ-
ному: імена із Х мають значення, імена із Y
– не мають значення.
Якщо Y = ∅, то отримуємо множину
Х-означених V-ІМ:
V, ХA = {d∈VA | Х ⊆ im(d)}.
Для випадку Х = ∅ отримуємо мно-
жину Y-неозначених V-ІМ:
V, –YA = {d∈VA | Y ∩ im(d) = ∅}.
Із визначень отримуємо такі співвід-
ношення:
V, Х–YA =
V, ХA ∩
V, –YA;
V, Х∪ZA =
V, ХA ∩
V, ZA;
V, –Y∪ZA =
V, –YA ∩
V, –ZA.
Твердження 1. Нехай Z, W, U ⊆ V –
диз’юнктні множини предметних імен.
Тоді , , ( \ )V W U V W Y U Z Y
Y Z
A A− ∪ − ∪
⊆
= U
Зокрема, для диз’юнктних Z, W ⊆ V
маємо , , \V W V W Y Z Y
Y Z
A A∪ −
⊆
= U ; для довіль-
ної Z ⊆ V маємо , \V V Y Z Y
Y Z
A A−
⊆
= U .
Х–Y-означені області істинності й
хибності. Для довільних диз’юнктних
Х, Y ⊆ V визначимо Х–Y-означені області
істинності й хибності предиката Р:
TХ–Y (P) = {d∈VA | P(d) = T та Х ⊆ im(d),
Y ∩ im(d) = ∅} = {d∈V, Х–YA | P(d) = T}.
FХ–Y (P) = {d∈VA | P(d) = F та Х ⊆ im(d),
Y ∩ im(d) = ∅} = {d∈V, Х–YA | P(d) = F}.
Таким чином, беремо до уваги тільки
ті елементи областей істинності та хибнос-
ті предиката, в яких імена із Х мають зна-
чення, імена із Y не мають значення.
Якщо Y = ∅, то маємо Х-означені
області істинності й хибності предиката Р:
TХ (P) = {d∈VA | P(d) = T та Х ⊆ im(d)} =
= {d∈V, ХA | P(d) = T}
FХ (P) = {d∈VA | P(d) = F та Х ⊆ im(d)} =
= {d∈V, ХA | P(d) = F}.
Якщо Х = ∅, то маємо Y-неозначені
області істинності й хибності предиката Р:
Теоретичні та методологічні основи програмування
40
T–Y (P) = {d∈VA | P(d) = T та
Y ∩ im(d) = ∅} = {d∈V, –YA | P(d) = T};
F–Y (P) = {d∈VA | P(d) = F та
Y ∩ im(d) = ∅} = {d∈V, –YA | P(d) = F}.
Твердження 2. Маємо
TХ–Y (P) ⊆ TХ (P) ⊆ T(P) та
FХ–Y (P) ⊆ FХ (P) ⊆ F(P);
TХ–Y (P) ⊆ T–Y (P) ⊆ T(P) та
FХ–Y (P) ⊆ F–Y (P) ⊆ F(P).
Теорема 1. Для логік квазіарних
предикатів справджуються співвідношення:
TY–Z ( x
yR (Р)) ⊆ TY–Z (∃x(Р))
при умові y∈Y (TR∃)
FY–Z (∃x(Р)) ⊆ FY–Z ( x
yR (Р))
при умові y∈Y (FR∃)
TY–Z (∀x(Р)) ⊆ TY–Z ( x
yR (Р))
при умові y∈Y (TR∀)
FY–Z ( x
yR (Р)) ⊆ FY–Z (∀x(Р))
при умові y∈Y (FR∀)
Доведення. Нехай d∈TY–Z ( ( )x
yR P ) та
y∈Y, тоді Y ⊆ im(d), Z ∩ im(d) = ∅ та
d∈T ( ( )x
yR P ), звідки маємо y∈im(d) та
d∇xad(y)∈T(P). Згідно y∈im(d) для деяко-
го a∈A маємо d(y)↓a. Отже, d∇xaa∈T(P)
для деякого a∈A та y∈Y ⊆ im(d), звідки
d∈T(∃x(P)) та y∈Y ⊆ im(d). Враховуючи
Z ∩ im(d) = ∅, тоді d∈TY–Z (∃x(Р)). Отже,
при y∈Y маємо TY–Z ( ( )x
yR P ) ⊆ TY–Z (∃x(Р)).
Нехай d∈FY–Z (∃x(Р)) та y∈Y, тоді
Y ⊆ im(d), Z ∩ im(d) = ∅ та d∇xab∈F(P)
для всіх b∈A. Згідно y∈im(d) маємо d(y)↓a
для деякого a∈A, тоді d∇xad(y)∈F(P).
Звідси d∈F ( ( )x
yR P ) та y∈Y ⊆ im(d). Врахо-
вуючи Z ∩ im(d) = ∅, тоді d∈FY–Z ( ( )x
yR P ).
Таким чином, при умові y∈Y отримуємо
FY–Z (∃x(Р)) ⊆ FY–Z ( ( )x
yR P ).
Нехай d∈TY–Z (∀x(Р)) та y∈Y, тоді
Y ⊆ im(d), Z ∩ im(d) = ∅ та d∇xab∈T(P)
для всіх b∈A. Згідно y∈im(d) маємо d(y)↓a
для деякого a∈A, тоді d∇xad(y)∈T(P).
Отже, d∈T ( ( )x
yR P ) та y∈Y ⊆ im(d). Врахо-
вуючи Z ∩ im(d) = ∅, тоді d∈TY–Z ( ( )x
yR P ).
Таким чином, при умові y∈Y отримуємо
TY–Z (∀x(Р)) ⊆ TY–Z ( ( )x
yR P ).
Нехай d∈FY–Z ( ( )x
yR P ) та y∈Y, тоді
Y ⊆ im(d), Z ∩ im(d) = ∅ та d∈F ( ( )x
yR P ),
звідки y∈im(d) та d∇xad(y)∈F(P). Згідно
y∈im(d) маємо d(y)↓a для деякого a∈A. Та-
ким чином, d∇xaa∈F(P) для деякого a∈A
та y∈Y ⊆ im(d), звідки d∈F(∀x(P)) та
y∈Y ⊆ im(d). Враховуючи Z ∩ im(d) = ∅, то-
ді d∈FY–Z (∀x(Р)). Отже, при умові y∈Y ма-
ємо FY–Z ( ( )x
yR P ) ⊆ FY–Z (∀x(Р)).
Х–Y-означені відношення логічного
наслідку. Для довільних диз’юнктних
Х, Y ⊆ V визначимо Х–Y-означені відношен-
ня наслідку для двох формул при фіксова-
ній моделі мови A.
Φ A, Х–Y |=Cl Ψ, якщо
TХ–Y (ΦA)∩FХ–Y (ΨA) = ∅;
Φ A, Х–Y |=Cm Ψ, якщо
TХ–Y (ΦA)∪FХ–Y (ΨA) = V, Х–YA;
Φ A, Х–Y |=T Ψ, якщо
TХ–Y (ΦA) ⊆ TХ–Y (ΨA);
Φ A, Х–Y |=F Ψ, якщо
FХ–Y (ΨA) ⊆ FХ–Y (ΦA);
Φ A, Х–Y |=TF Ψ, якщо
TХ–Y (ΦA) ⊆ TХ–Y (ΨA) та
FХ–Y (ΨA) ⊆ FХ–Y (ΦA).
Якщо Y = ∅, то отримуємо Х-означені
відношення наслідку:
Φ A, Х |=Cl Ψ, якщо
TХ (ΦA)∩FХ (ΨA) = ∅;
Φ A, Х |=Cm Ψ, якщо
TХ (ΦA)∪FХ (ΨA) = V, ХA;
Φ A, Х |=T Ψ, якщо TХ (ΦA) ⊆ TХ (ΨA);
Φ A, Х |=F Ψ, якщо FХ (ΨA) ⊆ FХ (ΦA);
Φ A, Х |=TF Ψ, якщо TХ (ΦA) ⊆ TХ (ΨA)
та FХ (ΨA) ⊆ FХ (ΦA).
Для випадку Х = ∅ отримуємо Y-нео-
значені відношення наслідку:
Φ A, –Y |=Cl Ψ, якщо
T–Y (ΦA)∩F–Y (ΨA) = ∅;
Φ A, –Y |=Cm Ψ, якщо
T–Y (ΦA)∪F–Y (ΨA) = V, –YA;
Φ A, –Y |=T Ψ, якщо
T–Y (ΦA) ⊆ T–Y (ΨA);
Φ A, –Y |=F Ψ, якщо
Теоретичні та методологічні основи програмування
41
F–Y (ΨA) ⊆ F–Y (ΦA);
Φ A, –Y |=TF Ψ, якщо
T–Y (ΦA) ⊆ T–Y (ΨA) та
F–Y (ΨA) ⊆ F–Y (ΦA).
У випадку Х = Y = ∅ мaємо відомі
[5] відношення A|=Cl, A|=Cm, A|=T, A|=F, A|=TF .
Із визначень випливає, що введені
відношення рефлексивні й транзитивні.
Твердження 3. Для введених відно-
шень маємо:
Φ A|=∗ Ψ ⇒ Φ A, Х |=∗ Ψ ⇒ Φ A, Х–Y |=∗ Ψ
та Φ A|=∗ Ψ ⇒ Φ A, –Y |=∗ Ψ ⇒ Φ A, Х–Y |=∗ Ψ.
Тут ∗ – одне з Cl, Cm, T, F, TF.
Для Cl-наслідків наше твердження
випливає з твердження 2.
Розглянемо Cm-наслідки. Нехай
Φ A|=Cm Ψ, тоді T(ΦA)∪F(ΨA) = VA. Пока-
жемо, що тоді TХ (ΦA)∪FХ (ΨA) = V, ХA. Як-
що це не так, то для деякого d∈V, ХA маємо
d∉TХ (ΦA) та d∉FХ (ΨA). Але Х ⊆ im(d), тому
d∉T(ΦA) та d∉F(ΨA), що суперечить
T(ΦA)∪F(ΨA) = VA. Тепер покажемо
Φ A|=Cm Ψ ⇒ Φ A, –Y |=Cm Ψ. Якщо це не так,
то T(ΦA)∪F(ΨA) = VA, проте для деякого
d∈V, –YA маємо d∉T–Y (ΦA) та d∉F–Y(ΨA).
Але Y ∩ im(d) = ∅, тому d∉T(ΦA) та
d∉F(ΨA), що суперечить T(ΦA)∪F(ΨA) = VA.
Аналогічно доводимо Φ A, Х |=Cm Ψ ⇒
⇒ Φ A, Х–Y |=Cm Ψ, Φ A, –Y |= Ψ ⇒ Φ A, Х–Y |=Cm Ψ.
Розглянемо T-наслідки. Нехай
Φ A|=T Ψ, тоді T(ΦA) ⊆ T(ΨA). Покажемо,
що тоді TХ (ΦA) ⊆ TХ (ΨA). Якщо це не так,
то для деякого d∈V, ХA маємо d∈TХ (ΦA) та
d∉TХ (ΨA). Але Х ⊆ im(d), тому d∈T(ΦA) та
d∉T(ΨA), що суперечить T(ΦA) ⊆ T(ΨA).
Тепер покажемо Φ A|=T Ψ ⇒ Φ A, –Y |=T Ψ.
Якщо це не так, то T(ΦA) ⊆ T(ΨA), проте
для деякого d∈V, –YA маємо d∈T–Y (ΦA) та
d∉T–Y (ΨA). Але Y ∩ im(d) = ∅, тому d∈T(ΦA)
та d∉F(ΨA), що суперечить T(ΦA) ⊆ T(ΨA).
Аналогічно доводимо Φ A, Х |=T Ψ ⇒
⇒ Φ A, Х–Y |=T Ψ, Φ A, –Y |=T Ψ ⇒ Φ A, Х–Y |= T Ψ.
Подібним чином розглядаємо випа-
дки F-наслідків та TF-наслідків.
Із теореми 1 для відповідних семан-
тик та наслідків отримуємо:
Твердження 4. При умові z∈X маємо
( )x
zR Φ A, Х–Y |=∗ ∃xΦ та ∀xΦ A, Х–Y |=∗ ( )x
zR Φ .
Тут ∗ – одне з Cl, Cm, T, F, TF.
Тут враховуємо, що для однозначних
предикатів TХ–Y (∃xΦA) ∩ FХ–Y (∃xΦA) = ∅ та
TХ–Y (∀xΦA) ∩ FХ–Y (∀xΦA) = ∅, для тоталь-
них – TХ–Y ( ( )x
zR Φ A) ∪ FХ–Y ( ( )x
zR Φ A) = VA.
Поширимо поняття Х–Y-означеного
логічного наслідку при фіксованій моделі
мови A на довільні множини формул.
Δ є Х–Y-означеним Cl-логічним нас-
лідком Γ в АС A (позн. Γ A, Х–Y |=Cl Δ), якщо
( ) ( )X Y A X Y AT F− −
Φ∈Γ Ψ∈Δ
Φ ∩ Ψ =∅I I .
Δ є Х–Y-означеним Cm-логічним нас-
лідком Γ в АС A (позн. Γ A, Х–Y |=Cm Δ), якщо
, ( ) ( ) V X Y
X Y A X Y AF T A−
− −
Φ∈Γ Ψ∈Δ
Φ ∪ Ψ =U U .
Δ є Х–Y-означеним T-логічним нас-
лідком Γ в АС A (позн. Γ A, Х–Y |=T Δ), якщо
( ) ( )X Y A X Y AT T− −
Φ∈Γ Ψ∈Δ
Φ ⊆ ΨI U .
Δ є Х–Y-означеним F-логічним нас-
лідком Γ в АС A (позн. Γ A, Х–Y |=F Δ), якщо
( ) ( )X Y A X Y AF F− −
Ψ∈Δ Φ∈Γ
Ψ ⊆ ΦI U .
Δ є Х–Y-означеним TF-логічним нас-
лідком Γ в АС A (позн. Γ A, Х–Y |=TF Δ), якщо
( ) ( )X Y A X Y AT T− −
Φ∈Γ Ψ∈Δ
Φ ⊆ ΨI U та
( ) ( )X Y A X Y AF F− −
Ψ∈Δ Φ∈Γ
Ψ ⊆ ΦI U .
Аналогічним чином вводимо Х-оз-
начені та Y-неозначені відношення наслід-
ку для множин формул при фіксованій мо-
делі мови A.
Γ A, Х |=Cl Δ, якщо
( ) ( )X A X AT F
Φ∈Γ Ψ∈Δ
Φ ∩ Ψ =∅I I .
Γ A, Х |=Cm Δ, якщо
, ( ) ( ) V X
X A X AF T A
Φ∈Γ Ψ∈Δ
Φ ∪ Ψ =U U .
Γ A, Х |=T Δ, якщо
( ) ( )X A X AT T
Φ∈Γ Ψ∈Δ
Φ ⊆ ΨI U .
Γ A, Х |=F Δ, якщо
( ) ( )X A X AF F
Ψ∈Δ Φ∈Γ
Ψ ⊆ ΦI U .
Γ A, Х |=TF Δ, якщо
Теоретичні та методологічні основи програмування
42
( ) ( )X A X AT T
Φ∈Γ Ψ∈Δ
Φ ⊆ ΨI U та
( ) ( )X A X AF F
Ψ∈Δ Φ∈Γ
Ψ ⊆ ΦI U .
Γ A, –Y |=Cl Δ, якщо
( ) ( )Y A Y AT F− −
Φ∈Γ Ψ∈Δ
Φ ∩ Ψ =∅I I .
Γ A, –Y |=Cm Δ, якщо
, ( ) ( ) V Y
Y A Y AF T A−
− −
Φ∈Γ Ψ∈Δ
Φ ∪ Ψ =U U .
Γ A, –Y |=T Δ, якщо
( ) ( )Y A Y AT T− −
Φ∈Γ Ψ∈Δ
Φ ⊆ ΨI U .
Γ A, –Y |=F Δ, якщо
( ) ( )Y A Y AF F− −
Ψ∈Δ Φ∈Γ
Ψ ⊆ ΦI U .
Γ A, –Y |=TF Δ, якщо
( ) ( )Y A Y AT T− −
Φ∈Γ Ψ∈Δ
Φ ⊆ ΨI U та
( ) ( )Y A Y AF F− −
Ψ∈Δ Φ∈Γ
Ψ ⊆ ΦI U .
У випадку Х = Y = ∅ отримуємо від-
ношення A |=Cl, A |=Cm, A,|=T, A |=F, A |=TF .
Твердження 5. Відношення наслід-
ку A, Х–Y |=∗ , A, Х |=∗ , A, –Y |=∗ рефлексивні, про-
те нетранзитивні.
Твердження 6. Для введених відно-
шень маємо:
Γ A|=∗ Δ ⇒ Γ A, Х |=∗ Δ ⇒ Γ A, Х–Y |=∗ Δ
та Γ A |=∗ Δ ⇒ Γ A, –Y |=∗ Δ ⇒ Γ A, Х–Y |=∗ Δ.
Тут ∗ – одне з Cl, Cm, T, F, TF.
Твердження 6 узагальнює твер-
дження 3 і доводиться подібним чином.
Якщо z тотально строго неістотне та
z∉nm(Φ), то для довільних A, d∈VA та a∈A
маємо ΦA(d∇xaa) = ΦA(d║-х). Звідси отри-
муємо
Твердження 7. Нехай z тотально
строго неістотне та z∉nm(Γ∪Δ). Тоді має-
мо:
1) Γ A, {z}∪Х–Y |=∗ Δ ⇔ Γ A, Х–Y |=∗ Δ;
2) Γ {z}∪Х–Y |=∗ Δ ⇔ Γ Х–Y |=∗ Δ.
Тут ∗ – одне з Cl, Cm, T, F, TF.
Теорема 2. Нехай Z, W, U ⊆ V – ди-
з’юнктні множини предметних імен. Тоді
Γ A, W–U |=∗ Δ ⇔ для кожної Y ⊆ Z
маємо Γ A, W∪Y–U∪(Z\Y) |=∗ Δ.
Тут ∗ – одне з Cl, Cm, T, F, TF.
Доведення. Для довільних Φ∈Γ,
Ψ∈Δ та диз’юнктних Z, W, U ⊆ V для кож-
ної Y ⊆ Z маємо TW∪Y–U∪(Z\Y) (ΦA) ⊆ TW–U (ΦA)
та FW∪Y–U∪(Z\Y) (ΨA) ⊆ FW–U (ΨA).
Доведемо для Cl-наслідків. Із наве-
дених вище включень маємо: із умови
Γ A, W–U |=Cl Δ випливає, що для кожної Y ⊆ Z
Γ A, W∪Y–U∪(Z\Y) |=Cl Δ. Покажемо зворотне.
Нехай Γ A, W∪Y–U∪(Z\Y) |=Cl Δ для кожної
Y ⊆ Z, проте Γ A, W–U |≠Cl Δ. Останнє означає,
що TW–U (ΦA) ∩ FW–U (ΨA) ≠ ∅ для деяких
Φ∈Γ та Ψ∈Δ. Звідси існує d∈V, W–UA таке:
d∈TW–U (ΦA) та d∈FW–U (ΨA). Нехай
Y = Z ∩ im(d), тоді d∈V, W∪Y–U∪(Z\Y)A, звідки
d∈TW∪Y–U∪(Z\Y) (ΦA) та d∈FW∪Y– U∪(Z\Y) (ΨA) для
деяких Φ∈Γ і Ψ∈Δ, тому Γ A, W∪Y–U∪(Z\Y) |≠Cl Δ.
Отримали суперечність. Отже, Γ A, W–U |≠Cl Δ
невірно, тому Γ A, W–U |=Cl Δ.
Доведемо для Cm-наслідків. Нехай
Γ A, W–U |=Cm Δ; покажемо, що для кожної
Y ⊆ Z тоді Γ A, W∪Y–U∪(Z\Y) |=Cm Δ. Маємо
, ( ) ( ) V W U
W U A W U AF T A−
− −
Φ∈Γ Ψ∈Δ
Φ ∪ Ψ =U U .
Припустимо супротивне: для деяких Y ⊆ Z
та d∈V, W∪Y–U∪(Z\Y)A маємо, що d∉
( \ ) ( \ )( ) ( ).W Y U Z Y A W Y U Z Y AF T∪ − ∪ ∪ − ∪
Φ∈Γ Ψ∈Δ
Φ ∪ ΨU U
Але ж W∪Y ⊆ im(d), U∪(Z\Y) ∩ im(d) = ∅,
тому неможливо ( )Ad F
Φ∈Γ
∈ ΦU і неможли-
во ( )Ad T
Ψ∈Δ
∈ ΨU . Згідно твердження 2, зві-
дси ( ) ( )W U A W U Ad F T− −
Φ∈Γ Ψ∈Δ
∉ Φ ∪ ΨU U . Це
суперечить умові Γ A, W–U |=Cm Δ.
Нехай Γ A, W∪Y–U∪(Z\Y) |=Cm Δ для кож-
ної Y ⊆ Z; покажемо, що тоді Γ A, W–U |=Cm Δ.
Нехай супротивне, тоді для кожної Y ⊆ Z
( \ ) ( \ )( ) ( )W Y U Z Y A W Y U Z Y AF T∪ − ∪ ∪ − ∪
Φ∈Γ Ψ∈Δ
Φ ∪ ΨU U
, ( \ ) ,V W Y U Z Y A∪ − ∪= проте існує d∈V, W–UA :
( ) ( )W U A W U Ad F T− −
Φ∈Γ Ψ∈Δ
∉ Φ ∪ ΨU U . Нехай
Y = Z ∩ im(d), тоді d∈V, W∪Y–U∪(Z\Y)A, тому d∉
( \ ) ( \ )( ) ( ).W Y U Z Y A W Y U Z Y AF T∪ − ∪ ∪ − ∪
Φ∈Γ Ψ∈Δ
Φ ∪ ΨU U
Отримали суперечність.
Доведемо для T-наслідків. Нехай
Γ A, W–U |=T Δ; покажемо, що для кожної
Y ⊆ Z тоді Γ A, W∪Y–U∪(Z\Y) |=T Δ. Нехай супро-
тивне: для деяких Y ⊆ Z та d∈V, W∪Y–U∪(Z\Y)A
Теоретичні та методологічні основи програмування
43
маємо ( \ ) ( )W Y U Z Y Ad T ∪ − ∪
Φ∈Γ
∈ ΦI та
( \ ) ( )W Y U Z Y Ad T ∪ − ∪
Ψ∈Δ
∉ ΨU . Згідно тверджен-
ня 2, із першого маємо ( )W U Ad T −
Φ∈Γ
∈ ΦI .
Але W∪Y ⊆ im(d), U∪(Z\Y) ∩ im(d) = ∅, то-
му із другого маємо ( )Ad T
Ψ∈Δ
∉ ΨU , звідки
( )W U Ad T −
Ψ∈Δ
∉ ΨU . Таким чином, невірно
( ) ( )W U A W U AT T− −
Φ∈Γ Ψ∈Δ
Φ ⊆ ΨI U , тому маємо
Γ A, W–U |≠T Δ. Отримали суперечність.
Нехай Γ A, W∪Y–U∪(Z\Y) |=T Δ для кожної
Y ⊆ Z; покажемо, що тоді Γ A, W–U |=T Δ. Не-
хай супротивне, тоді для кожної Y ⊆ Z
( \ ) ( \ )( ) ( ),W Y U Z Y A W Y U Z Y AT T∪ − ∪ ∪ − ∪
Φ∈Γ Ψ∈Δ
Φ ⊆ ΨI U
проте існує d∈V, W–UA: ( )W U Ad T −
Φ∈Γ
∈ ΦI та
( )W U Ad T −
Ψ∈Δ
∉ ΨU . Згідно твердження 2, із
другого маємо ( \ ) ( )W Y U Z Y Ad T ∪ − ∪
Ψ∈Δ
∉ ΨU .
Нехай Y = Z ∩ im(d), тоді d∈V, W∪Y–U∪(Z\Y)A,
тому з першого ( \ ) ( )W Y U Z Y Ad T ∪ − ∪
Φ∈Γ
∈ ΦI .
Це суперечить умові Γ A, W∪Y–U∪(Z\Y) |=T Δ.
Аналогічно доводимо твердження
теореми для F-наслідків та TF-наслідків.
При умовах U = ∅ та W = U = ∅ від-
повідно отримуємо такі наслідки.
Наслідок 1. Нехай Z, W ⊆ V – ди-
з’юнктні множини предметних імен. Тоді:
Γ A, W |=∗ Δ ⇔ Γ A, W∪Y–Z\Y |=∗ Δ для ко-
жної Y ⊆ Z.
Наслідок 2. Для довільної Z ⊆ V ма-
ємо: Γ A |=∗ Δ ⇔ Γ A, Y–Z\Y |=∗ Δ для кожної
Y ⊆ Z.
Тут ∗ – одне з Cl, Cm, T, F, TF.
Відповідні наслідки теореми 2 отри-
муємо у випадку відношень логічного нас-
лідку для двох формул.
Твердження 8. Для логіки еквітон-
них предикатів в неокласичній семантиці
при умові z∈X та y∈Y маємо:
1) ,
, ( ),x u
y vR Φ Γ A, Х–Y |=T
,
, ( ),x u
z vR Φ Δ та
,
, ( ),x u
y vR¬ Φ Γ A, Х–Y |=T
,
, ( ),x u
z vR¬ Φ Δ;
2) ,
, ( ),x u
z vR Φ Γ A, Х–Y |=F
,
, ( ),x u
y vR Φ Δ та
,
, ( ),x u
z vR¬ Φ Γ A, Х–Y |=F
,
, ( ),x u
y vR¬ Φ Δ.
Справді, для еквітонних предикатів
при z∈X, y∈Y маємо:
FХ–Y
,
,( ( ) )x u
y v AR Φ ⊆ FХ–Y
,
,( ( ) );x u
z v AR Φ
TХ–Y
,
,( ( ) )x u
y v AR Φ ⊆ TХ–Y
,
,( ( ) ).x u
z v AR Φ
Звідси й випливає твердження 8.
Аналогічне твердження формулює-
ться для дуального випадку логіки анти-
тонних предикатів в пересиченій семантиці.
Для формул вигляду v
xR Φ можна
ввести [5] поняття U-неозначуваної форми.
Тут U ⊆ V – довільна множина пред-
метних імен, її трактуємо як множину не-
означених імен. Це означає, що при інтер-
претаціях усі імена U не мають значення.
Нехай 1 1 1
1 1 1
,... , ,... , ,...
,... , ,... , ,...
k n m
k n m
r r x x u u
s s y y v vR Φ така: усі
r1,…, rk, s,…, sk, y1,…, yn ∈U, {x1,…, xn}∩U = ∅,
{v1,…, vm}∩U = ∅.
U-неозначувана форма формули
1 1 1
1 1 1
,... , ,... , ,...
,... , ,... , ,...
k n m
k n m
r r x x u u
s s y y v vR Φ – це вираз вигляду
1 1
1
,... , ,...,
,..., , ,...,
n m
m
x x u u
v vR⊥ ⊥ Φ , де ⊥ – спеціальний символ,
який позначає невизначене значення.
Нехай a
bR Φ та c
eR Φ мають однакові
U-неозначувані форми. Із визначень ви-
пливає, що на всіх моделях мови A преди-
кати a
AbR Φ та c
e AR Φ приймають однакові
значення на всіх d∈V, –UA, де усі імена U не
мають значення: ( ) ( )a c
A e AbR d R dΦ = Φ .
Таким чином, отримуємо наступну
властивість (тут ∗ – одне з Cl, Cm, T, F, TF).
UnD) Якщо v
xR Φ та z
yR Φ мають
однакові U-неозначувані форми, то
,v
xR Φ Γ A, –U |=∗ ,z
yR Φ Δ.
Узагальнимо для Х–Y-означених на-
слідків властивість U (тут ∗ – одне з Cl, Cm,
T, F, TF).
DU) Нехай Γ A, Х–Y |=∗ Δ та Δ ⊆ Σ, тоді
Γ A, Х–Y |=∗ Σ;
нехай Γ A, Х–Y |=∗ Δ та Γ ⊆ Λ, тоді
Λ A, Х–Y |=∗ Δ.
3. Властивості елімінації кванторів
Для спрощення запису далі будемо
позначати:
Теоретичні та методологічні основи програмування
44
( )X Y AT −
Φ∈Γ
ΦI як TХ–Y (ΓA),
( )X Y AT −
Ψ∈Δ
ΨU як TХ–Y (ΔA),
( )X Y AF −
Φ∈Γ
ΦU як FХ–Y (ΓA),
( )X Y AF −
Ψ∈Δ
ΨI як FХ–Y (ΔA).
Аналогічно вводимо позначення
TХ (ΓA), TХ (ΔA), FХ (ΓA), FХ (ΔA) та T–Y (ΓA),
T–Y (ΔA), F–Y (ΓA), F–Y (ΔA).
Теорема 3. При умові z∈X маємо
(тут ∗ – одне з Cl, Cm, T, F, TF):
1) Γ A, Х–Y |=∗ Δ, ∃хΦ, ( )x
zR Φ ⇒
⇒ Γ A, Х–Y |=∗ Δ, ∃хΦ;
2) Γ, ∀хΦ, ( )x
zR Φ A, Х–Y |=∗ Δ ⇒
⇒ Γ, ∀хΦ A, Х–Y |=∗ Δ.
Доведення. Доведемо для Cl-наслід-
ків. Згідно FR∃ при умові z∈X маємо
FХ–Y (∃xΦA) ⊆ FХ–Y ( ( ) )x
z AR Φ . Тому TХ–Y (ΓA) ∩
∩ FХ–Y (ΔA) ∩ FХ–Y ( ( ) )x
z AR Φ ∩ FХ–Y (∃хΦA) = ∅
⇒ TХ–Y (ΓA) ∩ FХ–Y (ΔA) ∩ FХ–Y (∃хΦA) = ∅,
тобто отримуємо Γ A, Х–Y |=Cl Δ, ∃хΦ, ( )x
zR Φ
⇒ Γ A, Х–Y |=Cl Δ, ∃хΦ.
Згідно TR∀ при умові z∈X маємо
TХ–Y (∀xΦA) ⊆ TХ–Y ( ( ) )x
z AR Φ . Звідси маємо
TХ–Y (ΓA) ∩ TХ–Y ( ( ) )x
z AR Φ ∩ TХ–Y (∀хΦA) ∩
∩ FХ–Y (ΔA) = ∅ ⇒ TХ–Y (ΓA) ∩ TХ–Y (∀хΦA) ∩
FХ–Y (ΔA) = ∅, тобто отримуємо, що
Γ, ∀хΦ, ( )x
zR Φ A, Х–Y |=Cl Δ ⇒ Γ, ∀хΦ A, Х–Y |=Cl Δ.
Доведемо для Cm-наслідків. Згідно
TR∃ при z∈X TХ–Y ( ( ) )x
z AR Φ ⊆ TХ–Y (∃xΦA).
Тому отримуємо FХ–Y (ΓA) ∪ TХ–Y (∃xΦA) ∪
∪ TХ–Y ( ( ) )x
z AR Φ ∪ TХ–Y (ΔA) =
VA ⇒ FХ–Y (ΓA) ∪
∪ TХ–Y (∃xΦA) ∪ TХ–Y ((ΔA) =
VA, тобто маємо
Γ A, Х–Y |=Cm Δ, ∃хΦ, ( )x
zR Φ ⇒ Γ A, Х–Y |=Cm Δ, ∃х.
Згідно FR∀ при умові z∈X маємо
FХ–Y ( ( ) )x
z AR Φ ⊆ FХ–Y (∀xΦA). Звідси маємо
FХ–Y (ΓA) ∪ FХ–Y ( ( ) )x
z AR Φ ∪ FХ–Y (∀xΦA) ∪
∪ TХ–Y (ΔA) = VA ⇒ FХ–Y (ΓA) ∪ FХ–Y (∀xΦA) ∪
∪ TХ–Y (ΔA) = VA, тобто отримуємо, що
Γ, ∀хΦ, ( )x
zR Φ A, Х–Y |=Cm Δ ⇒ Γ, ∀хΦ A, Х–Y |=Cm Δ.
Доведемо для T-наслідків. Згідно
TR∃ при z∈X TХ–Y ( ( ) )x
z AR Φ ⊆ TХ–Y (∃xΦA),
тому отримуємо TХ–Y (ΓA) ⊆ TХ–Y (∃xΦA) ∪
∪ TХ–Y ( ( ) )x
z AR Φ ∪ TХ–Y (ΔA) ⇒ TХ–Y (ΓA) ⊆
⊆ TХ–Y (∃xΦA) ∪ TХ–Y (ΔA), тобто отримуємо,
Γ A, Х–Y |=T Δ, ∃хΦ, ( )x
zR Φ ⇒ Γ A, Х–Y |=T Δ, ∃х.
Згідно TR∀ при умові z∈X маємо
TХ–Y (∀xΦA) ⊆ TХ–Y ( ( ) )x
z AR Φ , тому TХ–Y (ΓA) ∩
∩ TХ–Y ( ( ) )x
z AR Φ ∩ TХ–Y (∀xΦA) ⊆ TХ–Y (ΔA) ⇒
⇒ TХ–Y (ΓA) ∩ TХ–Y (∀xΦA) ⊆ TХ–Y (ΔA), тобто
Γ, ∀хΦ, ( )x
zR Φ A, Х–Y |=T Δ ⇒ Γ, ∀хΦ A, Х–Y |=T Δ.
Доведемо для F-наслідків. Згідно
FR∃ при z∈X FХ–Y (∃xΦA) ⊆ FХ–Y ( ( ) )x
z AR Φ ,
тому FХ–Y (ΔA) ∩ FХ–Y ( ( ) )x
z AR Φ ∩ FХ–Y (∃xΦA) ⊆
⊆ FХ–Y (ΓA) ⇒ FХ–Y (ΔA) ∩ FХ–Y (∃xΦA) ⊆
⊆ FХ–Y (ΓA), тобто Γ A, Х–Y |=F Δ, ∃хΦ, ( )x
zR Φ
⇒ Γ A, Х–Y |=F Δ, ∃х.
Згідно FR∀ при умові z∈X маємо
FХ–Y ( ( ) )x
z AR Φ ⊆ FХ–Y (∀xΦA), тому FХ–Y (ΔA) ⊆
⊆ FХ–Y ( ( ) )x
z AR Φ ∪ FХ–Y (∀xΦA) ∪ FХ–Y (ΓA) ⇒
⇒ FХ–Y (ΔA) ⊆ FХ–Y (∀xΦA) ∪ FХ–Y (ΓA), тобто
Γ, ∀хΦ, ( )x
zR Φ A, Х–Y |=F Δ ⇒ Γ, ∀хΦ A, Х–Y |=F Δ.
Об'єднуючи доведення для T-нас-
лідків та F-наслідків, отримуємо доведен-
ня для TF-наслідків. Таким чином:
Γ A, Х–Y |=TF Δ, ∃хΦ, ( )x
zR Φ ⇒ Γ A, Х–Y |=TF Δ, ∃х;
Γ, ∀хΦ, ( )x
zR Φ A, Х–Y |=TF Δ ⇒ Γ, ∀хΦ A, Х–Y |=TF Δ.
Для базового квантора ∃х п. 2 твер-
дження теореми можна записати так:
2') Γ, ¬∃хΦ, ( )x
zR¬ Φ A, Х–Y |=∗ Δ ⇒
⇒ Γ, ¬∃хΦ A, Х–Y |=∗ Δ.
Враховуючи властивість DU, із тео-
реми 3 отримуємо наступні властивості
елімінації кванторів для Х–Y-означених від-
ношень логічного наслідку:
∃Х–Y –| ) Γ A, Х–Y |=∗ Δ, ∃хΦ ⇔
⇔ Γ A, Х–Y |=∗ Δ, ∃хΦ, ( )x
zR Φ при z∈X;
∀Х–Y |– ) 2) Γ, ∀хΦ A, Х–Y |=∗ Δ ⇔
⇔ Γ, ∀хΦ, ( )x
zR Φ A, Х–Y |=∗ Δ при z∈X.
Перейшовши до базового квантора
∃х, властивість ∀Х–Y |– перепишемо так:
¬∃Х–Y |– ) Γ, ¬∃хΦ Х–Y |=∗ Δ ⇔
⇔Γ, ¬∃хΦ, ( )x
zR¬ Φ Х–Y |=∗ Δ.
Тут ∗ – одне з Cl, Cm, T, F, TF.
Зазначені властивості можна уза-
Теоретичні та методологічні основи програмування
45
гальнити.
Теорема 4. Нехай Z, W, U ⊆ V – ди-
з’юнктні множини, нехай Y ⊆ Z. Тоді:
1) Γ A, W∪Y–U∪(Z\Y) |=∗ Δ, ∃хΦ ⇔
Γ A, W∪Y–U∪(Z\Y) |=∗ Δ, ∃хΦ,
1
( ),..., ( ),...,
n
x x
y yR RΦ Φ
де всі yi∈Y ;
2) ¬∃хΦ, Γ A, W∪Y–U∪(Z\Y) |=∗ Δ ⇔
¬∃хΦ,
1
( ),..., ( ),...,
n
x x
y yR R¬ Φ ¬ Φ Γ A, W∪Y–U∪(Z\Y) |=∗ Δ,
де всі yi∈Y.
Тут ∗ – одне з Cl, Cm, T, F, TF.
Доведення теореми 4 подібне дове-
денню теореми 3, воно використовує тео-
рему 1, а також властивість DU.
Беручи до уваги теорему 2, отриму-
ємо такі властивості елімінації кванторів
для Х–Y-означених відношень логічного на-
слідку (тут ∗ – одне з Cl, Cm, T, F, TF).
Нехай Z, W, U ⊆ V – диз’юнктні
множини предметних імен. Тоді:
Br∃–|) Γ A, W–U |=∗ Δ, ∃хΦ ⇔
для кожної Y ⊆ Z Γ A, W∪Y–U∪(Z\Y) |=∗
Δ, ∃хΦ, 1
( ),..., ( ),...,
n
x x
y yR RΦ Φ де всі yi∈Y.
Br¬∃|–) ¬∃хΦ, Γ A, W–U |=∗ Δ ⇔
для кожної Y ⊆ Z
¬∃хΦ,
1
( ),..., ( ),...,
n
x x
y yR R¬ Φ ¬ Φ Γ A, W∪Y–U∪(Z\Y) |=∗ Δ,
де всі yi∈Y.
Теорема 5. Для логік квазіарних
предикатів при умові z∈X маємо:
1) Γ, ∃хΦ A, Х –Y |=∗ Δ ⇒
⇒ Γ, ( )x
zR Φ A, Х–Y |=∗ Δ;
2) Γ A, Х–Y |=∗∀хΦ, Δ ⇒
⇒ Γ A, Х–Y |=∗ ( ),x
zR Φ Δ.
Тут ∗ – одне з Cl, Cm, T, F, TF.
Доведення. Доведемо для Cl-наслід-
ків. Згідно TR∃ при z∈X TХ–Y ( ( ) )x
z AR Φ ⊆
⊆ TХ–Y (∃xΦA). Звідси TХ–Y (ΓA) ∩ TХ–Y (∃хΦA) ∩
∩ FХ–Y (ΔA) = ∅ ⇒ TХ–Y (ΓA) ∩ TХ–Y ( ( ) )x
z AR Φ ∩
∩ FХ–Y (ΔA) = ∅, тобто Γ, ∃хΦ A, Х–Y |=Cl Δ ⇒
Γ, ( )x
zR Φ A, Х–Y |=Cl Δ.
Згідно FR∀ при умові z∈X маємо
FХ–Y ( ( ) )x
z AR Φ ⊆ FХ–Y (∀xΦ). Звідси TХ–Y (ΓA) ∩
∩ FХ–Y (∀хΦA) ∩ FХ –Y (ΔA) = ∅ ⇒ TХ–Y (ΓA) ∩
∩ FХ–Y ( ( ) )x
z AR Φ ∩ FХ –Y(ΔA) = ∅, що й дає
Γ A, Х –Y |=Cl ∀хΦ, Δ ⇒ Γ A, Х–Y |=Cl ( ),x
zR Φ Δ.
Доведемо для Cm-наслідків. Згідно
FR∃ при z∈X FХ–Y (∃xΦA) ⊆ FХ–Y ( ( ) )x
z AR Φ ,
тому FХ–Y (∃xΦA) ∪ FХ–Y (ΓA) ∪ TХ–Y (ΔA) =
VA ⇒
⇒ FХ–Y ( ( ) )x
z AR Φ ∪ FХ–Y (ΓA) ∪ TХ–Y (ΔA) =
VA,
або Γ, ∃хΦ A, Х–Y |=Cm Δ ⇒ Γ, ( )x
zR Φ A, Х–Y |=Cm Δ.
Згідно TR∀ при z∈X TХ–Y (∀xΦA) ⊆
⊆ TХ–Y ( ( ) )x
z AR Φ , тому маємо FХ–Y (ΓA) ∪
∪ TХ–Y (∀xΦA) ∪ TХ–Y (ΔA) =
VA ⇒ FХ–Y (ΓA) ∪
∪ TХ–Y ( ( ) )x
z AR Φ ∪ TХ–Y (ΔA) =
VA, тобто
Γ A, Х –Y |=Cm ∀хΦ, Δ ⇒ Γ A, Х–Y |=Cm ( ),x
zR Φ Δ.
Доведемо для T-наслідків. Згідно
TR∃ при z∈X TХ–Y ( ( ) )x
z AR Φ ⊆ TХ–Y (∃xΦA),
тому TХ–Y (ΓA) ∪ TХ–Y (∃xΦA) ⊆ TХ–Y (ΔA) ⇒
⇒ TХ–Y (ΓA) ∪ TХ–Y ( ( ) )x
z AR Φ ⊆ TХ–Y (ΔA), тоб-
то Γ, ∃хΦ A, Х–Y |=T Δ ⇒ Γ, ( )x
zR Φ A, Х–Y |=T Δ.
Згідно TR∀ при умові z∈X маємо
TХ–Y (∀xΦA) ⊆ TХ–Y ( ( ) )x
z AR Φ , тому TХ–Y (ΓA) ⊆
⊆ TХ–Y (∀xΦA) ∪ TХ–Y (ΔA) ⇒ TХ–Y (ΓA) ⊆
⊆ TХ–Y ( ( ) )x
z AR Φ ∪ TХ–Y (ΔA), тобто маємо
Γ A, Х –Y |=T ∀хΦ, Δ ⇒ Γ A, Х–Y |=T ( ),x
zR Φ Δ.
Доведемо для F-наслідків. Згідно
FR∃ при z∈X FХ–Y (∃xΦA) ⊆ FХ–Y ( ( ) )x
z AR Φ ,
тому FХ–Y (ΔA) ⊆ FХ–Y (∃xΦA) ∪ FХ–Y (ΓA) ⇒
⇒ FХ–Y (ΔA) ⊆ FХ–Y ( ( ) )x
z AR Φ ∪ FХ–Y (ΓA), або
Γ, ∃хΦ A, Х–Y |=F Δ ⇒ Γ, ( )x
zR Φ A, Х–Y |=F Δ.
Згідно FR∀ при z∈X FХ–Y ( ( ) )x
z AR Φ ⊆
⊆ FХ–Y (∀xΦA), тому FХ–Y (∀xΦA) ∩ FХ–Y (ΔA) ⊆
⊆ FХ–Y (ΓA) ⇒ FХ–Y ( ( ) )x
z AR Φ ∩ FХ–Y (ΔA) ⊆
⊆ FХ–Y (ΓA), що й дає Γ A, Х –Y |=F ∀хΦ, Δ ⇒
⇒ Γ A, Х–Y |=F ( ),x
zR Φ Δ.
Об'єднуючи доведення для T-нас-
лідків та F-наслідків, отримуємо доведен-
ня для TF-наслідків. Таким чином, маємо
Γ, ∃хΦ A, Х–Y |=TF Δ ⇒ Γ, ( )x
zR Φ A, Х–Y |=TF Δ та
Γ A, Х –Y |=TF ∀хΦ, Δ ⇒ Γ A, Х–Y |=TF ( ),x
zR Φ Δ.
Теорема 6. Нехай z тотально строго
неістотне та z∉пт(Γ, Δ, Φ). Тоді при z∈X:
1) ( ),x
zR Φ Γ A, Х–Y |=∗ Δ ⇒
⇒ ∃хΦ, Γ A, Х–Y |=∗ Δ;
Теоретичні та методологічні основи програмування
46
2) Γ A, Х–Y |=∗ ( ),x
zR Φ Δ ⇒
⇒ Γ A, Х–Y |=∗ ∀хΦ, Δ.
Тут ∗ – одне з Cl, Cm, T, F, TF.
Зауважимо, що п. 2 можна перефор-
мулювати так:
2') Γ A, Х–Y |=∗ ( ),x
zR¬ Φ Δ ⇒
⇒ Γ A, Х–Y |=∗ ¬∃хΦ, Δ.
Доводимо п.1 для A, Х–Y |=Cl . Покажемо:
із TХ–Y (ΓA) ∩ TХ–Y ( ( )x
z AR Φ ) ∩ FХ–Y (ΔA) = ∅
випливає TХ–Y (ΓA) ∩ TХ–Y (∃хΦA) ∩ FХ–Y (ΔA) = ∅.
Нехай супротивне: існує d∈TХ–Y (ΓA) ∩
∩ TХ–Y (∃хΦA) ∩ FХ–Y (ΔA), проте TХ–Y (ΓA) ∩
∩ TХ–Y ( ( )x
z AR Φ ) ∩ FХ–Y (ΔA) = ∅ (∗). Із пер-
шої умови маємо d∈TХ–Y (∃хΦA), d∈TХ–Y (ΓA)
та d∈FХ–Y (ΔA); із d∈TХ–Y (∃хΦA) далі маємо
d∇xaa∈TХ–Y (ΦA) для деякого a∈A. Але z
тотально строго неістотне та z∉пт(Γ, Δ, Φ),
тому d∇zaa∈TХ–Y (ΓA), d∇zaa∈FХ–Y (ΔA),
d∇xaa∇zaa∈TХ–Y (ΦA). Із останнього ви-
пливає d∇zaa∈TХ–Y ( ( )x
z AR Φ ), тому маємо
d∇zaa∈TХ–Y (ΓA) ∩ T( ( )x
z AR Φ ) ∩ FХ–Y (ΔA),
що суперечить умові (∗).
Доводимо п.1 для A, Х–Y |=Cm . Покаже-
мо: із FХ–Y (ΓA) ∪ FХ–Y ( ( )x
z AR Φ ) ∪ TХ–Y (ΔA) =
= V, Х–YA випливає FХ–Y (ΓA) ∪ FХ–Y (∃хΦA) ∪
∪ TХ–Y (ΔA) = V, Х–YA. Нехай супротивне: іс-
нує d∈V, Х–YA таке, що d∉FХ–Y (ΓA) ∪
∪ FХ–Y (∃хΦA) ∪ TХ–Y (ΔA), проте FХ–Y (ΓA) ∪
∪ FХ–Y ( ( )x
z AR Φ ) ∪ TХ–Y (ΔA) = V, Х–YA (∗). Із
першого маємо d∉FХ–Y (ΓA), d∉FХ–Y (∃хΦA)
та d∉TХ–Y (ΔA); із d∉FХ–Y (∃хΦA) маємо
d∇xaa∉FХ–Y (ΦA) для деякого a∈A. Але z
тотально строго неістотне та z∉пт(Γ, Δ, Φ),
тому d∇zaa∉FХ–Y (ΓA), d∇zaa∉TХ–Y (ΔA),
d∇xaa∇zaa∉FХ–Y (ΦA). Із останнього от-
римуємо d∇zaa∉FХ–Y ( ( )x
z AR Φ ), тому
d∇zaa∉FХ–Y (ΓA) ∪ FХ–Y ( ( )x
z AR Φ ) ∪ TХ–Y (ΔA),
що суперечить (∗).
Враховуючи, що для відношень |=Cl
та |=Cm можна [2] знімати заперечення, пе-
реносячи формулу з лівої частини у праву і
навпаки, отримуємо, що п.2 для |=Cm та |=Cl
випливає з п.1.
Доводимо п.1 для |=T . Покажемо: з
умови TХ–Y (ΓA) ∩ TХ–Y ( ( )x
z AR Φ ) ⊆ T(Х–Y ΔA)
випливає TХ–Y (ΓA) ∩ TХ–Y (∃хΦA) ⊆ TХ–Y (ΔA).
Нехай супротивне: TХ–Y (ΓA) ∩ TХ–Y ( ( )x
z AR Φ ) ⊆
⊆ TХ–Y (ΔA), проте існує d таке: d∈TХ–Y (ΓA) ∩
∩ TХ–Y (∃хΦA) та d∉TХ–Y (ΔA). Із d∈TХ–Y (∃хΦA)
маємо d∇xaa∈TХ–Y (ΦA) для деякого a∈A.
Але z тотально строго неістотне та
z∉пт(Γ, Δ, Φ), тому маємо d∇zaa∈TХ–Y (ΓA),
d∇zaa∉TХ–Y (ΔA), d∇xaa∇zaa∈T(ΦA). Із
останнього маємо d∇zaa∈TХ–Y ( )x
z AR Φ ),
тому d∇zaa∈TХ–Y (ΓA) ∩ TХ–Y ( ( )x
z AR Φ ) та
d∇zaa∉TХ–Y (ΔA), але це суперечить умові
TХ–Y (ΓA) ∩ TХ–Y (∃хΦA) ⊆ TХ–Y (ΔA).
Доводимо п.2 для |=T . Покажемо, що
TХ–Y (ΓA) ⊆ TХ–Y ( ( )x
z AR Φ ) ∪ TХ–Y (ΔA) ⇒
⇒ TХ–Y (ΓA) ⊆ TХ–Y (∀хΦA) ∪ TХ–Y(ΔA). Нехай
супротивне: TХ–Y (ΓA) ⊆ TХ–Y ( ( )x
z AR Φ ) ∪
∪ TХ–Y (ΔA), водночас існує d: d∈TХ–Y (ΓA),
d∉TХ–Y (∀хΦA), d∉TХ–Y (ΔA). Із d∉TХ–Y (∀хΦA)
отримуємо d∇xaa∉TХ–Y (ΦA) для деякого
a∈A. Але z тотально строго неістотне та
z∉пт(Γ, Δ, Φ), тому d∇zaa∈TХ–Y (ΓA),
d∇zaa∉TХ–Y (ΔA), d∇xaa∇zaa∉TХ–Y (ΦA).
Із останнього маємо d∇zaa∉TХ–Y ( ( )x
z AR Φ ),
тому d∇zaa∉TХ–Y( ( )x
z AR Φ ) ∪ TХ–Y (ΔA) та
d∇zaa∈TХ–Y (ΓA), але це суперечить умові
TХ–Y (ΓA) ⊆ TХ–Y ( ( )x
z AR Φ ) ∪ TХ–Y (ΔA).
Доводимо п.1 для |=F . Покажемо: з
умови FХ–Y (ΔA) ⊆ FХ–Y (ΓA) ∪ FХ–Y ( ( )x
z AR Φ )
випливає FХ–Y (ΔA) ⊆ FХ–Y (ΓA) ∪ FХ–Y (∃хΦA).
Нехай супротивне: FХ–Y (ΔA) ⊆ FХ–Y (ΓA) ∪
∪ FХ–Y ( ( )x
z AR Φ ), водночас існує d таке:
d∈FХ–Y (ΔA), d∉FХ–Y (∃хΦA), d∉FХ–Y (ΓA). Із
d∉FХ–Y (∃хΦA) отримуємо d∇xaa∉FХ–Y (ΦA)
для деякого a∈A. Але z тотально строго
неістотне та z∉пт(Γ, Δ, Φ), тому маємо
d∇zaa∈FХ–Y (ΔA), d∇zaa∉FХ–Y (ΓA) та
d∇xaa∇zaa∉FХ–Y (ΦA). Із останнього
отримуємо d∇zaa∉FХ–Y ( ( )x
z AR Φ ), тому
маємо d∇zaa∉FХ–Y (ΓA) ∪ FХ–Y ( ( )x
z AR Φ ) та
d∇zaa∈FХ–Y (ΔA). Але це суперечить умові
FХ–Y (ΔA) ⊆ FХ–Y (ΓA) ∪ FХ–Y ( ( )x
z AR Φ ).
Доводимо п.2 для |=F . Покажемо: з
Теоретичні та методологічні основи програмування
47
умови FХ–Y ( ( )x
z AR Φ ) ∩ FХ–Y (ΔA) ⊆ FХ–Y (ΓA)
випливає FХ–Y (∀хΦA) ∩ FХ–Y (ΔA) ⊆ FХ–Y (ΓA).
Припустимо супротивне: FХ–Y ( ( )x
z AR Φ ) ∩
∩ FХ–Y (ΔA) ⊆ FХ–Y (ΓA), водночас існує d:
d∈FХ–Y (ΔA), d∈FХ–Y (∀хΦA), d∉FХ–Y (ΓA). Із
d∈FХ–Y(∀хΦA) отримуємо d∇xaa∈FХ–Y (ΦA)
для деякого a∈A. Але z тотально строго
неістотне та z∉пт(Γ, Δ, Φ), тому маємо
d∇zaa∈FХ–Y (ΔA), d∇zaa∉FХ–Y (ΓA) та
d∇xaa∇zaa∈FХ–Y (ΦA). Із останнього
отримуємо d∇zaa∈FХ–Y ( ( )x
z AR Φ ), тому
маємо d∇zaa∈FХ–Y ( ( )x
z AR Φ ) ∩ FХ–Y (ΔA) та
d∇zaa∉FХ–Y (ΓA). Але це суперечить умові
FХ–Y ( ( )x
z AR Φ ) ∩ FХ–Y (Δ) ⊆ FХ–Y (Γ).
Доводимо п.1 для |=TF . Покажемо: з
умови TХ–Y (ΓA) ∩ TХ–Y ( ( )x
z AR Φ ) ⊆ TХ–Y (ΔA)
та FХ–Y (ΔA) ⊆ FХ–Y (ΓA) ∪ FХ–Y ( ( )x
z AR Φ ) (∗)
випливає TХ–Y (ΓA) ∩ TХ–Y (∃хΦA) ⊆ TХ–Y (ΔA)
та FХ–Y (ΔA) ⊆ FХ–Y (ΓA) ∪ FХ–Y (∃хΦA). Припу-
стимо супротивне: маємо умову (∗), проте
невірно TХ–Y (ΓA) ∩ TХ–Y (∃хΦA) ⊆ TХ–Y (ΔA)
або невірно FХ–Y (ΔA) ⊆ FХ–Y (ΓA) ∪ FХ–Y (∃хΦA).
У першому випадку доводимо так, як для
|=T , а в другому – як для |=F .
Доводимо п.2 для |=TF . Покажемо: з
умови TХ–Y (ΓA) ⊆ TХ–Y ( ( )x
z AR Φ ) ∪ TХ–Y (ΔA)
та FХ–Y ( ( )x
z AR Φ ) ∩ FХ–Y (ΔA) ⊆ F Х–Y (ΓA) (∗)
випливає T Х–Y (ΓA) ⊆ TХ–Y (∀хΦA) ∪ TХ–Y (ΔA)
та FХ–Y (∀хΦA) ∩ FХ–Y (ΔA) ⊆ FХ–Y (ΓA). При-
пустимо супротивне: маємо (∗), проте не-
вірно TХ–Y (ΓA) ⊆ TХ–Y (∀хΦA) ∪ TХ–Y (ΔA) або
невірно FХ–Y (∀хΦA) ∩ FХ–Y (ΔA) ⊆ FХ–Y (ΓA). У
першому випадку доводимо так, як для |=T ,
а в другому – як для |=F .
Із теорем 5 та 6 отримуємо наступні
властивості елімінації кванторів для Х–Y-
означених відношень логічного наслідку.
Нехай z тотально строго неістотне
та z∉пт(Γ, Δ, Φ). Тоді при z∈X маємо:
∃Х–Y |– ) Γ, ∃хΦ Х –Y |=∗ Δ ⇔
⇔ Γ, ( )x
zR Φ Х–Y |=∗ Δ;
∀Х–Y –| ) Γ A, Х–Y |=∗ ∀хΦ, Δ ⇔
⇔ Γ A, Х–Y |=∗ ( ),x
zR Φ Δ.
Перейшовши до базового квантора
∃х, властивість ∀Х–Y –|перепишемо так:
¬∃Х–Y –| ) Γ Х–Y |=∗ ¬∃хΦ, Δ ⇔
⇔ Γ Х–Y |=∗ ( ),x
zR¬ Φ Δ.
Тут ∗ – одне з Cl, Cm, T, F, TF.
Підсумовуючи, випишемо власти-
вості елімінації кванторів для різних логі-
чних наслідків у різних семантиках в яв-
ному вигляді, виділивши логіки еквітон-
них та логіки антитонних предикатів. За-
значені властивості будуть використані
для побудови числень секвенційного типу,
які формалізують відповідні відношення
логічного наслідку.
Замість ∃Х–Y –| та ¬∃Х–Y |– братимемо
загальніші властивості Br∃–| та Br¬∃|– .
В логіках еквітонних предикатів
(неокласична семантика) та в логіках анти-
тонних предикатів (пересичена семантика)
можна брати [2] властивості ∃|– , ∃–| , ¬∃|– ,
¬∃–| :
∃|– ) ∃хΦ, Γ |=∗ Δ ⇔ ( ),x
zR Φ Γ |=∗ Δ,
де z тотально строго неістотне та
z∉пт(Γ, Δ, Φ);
∃–| ) Γ |=∗ Δ, ∃хΦ ⇔ Γ |=∗ Δ, ∃хΦ, ( )x
zR Φ ;
¬∃|– ) ¬∃хΦ, Γ |=∗ Δ ⇔
⇔ ¬∃хΦ, ( ),x
zR¬ Φ Γ |=∗ Δ;
¬∃–| ) Γ |=∗ Δ, ¬∃хΦ ⇔ Γ |=∗ Δ, ( ),x
zR¬ Φ
де z тотально строго неістотне та
z∉пт(Γ, Δ, Φ).
Для відношень |=Cl в неокласичній
семантиці та |=Cт в пересиченій семантиці
можна обмежитись властивостями ∃Х–Y |– та
Br∃–| (∃|– та ∃–| у випадках еквітонних чи
антитонних предикатів) адже для |=Cl та
|=Cт можна знімати заперечення, перено-
сячи формулу з лівої частини відношення
у праву.
Для відношення |=Cl в неокласичній
семантиці маємо ∃Х–Y |– та Br∃–| .
Для відношення |=Cl в неокласичній
семантиці логіки еквітонних предикатів
маємо ∃|– та ∃–| (зауважимо, що для ∃|– мо-
жна [4] ослабити умову на z до тотально
неістотності).
Для відношення |=Cт в пересиченій
семантиці маємо ∃Х–Y |– та Br∃–| .
Для відношення |=Cт в пересиченій
семантиці логіки антитонних предикатів
маємо ∃|– та ∃–| .
Теоретичні та методологічні основи програмування
48
Для відношення |=T в неокласичній
семантиці маємо
∃ Х–Y |– , Br∃–| , Br¬∃|– , ¬∃ Х–Y –| .
Для відношення |=T в неокласичній
семантиці логіки еквітонних предикатів
маємо
∃ |– , ∃–| , Br¬∃|– , ¬∃ Х–Y –| .
Для відношення |=T в пересиченій
семантиці маємо такі ж властивості
∃ Х–Y |– , Br∃–| , Br¬∃|– , ¬∃ Х–Y –| ,
як і для випадку неокласичної семантики.
Для відношення |=T в пересиченій
семантиці логіки антитонних предикатів
маємо
∃ Х–Y |– , Br∃–| , ¬∃ |– , ¬∃–| .
Для відношення |=F в неокласичній
семантиці маємо
∃ Х–Y |– , Br∃–| , Br¬∃|– , ¬∃ Х–Y –| .
Для відношення |=F в неокласичній
семантиці логіки еквітонних предикатів
маємо ∃ Х–Y |– , Br∃–| , ¬∃|– , ¬∃–| .
Для відношення |=F в пересиченій
семантиці маємо такі ж властивості
∃Х–Y |– , Br∃–| , Br¬∃|– , ¬∃ Х–Y –| ,
як і для випадку неокласичної семантики.
Для відношення |=F в пересиченій
семантиці логіки антитонних предикатів
маємо ∃ |– , ∃–| , Br¬∃|– , ¬∃ Х–Y –| .
Для відношення |=TF в неокласичній
семантиці маємо ∃ Х–Y |– , Br∃–| , Br¬∃|– ,
¬∃ Х–Y –| .
Такі ж властивості ∃ Х–Y |– , Br∃–| ,
Br¬∃|– , ¬∃ Х–Y –| записуємо для відношення
|=TF в пересиченій семантиці та загальній
семантиці, а також в неокласичній семан-
тиці логіки еквітонних предикатів та в пе-
ресиченій семантиці логіки антитонних
предикатів.
Висновки
У роботі вивчається фундаменталь-
не поняття логічного наслідку для першо-
порядкових композиційно-номінативних
логік часткових однозначних, тотальних
неоднозначних та часткових неоднознач-
них квазіарних предикатів. Для таких логік
кванторного рівня запропоновано і дослі-
джено Х–Y-означені відношення логічного
наслідку для пар та множин формул. От-
римано низку властивостей таких відно-
шень в різних семантиках, зокрема, вла-
стивості елімінації кванторів.
На основі властивостей відношень
логічного наслідку для композиційно-но-
мінативних логік часткових однозначних,
тотальних неоднозначних та часткових не-
однозначних квазіарних предикатів в на-
ступних статтях планується побудова від-
повідних числень секвенційного типу
1. Смирнова Е.Д. Логика и философия. – М.,
1996. – 304 с.
2. Шкільняк С.С. Відношення логічного наслід-
ку в композиційно-номінативних логіках //
Проблеми програмування. – 2010. – № 1. –
C. 15–38.
3. Никитченко Н.С. Композиционно-номина-
тивный подход к уточнению понятия про-
граммы // Проблемы программирования. –
1999. – № 1. – С. 16–31.
4. Нікітченко М.С., Шкільняк С.С. Математи-
чна логіка та теорія алгоритмів – К., 2008. –
528 с.
5. Шкильняк С.С. Логики квазиарных преди-
катов первого порядка // Кибернетика и си-
стемный анализ. — 2010. – № 6 – С. 32–49.
Отримано 29.08.2011
Про автора:
Шкільняк Степан Степанович,
доктор фізико-математичних наук, доцент
кафедри теорії та технології програмуван-
ня Київського національного універси-
тету імені Тараса Шевченка.
Місце роботи автора:
Київський національний університет
імені Тараса Шевченка,
01601, Київ,
вул. Володимирська, 60.
Тел.: (044) 259 0519; (044) 522 0640 (д)
e-mail: sssh@unicyb.kiev.ua
|