Logical consequence relations in logics of monotone predicates and logics of antitone predicates
Logical consequence is one of the fundamental concepts in logic. In this paper we study logical consequence relations for program-oriented logical formalisms: pure first-order composition nominative logics of quasiary predicates. In our research we are giving special attention to different types of...
Збережено в:
| Дата: | 2018 |
|---|---|
| Автор: | |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
Інститут програмних систем НАН України
2018
|
| Теми: | |
| Онлайн доступ: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/219 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Репозитарії
Problems in programming| id |
pp_isofts_kiev_ua-article-219 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/b9/827aa08e8ec6a940ad887545ddc6bbb9.pdf |
| spelling |
pp_isofts_kiev_ua-article-2192024-04-28T11:56:41Z Logical consequence relations in logics of monotone predicates and logics of antitone predicates Отношения логического следствия в логиках монотонных предикатов и логиках антитонных предикатов Відношення логічного наслідку в логіках монотонних предикатів тa логіках антитонних предикатів Shkilniak, O.S. logic; predicate; semantics; logical consequence UDC 004.42:510.69 логика; предикат; семантика; логическое следствие УДК 004.42:510.69 логіка; предикат; семантика; логічний наслідок УДК 004.42:510.69 Logical consequence is one of the fundamental concepts in logic. In this paper we study logical consequence relations for program-oriented logical formalisms: pure first-order composition nominative logics of quasiary predicates. In our research we are giving special attention to different types of logical consequence relations in various semantics of logics of monotone predicates and logics of antitone predicates. For pure first-order logics of quasiary predicates we specify composition algebras of predicates, languages, interpretation classes (sematics) and logical consequence relations. We obtain the pairwise distinct relations: irrefutability consequence P |= IR , consequence on truth P |= T , consequence on falsity P |= F, strong consequence P |= TF in P-sеmantics of partial singlevalued predicates and strong consequence R |= TF in R-sеmantics of partial multi-valued predicates. Of the total of 20 of defined logical consequence relations in logics of monotone predicates and of antitone predicates, the following ones are pairwise distinct: PE |= IR, PE |= T, PE |= F, PE |= TF, RM |= T, RM |= F, RM |= TF. A number of examples showing the differences between various types of logical consequence relations is given. We summarize the results concerning the existence of a particular logical consequence relation for certain sets of formulas in a table and determine interrelations between different types of logical consequence relations.Problems in programming 2017; 1: 21-29 Исследованы отношения логического следствия в чистых первопорядковых композиционно-номинативных логиках частичных однозначных и частичных неоднозначных квазиарных предикатов. Описаны композиционные предикатные алгебры, языки и классы интерпретаций (семантики) этих логик, выделен ряд отношений логического следствия. Основное внимание акцентировано на изучении таких отношений в логиках монотонных предикатов и логиках антитонных предикатов. Для этих логик определено 20 отношений логического следствия, установлено, что из них лишь 7 раз-личных: PE |= IR , PE |= T , PE |= F , PE |= TF , RM |= T , RM |= F , RM |= TF . Приведены примеры, свидетельствующие о различии рассмотренных отношений логического следствия, установлены соотношения между такими отношениями.Problems in programming 2017; 1: 21-29 Досліджено відношення логічного наслідку в чистих першопорядкових композиційно-номінативних логіках часткових однозначних та часткових неоднозначних квазіарних предикатів. Описано відношення неспростовнісного, істиннісного, хибнісного та сильного логічного наслідку в логіках монотонних предикатів і логіках антитонних предикатів. Наведено приклади, які засвідчують відмінності одних відношень від інших, та встановлено співвідношення між різними відношеннями логічного наслідку. Ключові слова: логіка, предикат, семантика, логічний наслідок.Problems in programming 2017; 1: 21-29 Інститут програмних систем НАН України 2018-11-20 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/219 10.15407/pp2017.01.021 PROBLEMS IN PROGRAMMING; No 1 (2017); 21-29 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 1 (2017); 21-29 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 1 (2017); 21-29 1727-4907 10.15407/pp2017.01 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/219/211 Copyright (c) 2018 ПРОБЛЕМИ ПРОГРАМУВАННЯ |
| institution |
Problems in programming |
| baseUrl_str |
https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| datestamp_date |
2024-04-28T11:56:41Z |
| collection |
OJS |
| language |
Ukrainian |
| topic |
logic predicate semantics logical consequence UDC 004.42:510.69 |
| spellingShingle |
logic predicate semantics logical consequence UDC 004.42:510.69 Shkilniak, O.S. Logical consequence relations in logics of monotone predicates and logics of antitone predicates |
| topic_facet |
logic predicate semantics logical consequence UDC 004.42:510.69 логика предикат семантика логическое следствие УДК 004.42:510.69 логіка предикат семантика логічний наслідок УДК 004.42:510.69 |
| format |
Article |
| author |
Shkilniak, O.S. |
| author_facet |
Shkilniak, O.S. |
| author_sort |
Shkilniak, O.S. |
| title |
Logical consequence relations in logics of monotone predicates and logics of antitone predicates |
| title_short |
Logical consequence relations in logics of monotone predicates and logics of antitone predicates |
| title_full |
Logical consequence relations in logics of monotone predicates and logics of antitone predicates |
| title_fullStr |
Logical consequence relations in logics of monotone predicates and logics of antitone predicates |
| title_full_unstemmed |
Logical consequence relations in logics of monotone predicates and logics of antitone predicates |
| title_sort |
logical consequence relations in logics of monotone predicates and logics of antitone predicates |
| title_alt |
Отношения логического следствия в логиках монотонных предикатов и логиках антитонных предикатов Відношення логічного наслідку в логіках монотонних предикатів тa логіках антитонних предикатів |
| description |
Logical consequence is one of the fundamental concepts in logic. In this paper we study logical consequence relations for program-oriented logical formalisms: pure first-order composition nominative logics of quasiary predicates. In our research we are giving special attention to different types of logical consequence relations in various semantics of logics of monotone predicates and logics of antitone predicates. For pure first-order logics of quasiary predicates we specify composition algebras of predicates, languages, interpretation classes (sematics) and logical consequence relations. We obtain the pairwise distinct relations: irrefutability consequence P |= IR , consequence on truth P |= T , consequence on falsity P |= F, strong consequence P |= TF in P-sеmantics of partial singlevalued predicates and strong consequence R |= TF in R-sеmantics of partial multi-valued predicates. Of the total of 20 of defined logical consequence relations in logics of monotone predicates and of antitone predicates, the following ones are pairwise distinct: PE |= IR, PE |= T, PE |= F, PE |= TF, RM |= T, RM |= F, RM |= TF. A number of examples showing the differences between various types of logical consequence relations is given. We summarize the results concerning the existence of a particular logical consequence relation for certain sets of formulas in a table and determine interrelations between different types of logical consequence relations.Problems in programming 2017; 1: 21-29 |
| publisher |
Інститут програмних систем НАН України |
| publishDate |
2018 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/219 |
| work_keys_str_mv |
AT shkilniakos logicalconsequencerelationsinlogicsofmonotonepredicatesandlogicsofantitonepredicates AT shkilniakos otnošeniâlogičeskogosledstviâvlogikahmonotonnyhpredikatovilogikahantitonnyhpredikatov AT shkilniakos vídnošennâlogíčnogonaslídkuvlogíkahmonotonnihpredikatívtalogíkahantitonnihpredikatív |
| first_indexed |
2024-09-16T04:07:35Z |
| last_indexed |
2024-09-16T04:07:35Z |
| _version_ |
1818568180256210944 |
| fulltext |
Теоретичні та методологічні основи програмування
© О.С. Шкільняк, 2017
ISSN 1727-4907. Проблеми програмування. 2017. № 1 21
УДК 004.42:510.69
О.С. Шкільняк
ВІДНОШЕННЯ ЛОГІЧНОГО НАСЛІДКУ В ЛОГІКАХ
МОНОТОННИХ ПРЕДИКАТІВ TA ЛОГІКАХ АНТИТОННИХ
ПРЕДИКАТІВ
Досліджено відношення логічного наслідку в чистих першопорядкових композиційно-номінативних
логіках часткових однозначних та часткових неоднозначних квазіарних предикатів. Описано відношен-
ня неспростовнісного, істиннісного, хибнісного та сильного логічного наслідку в логіках монотонних
предикатів і логіках антитонних предикатів. Наведено приклади, які засвідчують відмінності одних
відношень від інших, та встановлено співвідношення між різними відношеннями логічного наслідку.
Ключові слова: логіка, предикат, семантика, логічний наслідок.
Вступ
Апарат математичної логіки лежить
в основі сучасних інформаційних і про-
грамних систем (див., напр., [1]). Для цьо-
го зазвичай використовується класична
логіка предикатів та базовані на її основі
спеціальні логіки. Проте класична логіка
має [2] низку обмежень, що ускладнює її
використання. Тому набуває актуальності
проблема побудови нових, програмно-
орієнтованих логічних формалізмів. Таки-
ми є композиційно-номінативні логіки ча-
сткових квазіарних предикатів.
Центральним для логіки є поняття
логічного наслідку. Широке використання в
програмуванні часткових відображень, які
можуть бути неоднозначними, виводить на
перший план проблему вивчення відно-
шень логічного наслідку для логік із не-
традиційними семантиками. Для першопо-
рядкових композиційно-номінативних ло-
гік такі відношення описано в [2–5]. Ви-
вченню відношень логічного наслідку для
логік монотонних предикатів i логік анти-
тонних предикатів присвячена дана робо-
та, вона є безпосереднім продовженням
роботи [4].
Метою даної статті є дослідження
відношень логічного наслідку в чистих
першопорядкових композиційно-номіна-
тивних логік (ЧКНЛ) однозначних та не-
однозначних квазіарних предикатів. Розг-
лядаються відношення неспростовнісного,
істиннісного, хибнісного, сильного логіч-
ного наслідку. Основний акцент зроблено
на вивченні цих відношень в різних семан-
тиках логік монотонних предикатів i логік
антитонних предикатів. Виділено 20 таких
відношень, з’ясовано, що із цих відношень
лише 7 попарно різних. Наведено прикла-
ди, які засвідчують відмінності одних від-
ношень від інших. Встановлено співвід-
ношення між різними відношеннями логі-
чного наслідку.
Невизначені в цій статті поняття
тлумачимо в сенсі робіт [2, 5].
Для полегшення читання опишемо
основні поняття і визначення.
1. Композиційні алгебри
квазіарних предикатів
В першопорядкових логіках преди-
кати задаються на множинах пар, перша
компонента яких – ім’я, а друга – його
значення. Такі множини пар названо імен-
ними множинами (ІМ). Предикати, задані
на ІМ, називають квазіарними.
V-A-іменна множина (V-A-ІМ) – це
часткова однозначна функція вигляду
d : V A. Трактуємо V і A як множини
предметних імен (змінних) і предметних
(базових) значень. Клас всіх V-A-іменних
множин будемо позначати VA.
V-A-квазіарний предикат – це част-
кова (неоднозначна, взагалі кажучи) функ-
ція вигляду P : VA {T, F}. Тут {T, F} –
множина істиннісних значень.
Неоднозначні V-A-квазіарні преди-
кати трактуємо як відношення між VA та
{T, F}. Tакі предикати названо [2] преди-
катами реляційного типу, або R-предика-
тами. Множину значень, які R-предикат P
Теоретичні та методологічні основи програмування
22
може прийняти на dVА, позначимо P(d).
Маємо P(d) {T , F}, тому P(d) може набу
вати одне із значень {}, {T }, {F}, {T, F}.
Клас V-A-квазіарних R-предикатів
позначають V
APrR .
Кожний R-предикат P : VA {T, F}
задається двома множинами – областю іс-
тинності )(PT та областю хибності F(P):
)(PT = {dVA | TP(d)};
)(PF = {dVA | FP(d)}.
V-A-квазіарний предикат P :
– однозначний, якщо )(PT F(P) = ;
– тотальний, якщо )(PT F(P) =
VA;
– неспростовний, якщо )(PF = ;
– виконуваний, якщо )(PT ;
– тотожно істинний (позначаємо T), якщо
)(PT = VА та )(PF = ;
– тотожно хибний (позначаємо F), якщо
)(PT = та F(P) = VА;
– всюди невизначений (позначаємо ),
якщо )(PT = та F(P) = ;
– тотально насичений (позначаємо ),
якщо )(PT = VА та F(P) = VА.
Часткові однозначні предикати на-
звано [4, 5] P-предикатами, тотальні назва-
но T-предикатами, тотальні однозначні –
TS-предикатами. Класи таких V-A-
квазіарних предикатів будемо відповідно
позначати V
APrP , V
APrT , V
APrTS .
Предикат P : VА {T , F} монотон-
ний, якщо: d d' )(dP P(d').
Предикат P : VА {T , F} антитон-
ний, якщо: d d' )(dP P(d').
Для однозначних предикатів моно-
тонність стає еквітонністю. Однозначний
P : VА {T, F} еквітонний, якщо:
(P(d) та d d') P(d') = P(d).
Монотонні R-предикати, антитонні
R-предикати, еквітонні P-предикати, анти-
тоннi T-предикати відповідно називають
(див. [5]) RM -предикатами, RA -предика-
тами, PE-предикатами, TА-предикатами.
Класи цих предикатів будемо позначати
, , V
A
V
A PrRAPrRM V
A
V
A PrTAPrPE , .
Константні предикати , ,T,F мо-
нотонні (еквітонні) й антитонні, при цьому
предикати ,T, F – однозначні.
Предикати-індикатори Ex наявності
у вхідних даних компоненти з іменем xV
задаємо [5] так:
)(ExT = {d | d(x)}, )(ExF = {d | d(x)}.
Предикати-індикатори Ex тотальні,
однозначні, немонотонні, неантитонні.
Предикат P
~
називають [5] дуаль
ним до предиката P , якщо:
)()
~
( ;)()
~
( PTPFPFPT .
Безпосередньо із визначень маємо:
Q – P-предикат Q – T-предикат;
Q – T-предикат Q – P-предикат;
Q – PE-предикат Q – TA-предикат;
Q – TA-предикат Q – PE-предикат;
якщо Q – TS-предикат, то Q Q .
Спеціальне відображення дуалізації
V
A
V
A PrRPrR : задають [5] так: ( ) P P .
Маємо [5] такі властивості:
(T) = T, (F) = F, () = , ( ) = ;
V
A
V
A PrRPrR )( , V
A
V
A PrTSPrTS )( ,
)( V
APrP = ,V
APrT )( V
APrT = V
APrP ;
)( V
APrPE = ,V
APrTA )( V
APrTA = ,V
APrPE
)( V
APrRM = ,V
APrRA (Pr )
V
ARA = Pr
V
ARM .
Базовими композиціями ЧКНЛ є [2]
логiчні зв’язки і , композиції реноміна-
ції
v
xR та квантифікації x.
Для , , T та F маємо (див. [5]):
= , = , )(Rv
x , x() = ;
= , = , )(R v
x = , x ( ) = ;
T = F, F = T, F F = F;
F)F( ,F)F(R T,)T( ,T)T(R xx v
x
v
x ;
Теоретичні та методологічні основи програмування
23
T T = T = T = T F = F T = T;
F = F = ; = = T;
T = T = F = F = .
Позначимо CQ = {, , ,R v
x x}.
Чиста першопорядкова алгебра ква-
зіарних предикатів – це композиційна ал-
гебра ),( CQPrRQR V
A
V
A .
Композиції , , ,R v
x x зберігають
[2] однозначність, тотальність, монотон-
ність, антитонність предикатів. Тому щодо
, , ,R v
x x замкнені такі класи:
P-предикатів, T-предикатів, TS-предикатів;
монотонних (еквітонних) предикатів, анти-
тонних предикатів.
Таким чином, можна виділити такі
підалгебри алгебри V
AQR :
),,( CQPrPQP V
A
V
A
),,( CQPrTQT V
A
V
A
),( CQPrTSQTS V
A
V
A ,
),,( CQPrRMQRM V
A
V
A
),,( CQPrRAQRA V
A
V
A
),,( CQPrPEQPE V
A
V
A
),( CQPrTAQTA V
A
V
A .
Те, що є підалгеброю алгебри ,
позначаємо . Тоді [5] маємо:
V
A
V
A QPQTS та V
A
V
A QTQTS ;
V
A
V
A QPQPE та V
A
V
A QRMQPE ;
V
A
V
A QTQTA та V
A
V
A QRAQTA .
Нехай – відображення дуалізації.
Алгебри ),Pr( 1 CQ та ),Pr( 2 CQ дуа-
льні, якщо ( 1Pr )= 2Pr та )(Pr2 = 1Pr .
Маємо такі дуальні пари алгебр:
V
AQP та ,V
AQT
V
AQPE та ,V
AQTA
V
AQRM та V
AQRA .
Алгебри V
AQR та V
AQTS авто-
дуальні.
2. Мови та їх інтерпретації
Семантичними моделями ЧКНЛ є
[2] чисті першопорядкові композиційні
системи квазіарних предикатів вигляду
(A, Pr, CQ). Така система задає алгебру
даних (A, Pr ) і композиційну алгебру пре-
дикатів ( Pr , CQ). Терми композиційної
алгебри трактуємо як формули мови
ЧКНЛ.
Алфавiт мови: множини V предме-
тних імен (змінних) та U V тотально не-
істотних [2] імен; множина символів базо-
вих композицій },,,{ xRCs v
x , множи-
на Ps предикатних символів (сигнатура).
Розширена сигнатура мови – це
= (V , U, Cs, Ps).
Індуктивне визначення множини Fr
формул таке:
– Ps Fr; формули pPs – атомарні;
– , Fr , , ,v
xR xFr.
Інтерпретуємо мову сигнатури на
композиційній системі (A, Pr, CQ) за до-
помогою тотального однозначного відо-
браження I : Ps Pr . Розширимо I до відо-
браження I : Fr Pr згідно побудови скла-
дних формул за допомогою символів Cs:
– I() = (I()),
– I() = (I(), I()),
– )),((R))(( IRI v
x
v
x
– I(x) = x(I()).
Інтерпретація мови ЧКНЛ сигна-
тури – це J = (CS, , I). Скорочено інтер-
претації будемо позначати (A, I).
Предикат J() – значення формули
при інтерпретації J – позначимо J .
Виділення підалгебр квазіарних
предикатів виділяє відповідні класи інтер-
претацій. Такі класи інтерпретацій нази-
вають семантиками.
Теоретичні та методологічні основи програмування
24
Маємо загальний клас R-інтерпре-
тацій та підкласи P-інтерпретацій, T-інтер-
претацій, TS-інтерпретацій, PE-інтер-
претацій, TA-інтерпретацій, RM-інтер-
претацій, RA-інтерпретацій. Ці класи
інтерпретацій, або семантики, відповідно
позначають так: R, P, T, TS, PE, TA,
RM, RA.
Для семантик маємо (див. [5]):
PE P, TA T;
TS P R, TS T R;
PE RM R, TA RA R.
Дуальна до інтерпретації J = (A, I)
інтерпретація (J) = (A, I) задається так:
для всіх pPs маємо )()( )( JJ pFpT та
)()( )( JJ pTpF .
Тоді J дуальна до (J).
Якщо інтерпретації J та дуальні,
то (див. [2]): для всіх Fr маємо
)()( FT J та )()( JTF .
Якщо J та G дуальні, то:
– J монотонний G антитонний;
– G антитонний J монотонний.
Виділення дуальних пар предикат-
них алгебр індукує виділення дуальних
пар семантик P та T, PE та TA, RM та RA.
Семантики R та TS автодуальні.
Для формул мови ЧКНЛ введено [2]
поняття виконуваної, неспростовної, тото-
жно істинної, тотожно хибної формули.
Семантичні властивості ЧКНЛ дос-
ліджено, зокрема, в [2–5].
3. Відношення логічного наслідку
На множині формул можна ввести
[2, 4, 5] низку відношень, які формалізують
центральне для логіки поняття логічного
наслідку. Спочатку вводимо відношення
наслідку для двох формул при фіксованій
інтерпретації J.
1. Істиннісний, або T-наслідок
J |= T :
J |= T )( JT )( JT .
2. Хибнісний, або F-наслідок J |= F :
J |= F )( JF F )( J .
3. Cильний, або TF-наслідок J |= TF :
J |= TF J |= T та J |= F .
4. Неспростовнісний, або IR-наслі-
док J |= IR :
J |= IR )( JT )( JF = .
5. Дуальний до IR, або DI-наслідок
J |= DI :
J |= DI )( JF )( JT = VA.
Відповідні відношення логічного на-
слідку в семантиці визначаємо за такою
схемою:
|= * , якщо J |= * для кожної
J.
Зазначені відношення описано в [2].
Нехай інтерпретації A, B дуальні.
Тоді [2, 5] маємо:
A |= T B |= F ,
A |= F B |= T ,
A |= IR B |= DI ,
A |= DI B |= IR ,
A |= TF B |= TF .
При розширенні семантики відно-
шення логічного наслідку звужується (тут
– це T , F , TF , IR, DI):
Теорема 1. Нехай для семантик та
маємо . Тоді |=
|=
Справді, нехай
|= , тоді
J |= для кожної J. Але , тому
J |= для кожної J. Звідси
|= .
Отже, |=
|= .
Для наведених відношень логічного
наслідку маємо (див. [2, 4]):
P |= DI =T |= IR = R |= IR = R |= DI = ;
P |= T = T |= F ; P |= F =T |=T ; P |= IR =T |= DI ;
Теоретичні та методологічні основи програмування
25
P |= TF = T |= TF ; R |= T = R |= F = R |= TF .
Серед цих відношень виявилося
[2, 4] лише 5 попарно різних:
P |= IR , P |= T , P |= F , P |= TF , R |= TF .
Для логіки TS-предикатів і класич-
ної логіки ці 5 відношень втрачають від-
мінності та стають єдиним відношенням:
TS |= TF = TS |= T = TS |= F =TS |= IR =TS |= DI .
Маємо [4, 5] такі співвідношення:
P |= TF
P |= T , P |= TF
P |= F ;
R |= TF
P |= TF ;
P |= T
P |= F P |= IR ;
P |= T
P |= F , P |= F P |=T .
Обмежуючи розглянуті відношення
на семантики монотонних (еквітонних)
предикатів і антитонних предикатів, отри-
муємо такі відношення:
PE |= IR , TA |=DI,
PE |= DI , TA |= IR ,
PE |= T , TA |= F , PE |= F , TA |= T ,
PE |= TF , TA |= TF ;
RM |= IR , RA |= IR , RM |= DI , RA |= DI ,
RM |= T , RA |=F, RA |= T , RM |= F ,
RM |= TF , RA |= TF .
Беручи до уваги дуальність пар PE і
TA та RM і RA, отримуємо:
Теорема 2.
1) PE |= IR =TA |= DI , PE |= T = TA |= F ,
PE |= F = TA |= T , PE |= TF =TA |= TF ;
2) RM |= T = RA |= F , RM |= F = RA |= T ,
RM |= TF = RA |= TF ;
3) PE |= DI =TA |= IR = ,
RM |= IR = RA |= IR = RM |= DI = RA |= DI = .
Таким чином, із роглянутих відно-
шень логічного наслідку для монотонних
(еквітонних) предикатів і антитонних пре-
дикатів залишається не більше 7 різних:
PE |= IR , PE |= T , PE |= F , PE |= TF ,
RM |= T , RM |= F , RM |=TF .
Розглянемо співвідношення між від-
ношеннями логічного наслідку.
Беручи до уваги теорему 1, отри-
муємо:
Теорема 3.
RM |= TF
RM |=T ,
RM |= TF
RM |= F ,
RM |= TF
PE |=TF , RM |= T
PE |=T ,
RM |= F PE |= F ;
PE|=TF
PE |= T
PE |= IR ,
PE |= TF
PE |= F PE |= IR ;
R |= TF
RM |=TF , P |= TF
PE |=TF ,
P |= T
PE |=T , P |= F PE |= F ,
P |= IR
PE |= IR .
Відомо [2], що:
& P |= T , P |= F ,
& P |= TF .
За теоремою 3 тоді отримуємо:
Твердження 1. 1) & PE |=T ;
2) PE |= F ;
3) & PE |= TF .
Водночас [2] маємо:
& P | F , P | T ,
& R | TF .
Останні твердження можна посили-
ти, формулюючи їх для семантик PE і RM.
Для цього розглянемо декілька прикладів.
При формулюванні прикладів для зручнос-
Теоретичні та методологічні основи програмування
26
ті використовуємо символи розширеної си-
гнатури: Ex для предикатів-індикаторів та
, ,T,F для константних предикатів.
Зафіксуємо довільну J = (A, I).
Приклад 1. & J | F F.
Маємо F(F) = VA, проте F( & ) =
= F() F() = F() T() = = .
Приклад 2. T J |T .
Маємо T(T) = VA, проте T( ) =
= T() T() = T() F() = = .
Приклад 3. & |J T та
& | J F .
Справді, маємо:
( & ) ( ) ( ) T T F VA VA = VA;
T( ) = T() T() = = ;
( ) ( ) ( ) F F T VA VA = VA;
F( & ) = F() F() = = .
Таким чином, отримуємо:
Твердження 2. 1) & PE | F ;
2) PE | T ;
3) &
RM | T ,
&
RM | F .
Згідно теореми 3 тоді отримуємо
Наслідок 1.
1) & PE |TF ;
2) PE | TF ;
3) &
RM | TF .
Маємо P | IR x та x P | IR
(див. [2]). Зазначені твердження можна по-
силити до &x P | IR x. Наведемо
відповідні приклади.
Приклад 4. Маємо
Ex J | IR xEx, xEx J | IR Ex,
Ex & xEx J | IR xEx Ex.
Маємо (Ex) J (d) = F і (Ex) J (d) = T
для всіх dVA, тому (xEx) J = F і
(xEx) J = T. Для dVA такого, що d(x),
маємо dT(Ex J ), dF(Ex J ),
dT((Ex & xEx) J ), dF((xEx Ex) J ).
Тому Ex J | IR xEx, xEx J | IR Ex,
Ex & xEx J | IR xEx Ex.
Таким чином.
Твердження 3.
1) P | IR x;
2) x P | IR ;
3) &x P | IR x.
Беручи до уваги теорему 3, отриму-
ємо (тут | – це P | IR , P |T , P | F ,
P |TF , R |TF ):
Теорема 4.
1) | x ;
2) x | ;
3) &x | x .
Для монотонних (еквітонних) преди-
катів маємо (див. [2]):
T(Q) T(xQ) та F(Q) F(xQ),
( ) ( )F xQ F Q та ( ) ( )T xQ T Q .
Звідси отримуємо:
Твердження 4.
RM |= T x та x RM |= F ,
PE | F x та x PE |T .
Відмінність PE |=T та PE |= F засві-
дчує
Теорема 5.
1) & PE |=T x,
x PE |= F &();
2) & PE | F x,
Теоретичні та методологічні основи програмування
27
x PE | T &().
Для Р-предикатів маємо T(Q&Q) =
= F(QQ) = , звідки T(Q&QS) = T(S)
та F(S&(QQ)) = F(S); також маємо
F(Q&QS) F(S) та T(S&(QQ)) T(S).
Враховуючи T(S) T(xS) та F(S) F(xS),
мaємо п. 1, a враховуючи ( ) ( )F xS F S
та ( ) ( )T xS T S , отримуємо п. 2.
Теорема 6.
1) & RM |T x,
x RM | F &();
2) & RM | F x,
x RM |T &().
Для доведення розглянемо приклад.
Приклад 5. & J |T x
та x J | F &( ) .
Маємо ( ) ( )T F VA, звідки
( & ) T ( ) F VA. Проте
T() = F() = , тому )&( T VA та
))&(( F VA. Водночас маємо
T(x) = F(x) = T(x) = F(x) = , зві-
дки отримуємо:
( & )T T(x),
( &( ))F F(x).
Звідси випливає п. 1 теореми 6.
П. 2 теореми 6 випливає з теорем 3
та 5.
Твердження 5.
&x RM |= TF x.
Із RM |= T x та x RM |= F
за монотонністю відношень RM |=T та
RM |= F маємо &x RM |=T x і
&x RM |= F x, звідки отримуємо
&x RM |= TF x.
Беручи до уваги теорему 3, отриму-
ємо (тут |= – це PE |= IR , PE |= T , PE |= F ,
PE |= TF , RM |= T , RM |= F , RM |=TF ):
Теорема 7. &x |= x.
Теорема 8. Маємо
(&)&x
PE
|=TF x&(),
(&)&x RM |T x&(),
(&)&x RM | F x&().
Перше твердження теореми випли-
ває з п. 1 теореми 5 і монотонності відно-
шень
PE
|= T та
PE
|= F .
Маємо x = , xEx = T, xEx = F;
VA =T ( )= T ( )= F ( )=
= T ( ). Нехай ( )&xEx,
xEx& ( ) , ( Ex )&,
xEx& ( ) – це , , , . Тоді
T() =
VA, T()
VA, F()
VA, F() = VA. Тому
( &xEx J|T xEx& ( ),
( Ex)&x J|F xEx& ( ).
Звідси друге та третє твердження теореми.
Для Р-предикатів завжди маємо
T (Q&QS) =T (S) та F(S&(QQ)) = F(S),
тому, згідно теореми 4, отримуємо:
Твердження 6.
& P | IR x, x P | IR &(),
&&x P | IR (x)&().
Враховуючи теорему 3, остаточно
отримуємо:
Теорема 9. Маємо
& | x, x | &(),
(& )&x | x&().
Тут | – це P | IR , P |T , P | F ,
P |TF , R |TF .
Зведемо отримані результати щодо
наявності чи відсутності того чи іншого
логічного наслідку для відповідних пар
формул в таблицю (таблиця).
Теоретичні та методологічні основи програмування
28
В цій таблиці використано такі ско-
рочення (тут |= позначає одне з описаних
відношень):
1 – це & |= ,
2 – це |= ,
3 – це & |= ,
4 – це |= x ,
5 – це x |= ,
6 – це &x |= x,
7 – це & |= x ,
8 – це x |= &(),
9 – це
(& )&x |= x&().
Таблиця. Наявність логічного наслідку для
певних пар формул
1 2 3 4 5 6 7 8 9
P
|= IR + + + – – – – – –
P
|= T + – + – – – – – –
P
|= F – + + – – – – – –
P
|= TF – – + – – – – – –
R
|= TF – – – – – – – – –
PE
|= IR + + + + + + + + +
PE
|= T + – + + – + + – +
PE
|= F – + + – + + – + +
PE
|= TF – – + – – + – – +
RM
|= T – – – + – + – – –
RM
|= F – – – – + + – – –
RM
|= TF – – – – – + – – –
Усі відношення логічного наслідку,
які фігурують в таблиці, виявилися різ-
ними.
Беручи до уваги вищенаведені ре-
зультати, маємо такі співвідношення між
відношеннями логічного наслідку:
Теорема 10.
RM |= TF
RM |=T
PE |= T ,
RM |= TF
RM |= F PE |= F ,
RM |= TF
PE |=TF ;
PE |= TF
PE |=T , PE |= TF
PE |= F ,
PE |= T
PE |= IR , PE |= F PE |= IR ;
R |= TF
RM |=TF , P |= TF
PE |=TF ,
P |=T
PE |= T , P |= F PE |= F ,
P |= IR
PE |= IR ;
R |=TF
P |= TF , P |= TF
P |=T ,
P |= TF
P |= F ,
P |= T
P |= IR , P |= F P |= IR ;
P |=T
P |= F та P |= F P |=T ;
PE |=T
PE |= F та PE |= F
PE |=T ;
відношення RM |= T , RM |= F , PE |=TF не
включаються одне в інше.
Відношення логічного наслідку ін-
дукують відповідні відношення логічної
еквівалентності, вони поширюються на
множини формул.
Відношення логічного наслідку для
множин формул в загальному випадку ло-
гік квазіарних предикатів описано, зокре-
ма, в [2–5]. Дослідження таких відношень
в логіках монотонних і логіках антитонних
предикатів планується продовжити в на-
ступних роботах.
Висновки
Досліджено відношення логічного
наслідку для чистих першопорядкових
композиційно-номінативних логік квазіа-
Теоретичні та методологічні основи програмування
29
рних предикатів. Описано композиційні
предикатні алгебри, мови і класи інтерп-
ретацій (семантики) цих логік, виділено
низку відношень логічного наслідку. Ос-
новну увагу зосереджено на вивченні та-
ких відношень в логіках монотонних пре-
дикатів і логіках антитонних предикатів,
для них визначено 20 відношень логічно-
го наслідку, із яких попарно різними є
PE |= IR , PE |= T , PE |= F , PE |= TF , RM |= T ,
RM |= F , RM |= TF . Наведено приклади, які
засвідчують відмінності одних відношень
від інших, встановлено співвідношення
між різними відношеннями. Результати
щодо наявності чи відсутності того чи ін-
шого відношення логічного наслідку для
певних пар формул зведено в таблицю.
1. Handbook of Logic in Computer Science /
Edited by S. Abramsky, Dov M. Gabbay and
T. S. E. Maibaum. – Oxford University Press,
Vol. 1–5, 1993–2000.
2. Нікітченко М.С., Шкільняк С.С. Приклад-
на логіка. Київ: ВПЦ Київський універси-
тет, 2013. 278 с.
3. Nikitchenko М., Shkilniak S. Semantic
Properties of Logics of Quasiary Predicates.
Workshop on Foundations of Informatics:
Proceedings FOI-2015. Chisinau, Moldova.
P. 180–197.
4. Шкільняк О.С. Відношення логічного нас-
лідку в логіках квазіарних предикатів.
Проблеми програмування. 2016. № 1.
C. 29–43.
5. Нікітченко М.С., Шкільняк О.С., Шкільняк
С.С. Чисті першопорядкові логіки квазіа-
рних предикатів. Проблеми програмуван-
ня. 2016. № 2–3. C. 73–86.
References
1. Abramsky S., Gabbay D. and Maibaum T.
(editors). (1993–2000). Handbook of Logic in
Computer Science. Oxford University Press.
2. Nikitchenko M. and Shkilniak S. (2013).
Applied logic. Кyiv: VPC Кyivskyi
Universytet. (in Ukrainian).
3. Nikitchenko M. and Shkilniak S. (2015).
Semantic Properties of Logics of Quasiary
Predicates. In Workshop on Foundations of
Informatics: Proceedings FOI-2015. Chisinau,
Moldova. P. 180–197.
4. Shkilniak O. (2016). Logical consequence
relations in logics of quasiary predicates. In
Problems in Programming. N 1, P. 29–43.
(in Ukrainian).
5. Nikitchenko M., Shkilniak O. and
Shkilniak S. (2016). Pure first-order logics of
quasiary predicates. In Problems in
Programming. N 2–3, P. 73–86. (in
Ukrainian).
Одержано 22.12.2016
Про автора:
Шкільняк Оксана Степанівна,
кандидат фізико-математичних наук,
доцент, доцент кафедри інформаційних
систем.
Кількість наукових публікацій в
українських виданнях – 81, у тому числі
у фахових виданнях – 30.
Кількість наукових публікацій в
зарубіжних виданнях – 9.
http://orcid.org/0000-0003-4139-2525.
Місце роботи авторa:
Київський національний університет
імені Тараса Шевченка,
01601, Київ, вул. Володимирська, 60.
Тел.: (044) 259 0511, (050) 356 4875.
E-mail: me.oksana@gmail.com
|