Semantic properties of composition nominative modal logics
In this paper composition nominative modal and temporal logics of nominative, quantifier and quantifier-equational levels are studied on the basis of the integrated intentional-extensional approach to construction of systems of logic and software. For such logics, a special refinement of the notion...
Gespeichert in:
| Datum: | 2026 |
|---|---|
| 1. Verfasser: | |
| Format: | Artikel |
| Sprache: | Ukrainisch |
| Veröffentlicht: |
PROBLEMS IN PROGRAMMING
2026
|
| Schlagworte: | |
| Online Zugang: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/977 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Institution
Problems in programming| _version_ | 1867660255527174144 |
|---|---|
| author | Shkilnyak, O.S. |
| author_facet | Shkilnyak, O.S. |
| author_institution_txt_mv | [
{
"author": "O.S. Shkilnyak",
"institution": "Kiev Taras Shevchenko National University"
}
] |
| author_sort | Shkilnyak, O.S. |
| baseUrl_str | https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| collection | OJS |
| datestamp_date | 2026-06-10T11:10:03Z |
| description | In this paper composition nominative modal and temporal logics of nominative, quantifier and quantifier-equational levels are studied on the basis of the integrated intentional-extensional approach to construction of systems of logic and software. For such logics, a special refinement of the notion of composition nominative modal system is introduced, and semantic properties are investigated.Problems in programming 2009; 4: 11-23 |
| first_indexed | 2026-06-11T01:00:17Z |
| format | Article |
| fulltext |
Теоретичні та методологічні основи програмування
11
УДК 681.3.06
О.С. Шкільняк
СЕМАНТИЧНІ ВЛАСТИВОСТІ КОМПОЗИЦІЙНО-
НОМІНАТИВНИХ МОДАЛЬНИХ ЛОГІК
На основі інтегрованого інтенсіонально-екстенсіонального підходу до побудови логічних та програмних
систем вивчаються композиційно-номінативні модальні та темпоральні логіки реномінативного, кван-
торного, кванторно-екваційного рівнів. Для цих логік уточнюється поняття композиційно-номінативної
модальної системи, досліджуються їх семантичні властивості.
Апарат модальних і темпоральних
логік успішно використовується для спе-
цифікації програм та моделювання різно-
манітних предметних областей. Можли-
вості модальних логік та композиційно-
номінативних логік квазіарних предика-
тів [1] поєднують композиційно-номіна-
тивні модальні логіки [2]. Композиційно-
номінативні логіки будуються на основі
інтегрованого інтенсіонально-екстенсіона-
льного підходу [3]. Він базується на спіль-
ному для логіки та програмування компо-
зиційно-номінативному підході [4], розши-
реному принципом інтегрованості інтен-
сіонального та екстенсіонального аспектів.
Застосування його дало змогу побудувати
[1] широкий спектр логічних формалізмів,
що знаходяться на різних рівнях абстракт-
ності та загальності.
На базі інтегрованого інтенсіональ-
но-екстенсіонального підходу в [5] запро-
поноване спеціальне уточнення поняття
композиційно-номінативної модальної си-
стеми, визначені транзиційні та темпо-
ральні модальні системи. В даній роботі
вивчаються композиційно-номінативні мо-
дальні та темпоральні логіки номінативних
рівнів: реномінативного, кванторного,
кванторно-екваційного. Досліджуються се-
мантичні властивості цих логік, зокрема,
відношення логічного наслідку для мно-
жин формул.
Поняття, які не визначаються у ро-
боті, тлумачимо в сенсі [1, 5].
1. Композиційно-номінативні
модальні системи
Поняття композиційно-номінатив-
ної модальної системи (КНМС) [2] є цен-
тральним поняттям композиційно-номіна-
тивної модальної логіки (КНМЛ). В роботі
[5] запропоноване спеціальне уточнення
поняття КНМС. Відмінність визначення
КНМС із [5] від початкового визначення з
[2] полягає у тому, що для логік номі-
нативних рівнів станами світу будуть алге-
браїчні системи.
Композиційно-номінативна модаль-
на система – це об'єкт вигляду M = ((S, R,
Pr, C), Fт, Jт). Тут:
– S – множина станів світу;
– R – множина відношень на станах
світу;
– Pr – множина предикатів на даних
станів світу;
– C – множина композицій на Pr;
– Fm – множина формул мови модаль-
ної логіки;
– Jт – відображення інтерпретації
формул в станах світу.
Множина композицій КНМС визна-
чається базовими загальнологічними ком-
позиціями відповідного рівня та базовими
модальними композиціями.
Важливим випадком КНМС є тран-
зиційні модальні системи (ТМС) [1, 2].
Вони лежать в основі транзиційних
модальних логік (ТМЛ). У межах ТМЛ
природним чином можна розглядати
традиційні [6, 1] модальні логіки (алетичні,
темпоральні, епістемічні тощо).
Для ТМС множина R відношень на
станах світу складається з відношень
вигляду R ⊆ S × S, які природно назвати
відношеннями переходу.
В подальшому будемо розглядати
ТМС, у яких множина R складається з
єдиного бінарного відношення. Слідуючи
© О.С. Шкільняк, 2009
ISSN 1727-4907. Проблеми програмування. 2009. № 4
Теоретичні та методологічні основи програмування
12
[1, 2], таке відношення будемо позначати
як >>>>.
ТМС із єдиним бінарним відно-
шенням >>>> та базовими модальними ком-
позиціями ���� (необхідно) і ���� (можливо)
називають загальними ТМС.
Як і в традиційних алетичних
модальних логіках, композиції ���� і ����
пов'язані наступними співвідношеннями:
¬¬¬¬����Р = ����¬¬¬¬Р та ¬¬¬¬����Р = ����¬¬¬¬Р.
Для загальних ТМС базовою
модальною композицією вважаємо ����. Тоді
���� є похідною, вона визначається через ����
так: ����Р означає ¬¬¬¬����¬¬¬¬Р.
ТMС із єдиним бінарним відно-
шенням на станах >>>> та базовими модаль-
ними композиціями ����↑↑↑↑ (завжди буде), ����↓↓↓↓
(завжди було), ����↑↑↑↑ (колись буде) і ����↓↓↓↓
(колись було) називають [2] темпо-
ральними КНМС, а також темпоральними
ТМС (ТмМС).
Композиції ����↑↑↑↑, ����↓↓↓↓, ����↑↑↑↑, ����↓↓↓↓ нази-
вають базовими часовими композиціями.
Вони пов’язані співвідношеннями:
¬¬¬¬����↑↑↑↑Р = ����↑↑↑↑¬¬¬¬Р; ¬¬¬¬����↓↓↓↓Р = ����↓↓↓↓¬¬¬¬Р;
¬¬¬¬����↑↑↑↑Р = ����↑↑↑↑¬¬¬¬Р; ¬¬¬¬����↓↓↓↓Р = ����↓↓↓↓¬¬¬¬Р.
Для ТмМС вважаємо базовими ком-
позиції ����↑↑↑↑ та ����↓↓↓↓. Тоді композиції ����↑↑↑↑ та
����↓↓↓↓ є похідними, вони визначаються через
базові: ����↑↑↑↑Р означає ¬¬¬¬����↑↑↑↑¬¬¬¬Р; ����↓↓↓↓Р означає
¬¬¬¬����↓↓↓↓¬¬¬¬Р.
Залежно від умов, які накладаються
на відношення >, можна визначати різні
класи загальних ТMС та ТмМС. Для прик-
ладу розглянемо випадки, коли >>>> може
бути рефлексивним, симетричним чи тран-
зитивним.
Якщо >>>> рефлексивне, то в назві
ТМС пишемо символ R; якщо >>>> транзи-
тивне, то – T; якщо >>>> симетричне, то – S.
Таким чином, отримуємо наступні системи:
1) загальних ТMС: R-ТМС, T-ТМС,
S-ТМС, RT-ТМС, RS-ТМС, TS-ТМС,
RTS-ТМС;
2) ТмМС: R-ТмМС, T-ТмМС,
S-ТмМС, RT-ТмМС, RS-ТмМС, TS-ТмМС,
RTS-ТмМС.
Введені поняття можна конкрети-
зувати на різних рівнях абстракції. Зокре-
ма, отримуємо загальні ТМС та ТмМС
пропозиційного, реномінативного, кван-
торного, кванторно-екваційного рівнів.
Композиції КНМС пропозиційного
рівня визначаються базовими модальними
композиціями та базовими пропозицій-
ними композиціями ¬¬¬¬, ∨∨∨∨.
Базовими композиціями КНМС
реномінативного рівня є базові модальні
композиції та базові пропозиційні ком-
позиції ¬¬¬¬ і ∨∨∨∨, до яких додається компо-
зиція реномінації v
xR .
На кванторному рівні додатково
з'являються композиції квантифікації ∃х та
∀х. При цьому дія квантора на предикат в
стані світу обмежена базовими даними
цього стану.
На кванторно-екваційному рівні,
або кванторному з рівністю, можна також
порівнювати значення предметних імен,
використовуючи спеціальні 0-арні
композиції – параметризовані за іменами
предикати рівності =xy.
2. КНМС номінативних рівнів
Для випадку КНМС реномінатив-
ного, кванторного, кванторно-екваційного
рівнів множину станів світу S конкре-
тизуємо як множину неокласичних [1]
алгебраїчних систем вигляду α = (Aα, Prα).
Тут Prα – це множина V-квазіарних екві-
тонних предикатів VAα →{ T, F}.
У цьому випадку
S
Pr Prα
α∈
= U – це
множина предикатів на даних усіх станів
світу.
Множину
S
A Aα
α∈
= U трактуємо як
множину базових даних світу.
Зауважимо, що в початковому ви-
значенні КНМС [2] для логік номінатив-
них рівнів множина станів світу трактує-
ться як іменна множина вигляду VA, де A –
множина базових даних світу. Тоді Pr – це
множина V-квазіарних еквітонних преди-
катів VA →{ T, F}.
Мова КНМЛ кванторного рівня
описується [1, 2] наступним чином.
Теоретичні та методологічні основи програмування
13
Алфавіт мови складається з множи-
ни V предметних імен, множини Ps преди-
катних символiв, символів базових компо-
зицій ¬, ∨, v
xR , ∃x і множини Ms символів
базових модальних композицій.
Множину Ms називають модальною
сигнатурою КНМС.
Множину Fт формул мови КНМЛ
кванторного рівня визначаємо індуктивно:
1) кожний p∈Ps є формулою, такi
формули назвемо атомарними;
2) нехай Φ та Ψ – формули, тодi ¬Φ
та ∨ΦΨ – формули;
3) нехай Φ – формула, тодi v
xR Φ –
формула;
4) нехай Φ – формула, тодi ∃xΦ –
формула.
5) нехай Φ – формула, � – символ
базової модальної композиції, тодi �Φ –
формула.
Для випадку загальних ТМС п. 5
уточнюється так:
5�) нехай Φ – формула, тодi �Φ –
формула.
Для випадку темпоральних КНМС
п. 5 уточнюється так:
5�↑↓) нехай Φ – формула, тодi �↑Φ
та �↓Φ – формули.
Для кожного p∈Ps визначається [1]
множина синтетично неістотних пред-
метних імен за допомогою тотального
відображення µ : Ps→2V, яке продовжуємо
до µ : Fт→2V.
Пару σ = (Ps, µ) називають сигна-
турою синтетичної неістотності кванторної
КНМС.
Тип кванторної КНМС визначається
її модальною сигнатурою Ms, однотипні-
стю відношень із R для кожного �∈Ms та
сигнатурою синтетичної неістотності.
Задамо відображення інтерпретації
атомарних формул на світах I : Рs × S →Pr.
При цьому I(p, α) ∈ Prα.
Продовжимо I до Jт : Fт × S →Pr.
При цьому Jт(Φ, α) ∈ Prα.
1) Jт(p, α) = I(p, α) для всіх p∈Ps;
2) Jт(¬Φ, α) = ¬¬¬¬(Jт(Φ, α));
Jт(∨ΦΨ, α) = ∨∨∨∨(Jт(Φ, α), Jт(Ψ, α));
3) Jm( ,v
xR Φ α) = v
xR (Jm(Φ, α));
4) Jт(∃xΦ, α)(d) =
, якщо існує : ( , )( ) ,
, якщо ( , )( ) для всіх ,
невизначене в усіх інших випадках.
T a A Jm d x a T
F Jm d x a F a A
α
α
∈ Φ α ∇ == Φ α ∇ = ∈
a
a
Звідси для формул вигляду ∀xΦ
отримуємо
Jт(∀xΦ, α)(d) =
, якщо ( , )( ) для всіх ,
, якщо існує : ( , )( ) ,
невизначене в усіх інших випадках.
T Jm d x a T a A
F a A Jm d x a F
α
α
Φ α ∇ = ∈= ∈ Φ α ∇ =
a
a
5) Значення Jт(�Φ, α)(d) визначає-
ться значеннями Jт(Φ, δ)(d) для певних
станів δ, таких, що α та δ перебувають у
відповідних пов'язаних із ���� відношеннях
з R.
Для випадку загальних ТМС п. 5
уточнюється так:
5�) для кожних α∈S та d∈VAα ви-
значимо
Jт(�Φ, α)(d) =
, якщо ( , )( ) для всіх : ,
, якщо існує : та ( , )( ) ,
невизначене в усіх інших випадках.
T Jm d T S
F S Jm d F
Φ δ = δ∈ α δ= δ∈ α δ Φ δ =
>
>
Звідси отримуємо
Jт(����Φ, α)(d) =
, якщо ( , )( ) для всіх : ,
, якщо існує : та ( , )( ) ,
невизначене в усіх інших випадках.
F Jm d F S
T S Jm d T
Φ δ = δ∈ α δ= δ∈ α δ Φ δ =
>
>
Для випадку темпоральних КНМС
п. 5 уточнюється так:
5�↑↓) для кожних α∈S та d∈VAα ви-
значимо
Jт(�↑Φ, α)(d) =
, якщо ( , )( ) для всіх : ,
, якщо існує : та ( , )( ) ,
невизначене в усіх інших випадках.
T Jm d T S
F S Jm d F
Φ δ = δ∈ α δ= δ∈ α δ Φ δ =
>
>
Jт(�↓Φ, α)(d) =
, якщо ( , )( ) для всіх : ,
, якщо існує : та ( , )( ) ,
невизначене в усіх інших випадках.
T Jm d T S
F S Jm d F
Φ δ = δ∈ δ α= δ∈ δ α Φ δ =
>
>
Звідси отримуємо
Jт(����↑Φ, α)(d) =
, якщо ( , )( ) для всіх : ,
, якщо існує : та ( , )( ) ,
невизначене в усіх інших випадках.
F Jm d F S
T S Jm d T
Φ δ = δ∈ α δ= δ∈ α δ Φ δ =
>
>
Jт(����↓Φ, α)(d) =
, якщо ( , )( ) для всіх : ,
, якщо існує : та ( , )( ) ,
невизначене в усіх інших випадках.
F Jm d F S
T S Jm d T
Φ δ = δ∈ δ α= δ∈ δ α Φ δ =
>
>
Теоретичні та методологічні основи програмування
14
Предикат Jт(Φ, α), який є значен-
ням формули Φ у стані α, будемо позна-
чати Φα.
Формула Φ істинна в стані α, якщо
Φα – істинний предикат. Це позначаємо
α |= Φ.
Формула Φ істинна в КНМС M,
якщо для кожного α∈S предикат Φα є
істинним. Це позначаємо M |= Φ.
Формула Φ всюди істинна, якщо
M |= Φ для всіх КНМС M одного типу.
Те, що формула Φ всюди істинна,
позначаємо |= Φ.
Алфавіт мови КНМЛ реномінатив-
ного рівня складається з множини V пред-
метних імен, множини Ps предикатних
символiв, символів базових композицій ¬,
∨, v
xR і символів базових модальних ком-
позицій. Множина Fт формул мови такої
логіки визначається індуктивно (див.
пп. 1–3 і 5 визначення мови КНМЛ кван-
торного рівня).
Відображення I : Ps × S → Pr про-
довжується до Jт : Fm × S → Pr так, як і
для кванторного рівня (див. пп. 1–3, 5).
При цьому Jт(Φ, α) ∈ Prα.
Загальні ТМС та ТмМС реноміна-
тивного рівня визначаються аналогічно
загальним ТМС та ТмМС кванторного рів-
ня, вилучаючи при цьому пункт для ∃xΦ.
Поняття типу КНМС, істинної в
стані формули, істинної в КНМС формули
та всюди істинної формули на реномі-
нативному рівні визначаємо так, як на
кванторному рівні.
На кванторно-екваційному рівні
з’являються спеціальні 0-арні композиції –
предикати рівності =xy, які визначаються
[7] наступним чином.
Для кожного d∈V
А покладемо
=ху(d) =
=
, якщо ( ) , ( ) та ( ) ( );
, якщо ( ) , ( ) та ( ) ( );
невизначене, якщо ( ) або ( ) .
T d x d y d x d y
F d x d y d x d y
d x d y
↓ ↓ =
↓ ↓ ≠
↑ ↑
Множиною неістотних для =ху пред-
метних iмен є множина V \{ х, у }.
Алфавіт мови КНМЛ кванторно-
екваційного рівня: множина V предметних
імен, множина Ps предикатних символiв,
символи базових композицій ¬, ∨, v
xR , ∃x,
=xy та множина Ms символів базових мо-
дальних композицій – модальна сигнатура.
Множина Fт формул мови КНМЛ
кванторно-екваційного рівня визначається
індуктивно згідно пп. 2–5 визначення мови
КНМЛ кванторного рівня та п. 1E:
1E) кожний p∈Ps та кожний символ
=ху є формулою. Такi формули атомарні.
Для кожного p∈Ps визначається
множина його синтетично неістотних пред-
метних імен за допомогою тотального
відображення µ : Ps→2V. Таке відображен-
ня продовжується до µ : Fт→2V аналогічно
[1] випадку КНМЛ кванторного рівня, дода-
ючи µ(=ху) = V \{ х, у}.
Задамо відображення інтерпретації
атомарних формул на світах I : Рs × S →Pr.
При цьому I(p, α) ∈ Prα та I(=ху) = =ху для
всіх х, у∈V.
Відображення I продовжимо до
Jт : Fт × S →Pr так, як це зроблено для
випадку КНМС кванторного рівня,
додаючи при цьому пункт для =ху:
Jт(=ху, α) = I(=ху, α).
Загальні ТМС та ТмМС кванторно-
екваційного рівня визначаємо аналогічно
кванторному рівню, додаючи при цьому
пункт для =ху.
Поняття типу КНМС, істинної в
стані формули, істинної в КНМС формули
та всюди істинної формули на кванторно-
екваційному рівні визначаємо так, як на
кванторному рівні.
3. КНМС із сильною умовою
визначеності на станах
Нехай із Φδ(d)↓ випливає d∈VAδ.
Тоді із (�Φ)α(d) = T випливає d∈VAδ для
всіх δ таких, що α>>>>δ. Це означає, що
об’єкти не можуть зникати при переході
до стану-наступника.
КНМС, в яких із Φδ(d)↓ випливає
d∈VAδ, назвемо КНМС з сильною умовою
визначеності на станах. У таких КНМС
умова Φδ(d)↓ спонукає умову d∈VAδ, тобто
при d∉VAδ маємо Φδ(d)↑. Це веде до
порушення умови еквітонності.
ТМС з сильною умовою визначено-
сті назвемо St-ТМС.
Теоретичні та методологічні основи програмування
15
Приклад 1.
Задамо загальну St-ТМС M таким
чином. Нехай S = { α, β}, Aα = { a, b},
Aβ = { b}, R = { α>>>>β}. Нехай d = [xab],
d’ = [xab, yaa]. Задамо тепер pα(d) = T,
pα(d’) = T, pβ(d) = T.
Нехай предикати pα та pβ еквітонні.
Згідно d’∉VAβ маємо pβ(d’)↑, звідки d ⊂ d’,
(�p)α(d) = T та (�p)α(d’)↑, що суперечить
еквітонності предиката (�p)α.
Таким чином, модальні композиції
St-ТМС не зберігають еквітонність, проте
вони зберігають слабшу умову, яку наз-
вемо слабкою еквітонністю.
Функція Q на D слабко еквітонна,
якщо для довільних d, d’∈D таких, що
d ⊆ d’, із умов Q(d)↓ та Q(d’)↓ випливає
Q(d) = Q(d’).
Приклад 2.
Слабко еквітонна функція (зокрема,
предикат) не завжди продовжується до
еквітонної. Справді, нехай A = {0}, а для
Q : VA →{ T, F} маємо Q([xa0]) = T,
Q([ya0]) = F, Q([xa0, ya0])↑, причому для
Q неістотні всі імена, окрім x та y. Тоді Q
не можна продовжити до еквітонного, хоча
слабка еквітонність для Q виконується.
Теорема 1. Композиція � зберігає
слабку еквітонність.
Нехай предикат Φα слабко еквітон-
ний та для кожного β такого, що α>>>>β,
предикат Φβ слабко еквітонний. Нехай
d, d’∈VAα, d ⊆ d’, (�Φ)α(d)↓ та (�Φ)α(d’)↓.
Припустимо супротивне: (�Φ)α(d) ≠
≠ (�Φ)α(d’). Можливі два випадки.
Нехай (�Φ)α(d) = T і (�Φ)α(d’) = F.
Друге означає, що для деякого β такого,
що α>>>>β, маємо Φβ(d’) = F. Перше означає,
що для кожного γ, такого, що α>>>>γ, маємо
Φγ(d) = T. Але це вірно і для стану β, тобто
Φβ(d) = T. Маємо d ⊆ d’, Φβ(d) = T та
Φβ(d’) = F, що суперечить умові слабкої
еквітонності для Φβ.
Нехай (�Φ)α(d) = F і (�Φ)α(d’) = T.
Перше означає, що для деякого β такого,
що α>>>>β, маємо Φβ(d) = F. Друге означає,
що для кожного γ, такого, що α>>>>γ, маємо
Φγ(d’) = T. Але це вірно і для стану β,
тобто Φβ(d’) = T. Маємо d ⊆ d’, Φβ(d) = F та
Φβ(d’) = T, що суперечить умові слабкої
еквітонності для Φβ.
Обидва випадки привели до супе-
речності. Отже, предикат (�Φ)α слабко
еквітонний.
Немодальні базові композиції збері-
гають [1] еквітонність, тому вони зберіга-
ють і слабку еквітонність. Звідси маємо як
наслідок: базові композиції загальних
ТМС зберігають слабку еквітонність.
Приклад 3.
У випадку загальних St-ТМС
можливо (�Φ)α(d ||–y) = T та (�Φ)α(d)↑.
Задамо загальну St-ТМС M таким
чином. Нехай S = { α, β}, Aα = { a, b},
Aβ = { b}, R = { α>>>>β}. Нехай d = [xab, yaa].
Тоді d ||–y = [xab]. Задамо pα([xab]) = T,
pα([xab, yaa]) = T, pβ([xab]) = T. Звідси
(�p)α([xab]) = T, (�p)α([xab, yaa])↑,
тобто взявши Φ як p, маємо (�Φ)α(d)↑,
(�Φ)α(d ||–y) = T.
Аналогічно показуємо, що можливо
(� )y
xR αΦ (d ||– y) = T та (� )y
xR αΦ (d)↑.
Водночас неважко переконатись,
що в композиційно-номінативних логіках
для довільних Q та d справджується
y
xR Q(d ||– y) = y
xR Q(d). Зокрема, в загальних
ТМС завжди ( y
xR �Φ)α(d ||– y) = ( y
xR �Φ)α(d).
Покажемо, що у випадку загальних
St-ТМС номінативних рівнів справджу-
ється
Теорема 2. Для довільних α, Φ та
d∈VAα виконується v
xR �Φ(d) = �
v
xR Φ(d).
Тут рівність розуміємо як строгу.
Розглянемо всі можливі випадки.
1. Нехай ( v
xR �Φ)α(d) = F. Тоді
(�Φ)αd∇vad(x)) = F, звідки для деякого
стану β∈S, такого, що α>>>>β, маємо
Φβ(d∇vad(x)) = F. Але із (� v
xR Φ)α(d) = T
випливає, що для такого β необхідно
( v
xR Φ)β(d) = T, звідки Φβ(d∇vad(x)) = T.
Отримали суперечність. Із (� v
xR Φ)α(d)↑
Теоретичні та методологічні основи програмування
16
випливає, що для кожного γ, такого, що
α>>>>γ, неможливо ( v
xR Φ)γ(d) = F, тому немо-
жливо Φγ(d∇vad(x)) = F, звідки неможли-
во Φβ(d∇vad(x)) = F. Знову суперечність.
Нехай (� v
xR Φ)α(d) = F. Тоді для
деякого стану β∈S, такого, що α>>>>β, маємо
( v
xR Φ)β(d) = F, звідки Φβ(d∇vad(x)) = F.
Але із ( v
xR �Φ)α(d) = T випливає, що
(�Φ)αd∇vad(x)) = T, тому для такого β
необхідно Φβ(d∇vad(x)) = T. Маємо
суперечність. Із ( v
xR �Φ)α(d)↑ випливає
(�Φ)αd∇vad(x))↑, тому для кожного γ,
такого, що α>>>>γ, неможливо Φγ(d∇vad(x)) = F,
звідки неможливо Φβ(d∇vad(x)) = F. Знову
суперечність.
Таким чином, ( v
xR �Φ)α(d) = F ⇔
⇔ (� v
xR Φ)α(d) = F.
2. Нехай ( v
xR �Φ)α(d) = T. Якщо
(� v
xR Φ)α(d)↑, то для кожного γ такого, що
α>>>>γ, неможливо ( v
xR Φ)γ(d) = F, причому
( v
xR Φ)β(d)↑ хоч для одного β, такого, що
α>>>>β, звідки для такого β маємо
Φβ(d∇vad(x))↑. Але з ( v
xR �Φ)α(d) = T
отримуємо (�Φ)α(d∇vad(x)) = T, тому для
такого β мусить бути Φβ(d∇vad(x)) = T.
Маємо суперечність.
Неможливість ( v
xR �Φ)α(d) = T та
(� v
xR Φ)α(d) = F була показана раніше.
Нехай (� v
xR Φ)α(d) = T. Якщо
( v
xR �Φ)α(d)↑, то (�Φ)α(d∇vad(x))↑, тому
для кожного γ, такого, що α>>>>γ, неможливо
Φγ(d∇vad(x)) = F, причому Φβ(d∇vad(x))↑
хоч для одного β, такого, що α>>>>β. Але з
(� v
xR Φ)α(d) = T для такого β маємо
( v
xR Φ)β(d) = T, звідки Φβ(d∇vad(x)) = T.
Маємо суперечність.
Неможливість (� v
xR Φ)α(d) = T та
( v
xR �Φ)α(d) = F вже показана раніше.
Таким чином, ( v
xR �Φ)α(d) = T ⇔
⇔ (� v
xR Φ)α(d) = T.
Отримали ( v
xR �Φ)α(d) = (�
v
xR Φ)α(d),
що й доводить теорему.
Наслідок 1. Для довільних α, Φ та
d∈VAα виконується v
xR ����Φ(d) = ����
v
xR Φ(d).
Наслідок 2. Для довільних α та Φ
виконується:
1) α |= v
xR �Φ ↔ �
v
xR Φ та
α |= v
xR ���� Φ ↔ ����
v
xR Φ;
2) α |= v
xR �Φ ⇔ α |= �
v
xR Φ та
α |= v
xR ����Φ ⇔ α |= ����
v
xR Φ.
Наслідок 3. Для загальних St-ТМС
маємо M |= v
xR �Φ ↔ �
v
xR Φ та
M |= v
xR ����Φ ↔����
v
xR Φ.
Наслідок 4. Формули
v
xR �Φ ↔ �
v
xR Φ та v
xR ����Φ ↔����
v
xR Φ
всюди істинні.
Теорема 3. Для загальних St-ТМС
маємо:
1) M |= ∃x�Φ→�∃xΦ;
2) M |= �∀xΦ→∀x�Φ.
Доводимо п. 1. Доведення п. 2 про-
водиться аналогічно.
Припустимо супротивне: для
деяких α∈S та d∈VAα маємо
(∃x�Φ)α(d) = T та (�∃xΦ)α(d) = F. Друга
умова означає, що для деякого стану β∈S
такого, що α>>>>β, маємо (∃xΦ)β(d) = F.
Перша умова означає, що для деякого
а∈Aα маємо (�Φ)α(d∇xaa) = T, тому для
кожного стану γ∈S такого, що α>>>>γ, маємо
Φγ(d∇xaa) = T. Зокрема, для стану β
маємо: Φβ(d∇xaa) = T для деякого а∈Aα. Із
визначеності Φβ(d∇xaa) випливає
d∇xaa∈VAβ, звідки a∈Aβ. Але із
(∃xΦ)β(d) = F випливає: Φβ(d∇xab) = F для
всіх b∈Aβ. Згідно a∈Aβ це вірно для a, тому
Φβ(d∇xaa) = F. Отримали суперечність.
Наслідок 5. Формули ∃x�Φ→�∃xΦ,
�∀xΦ→∀x�Φ, �∀xΦ→∀x�Φ та
∃x�Φ→�∃xΦ усюди істинні.
Теоретичні та методологічні основи програмування
17
4. КНМС із загальною умовою
визначеності на станах
Будемо вважати, що d∈VAδ не є
обов’язковим для Φδ(d)↓. Для цього при
d∉VAδ задамо Φδ(d) = Φδ(d∩VAδ). ТМС із
такою загальною умовою визначеності на-
звемо Gn-ТМС.
Теорема 4. Для випадку загальних
Gn-ТМС композиція � зберігає еквітон-
ність.
Нехай предикат Φα еквітонний та
для кожного β, такого, що α>>>>β, предикат
Φβ еквітонний. Нехай d, d’∈VAα, d ⊆ d’ та
(�Φ)α(d)↓. Можливі два випадки.
Нехай (�Φ)α(d) = F. Тоді для деяко-
го β, такого, що α>>>>β, маємо Φβ(d∩VAβ) = F.
При d ⊆ d’ маємо d∩VAβ ⊆ d’∩VAβ, тому
Φβ(d’∩VAβ) = F за еквітонністю Φβ, звідки
(�Φ)α(d’) = F.
Нехай (�Φ)α(d) = T. Тоді для
кожного γ, такого, що α>>>>γ, маємо
Φγ(d∩VAγ) = T. При умові d ⊆ d’ маємо
d∩VAγ ⊆ d’∩VAγ, тому за еквітонністю Φγ
маємо Φγ(d’∩VAγ) = T. Це вірно для
кожного γ, такого, що α>>>>γ, звідки
(�Φ)α(d’) = T.
Отже, предикат (�Φ)α еквітонний.
Наслідок 6. Базові композиції за-
гальних Gn-ТМС зберігають еквітонність.
Для загальних Gn-ТМС справджу-
ється твердження, аналогічне теоремі 2.
Теорема 5. Для довільних α, Φ та
d∈VAα виконується v
xR �Φ(d) = �
v
xR Φ(d).
Спочатку сформулюємо технічне
твердження, яке доводиться на основі
визначень.
Лема. Для довільних β та d∈VAα
(d∩VAβ)∇v a(d∩VAβ)( x ) = (d∇v ad( x ))∩VAβ.
Доводимо теорему 5. Припустимо
супротивне: для деяких α∈S, d∈VAα та Φ
маємо ( v
xR �Φ)α(d) ≠ (�
v
xR Φ)α(d).
Розглянемо всі можливі випадки.
Нехай (� v
xR Φ)α(d) = F. Це означає,
що для деякого β∈S, такого, що α>>>>β,
маємо ( v
xR Φ)β(d∩VAβ) = F, звідки отримуємо
Φβ((d∩VAβ)∇v a(d∩VAβ)( x )) = F. Згідно леми
(d∩VAβ)∇v a(d∩VAβ)( x ) = (d∇v ad( x ))∩VAβ,
звідки Φβ((d∇v ad( x ))∩VAβ) = F.
Якщо ( v
xR �Φ)α(d) = T, то маємо
(�Φ)α(d∇ v ad( x )) = T, звідки для такого
β отримуємо Φβ((d∇ v ad( x ))∩VAβ) = T –
суперечність. Якщо ( v
xR �Φ)α(d)↑, то
маємо (�Φ)α(d∇ v ad( x ))↑. Це означає,
що для кожного γ такого, що α>>>>γ,
неможливо Φγ((d∇ v ad( x ))∩VAγ) = F,
адже тоді (�Φ)α(d∇v ad( x )) = F. Згідно
α>>>>β, це вірно, зокрема, і для стану β, тобто
неможливо Φβ((d∇ v ad( x ))∩VAβ) = F.
Знову отримали суперечність.
Таким чином, (� v
xR Φ)α(d) = F ⇔
⇔ ( v
xR �Φ)α(d) = F.
Нехай (� v
xR Φ)α(d) = T. Немож-
ливим є ( v
xR �Φ)α(d) = F, адже тоді
(� v
xR Φ)α(d) = F. Нехай ( v
xR �Φ)α(d)↑, тоді
(�Φ)α(d∇ v ad( x ))↑.
Згідно (� v
xR Φ)α(d) = T для кожного
γ, такого, що α>>>>γ, маємо ( v
xR Φ)γ(d∩VAγ) = T,
тому Φγ((d∩VAγ)∇ v a(d∩VAγ)( x )) = T. Але
згідно леми (d∩VAγ)∇ v a(d∩VAγ)( x ) =
= (d∇ v ad( x ))∩VAγ, звідки для кожного γ,
такого, що α>>>>γ, отримуємо
Φγ((d∇ v ad( x ))∩VAγ) = T. Це суперечить
умові (�Φ)α(d∇ v ad( x ))↑. Отже, якщо
(� v
xR Φ)α(d) = T, то ( v
xR �Φ)α(d) = T.
Нехай ( v
xR �Φ)α(d) = T. Неможли-
вим є (� v
xR Φ)α(d) = F, адже згідно вище-
доведеного тоді ( v
xR �Φ)α(d) = F. Нехай
(� v
xR Φ)α(d)↑, тоді ( v
xR Φ)β(d∩VAβ)↑ хоча б
для одного β, такого, що α>>>>β, звідки
Φβ((d∩VAβ)∇v a(d∩VAβ)( x ))↑. Але згідно
леми маємо (d∩VAγ)∇ v a(d∩VAγ)( x ) =
= (d∇ v ad( x ))∩VAγ, звідки отримуємо
Φβ((d∇v ad( x ))∩VAβ)↑.
Із умови ( v
xR �Φ)α(d) = T маємо
(�Φ)α(d∇ v ad( x )) = T, звідки для такого
Теоретичні та методологічні основи програмування
18
стану β маємо Φβ((d∇ v ad( x ))∩VAβ) = T
Отримали суперечність. Отже, якщо
( v
xR �Φ)α(d) = T, то (� v
xR Φ)α(d) = T.
Таким чином, (� v
xR Φ)α(d) = T ⇔
⇔ ( v
xR �Φ)α(d) = T.
Отже, ( v
xR �Φ)α(d) = (�
v
xR Φ)α(d),
що завершує доведення теореми.
Як наслідок теореми 5, для Gn-ТМС
отримуємо твердження, вищесформульо-
вані як наслідки 1–4.
Таким чином, символи реномінації
можна проносити через символи модаль-
них композицій, що за умови нескінчен-
ності множини тотально неістотних імен
[1] дає змогу перетворити формулу до
класичноподібного вигляду, коли символи
реномінації застосовні тільки до символів
базових предикатів.
Для випадку Gn-ТМС справджує-
ться твердження, аналогічне теоремі 3.
Теорема 6. Для загальних Gn-ТМС
маємо
1) M |= ∃x�Φ→�∃xΦ;
2) M |= �∀xΦ→∀x�Φ.
Доведемо п. 2. Доведення п. 1
проводиться аналогічно.
Припустимо супротивне: для
деяких α∈S та d∈VAα маємо
(�∀xΦ)α(d) = T та (∀x�Φ)α(d) = F. Друга
умова означає, що для деякого а∈Aα маємо
(�Φ)α(d∇xaa) = F, тому для деякого
стану β∈S, такого, що α>>>>β, маємо
Φβ((d∇xaa)∩VAβ) = F.
Згідно (�∀xΦ)α(d) = T для такого
стану β маємо (∀xΦ)β(d∩VAβ) = T, звідки
Φβ((d∩VAβ)∇xab) = T для всіх b∈Aβ.
Розглянемо два випадки.
Нехай a∈Aβ. Тоді маємо
(d∇xaa)∩VAβ) = (d∩VAβ)∇xaa, звідки
Φβ((d∇xaa)∩VAβ) = Φβ((d∩VAβ)∇xaa) = F.
Але Φβ((d∩VAβ)∇xab) = T для всіх b∈Aβ,
зокрема, для стану a∈Aβ маємо
Φβ((d∩VAβ)∇xaa) = T – суперечність.
Нехай a∉Aβ. Тоді отримуємо
(d∇xaa)∩VAβ) = (d∩VAβ)||–x, звідки маємо
Φβ((d∇xaa)∩VAβ) = Φβ((d∩VAβ)||–x) = F. Але
(d∩VAβ)||–x ⊂ (d∩VAβ)∇xab для кожного
b∈Aβ , звідки за еквітонністю Φβ маємо
Φβ((d∩VAβ)∇xab) = F. Це суперечить
умові Φβ((d∩VAβ)∇xab) = T для всіх b∈Aβ.
Наслідок 7. Формули ∃x�Φ→�∃xΦ,
�∀xΦ→∀x�Φ, �∀xΦ→∀x�Φ та
∃x�Φ→�∃xΦ є всюди істинними.
Приклад 4. Формули �∃xΦ→∃x�Φ
та ∀x�Φ→�∀xΦ не є всюди істинними.
Побудуємо загальну ТМС, в якій
спростовується формула �∃xΦ→∃x�Φ.
Нехай S = { α, β}, R = { α>>>>β}, Aα = { a},
Aβ = { a, b}. Візьмемо ПС р, для якого
неістотні всі імена, окрім x. Задамо
рα([xaa]) = F, рβ([xaa]) = F, рβ([xab]) = T.
Тоді (�р)α([xaa]) = F, звідки згідно
Aα = { a} маємо (∃x�р)α([xaa]) = F Згідно
рβ([xab]) = T отримуємо (∃x р)β([xaa]) = T,
звідки (�∃x р)α([xaa]) = T.
Отже, (�∃x р→∃x�р)α([xaa]) = F,
тому α |≠(�∃x р→∃x�р.
Загальну ТМС, в якій спросто-
вується формула ∀x�Φ→�∀xΦ, будуємо
аналогічно, з тією лише відмінністю, що
задамо рα([xaa]) = T, рβ([xaa]) = T,
рβ([xab]) = F. Тоді (∀x р)β([xaa]) = F,
звідки (�∀x р)α([xaa]) = F. Згідно
R = { α>>>>β} із рβ([xaa]) = T випливає
(�р)α([xaa]) = T. Згідно Aα = { a} звідси
отримуємо (∀x�р)α([xaa]) = T.
Отже, (∀x�р→�∀x р)α([xaa]) = F,
звідки α |≠∀x�р→�∀x р.
Звідси як наслідок: формули
∀x�Φ→�∀xΦ та �∃xΦ→∃x�Φ не є
всюди істинними.
Зауваження. �∀xΦ→∀x�Φ – це
конверсія формули ∀x�Φ→�∀xΦ, відо-
мої як формула Баркан. Як показує прик-
лад 4, формула Баркан не є всюди істин-
ною. Згідно наслідку теореми 6 конверсія
формули Баркан істинна в кожній загаль-
ній КМС. Водночас конверсія формули
Баркан спростовується [8] на деяких реля-
ційних моделях алетичної модальної логі-
ки. Проте суперечності тут немає, адже ми
розглядаємо часткові предикати. При
умові d∉VAβ в реляційній моделі тради-
ційної модальної логіки значення Φβ(d)
вважається хибним. У нас для випадку
Теоретичні та методологічні основи програмування
19
St-ТМС при d∉VAβ значення Φβ(d)
вважається невизначеним, а для випадку
Gn-ТМС при d∉VAβ значення
Φβ(d) = Φβ(d∩VAβ) може бути як невизна-
ченим, так і визначеним, причому як
істинним, так і хибним.
5. ТМС кванторно-екваційного
рівня
Семантичні властивості ТМС кван-
торно-екваційного рівня успадковують
властивості ТМС кванторного рівня. Наве-
демо тепер нові властивості, пов'язані з
рівністю. У першу чергу, це відомі [7]
загальнологічні властивості, притаманні як
КНМЛ, так і композиційно-номінативним
логікам квазіарних предикатів.
Rf) рефлексивність: |= =хх ;
Sm) cиметричність: |= =xy ↔ =yx ;
Tr) транзитивність: |= =xy → =yz → =xz;
EΦ) |=
1 1x y= → … →
n nx y= →
→( 1
1
,..., ,
,..., ,
n
n
z z u
x x vR Φ ↔ 1
1
,..., ,
,..., ,
n
n
z z u
y y vR Φ ).
Неважко переконатись, що для
довільних Q та d∈VA за умови d(x) = d(y)
маємо ( )x
yR Q d = ( )y
xR Q d = Q(d). Зокрема,
( )x
yR Q d = ( )y
xR Q d = Q(d) за умови =xy(d) = T.
Аналогічно за умови d(x) = d(y) маємо
, ,
, ,( ) ( ) ( )y u x u u
x v y v vR Q d R Q d R Q d= = .
Звідси отримуємо такі властивості
рівності:
ER) |= =xy → ( )x
yR Φ ↔ Φ та
|= =xy → ,
,( )x u u
y v vR RΦ ↔ Φ ;
|= =xy → ( )x y
y xR RΦ ↔ Φ та
|= =xy → , ,
, ,( )y u x u
x v y vR RΦ ↔ Φ .
Замість =xy будемо надалі також тра-
диційно писати x = y.
Зауважимо, що вибране нами
трактування рівності як тотожності веде до
того, що для одного і того ж даного d
неможливо в одному стані d(x)↓ = d(y)↓, а
в іншому – d(x)↓ ≠ d(y)↓.
Для загальних St-ТМС і Gn-ТМС
справджуються такі властивості, пов’язані
з рівністю.
Твердження 1. x = y → � x = y –
всюди істинна формула.
Припустимо супротивне: для
деяких α∈S та d∈VAα маємо (x = y)α(d) = T
та (� x = y)α(d) = F. Друга умова означає,
що для деякого стану β∈S, такого, що
α>>>>β, маємо (x = y)β(d) = F. Звідси випливає
d(x)↓, d(y)↓ та d(x) ≠ d(y). Із визначеності
(x = y)α(d) випливає d(x)∈Aα та d(y)∈Aα,
Тоді d(x) ≠ d(y) дає (x = y)α(d) = F. Отримали
суперечність.
Твердження 2. � x = y → x = y –
всюди істинна формула.
Припустимо супротивне: для
деяких α∈S та d∈VAα маємо
(� x = y)α(d) = T та (x = y)α(d) = F. Друга
умова означає, що d∈VAα, d(x)↓, d(y)↓ та
d(x) ≠ d(y). Умова (� x = y)α(d) = T означає,
що для всіх β∈S, таких, що α>>>>β, маємо
(x = y)β(d) = T. Візьмемо деякий такий стан
β. Тоді маємо d(x)↓, d(y)↓ та d(x) = d(y).
Отримали суперечність.
Наслідок 8. x = y ↔ � x = y – всюди
істинна формула.
Твердження 3. Неможливо α |= x = y
та α |≠ � x = y.
Припустимо супротивне: α |= x = y
та (� x = y)α(d)↓ = F для деякого d∈VAα.
Але (� x = y)α(d) = F означає, що для
деякого стану β∈S, такого, що α>>>>β, маємо
(x = y)β(d) = F. Звідси випливає d(x)↓, d(y)↓
та d(x) ≠ d(y). Згідно d∈VAα звідси d(x)∈Aα,
d(y)∈Aα та d(x) ≠ d(y), що дає (x = y)α(d) = F.
Отримали суперечність із α |= x = y.
Твердження 4. Можливо α |≠ x = y
та α |= � x = y.
Умова α |≠ x = y означає: для
деякого d∈VAα маємо (x = y)α(d) = F, звідки
d(x)↓, d(y)↓ та d(x) ≠ d(y). Побудуємо
загальну ТМС, в якій для деякого стану α
маємо α |= � x = y та α |≠ x = y. Нехай
S = { α, β}, де Aα = {0, 1}, Aβ = {1}. Нехай
R = { α>>>>β}. Тоді для d∈{0, 1} { x, y} маємо:
Теоретичні та методологічні основи програмування
20
якщо den (d) = {1}, то (x = y)α(d) = T та
(x = y)β(d) = T; якщо den(d) = {0}, то
(x = y)α(d) = T та (x = y)β(d)↑; якщо
den(d) = {0, 1}, то (x = y)α(d) = F та
(x = y)β(d)↑.
Враховуючи неістотність для x = y
всіх предметних імен, відмінних від x та y,
звідси α |= � x = y та α |≠ x = y.
Зауважимо, що α |= � x = y можливе
вже при неіснуванні станів, досяжних із α,
тоді (� x = y)α(d)↑ для всіх d∈VAα.
6. Темпоральні КНМС
Як і для випадку загальних ТМС,
можна розглядати темпоральні КНМС із
сильною умовою та загальною умовою
визначеності на станах, які назвемо
St-ТмМС та Gn-ТмМС.
Твердження теореми 4 переносить-
ся на випадок Gn-ТмМС.
Теорема 7. У випадку Gn-ТмМС
композиції �↑ та �↓ зберігають еквітон-
ність.
Наслідок 9. Базові композиції
Gn-ТмМС зберігають еквітонність.
Вищенаведені властивості загальних
ТМС переносяться на випадок темпораль-
них КНМС. Зокрема, для St-ТмМС та
Gn-ТмМС справджуються твердження:
Теорема 8. Для довільних Φ, α,
d∈VAα виконується v
xR �↑Φ(d) = �↑
v
xR Φ(d)
та v
xR �↓Φ(d) = �↓
v
xR Φ(d).
Наслідок 10. Для довільних Φ, α,
d∈VAα виконується v
xR ����↑Φ(d) = ����↑
v
xR Φ(d)
та v
xR ����↓Φ(d) = ����↓
v
xR Φ(d).
Наслідок 11. Для довільних α та Φ
виконується:
1) α |= v
xR �↑Φ ↔ �↑
v
xR Φ,
α |= v
xR �↓Φ ↔ �↓
v
xR Φ,
α |= v
xR ����↑Φ ↔����↑
v
xR Φ,
α |= v
xR ����↓Φ ↔����↓
v
xR Φ;
2) α |= v
xR �↑Φ ⇔ α |= �↑
v
xR Φ,
α |= v
xR �↓Φ ⇔ α |= �↓
v
xR Φ,
α |= v
xR ����↑Φ ⇔ α |=����↑
v
xR Φ,
α |= v
xR ����↓Φ ⇔ α |=����↓
v
xR Φ.
Наслідок 12. Для ТмМС маємо:
M |= v
xR �↑Φ ↔ �↑
v
xR Φ,
M |= v
xR �↓Φ ↔ �↓
v
xR Φ,
M |= v
xR ����↑Φ ↔����↑
v
xR Φ,
M |= v
xR ����↓Φ ↔����↓
v
xR Φ.
Наслідок 13. Формули
v
xR �↑Φ ↔ �↑
v
xR Φ, v
xR �↓Φ ↔ �↓
v
xR Φ,
v
xR ����↑Φ ↔����↑
v
xR Φ, v
xR ����↓Φ ↔����↓
v
xR Φ
усюди істинні.
Таким чином, у випадку ТмМС но-
мінативних рівнів символи реномінації мо-
жна проносити через символи модальних
композицій.
Теорема 9. Для ТмМС маємо
1) M |= ∃x�↑Φ→�↑∃xΦ та
M |= ∃x�↓Φ→�↓∃xΦ;
2) M |= �↑∀xΦ→∀x�↑Φ та
M |= �↓∀xΦ→∀x�↓Φ.
Наслідок 14.
1)∃x�↑Φ→�↑∃xΦ, ∃x�↓Φ→�↓∃xΦ та
�↑∀xΦ→∀x�↑Φ, �↓∀xΦ→∀x�↓Φ –
всюди істинні формули;
2) �↑∀xΦ→∀x�↑Φ, �↓∀xΦ→∀x�↓Φ
та ∃x�↑Φ→�↑∃xΦ, ∃x�↓Φ→�↓∃xΦ –
всюди істинні формули.
7. Відношення логічного наслідку
для множин формул КНМЛ
Для КНМЛ номінативних рівнів по-
няття логічного наслідку для множин спе-
цифікованих станами формул визначається
наступним чином.
Множини вигляду d ∩VAα, де d∈VA,
будемо позначати dα.
Теоретичні та методологічні основи програмування
21
∆∆∆∆ є логічним наслідком ΓΓΓΓ в КНМС
M, якщо для всіх d∈VA із того, що
Φα(dα) = T для всіх Φα∈ΓΓΓΓ, випливає, що
неможливо Ψβ(dβ) = F для всіх Ψβ∈∆∆∆∆.
Те, що ∆∆∆∆ є логічним наслідком ΓΓΓΓ в
КНМС M, позначаємо ΓΓΓΓ |=M ∆∆∆∆.
∆∆∆∆ є логічним наслідком ΓΓΓΓ (щодо
КНМС певного типу), якщо ΓΓΓΓ |=M ∆∆∆∆ для
всіх КНМС M відповідного типу.
Те, що ∆∆∆∆ є логічним наслідком ΓΓΓΓ,
позначаємо ΓΓΓΓ |= ∆∆∆∆.
Отже, ΓΓΓΓ |≠≠≠≠ ∆∆∆∆ ⇔⇔⇔⇔ існують КНМС M
та d∈VA такі:
для всіх Φα∈ΓΓΓΓ маємо Φα(dα) = T та
для всіх Ψ
β∈∆∆∆∆ маємо Ψβ(dβ) = F.
Наведемо властивості відношення
логічного наслідку для множин специфі-
кованих станами формул. Найперше, це
немодальні властивості (див. [1]), фактич-
но успадковані від традиційної логіки.
Властивості пропозиційного рівня:
ПС) Якщо ΓΓΓΓ∩∆∆∆∆ ≠ ∅, то ΓΓΓΓ |=M ∆∆∆∆.
П1) ¬Φα, ΓΓΓΓ |=M ∆∆∆∆ ⇔ ΓΓΓΓ |=M ∆∆∆∆, Φα.
П2) ΓΓΓΓ |=M ∆∆∆∆,¬Φα ⇔ Φα, ΓΓΓΓ |=M ∆∆∆∆.
П3) Φ∨Ψα, ΓΓΓΓ |=M ∆∆∆∆ ⇔ Φα, ΓΓΓΓ |=M ∆∆∆∆
та Ψα, ΓΓΓΓ |=M ∆∆∆∆.
П4) ΓΓΓΓ |=M ∆∆∆∆, Φ∨Ψα ⇔ ΓΓΓΓ |=M ∆∆∆∆, Φα, Ψα.
Властивості реномінативного рівня:
ΦN|−−−−)
,
, ( )y v
z xR Φ α, ΓΓΓΓ |=M ∆∆∆∆ ⇔
⇔ ( )v
xR Φ α, ΓΓΓΓ |=M ∆∆∆∆ за умови у∈µ(Φ).
ΦN–|) ΓΓΓΓ |=M ∆∆∆∆, ,
, ( )y v
z xR Φ α ⇔
⇔ ΓΓΓΓ |=M ∆∆∆∆, ( )v
xR Φ α за умови у∈µ(Φ).
RT|−−−−)
,
, ( )z v
z xR Φ α, ΓΓΓΓ |=M ∆∆∆∆ ⇔
⇔ ( )v
xR Φ α, ΓΓΓΓ |=M ∆∆∆∆.
RT–|) ΓΓΓΓ |=M ∆∆∆∆, ,
, ( )z v
z xR Φ α ⇔
⇔ ΓΓΓΓ |=M ∆∆∆∆, ( )v
xR Φ α.
R¬|−−−−) ( )v
xR ¬Φ α, ΓΓΓΓ |=M ∆∆∆∆ ⇔
⇔ ( )v
xR¬ Φ α, ΓΓΓΓ |=M ∆∆∆∆.
R¬–|) ΓΓΓΓ |=M ∆∆∆∆, ( )v
xR ¬Φ α ⇔
⇔ ΓΓΓΓ |=M ∆∆∆∆, ( )v
xR¬ Φ α.
R∨|−−−−) ( )v
xR Φ ∨ Ψ α, ΓΓΓΓ |=M ∆∆∆∆ ⇔
⇔ ( ) ( )v v
x xR RΦ ∨ Ψ α, ΓΓΓΓ |=M ∆∆∆∆.
R∨–|) ΓΓΓΓ |=M ∆∆∆∆, ( )v
xR Φ ∨ Ψ α ⇔
⇔ ΓΓΓΓ |=M ∆∆∆∆, ( ) ( )v v
x xR RΦ ∨ Ψ α.
RR|−−−−) ( ( ))v w
x yR R Φ α, ΓΓΓΓ |=M ∆∆∆∆ ⇔
⇔ ( )v w
x yR Φo
α, ΓΓΓΓ |=M ∆∆∆∆.
RR–|) ΓΓΓΓ |=M ∆∆∆∆, ( ( ))v w
x yR R Φ α ⇔
⇔ ΓΓΓΓ |=M ∆∆∆∆, ( )v w
x yR Φo
α.
R|−−−−) ΓΓΓΓ, v
xR (�Φ)α |=M ∆∆∆∆ ⇔
⇔ ΓΓΓΓ, � ( )v
xR Φ α |=M ∆∆∆∆.
R−−−−|) ΓΓΓΓ |=M ∆∆∆∆, v
xR (�Φ)α ⇔
⇔ ΓΓΓΓ |=M ∆∆∆∆, � ( )v
xR Φ α.
Властивості кванторного рівня:
R∃|−−−−) ( )v
xR y∃ Φ α, ΓΓΓΓ |=M ∆∆∆∆ ⇔
⇔ ( )v
xyR∃ Φ α, ΓΓΓΓ |=M ∆∆∆∆, якщо y∉{ ,v x }.
R∃–|) ΓΓΓΓ |=M ∆∆∆∆, ( )v
xR y∃ Φ α ⇔
⇔ ΓΓΓΓ |=M ∆∆∆∆, ( )v
xyR∃ Φ α, якщо y∉{ ,v x }.
R∃∃|−−−−) ( )v
xR y∃ Φ α, ΓΓΓΓ |=M ∆∆∆∆ ⇔
⇔ ∃z ( )v y
x zR Φo
α, ΓΓΓΓ |=M ∆∆∆∆, якщо y∈{ ,v x }.
R∃∃–|) ΓΓΓΓ |=M ∆∆∆∆, ( )v
xR y∃ Φ α ⇔
⇔ ΓΓΓΓ |=M ∆∆∆∆, ∃z ( )v y
x zR Φo
α, якщо y∈{ ,v x }.
∃∃∃∃|–) ∃хΦα, ΓΓΓΓ |= ∆∆∆∆ ⇔ ( )x
yR Φ α, ΓΓΓΓ |= ∆∆∆∆,
якщо у тотально неістотне та у∉пт(ΓΓΓΓ, ∆∆∆∆, Φ).
∃∃∃∃–|) ΓΓΓΓ |=M ∆∆∆∆, ∃∃∃∃хΦα ⇔
⇔ ΓΓΓΓ |=M ∆∆∆∆,
1
( )x
yR Φ α,…, ( )
n
x
yR Φ α, ∃хΦα.
Властивості кванторно-екваційного
рівня:
SmE) x = y
α, ΓΓΓΓ |=M ∆∆∆∆ ⇔ x = y
α,
y = x
α, ΓΓΓΓ |=M ∆∆∆∆.
TrE) x = y
α, y = z
α, ΓΓΓΓ |=M ∆∆∆∆ ⇔
⇔ x = y
α, y = z
α, s = r
α, x = z
α, ΓΓΓΓ |=M ∆∆∆∆.
ЕΦ|−−−−) y = x
α, ,
, ( )z u
y vR Φ α, ΓΓΓΓ |=M ∆∆∆∆ ⇔
⇔ y = x
α, ,
, ( )z u
y vR Φ α, ,
, ( )z u
x vR Φ α, ΓΓΓΓ |=M ∆∆∆∆
EΦ−−−−|) y = x
α,ΓΓΓΓ |=M ∆∆∆∆, ,
, ( )z u
y vR Φ α ⇔
⇔ y = x
α, ΓΓΓΓ |=M ∆∆∆∆,
,
, ( )z u
y vR Φ α, ,
, ( )z u
x vR Φ α.
Згідно SmE, для ЕΦ немає потреби
зазначати два випадки з x = y
α та y = x
α,
тому ми обмежились випадком y = x
α.
ER|−−−−) x = y
α, Φα, ΓΓΓΓ |=M ∆∆∆∆ ⇔
⇔ x = y
α, Φα, ,x
yR αΦ ,y
xR αΦ ΓΓΓΓ |=M ∆∆∆∆.
Теоретичні та методологічні основи програмування
22
ER−−−−|) x = y
α, ΓΓΓΓ |=M ∆∆∆∆, Φα ⇔
⇔ x = y
α, ΓΓΓΓ |=M ∆∆∆∆, Φα, ,x
yR αΦ y
xR αΦ .
Модальні властивості формулю-
ються однаково на пропозиційному та но-
мінативних рівнях. Вони справджуються
як для St-ТМС, так і для Gn-ТМС.
У випадку загальних ТМЛ для мо-
дального оператора � маємо
|–) �Φα, ΓΓΓΓ |=M ∆∆∆∆ ⇔ {Φβ |
α>>>>β} ∪ΓΓΓΓ |=M ∆∆∆∆.
–|) ΓΓΓΓ |=M ∆∆∆∆, �Φα ⇔ ΓΓΓΓ |=M ∆∆∆∆, Φβ
для деякого стану β, такого, що α>>>>β.
У випадку темпоральних КНМЛ
властивості |– та –| розщеплюються:
↑|–) �↑Φα, ΓΓΓΓ |=M ∆∆∆∆ ⇔
⇔ {Φβ | α>>>>β} ∪ΓΓΓΓ |=M ∆∆∆∆.
↑–|) ΓΓΓΓ |=M ∆∆∆∆, �↑Φα ⇔ ΓΓΓΓ |=M ∆∆∆∆, Φβ
для деякого стану β, такого, що α>>>>β.
↓|–) �↓Φα, ΓΓΓΓ |=M ∆∆∆∆ ⇔
⇔ {Φβ | β>>>>α} ∪ΓΓΓΓ |=M ∆∆∆∆.
↓–|) ΓΓΓΓ |=M ∆∆∆∆, �↓Φα ⇔ ΓΓΓΓ |=M ∆∆∆∆, Φβ
для деякого стану β, такого, що β>>>>α.
Для КНМЛ кванторно-екваційного
рівня справджуються також властивості
EN|–) x = y
α, ΓΓΓΓ |=M ∆∆∆∆ ⇒⇒⇒⇒ � x = y
α, ΓΓΓΓ |=M ∆∆∆∆.
EN–|) ΓΓΓΓ |=M ∆∆∆∆, x = y
α ⇒ ΓΓΓΓ |=M ∆∆∆∆, � x = y
α.
Доведемо EN|–. Припустимо супро-
тивне: для деякої КНМС M x = y
α, ΓΓΓΓ |=M ∆∆∆∆
та � x = y
α, ΓΓΓΓ |≠≠≠≠M ∆∆∆∆. Останнє означає: існує
d∈VA, таке, що для всіх Φα∈ΓΓΓΓ маємо
Φα(dα) = T, � x = yα(dα) = T, для всіх Ψ
β∈∆∆∆∆
маємо Ψβ(dβ) = F. Умова � x = yα(dα) = T
означає, що для всіх станів β, таких, що
α>>>>β, маємо x = yβ(dα∩VAβ) = T, звідки
(dα∩VAβ)(x)↓ = (dα∩VAβ)↓ = a для деякого a.
Зрозуміло, що a∈Aα. Але тоді x = yα(dα) = T,
звідки, враховуючи Φα(dα) = T для всіх
Φα∈ΓΓΓΓ та Ψβ(dβ) = F для всіх Ψ
β∈∆∆∆∆, отри-
муємо x = y
α, ΓΓΓΓ |≠≠≠≠M ∆∆∆∆, що суперечить припу-
щенню.
Доведемо EN–|. Припустимо супро-
тивне: для деякої КНМС M ΓΓΓΓ |=M ∆∆∆∆, x = y
α
та ΓΓΓΓ |≠≠≠≠M ∆∆∆∆, � x = y
α. Останнє означає: існує
d∈VA, таке, що для всіх Φα∈ΓΓΓΓ маємо
Φα(dα) = T, � x = yα(dα) = F, а для всіх Ψβ∈∆∆∆∆
маємо Ψβ(dβ) = F. Умова � x = yα(dα) = F оз-
начає, що для деякого β, такого, що α>>>>β,
маємо x = yβ(dα∩VAβ) = F, звідки отримуємо
(dα∩VAβ)β(x)↓ = a та (dα∩VAβ)β(y)↓ = b для
деяких a, b: a ≠≠≠≠ b. Маємо a, b∈Aα∩VAβ ⊆Aα,
але тоді x = yα(dα) = F, звідки, враховуючи
Φα(dα) = T для всіх Φα∈ΓΓΓΓ та Ψβ(dβ) = F для
всіх Ψ
β∈∆∆∆∆, отримуємо ΓΓΓΓ |≠≠≠≠M ∆∆∆∆, x = y
α, що
суперечить припущенню.
У загальному випадку для EN|– та
EN–| умову “⇒⇒⇒⇒“ не можна посилити до
“⇔“.
Приклад 5.
Можливо x = y
α, ΓΓΓΓ |≠≠≠≠M ∆∆∆∆ та � x = y
α,
ΓΓΓΓ |=M ∆∆∆∆.
Задаємо КНМС M такого вигляду:
S = { α, β}, R = { α>>>>β}. Нехай Aα = { a, b},
Aβ = { b}. Візьмемо ΓΓΓΓ = ∅, ∆∆∆∆ = {Ψ
α}. Нехай
для Ψ неістотними є всі імена, окрім x та y.
Задамо Ψ
α([xaa, yaa]) = F, а у випадку
δ∈{ a, b} {x, y} та b∈den(δ) задамо Ψ
α(δ) = T.
Нехай d = [xaa, yaa]. Тоді dα = d. Маємо
dα(x)↓ = dα(y)↓ = a, звідки x = yα(dα) = T.
Отже, x = y
α
|≠≠≠≠M Ψ
α. Проте dα∉VAβ, звідки
x = yβ(dα)↑, що дає � x = yα(dα)↑. У випадку
δ∈{ a, b} {x, y} та b∈den(δ) маємо Ψα(δ) = T; у
випадку δ∈{ a, b} {x, y} та b∉den(δ) маємо
δ = dα = d, тоді dα∉VAβ, звідки x = yβ(dα)↑, що
дає � x = yα(dα)↑. Отже, � x = y
α
|=M Ψ
α.
Приклад 6.
Можливо ΓΓΓΓ |≠≠≠≠M ∆∆∆∆, x = y
α та
ΓΓΓΓ |=M ∆∆∆∆, � x = y
α.
Візьмемо ΓΓΓΓ = {Φα}, ∆∆∆∆ = ∅. Нехай
Aα = { a, b}, Aβ = { b}, а для Φ неістотними є
всі імена, окрім x та y. Задамо Φα(δ) = T для
всіх δ∈{ a, b} {x, y}. Нехай d = [xaa, yab].
Тоді dα = d. Маємо dα(x)↓ ≠ dα(y)↓, звідки
x = yα(dα) = F. Отже, Φα |≠≠≠≠M x = y
α. Проте у
випадку a∈den(δ) маємо δα∉VAβ, звідки
x = yβ(δα)↑, що дає � x = yα(δα)↑. У випадку
δ = [xab, yab] маємо x = yβ(δα) = T, що дає
� x = yα(δα) =T. Отже, Φα |=M � x = y
α.
При трактуванні рівності як строгої
властивості EN|– та EN–| можна посилити:
ENS|–) x = y
α, ΓΓΓΓ |=M ∆∆∆∆ ⇔
⇔ � x = y
α, ΓΓΓΓ |=M ∆∆∆∆.
ENS–|) ΓΓΓΓ |=M ∆∆∆∆, x = y
α ⇔
⇔ ΓΓΓΓ |=M ∆∆∆∆, � x = y
α.
Теоретичні та методологічні основи програмування
23
Для темпоральних КНМЛ квантор-
но-екваційного рівня EN|– та EN–| природ-
ним чином модифікуються у властивості
EN↑|–, EN↓|– та EN↑–|, EN↓–|.
Висновки
На базі інтегрованого інтенсіональ-
но-екстенсіонального підходу до побудови
логічних та програмних систем досліджені
композиційно-номінативні модальні та
темпоральні логіки номінативних рівнів:
реномінативного, кванторного, кванторно-
екваційного. Для цих логік розглядається
спеціальне уточнення поняття компо-
зиційно-номінативної модальної системи,
визначаються транзиційні та темпоральні
модальні системи. Вивчаються семантичні
властивості таких логік, зокрема, власти-
вості логічного наслідку для множин фор-
мул. На основі цих властивостей будуть
збудовані секвенційні числення компо-
зиційно-номінативних модальних і темпо-
ральних логік номінативних рівнів.
1. Нікітченко М.С., Шкільняк С.С. Мате-
матична логіка та теорія алгоритмів. –
К.: ВПЦ «Київський університет». –
2008. – 528 с.
2. Нікітченко М.С., Шкільняк С.С. Компо-
зиційно-номінативні модальні логіки //
Проблемы программирования. – 2002. –
№ 1–2. – С. 27–33.
3. Нікітченко М.С., Шкільняк С.С. Інтен-
сіонально-орієнтований підхід до побу-
дови логічних систем // Проблеми про-
грамування. – 2007. – № 2. – C. 15–40.
4. Никитченко Н.С. Предикатные компо-
зиционно–номинативные системы //
Проблемы программирования. – 1999.
– № 2. – С. 3–19.
5. Шкільняк О.С. Композиційно-номіна-
тивні модальні та темпоральні логіки:
семантичні властивості, секвенційні
числення // Наукові записки НаУКМА.
Серія: Комп’ютерні науки. – 2008. –
Т. 6. – C. 25–34.
6. Фейс Р. Модальная логика.– M.: Наука.
– 1974. – 520 с.
7. Шкільняк C.С. Неокласичні кванторні
логіки з рівністю // Вісник Київського
університету. Серія: фіз.-мат. науки. –
2003. – Вип.1. – С. 222–225.
8. Семантика модальных и интенсио-
нальных логик. – M.: Прогресс, 1981. –
494 с.
Отримано 15.10.2009
Про автора:
Шкільняк Оксана Степанівна,
асистент кафедри інформаційних систем
Київського національного університету
імені Тараса Шевченка.
Місце роботи автора:
Київський національний університет
імені Тараса Шевченка,
01601, Київ,
вул. Володимирська, 60.
Тел.: (044) 259-0511, (044) 522-0640 (д)
e-mail: me.oksana@gmail.com
|
| id | pp_isofts_kiev_ua-article-977 |
| institution | Problems in programming |
| keywords_txt_mv | keywords |
| language | Ukrainian |
| last_indexed | 2026-06-11T01:00:17Z |
| publishDate | 2026 |
| publisher | PROBLEMS IN PROGRAMMING |
| record_format | ojs |
| resource_txt_mv | ppisoftskievua/9c/11fcfd59ec15ce651fab70ceac5e4a9c.pdf |
| spelling | pp_isofts_kiev_ua-article-9772026-06-10T11:10:03Z Semantic properties of composition nominative modal logics Семантические свойства композиционно-номинативных модальных логик Семантичні властивості композиційно-номінативних модальних логік Shkilnyak, O.S. UDC 681.3.06 УДК 681.3.06 УДК 681.3.06 In this paper composition nominative modal and temporal logics of nominative, quantifier and quantifier-equational levels are studied on the basis of the integrated intentional-extensional approach to construction of systems of logic and software. For such logics, a special refinement of the notion of composition nominative modal system is introduced, and semantic properties are investigated.Problems in programming 2009; 4: 11-23 На основе интегрированного интенсионально-экстенсионального подхода к построению логических и программных систем изучаются композиционно-номинативные модальные и темпоральные логики реноминативного, кванторного, кванторно-эквационного уровней.Для этих логик уточняется понятие композиционно-номинативной модальной системы, исследуются их семантические свойстваProblems in programming 2009; 4: 11-23 На основі інтегрованого інтенсіонально-екстенсіонального підходу до побудови логічних та програмних систем вивчаються композиційно-номінативні модальні та темпоральні логіки реномінативного, кванторного, кванторно-екваційного рівнів. Для цих логік уточнюється поняття композиційно-номінативної модальної системи, досліджуються їх семантичні властивості.Problems in programming 2009; 4: 11-23 PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2026-06-10 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/977 PROBLEMS IN PROGRAMMING; No 4 (2009); 11-23 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 4 (2009); 11-23 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 4 (2009); 11-23 1727-4907 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/977/1045 Copyright (c) 2026 PROBLEMS IN PROGRAMMING |
| spellingShingle | UDC 681.3.06 Shkilnyak, O.S. Semantic properties of composition nominative modal logics |
| title | Semantic properties of composition nominative modal logics |
| title_alt | Семантические свойства композиционно-номинативных модальных логик Семантичні властивості композиційно-номінативних модальних логік |
| title_full | Semantic properties of composition nominative modal logics |
| title_fullStr | Semantic properties of composition nominative modal logics |
| title_full_unstemmed | Semantic properties of composition nominative modal logics |
| title_short | Semantic properties of composition nominative modal logics |
| title_sort | semantic properties of composition nominative modal logics |
| topic | UDC 681.3.06 |
| topic_facet | UDC 681.3.06 УДК 681.3.06 УДК 681.3.06 |
| url | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/977 |
| work_keys_str_mv | AT shkilnyakos semanticpropertiesofcompositionnominativemodallogics AT shkilnyakos semantičeskiesvojstvakompozicionnonominativnyhmodalʹnyhlogik AT shkilnyakos semantičnívlastivostíkompozicíjnonomínativnihmodalʹnihlogík |