Sequent calculi for first-order logics of single-valued quasi-ary predicates
On the basis of properties of various relations of logical consequence, we specify sequent calculi for first-order composition-nominative logics of single-valued quasi-ary predicates of quantifier level. Such calculi are constructed for logics of equtone predicates and for a general case of logics o...
Збережено в:
| Дата: | 2018 |
|---|---|
| Автор: | |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
PROBLEMS IN PROGRAMMING
2018
|
| Теми: | |
| Онлайн доступ: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/36 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Репозитарії
Problems in programming| id |
pp_isofts_kiev_ua-article-36 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/f2/9ccf278fcdc29b57fc606b49f3b5ddf2.pdf |
| spelling |
pp_isofts_kiev_ua-article-362018-10-02T21:07:26Z Sequent calculi for first-order logics of single-valued quasi-ary predicates Секвенційні числення першопорядкових логік однозначних квазіарних предикатів Shkilniak, S.S. On the basis of properties of various relations of logical consequence, we specify sequent calculi for first-order composition-nominative logics of single-valued quasi-ary predicates of quantifier level. Such calculi are constructed for logics of equtone predicates and for a general case of logics of single-valued quasi-ary predicates. For the introduced calculi soundness and completeness theorems are proved. На основі властивостей відношень логічного наслідку для першопорядкових композиційно-номінативних логік однозначних квазіарних предикатів кванторного рівня побудовано числення секвенційного типу. Такі числення пропонуються для логік еквітонних предикатів та для загального випадку логік однозначних квазіарних предикатів. Для побудованих числень доведено теореми коректності та повноти PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2018-07-23 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/36 PROBLEMS IN PROGRAMMING; No 1 (2012) ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 1 (2012) ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 1 (2012) 1727-4907 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/36/38 Copyright (c) 2015 ПРОБЛЕМИ ПРОГРАМУВАННЯ |
| institution |
Problems in programming |
| baseUrl_str |
https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| datestamp_date |
2018-10-02T21:07:26Z |
| collection |
OJS |
| language |
Ukrainian |
| topic |
|
| spellingShingle |
Shkilniak, S.S. Sequent calculi for first-order logics of single-valued quasi-ary predicates |
| topic_facet |
|
| format |
Article |
| author |
Shkilniak, S.S. |
| author_facet |
Shkilniak, S.S. |
| author_sort |
Shkilniak, S.S. |
| title |
Sequent calculi for first-order logics of single-valued quasi-ary predicates |
| title_short |
Sequent calculi for first-order logics of single-valued quasi-ary predicates |
| title_full |
Sequent calculi for first-order logics of single-valued quasi-ary predicates |
| title_fullStr |
Sequent calculi for first-order logics of single-valued quasi-ary predicates |
| title_full_unstemmed |
Sequent calculi for first-order logics of single-valued quasi-ary predicates |
| title_sort |
sequent calculi for first-order logics of single-valued quasi-ary predicates |
| title_alt |
Секвенційні числення першопорядкових логік однозначних квазіарних предикатів |
| description |
On the basis of properties of various relations of logical consequence, we specify sequent calculi for first-order composition-nominative logics of single-valued quasi-ary predicates of quantifier level. Such calculi are constructed for logics of equtone predicates and for a general case of logics of single-valued quasi-ary predicates. For the introduced calculi soundness and completeness theorems are proved. |
| publisher |
PROBLEMS IN PROGRAMMING |
| publishDate |
2018 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/36 |
| work_keys_str_mv |
AT shkilniakss sequentcalculiforfirstorderlogicsofsinglevaluedquasiarypredicates AT shkilniakss sekvencíjníčislennâperšoporâdkovihlogíkodnoznačnihkvazíarnihpredikatív |
| first_indexed |
2025-07-17T09:45:10Z |
| last_indexed |
2025-07-17T09:45:10Z |
| _version_ |
1850409995972116480 |
| fulltext |
Теоретичні та методологічні основи програмування
УДК 004.42:510.69
С.С. Шкільняк
СЕКВЕНЦІЙНІ ЧИСЛЕННЯ ПЕРШОПОРЯДКОВИХ ЛОГІК
ОДНОЗНАЧНИХ КВАЗІАРНИХ ПРЕДИКАТІВ
На основі властивостей відношень логічного наслідку для першопорядкових композиційно-номінатив-
них логік однозначних квазіарних предикатів кванторного рівня побудовано числення секвенційного
типу. Такі числення пропонуються для логік еквітонних предикатів та для загального випадку логік од-
нозначних квазіарних предикатів. Для побудованих числень доведено теореми коректності та повноти.
Вступ
Композиційно-номінативні логіки
(КНЛ) – це програмно-орієнтовані логічні
формалізми, будовані на основі компози-
ційно-номінативного підходу [1]. Дослі-
дження фундаментального поняття логіч-
ного слідування для таких логік проведене
в роботах [2–4]. Для першопорядкових
КНЛ квазіарних предикатів кванторного
рівня було запропоновано різні формалі-
зації цього поняття за допомогою відно-
шень логічного наслідку, досліджено вла-
стивості таких відношень, зокрема, власти-
вості відношень логічного наслідку для мно-
жин формул. У даній роботі на основі цих
властивостей для першопорядкових КНЛ
однозначних квазіарних предикатів кван-
торного рівня пропонуються числення сек-
венційного типу.
Секвенцію визначаємо (див. [5, 6])
як множину формул, специфікованих (від-
мічених) спеціальними символами |– та –| ,
які не входять до алфавіту мови. Секвенції
позначаємо як |–Γ–|Δ, де всі формули мно-
жини Γ специфіковані символом |– , усі фор-
мули множини Δ – символом –| . Не деталі-
зуючи, секвенції позначаємо як Σ.
Секвенційне числення для заданого
відношення логічного наслідку |= будується
так, що секвенція |–Γ–|Δ вивідна (має виве-
дення) тоді й тільки тоді, коли Γ |= Δ.
Роль аксіом секвенційного числення
грають замкнені секвенції. Це поняття уто-
чнюється по-різному в різних секвенційних
численнях для різних відношень |= . При
цьому має виконуватись умова: якщо сек-
венція |–Γ–|Δ замкнена, то Γ |= Δ.
Семантичним властивостям відно-
шення |= зіставимо їх синтаксичні аналоги –
секвенційні форми. Вони є правилами ви-
ведення секвенційних числень. Секвенційні
форми записуємо як Σ
Ω
або Σ Λ
Ω
(зверху
– засновки, внизу – висновок).
Виведення в секвенційних числен-
нях має вигляд дерева, вершинами якого є
секвенції. Такі дерева назвемо секвенцій-
ними. Секвенційне дерево замкнене, якщо
кожний його лист – замкнена секвенція.
Секвенція Σ вивідна, якщо існує зам-
кнене секвенційне дерево з коренем Σ. Та-
ке дерево назвемо виведенням секвенції Σ.
Різноманітність відношень логічно-
го наслідку дає побудову різних варіантів
секвенційних числень КНЛ. У випадку час-
ткових однозначних предикатів (неокласи-
чна семантика) можна розглядати такі від-
ношення (див. [2]): |=Cl , |=T , |=F , |=TF .
Першопорядкові секвенційні числення по-
будовані [6] для відношення |=Cl логік ек-
вітонних квазіарних предикатів. Для |=Cl в
загальному випадку логік однозначних
квазіарних предикатів збудоване [3] сек-
венційне числення кванторного рівня. Ме-
тою даної роботи є побудова числень кван-
торного рівня для відношень |=T , |=F , |=TF
логік еквітонних та логік однозначних ква-
зіарних предикатів.
Поняття, які тут не визначаються,
тлумачимо в сенсі робіт [2–4, 6].
1. Властивості відношень логічного
наслідку для множин формул
У наведених далі властивостях |= –
це |=Cl, |=T, |=F, |=TF.
Спочатку наведемо базові власти-
вості пропозиційного рівня:
© C.С.Шкільняк, 2012
ISSN 1727-4907. Проблеми програмування. 2012. № 1 34
Теоретичні та методологічні основи програмування
U) нехай Γ |= Δ та Δ ⊆ Σ, тоді Γ |= Σ;
нехай Γ |= Δ та Γ ⊆ Λ, тоді Λ |= Δ.
С) Φ, Γ |= Δ, Φ.
¬¬|–) ¬¬Φ, Γ |= Δ ⇔ Φ, Γ |= Δ.
¬¬–|) Γ |= Δ, ¬¬Φ ⇔ Γ |= Δ, Φ.
∨|–) Φ∨Ψ, Γ |= Δ ⇔ Φ, Γ |= Δ та Ψ, Γ |= Δ.
∨–|) Γ |= Δ, Φ∨Ψ ⇔ Γ |= Δ, Φ, Ψ.
¬∨|–) ¬(Φ∨Ψ), Γ |= Δ ⇔ ¬Φ, ¬Ψ, Γ |= Δ.
¬∨–|) Γ |= Δ, ¬(Φ∨Ψ) ⇔ Γ |= Δ, ¬Φ та
Γ |= Δ, ¬Ψ.
Для |=Cl також справджуються:
¬|– ) ¬Φ, Γ |=Cl Δ ⇔ Γ |= Cl Δ, Φ.
¬–| ) Γ |= Cl Δ, ¬Φ ⇔ Φ, Γ |= Cl Δ.
Це означає, що для |=Cl можна зні-
мати зовнішнє заперечення, переносячи
формулу з лівої частини у праву і навпаки.
Проте це не можна робити [2, 5] для |=T ,
|=F та |=TF, для цих наслідків властивості
¬|– та ¬–| невірні.
Додатково гарантують наявність ло-
гічного наслідку такі властивості:
СL) Φ, ¬Φ, Γ |= Δ (тут |= – це |=T, |=Cl ).
СR) Γ |= Δ, Φ, ¬Φ (тут |= – це |=F, |=Cl ).
СLR) Φ, ¬Φ, Γ |=TF Δ, Ψ, ¬Ψ.
Зрозуміло, що СLR правильна ⇔
одночасно правильні СL і СR (для |=TF ).
Для |=Cl можна знімати заперечення,
переносячи формулу з лівої частини у пра-
ву і навпаки, тому СLR, СL і СR зводяться
до С, що робить їх використання зайвим.
Наведемо базові властивості реномі-
нативного і кванторного рівнів. При кожній
інтерпретації предикати, що є значеннями
виділених формул, збігаються. Наведені
властивості правильні й для |=T, |=F, |=Cl.
RT|–) ,
, ( ),z v
z xR Φ Γ |=TF Δ ⇔ ( ),v
xR Φ Γ |=TF Δ.
RT–|) Γ |=TF Δ, ,
, ( )z v
z xR Φ ⇔ Γ |=TF Δ, ( ).v
xR Φ
¬RT|–) ,
, ( )z v
z xR¬ Φ , Γ |=TF Δ ⇔
⇔ ( )v
xR¬ Φ , Γ |=TF Δ.
¬RT–|) Γ |=TF Δ, ,
, ( )z v
z xR¬ Φ ⇔
⇔ Γ |=TF Δ, ( )v
xR¬ Φ .
RR|–) ( ( ))v w
x yR R Φ , Γ |=TF Δ ⇔
⇔ ( ),v w
x yR Φo Γ |=TF Δ.
RR–|) Γ |=TF Δ, ( ( )v w
x yR R Φ ) ⇔
⇔ Γ |=TF Δ, ( )v w
x yR Φo .
¬RR|–) ( ( ))v w
x yR R ,¬ Φ Γ |=TF Δ ⇔
⇔ ( ),v w
x yR¬ Φo Γ |=TF Δ.
¬RR–|) Γ |=TF Δ, ( ( )v w
x yR R )¬ Φ ⇔
⇔ Γ |=TF Δ, ( )v w
x yR¬ Φo .
R¬|–) ( )v
xR ,¬Φ Γ |=TF Δ ⇔
⇔ ( ),v
xR¬ Φ Γ |=TF Δ.
R¬–|) Γ |=TF Δ, (v
xR )¬Φ ⇔
⇔ Γ |=TF Δ, ( ).v
xR¬ Φ
¬R¬|–) ( )v
xR ,¬ ¬Φ Γ |=TF Δ ⇔
⇔ ( ),v
xR Φ Γ |=TF Δ.
¬R¬–|) Γ |=TF Δ, (v
xR )¬ ¬Φ ⇔
⇔ Γ |=TF Δ, ( ).v
xR Φ
R∨|–) v
xR (Φ∨Ψ), Γ |=TF Δ ⇔
⇔ v
xR (Φ)∨ v
xR (Ψ), Γ |=TF Δ.
R∨–|) Γ |=TF Δ, v
xR (Φ∨Ψ) ⇔
⇔ Γ |=TF Δ, v
xR (Φ)∨ v
xR (Ψ).
¬R∨|–) (v
xR ),¬ Φ∨Ψ Γ |=TF Δ ⇔
⇔ v
xR¬ (Φ), v
xR¬ (Ψ), Γ |=TF Δ.
¬R∨–|) Γ |=TF Δ, ( )v
xR¬ Φ∨Ψ ⇔
⇔ Γ |=TF Δ, ( )v
xR¬ Φ та
Γ |=TF Δ, ( ).v
xR¬ Ψ
Ми розглядаємо логіки квазіарних
предикатів, в яких за допомогою тотальної
функції ν : Ps→2V для кожного предикат-
ного символа задано множину строго неіс-
тотних предметних імен. Така ν продовжу-
ється [6] на множину всіх формул мови.
ΦN|–) ,
, ( ),y v
z xR Φ Γ |=TF Δ ⇔
⇔ ( ),v
xR Φ Γ |=TF Δ при у∈ν(Φ).
ΦN–|) Γ |=TF Δ, ,
, ( )y v
z xR Φ ⇔
⇔ Γ |=TF Δ, ( )v
xR Φ при у∈ν(Φ).
¬ΦN|–) ,
, ( ),y v
z xR¬ Φ Γ |=TF Δ ⇔
⇔ ( ),v
xR¬ Φ Γ |=TF Δ при у∈ν(Φ).
¬ΦN–|) Γ |=TF Δ, ,
, ( )y v
z xR¬ Φ ⇔
⇔ Γ |=TF Δ, ( )v
xR¬ Φ при у∈ν(Φ).
R∃|–) (v
xR y ),∃ Φ Γ |=TF Δ ⇔
⇔ ( ),v
xyR∃ Φ Γ |=TF Δ при у∉{ ,v x }.
35
Теоретичні та методологічні основи програмування
R∃–|) Γ |=TF Δ, (v
xR y∃ Φ) ⇔
⇔ Γ |=TF Δ, ( )v
xyR∃ Φ при у∉{ ,v x }.
¬R∃|–) (v
xR y¬ ∃ Φ), Γ |=TF Δ ⇔
⇔ ( ),v
xyR¬∃ Φ Γ |=TF Δ при у∉{ ,v x }.
¬R∃–|) Γ |=TF Δ, (v
xR y¬ ∃ Φ) ⇔
⇔ Γ |=TF Δ, ( )v
xyR¬∃ Φ при у∉{ ,v x }.
R∃S|–) (v
xR y∃ Φ),Γ |=TF Δ ⇔
⇔ ( ),v y
x zzR∃ o Φ Γ |=TF Δ.
R∃S–|) Γ |=TF Δ, (v
xR y∃ Φ) ⇔
⇔ Γ |=TF Δ, ( )v y
x zzR∃ Φo .
¬R∃S|–) (v
xR y¬ ∃ Φ), Γ |=TF Δ ⇔
⇔ ( ),v y
x zzR¬∃ Φo Γ |=TF Δ.
¬R∃S–|) Γ |=TF Δ, (v
xR y¬ ∃ Φ) ⇔
⇔ Γ |=TF Δ, ( )v y
x zzR¬∃ Φo .
Для R∃S|–, R∃S–|, ¬R∃S|–, ¬R∃S–| z то-
тально строго неістотне і z∉ ( ( ))v
xnm R x∃ Φ .
Для |=Cl можна знімати зовнішнє за-
перечення, переносячи формулу з лівої ча-
стини у праву і навпаки, тому властивості
типів ¬¬, ¬∨, ¬RT, ¬RR, ¬R¬, ¬R∨, ¬ΦN,
¬R∃, ¬R∃S не відносимо до базових.
Наведемо властивості, пов'язані з
елімінацією кванторів.
При умові z тотально строго неісто-
тне та z∉пт(Γ, Δ, Φ) маємо (див. [2]):
∃TN) Γ( ),x
zR Φ A|=∗ Δ ⇒ ∃хΦ, Γ A|=∗ Δ;
¬∃TN) Γ A|=∗ ( ),x
zR¬ Φ Δ ⇒ Γ A|=∗ ¬∃хΦ, Δ.
Тут і надалі, якщо інше явно не вка-
зано, ∗ – це одне з Cl, T, F, TF.
Для Х–Y-означених відношень логіч-
ного наслідку [3, 4] маємо такі властивості.
Нехай z тотально строго неістотне
та z∉nm(Γ∪Δ). Тоді:
TotN) Γ A, {z}∪Х–Y |=∗ Δ ⇔ Γ A, Х–Y |=∗ Δ.
Нехай Z, W, U ⊆ V – диз'юнктні мно-
жини. Тоді:
Br∃) Γ A, W–U |=∗ Δ, ∃хΦ ⇔ для кожної Y ⊆ Z
Γ A, W∪Y–U∪(Z\Y) |=∗ Δ, ∃хΦ, 1
( ),..., ( ),...,
n
x x
y yR RΦ Φ
де всі yi∈W∪Y.
Br¬∃) ¬∃хΦ, Γ A, W–U |=∗ Δ ⇔ для кожної Y ⊆ Z
¬∃хΦ, Γ
1
( ),..., ( ),...,
n
x x
y yR R¬ Φ ¬ Φ A, W∪Y–U∪(Z\Y) |=∗ Δ,
де всі yi∈W∪Y.
Нехай z тотально строго неістотне
та z∉пт(Γ, Δ, Φ). Тоді при z∈X маємо:
∃Х–Y |– ) Γ, ∃хΦ Х –Y |=∗ Δ ⇔ Γ, ( )x
zR Φ Х–Y |=∗ Δ;
¬∃Х–Y –| ) Γ Х–Y |=∗ ¬∃хΦ, Δ ⇔ Γ Х–Y |=∗ ( ),x
zR¬ Φ Δ.
Для |=Cl можна обмежитись власти-
востями ∃Х–Y |– та Br∃ .
Для відношення |=Cl логіки екві-
тонних предикатів немає потреби виділяти
Х–Y-означені відношення логічного наслід-
ку. Тоді маємо:
∃ |– ) ∃хΦ, Γ |=Cl Δ ⇔ Γ( ),x
zR Φ |=Cl Δ, де z то-
тально строго неістотне, z∉пт(Γ, Δ, Φ);
∃ –| ) Γ |=Cl Δ, ∃хΦ ⇔ Γ |=Cl Δ, ∃хΦ, ( )x
zR Φ .
Наведемо тепер спеціальні власти-
вості Х–Y-означених відношень логічного
наслідку, які додатково гарантують наяв-
ність логічного наслідку для логіки екві-
тонних предикатів:
CEqT) ,
, ( ),x u
y vR Φ Γ A, Х–Y |=T
,
, ( ),x u
z vR Φ Δ
при умові z∈X та y∈Y;
CEq¬T) ,
, ( ),x u
y vR¬ Φ Γ A, Х–Y |=T
,
, ( ),x u
z vR¬ Φ Δ
при умові z∈X та y∈Y;
CEqF) ,
, ( ),x u
z vR Φ Γ A, Х–Y |=F
,
, ( ),x u
y vR Φ Δ
при умові z∈X та y∈Y;
CEq¬F) ,
, ( ),x u
z vR¬ Φ Γ A, Х–Y |=F
,
, ( ),x u
y vR¬ Φ Δ
при умові z∈X та y∈Y.
Нехай v
xR Φ та z
yR Φ мають однако-
ві U-неозначувані [3] форми, де U – мно-
жина неозначених імен. Тоді маємо:
UnD) ,v
xR Φ Γ A, –U |=∗ ,z
yR Φ Δ.
Підсумовуючи, отримуємо умови,
які гарантують наявність відповідного ло-
гічного наслідку в неокласичній семантиці.
Відношення |=T, загальний випадок:
C ∨ CL ∨ UnD.
Відношення |=T логіки еквітонних
предикатів:
C ∨ CL ∨ CEqT ∨ CEq¬T ∨ UnD.
Відношення |=F, загальний випадок:
C ∨ CR∨ UnD.
Відношення |=F логіки еквітонних
предикатів:
C ∨ CR ∨ CEqF ∨ CEq¬F ∨ UnD.
Відношення |=TF, загальний випадок:
C ∨ CL & CR ∨ UnD, щo рівносильне
C ∨ CLR ∨ UnD.
36
Теоретичні та методологічні основи програмування
Відношення |=TF логіки еквітонних
предикатів:
C ∨ (CL ∨ CEqT ∨ CEq¬T) &
& (CR ∨ CEqF ∨ CEq¬F) ∨ UnD.
Для відношення |=Cl маємо C ∨ UnD.
2. Базові секвенційні форми та
умови замкненості секвенцій
Для ЧКНЛ можна отримати такі ва-
ріанти секвенційних числень.
Відношення |=Cl формалізуємо за
допомогою відомого [3] числення, яке тут
назвемо QCl. Для логіки еквітонних пре-
дикатів маємо відоме [6] неокласичне сек-
венційне числення, яке тут назвемо QEqCl.
Відношення |=T формалізуємо за
допомогою числення, яке назвемо QL. Для
логіки еквітонних предикатів отримуємо
числення, яке назвемо QEqL.
Відношення |=F формалізуємо за
допомогою числення, яке назвемо QR. Для
логіки еквітонних предикатів отримуємо
числення, яке назвемо QEqR.
Відношення |=TF формалізуємо за
допомогою числення, яке назвемо QLR.
Для логіки еквітонних предикатів отриму-
ємо числення, яке назвемо QEqLR.
Для числень QCl, QL, QR, QLR вво-
димо додаткову умову UnD замкненості сек-
венції у даній вершині дерева. Це пов'язане
із специфікою елімінації кванторів у загаль-
ному випадку квазіарних предикатів. Умова
UnD опирається на властивість UnD [4].
Нехай U – множина всіх неозначе-
них імен у даній вершині-секвенції Σ.
Секвенція Σ U-замкнена, якщо:
UnD) існує пара формул |– ,v
xR Φ –|
z
yR Φ∈Σ
таких, що v
xR Φ та z
yR Φ мають однакові
U-неозначувані форми.
Якщо секвенція |–Γ–|Δ U-замкнена, то
Γ A, –U |= Δ для довільної моделі мови A.
Cправді, при інтерпретаціях на да-
них, де всі імена U не мають значення,
предикати, що є інтерпретаціями формул із
однаковими U-неозначуваними формами,
приймають однакові значення. Звідси:
якщо |–Γ–|Δ U-замкнена, то Γ A, Х–U |=∗ Δ
для довільних A та Х ⊆ V: Х ∩ U = ∅.
Опишемо тепер введені числення.
Числення QCl. Базова умова замк-
неності секвенції Σ – умова С:
С) Σ замкнена, якщо існує формула Φ така,
що |–Φ∈Σ та –|Φ∈Σ.
Згідно властивості С, якщо секвенція
|–Γ–|Δ замкнена згідно умови С, то Γ |=Cl Δ.
Додаткова умова замкненості – це
умова UnD U-замкненості (тут U – множина
всіх неозначених імен у даній секвенції-
вершині).
Якщо секвенція |–Γ–|Δ U-замкнена, то
Γ A, Х–U |=Cl Δ для всіх A та Х ⊆ V: Х ∩ U = ∅.
Наведемо базові секвенційні форми
числення QCl. Такі форми записуються згі-
дно відповідних властивостей відношення
логічного наслідку |=Cl .
|− ¬ |
|
,
;
,
A
A
−
−
Σ
¬ Σ
−| ¬ |
|
,
;
,
A
A
−
−
Σ
¬ Σ
|−∨ | |
|
, ,
;
,
A B
A B
− −
−
Σ Σ
∨ Σ
−|∨ | |
|
, ,
;
,
A B
A B
− −
−
Σ
∨ Σ
|–RT |
,
| ,
( ),
;
( ),
v
x
z v
z x
R A
R A
−
−
Σ
Σ
–|RT |
,
| ,
( ),
;
( ),
v
x
z v
z x
R A
R A
−
−
Σ
Σ
|–RR |
|
( ),
;
( ( )),
v w
x y
v w
x y
R A
R R A
−
−
Σ
Σ
o
–|RR |
|
( ),
;
( ( )),
v w
x y
v w
x y
R A
R R A
−
−
Σ
Σ
o
|–R¬ |
|
( ),
;
( ),
v
x
v
x
R A
R A
−
−
¬ Σ
¬ Σ
–|R¬ |
|
( ),
;
( ),
v
x
v
x
R A
R A
−
−
¬ Σ
¬ Σ
|–R∨ |
|
( ) ( ),
;
( ),
v v
x x
v
x
R A R B
R A B
−
−
∨ Σ
∨ Σ
–|R∨ |
|
( ) ( ),
;
( ),
v v
x x
v
x
R A R B
R A B
−
−
∨ Σ
∨ Σ
|–ΦN |
,
| ,
( ),
( ),
v
u
y v
z u
R A
R A
−
−
Σ
Σ
при у∈ν(A);
–|ΦN |
,
| ,
( ),
( ),
v
u
y v
z u
R A
R A
−
−
Σ
Σ
при у∈ν(A);
|–R∃ |
|
( ),
( ),
v
x
v
x
yR A
R yA
−
−
∃ Σ
∃ Σ
при y∉{ ,v x };
–|R∃ |
|
( ),
( ),
v
x
v
x
yR A
R yA
−
−
∃ Σ
∃ Σ
при y∉{ ,v x };
|–R∃S |
|
( ),
;
( ),
v y
x z
v
x
zR A
R yA
−
−
∃ Σ
∃ Σ
o
37
Теоретичні та методологічні основи програмування
–|R∃S |
|
( ),
.
( ),
v y
x z
v
x
zR A
R yA
−
−
∃ Σ
∃ Σ
o
Для |–R∃S та –|R∃S умови: y∈{ ,v x },
z тотально строго неістотне, z∉ ( ( )v
xnm R A ) .
За умови y∉{ ,v x } використовуємо
форми |–R∃ та –|R∃.
За умови y∈{ ,v x } використовуємо
форми |–R∃S та –|R∃S.
|–∃ |
|
( ),
;
,
x
yR A
xA
−
−
Σ
∃ Σ
–|∃ | |
|
( ), ,
.
,
x
zR A xA
xA
− −
−
∃ Σ
∃ Σ
Для |–∃ у тотально строго неістотне та
у∉пт(Σ, А); таке у гарантовано означене.
Застосування форм |–∃ та –|∃ елімі-
нації кванторів уточняється процедурою
побудови секвенційного дерева.
Числення QEqCl. Базові секвенцій-
ні форми числення QEqCl такі ж, як для
QCl (єдина відмінність – умову строго не-
істотності можна послабити до умови неіс-
тотності). Замкненість секвенції визначаєть-
ся умовою С.
Істотна відмінність QEqCl-числень
та QCl-числень – різні процедури побудо-
ви секвенційного дерева, для QEqCl-чис-
лень така процедура [6] набагато простіша.
Числення QL. Базова умова замкне-
ності секвенції в QL-численні – умова С.
Перша додаткова умова замкненості
секвенції Σ в QL-численні – умова СL:
СL) Σ замкнена, якщо існує формула Φ така,
що |–Φ∈Σ та |–¬Φ∈Σ.
Секвенція Σ замкнена, якщо викону-
ється принаймі одна з умов С чи СL.
Згідно властивостей С та СL відно-
шення |=T , якщо |–Γ–|Δ замкнена, то Γ |=T Δ.
Друга додаткова умова – це умова
UnD U-замкненості (U – множина всіх не-
означених імен в даній секвенції-вершині).
Якщо секвенція |–Γ–|Δ U-замкнена, то
Γ A, Х– U |=T Δ для всіх A та Х ⊆ V: Х ∩ U = ∅.
Базові секвенційні форми числення
QL записуємо згідно відповідних власти-
востей відношення логічного наслідку. До
форм |−∨, −|∨, |–RT, –|RT, |–RR, –|RR, |–R¬,
–|R¬, |–R∨, –|R∨, |–ΦN, –|ΦN, |–R∃, –|R∃, |–R∃S,
–|R∃S, |–∃, –|∃ додаються форми із зовнішнім
запереченням.
|− ¬¬ |
|
,
;
,
A
A
−
−
Σ
¬¬ Σ
−| ¬¬ |
|
,
;
,
A
A
−
−
Σ
¬¬ Σ
|−¬∨ | |
|
, ,
;
( ),
A B
A B
− −
−
¬ ¬ Σ
¬ ∨ Σ
−|¬∨ | |
|
, ,
;
( ),
A B
A B
− −
−
¬ Σ ¬
¬ ∨ Σ
Σ
|–¬RT |
,
| ,
( ),
;
( ),
v
x
z v
z x
R A
R A
−
−
¬ Σ
¬ Σ
–|¬RT |
,
| ,
( ),
;
( ),
v
x
z v
z x
R A
R A
−
−
¬ Σ
¬ Σ
|–¬RR |
|
( ),
;
( ( )),
v w
x y
v w
x y
R A
R R A
−
−
¬ Σ
¬ Σ
o
–|¬RR |
|
( ),
;
( ( )),
v w
x y
v w
x y
R A
R R A
−
−
¬ Σ
¬ Σ
o
|–¬R¬
|
|
( ),
;
( ),
v
x
v
x
R A
R A
−
−
Σ
¬ ¬ Σ
–|¬R¬
|
|
( ),
;
( ),
v
x
v
x
R A
R A
−
−
Σ
¬ ¬ Σ
|–¬R∨ |
|
( ), ( ),
;
( ),
v v
x x
v
x
R A R B
R A B
−
−
¬ ¬ Σ
¬ ∨ Σ
–|¬R∨ | |
|
( ), ( ),
;
( ),
v v
x x
v
x
R A R B
R A B
− −
−
¬ Σ ¬ Σ
¬ ∨ Σ
|–¬ΦN |
,
| ,
( ),
( ),
v
u
y v
z u
R A
R A
−
−
¬ Σ
¬ Σ
при у∈ν(A);
–|¬ΦN |
,
| ,
( ),
( ),
v
u
y v
z u
R A
R A
−
−
¬ Σ
¬ Σ
при у∈ν(A);
|–¬R∃ |
|
( ),
( ),
v
x
v
x
yR A
R yA
−
−
¬∃ Σ
¬ ∃ Σ
при y∉{ ,v x };
–|¬R∃ |
|
( ),
( ),
v
x
v
x
yR A
R yA
−
−
¬∃ Σ
¬ ∃ Σ
при y∉{ ,v x };
|–¬R∃S |
|
( ),
;
( ),
v y
x z
v
x
zR A
R yA
−
−
¬∃ Σ
¬ ∃ Σ
o
–|¬R∃S |
|
( ),
.
( ),
v y
x z
v
x
zR A
R yA
−
−
¬∃ Σ
¬ ∃ Σ
o
За умови y∉{ ,v x } використовуємо
секвенційні форми |–R∃, –|R∃, |–¬R∃, –|¬R∃,
38
Теоретичні та методологічні основи програмування
а якщо y∈{ ,v x }, то використовуємо форми
|–R∃S, –|R∃S, |–¬R∃S, –|¬R∃S.
|–¬∃ | |
|
, ( ),
;
,
x
yxA R A
xA
− −
−
¬∃ ¬ Σ
¬∃ Σ
–|¬∃ |
|
( ),
.
,
x
zR A
xA
−
−
¬ Σ
¬∃ Σ
Для –|¬∃ у тотально строго неістотне
та у∉пт(Σ, А); таке у гарантовано означене.
Застосування форм |–∃, |–¬∃, –|∃, –|¬∃
елімінації кванторів уточняється процеду-
рою побудови секвенційного дерева.
Числення QEqL. Базові секвенційні
форми числення QEqL такі ж, як для QL.
Замкненість секвенції визначається
умовами C, CL, CEqT, CEq¬T, UnD.
Додаткові умови CEqT та CEq¬T
замкненості секвенції у даній вершині сек-
венційного дерева індуковані властивістю
еквітонності. При побудові дерева для неза-
мкненого шляху кожна формула секвенції
рано чи пізно буде розкладена до примітив-
них формул чи їх заперечень. Тому еквітон-
ність достатньо враховувати лише для фор-
мул вигляду ,
, ( )x u
y vR Φ чи ,
, ( )x u
y vR¬ Φ .
Умови CEqT та CEq¬T формулює-
мо на основі властивостей CEqT та CEq¬T.
Нехай Х і Y – множини всіх означе-
них і неозначених імен у даній вершині Σ.
Секвенція Σ TХ–Y -замкнена, якщо ви-
конується одна з умов:
CEqT) існує пара формул |–
,
, ( )x u
y vR Φ ∈Σ та
–|
,
, ( )x u
z vR Φ ∈Σ таких, що z∈X та y∈Y;
CEq¬T) існує пара формул |–
,
, ( )x u
y vR¬ Φ ∈Σ
та –|
,
, ( )x u
z vR¬ Φ ∈Σ таких, що z∈X та y∈Y.
Якщо секвенція |–Γ–|Δ TХ–Y -замкнена,
то Γ A, Х–Y |=T Δ для довільної моделі мови A.
Числення QR. Базові секвенційні
форми числення QR такі ж, як і для чис-
лення QL. Базова умова замкненості секвен-
ції в QR-численні – умова С.
Перша додаткова умова замкненості
секвенції Σ в QR-численні – умова СR:
СR) Σ замкнена, якщо існує формула Φ така,
що –|Φ∈Σ та –|¬Φ∈Σ.
Секвенція Σ замкнена, якщо викону-
ється принаймі одна з умов С чи СR.
Згідно відповідних властивостей С
та СR, якщо |–Γ–|Δ замкнена, то Γ |=F Δ.
Друга додаткова умова – це умова
UnD U-замкненості секвенції Σ.
Числення QEqR. Базові секвенційні
форми числення QEqR такі ж, як для QR.
Замкненість секвенції визначається
умовами C, CR, CEqF, CEq¬F, UnD.
Додаткові умови CEqF та CEq¬F за-
мкненості секвенції у даній вершині дерева
індуковані властивістю еквітонності. Цю
властивість достатньо враховувати лише для
формул вигляду ,
, ( )x u
y vR Φ чи ,
, ( )x u
y vR¬ Φ .
Умови CEqF та CEq¬F формулюємо
на основі властивостей CEqF та CEq¬F.
Нехай Х і Y – множини всіх означе-
них і неозначених імен у даній вершині Σ.
Секвенція Σ FХ–Y -замкнена, якщо ви-
конується одна з умов:
CEqF) існує пара формул |– ,
, ( )x u
z vR Φ ∈Σ та
–|
,
, ( )x u
y vR Φ ∈Σ таких, що z∈X та y∈Y;
CEq¬F) існує пара формул |– ,
, ( )x u
z vR¬ Φ ∈Σ та
–|
,
, ( )x u
y vR¬ Φ ∈Σ таких, що z∈X та y∈Y.
Якщо секвенція |–Γ–|Δ FХ–Y -замкнена,
то Γ A, Х–Y |=F Δ для довільної моделі мови A.
Числення QLR. Базові секвенційні
форми числення QLR такі ж, як і для чис-
лення QL. Базова умова замкненості секвен-
ції в QLR-численні – умова С.
Перша додаткова умова замкненості
секвенції Σ в QLR-численні – умова СLR:
СLR) Σ замкнена, якщо існують формули Φ
та Ψ: |–Φ∈Σ, |–¬Φ∈Σ, –|Ψ∈Σ, –|¬Ψ∈Σ.
Згідно відповідних властивостей С
та СLR, якщо |–Γ–|Δ замкнена, то Γ |=TF Δ.
Друга додаткова умова – це умова
UnD U-замкненості секвенції Σ.
Числення QEqLR. Базові секвен-
ційні форми числення QEqLR такі ж, як для
числення QLR.
Замкненість секвенції визначається
умовами C, CL, CR, CEqT, CEq¬T, CEqF,
CEq¬F, UnD. Для цього необхідно вико-
нання умови C, або одночасного виконання
однієї з умов CL, CEqT, CEq¬T та однієї з
умов CR, CEqF, CEq¬F, або умови UnD.
39
Теоретичні та методологічні основи програмування
3. Побудова секвенційного дерева.
Коректність секвенційних числень
Опишемо процедуру побудови сек-
венційного дерева для заданої секвенції Σ.
Вона придатна для скінченних та злічен-
них секвенцій. Зазначена процедура про-
водиться фактично однаково для числень
QL, QEqL, QR, QEqR, QLR, QEqLR. Заува-
жимо, що ця процедура придатна і для чи-
слень логік неоднозначних предикатів, які
будуть описані в наступній статті. Порів-
няно із відомою [6] процедурою для чис-
лення QEqCl логіки еквітонних предикатів,
описувана процедура істотно складніша.
Для числення QCl подібна процедура за-
пропонована в [3], із невеликими змінами
вона підходить для числень, які формалі-
зують |=T , |=F та |=TF (необхідно врахувати
наявність "дублікатів" секвенційних форм
для зовнішнього заперечення, а також спе-
цифічні для кожного числення умови замк-
неності секвенцій).
Для відношень |=T , |=F , |=TF , а та-
кож для відношення |=Cl в загальному ви-
падку (нееквітонність) треба враховувати,
що значення предиката P(d) може бути різ-
ним залежно від того, входить чи не вхо-
дить до d компонента з певним предмет-
ним іменем. Тому при інтерпретаціях фор-
мул треба явно вказувати множини означе-
них та неозначених імен. У процедурі по-
будови дерева така особливість проявляє-
ться при формуванні прикладів для специ-
фікованих формул вигляду –|∃uΦ та |–¬∃uΦ
за допомогою –|∃-форм та |–¬∃-форм: при-
клади можуть мати тільки вигляд відпові-
дно –| ( )u
yR Φ та |– ( ),u
yR¬ Φ де у означене.
Таким чином, при застосуванні –|∃-
форми чи |–¬∃-форми треба перебрати всі
можливі випадки розподілу наявних пред-
метних імен на означені й неозначені. Це
можна реалізувати за допомогою побудови
відповідних розгалужень секвенційного де-
рева: якщо у вершині Ξ вперше на етапі до
формули вигляду –|∃uΦ чи |–¬∃uΦ застосо-
вується –|∃-форма чи |–¬∃-форма, то для Ξ
будується не одна, а багато вершин-"сестер",
які є безпосередніми предками Ξ і мають од-
ну й ту ж множину наявних імен та відріз-
няються лише різними множинами означе-
них імен та відповідними множинами прик-
ладів вигляду –| ( )u
yR Φ чи |– ( ).u
yR¬ Φ Розпо-
діл імен на означені й неозначені індукує
також додаткову умову UnD замкненості
секвенції-вершини.
Процедура побудови дерева для
секвенції Σ починається з кореня дерева.
Таку процедуру розіб'ємо на етапи. Кожне
застосування секвенційної форми прово-
диться до скінченної множини доступних
на даний момент формул. На початку кож-
ного етапу виконується крок доступу: до
списку доступних формул додаємо по од-
ній формулі з списків |–-формул та –|-фор-
мул. Якщо недоступних |–-формул чи
–|-формул немає (відповідний список ви-
черпано), то на подальших кроках доступу
додаємо по одній формулі невичерпаного
списку.
На початку побудови доступна ли-
ше пара перших формул списків (або єди-
на |–-формула чи –|-формула, якщо один з
списків порожній).
Перед побудовою дерева для секвен-
ції Σ зафіксуємо деякий список TN (не-
скінченний) тотально строго неістотних
імен ("нових" імен) такий, що імена із TN
не зустрічаються у формулах секвенції Σ.
Із кожною вершиною дерева пов'я-
зуємо множину наявних та множину озна-
чених предметних імен. Множина означе-
них імен явно виділяється лише на шляхах,
де були хоч раз застосовані –|∃-форми чи
|–¬∃-форми (до такого застосування явне
виділення множини означених імен непот-
рібне). Множина наявних імен – це мно-
жина імен усіх формул, які доступні на
шляху від кореня до даної вершини. Усі
тотально строго неістотні імена, задіяні
при застосуванні |–∃-форм чи –|¬∃-форм, у
даному виведенні гарантовано означені.
Нехай виконано k етапів процедури.
На етапі k+1 перевіряємо, чи буде кожен з
листів дерева замкненою секвенцією (бе-
ремо до уваги тільки доступні формули
секвенцій).
Якщо всі листи замкнені, то проце-
дура завершена позитивно, ми отримали
замкнене секвенційне дерево.
40
Теоретичні та методологічні основи програмування
Якщо ні, то для кожного незамкне-
ного листа ξ робимо наступний крок до-
ступу, після чого добудовуємо скінченне
піддерево з вершиною ξ. Для цього активі-
зуємо всі доступні формули ξ, які не є при-
мітивними чи їх запереченнями. Далі по
черзі до кожної активної формули застосо-
вуємо відповідну секвенційну форму.
Секвенційні форми |–RT, –|RT, та
|–¬RT –|¬RT допоміжні: перед застосуван-
ням однієї з форм іншого типу усуваємо, у
разі наявності, тотожні перейменування,
застосовуючи належну кількість разів фор-
ми типу RT чи ¬RT.
Спочатку виконуємо всі |–∃-форми
та –|¬∃-форми. Застосування кожної такої
форми додає нове тотально неістотне ім'я у
до множини означених імен вершини, таке
у беремо як перше незадіяне на даному
шляху від кореня ім'я зі списку TN. Ім'я у
гарантовано означене, додаємо його до
множин наявних та означених імен; далі
для кожної доступної формули вигляду
–|∃uΦ чи |–¬∃uΦ додаємо відповідно при-
клад –| ( )u
yR Φ чи |– ( )u
yR¬ Φ .
Далі виконуємо R∃S-форми та
¬R∃S-форми, при цьому беремо
z∉ ( ( ))v
xnm R x∃ Φ із задіяних на даному
шляху від кореня дерева імен списку TN,
якщо такі є, інакше беремо z як перше ім'я
списку TN. В останньому випадку таке z
додаємо до множин наявних та означених
імен, далі для кожної доступної формули
вигляду –|∃uΨ чи |–¬∃uΨ додаємо приклад
–| ( )u
zR Ψ чи |– ( )u
zR¬ Ψ .
Після цього до кожної з решти ак-
тивних формул застосовуємо відповідну
форму – одну з форм типу ¬, ¬¬, ∨, ¬∨,
ΦN, ¬ΦN, RR, ¬RR, R¬, ¬R¬, R∨, ¬R∨,
R∃, ¬R∃.
Далі застосовуємо –|∃-форми та |–¬∃-
форми. Це робимо наступним чином.
Якщо –|∃-форма чи |–¬∃-форма впер-
ше застосується на шляху від кореня дере-
ва, то із даної вершини будуємо розгалу-
ження дерева. Для кожної вершини, що є
безпосереднім предком даної, задаємо мно-
жину означених імен як певну підмножину
наявних, при цьому до неї мусять входити
усі тотально строго неістотні імена, задіяні
при попередніх застосуваннях |–∃- та –|¬∃-
форм на шляху від кореня до даної вершини.
Нехай у даній вершині Σ із множи-
ною наявних імен Z –|∃-форма чи |–¬∃-фор-
ма застосовується вперше на шляху від ко-
реня до Σ. Це означає, що на цьому шляху
ще не було явного виділення множин означе-
них та неозначених імен, окрім, можливо,
виділення гарантовано означених при попе-
редніх застосуваннях |–∃- та –|¬∃-форм. Не-
хай G – множина гарантовано означених
імен, задіяних при застосуванні |–∃-форм та
–|¬∃-форм на шляху від кореня до даної вер-
шини Σ, нехай –|∃хΦ чи |–¬∃хΦ – та специ-
фікована формула, до якої застосовується
–|∃-форма чи |–¬∃-форма. Добудовуємо без-
посередніх предків вершини Σ для кожної
X ⊆ Z\G (фактично розглядаємо всеможливі
розподіли імен із Z\G на означені й неозна-
чені). Тоді X∪G та Z\(X∪G) – це множини
означених та неозначених імен відповідної
вершини-предка. В кожній такій вершині-
предку додаємо приклад –| ( )x
zR Φ формули
–|∃хΦ чи приклад |– ( )x
zR¬ Φ формули
|–¬∃хΦ для кожного z∈X∪G; надалі в усіх
шляхах із цієї вершини-предка імена із
X∪G означені.
Окремого розгляду вимагає випадок
G = ∅. Тоді для вершини-предка із X = ∅ ма-
ємо X∪G = ∅, тому при додаванні приклада
формули –|∃хΦ чи |–¬∃хΦ необхідно взяти
нове тотально строго неістотне імя (такий
вибір зумовлений необхідністю збереження
відношення логічного наслідку, див. власти-
вість TotN). Тому беремо із TN тотально
строго неістотне t∉nm(Σ) та записуємо при-
клад –| ( )x
tR Φ чи приклад |– ( )x
tR¬ Φ .
Нехай у вершині Σ з множинами на-
явних імен Z та означених імен W до –|∃хΦ
чи |–¬∃хΦ вперше на етапі застосовується
–|∃-форма чи |–¬∃-форма, проте застосування
–|∃-форм та |–¬∃-форм на на шляху від коре-
ня до вершини Σ вже були, тому для Σ мно-
жини означених та неозначених імен вже
виділені. Розширення множини наявних
імен при появі нових доступних формул
після виконання кроку доступу веде також
до повторного застосування –|∃-форм та
41
Теоретичні та методологічні основи програмування
|–¬∃-форм до старих доступних формул.
Нехай X – множина доданих нових
імен після виконання кроку доступу у вер-
шині з множинами наявних імен Z та озна-
чених імен W. Перше на етапі застосу-
вання –|∃-форми до –|∃хΦ чи |–¬∃-форми до
|–¬∃хΦ дає розгалуження для кожної Y ⊆ X, у
кожній такій вершині-предку для кожного
z∈Y∪W додаємо –| ( )x
zR Φ чи |– ( )x
zR¬ Φ , при
цьому множиною наявних імен вершини-
предка буде Z∪X, множиною означених
імен буде W∪Y. Якщо застосування –|∃-фор-
ми чи |–¬∃-форми не перше на етапі, то в
даній вершині X = ∅, тобто вже немає імен,
нерозподілених на означені й неозначені.
Тоді в єдиній вершині-предку для кожного
z∈W додаємо –| ( )x
zR Φ чи |– ( )x
zR¬ Φ .
Всі повтори специфікованих фор-
мул у секвенції усуваємо.
Після виконання базової секвенцій-
ної форми (окрім допоміжних типу RT чи
¬RT) формула дезактивується і стає па-
сивною. До пасивних та утворених на да-
ному етапі формул базові секвенційні фор-
ми незастосовні.
При побудові секвенційного дерева
можливі такі випадки:
1) процедуру завершено позитивно,
маємо скінченне замкнене дерево;
2) процедуру завершено негативно,
маємо скінченне незамкнене дерево;
3) процедура не завершується, маємо
нескінченне незамкнене дерево. За лемою
Кеніга [7] нескінченне дерево зі скінченним
розгалуженням має хоча б один нескінчен-
ний шлях. Вершини цього шляху не можуть
бути замкненими секвенціями, тому що при
появі замкненої секвенції до неї незасто-
совна жодна секвенційна форма, і процес
побудови для цього шляху обривається.
Отже, у випадках 2) і 3) у дереві іс-
нує скінченний чи нескінченний шлях ℘,
усі вершини якого – незамкнені секвенції.
Такий шлях назвемо незамкненим. Кожна
з формул секвенції Σ зустрінеться на цьо-
му шляху і стане доступною.
Із наведеної процедури побудови
секвенційного дерева випливає, що для
кожної його вершини |–Λ–|Κ з множинами
означених імен W та неозначених імен U
для кожної моделі мови A справджується
Λ A, W–U |=∗ Κ (тут ∗ – одне з Cl, T, F, TF).
Для листів дерева це випливає з ви-
конання умов замкненості секвенції:
– для числень QL, QR, QLR – умов
замкненості та U-замкненості;
– для числення QEqL – умов замкне-
ності, U-замкненості, TХ–Y –замкненості;
– для числення QEqR – умов замкне-
ності, U-замкненості, FХ–Y –замкненості;
– для числення QEqLR – умов зам-
кненості, U-замкненості, TХ–Y –замкненості,
FХ–Y –замкненості.
Збереження секвенційними формами
(від засновків до висновків) вищезазначених
відношень логічного наслідку виконується
для секвенційних форм типу ¬, ¬¬, ∨, ¬∨,
RT, ¬RT, ΦN, ¬ΦN, RR, ¬RR, R¬, ¬R¬,
R∨, ¬R∨, R∃, ¬R∃, R∃S, ¬R∃S. Це безпо-
середньо випливає із відповідних властивос-
тей для відношень логічного наслідку.
Окремого розгляду вимагають фор-
ми для елімінації кванторів.
Для |–∃-форм та –|¬∃-форм збере-
ження відповідних відношень логічного
наслідку від засновку до висновку гаран-
тується властивостями ∃ Х–Y |– та ¬∃ Х–Y –| , а
також TotN.
Для –|∃-форм та |–¬∃-форм збережен-
ня відповідних відношень логічного наслідку
при русі до вершини Σ, яка містить активну
–|∃хΦ чи |–¬∃хΦ, від вершин, які є її безпосе-
редніми предками та містять приклади ви-
гляду –| ( )x
zR Φ чи |– ( )x
zR¬ Φ , гарантується
властивостями Br∃, Br¬∃, а також TotN.
Нехай секвенція |–Γ–|Δ вивідна, тоді
для неї згідно нашої процедури збудоване
замкнене секвенційне дерево. При такій
побудові введені |–∃-формами та –|¬∃-фор-
мами (в окремих випадках також –|∃-форма-
ми та |–¬∃-формами) нові тотально строго
неістотні імена гарантовано означені в цьо-
му виведенні секвенції |–Γ–|Δ, тому можна
обмежитись розглядом тільки інтерпретацій
(моделей мови) A із G-означеними даними,
де G – множина таких гарантовано означе-
них імен. Неформально кажучи, гарантовано
означені імена ведуть себе подібно до конс-
тантних символів класичної логіки предика-
тів. Беручи до уваги TotN, отримуємо:
Γ |=∗ Δ ⇔ для кожної A маємо Γ A |=∗ Δ ⇔
42
Теоретичні та методологічні основи програмування
⇔ для кожної A маємо Γ A, G |=∗ Δ, де G –
множина таких гарантовано означених то-
тально строго неістотних імен (тут ∗ – одне
з Cl, T, F, TF для відповідного числення).
Таким чином, для побудованих сек-
венційних числень справджується теорема
коректності. Для різних числень та наслід-
ків вона формулюється однотипно.
Теорема 1 (коректності). Нехай сек-
венція |–Γ–|Δ вивідна. Тоді Γ |= Δ.
Для різних числень та відношень
логічного наслідку теорема 1 конкретизу-
ється так.
Теорема коректності. Нехай сек-
венція |–Γ–|Δ вивідна в QCl-численні. Тоді
Γ |=Cl Δ.
Нехай |–Γ–|Δ вивідна в QEqCl-чис-
ленні. Тоді Γ |=Cl Δ для логіки еквітонних
предикатів.
Нехай |–Γ–|Δ вивідна в QL-численні.
Тоді Γ |=T Δ.
Нехай |–Γ–|Δ вивідна в QEqL-чис-
ленні. Тоді Γ |=T Δ для логіки еквітонних
предикатів.
Нехай |–Γ–|Δ вивідна в QR-численні.
Тоді Γ |=F Δ.
Нехай |–Γ–|Δ вивідна в QEqR-чис-
ленні. Тоді Γ |=F Δ для логіки еквітонних
предикатів.
Нехай |–Γ–|Δ вивідна в QLR-чис-
ленні. Тоді Γ |=TF Δ.
Нехай |–Γ–|Δ вивідна в QEqLR-чис-
ленні. Тоді Γ |=TF Δ для логіки еквітонних
предикатів.
4. Модельні множини
Для доведення повноти збудованих
секвенційних числень використаємо метод
модельних (хінтікківських) множин [5, 6].
Для різних секвенційних числень визначен-
ня модельної множини дещо відмінні
Числення QL. Нехай Н – множина
специфікованих формул із виділеною мно-
жиною W ⊆ nm(Н) означених імен; тоді
U = nm(Н) \ W – множина її неозначених
імен.
Множина Н L-модельна, якщо ви-
конуються такі умови.
НС) не існує формули Φ такої, що
|–Φ∈Н та –|Φ∈Н.
НСL) не існує формули Φ такої, що
|–Φ∈Н та |–¬Φ∈Н.
НСU) не існує пари формул вигляду
|–
v
xR A∈Н та –|
u
yR A∈Н таких, що v
xR A та
u
yR A мають однакові U-неозначувані
форми.
НС, НСL та НСU – це умови корек-
тності L-модельної можини.
Н¬¬) якщо |–¬¬Φ∈Н, то |–Φ∈Н;
якщо –|¬¬Φ∈Н,то –|Φ∈Н.
Н∨) якщо |–Φ∨Ψ∈Н, то |–Φ∈Н або |–Ψ∈Н;
якщо –|Φ∨Ψ∈Н, то –|Φ∈Н та –|Ψ∈Н.
Н¬∨) якщо |–¬(Φ∨Ψ)∈Н, то
|–¬Φ∈Н та |–¬Ψ∈Н;
якщо –|¬(Φ∨Ψ)∈Н, то
–|¬Φ∈Н або –|¬Ψ∈Н.
НRT) якщо |– ,
, ( )z v
z xR Φ ∈Н, то |– ( )v
xR Φ ∈Н;
якщо –|
,
, ( )z v
z xR Φ ∈Н, то –| ( )v
xR Φ ∈Н.
Н¬RT) якщо |– ,
, ( )z v
z xR¬ Φ ∈Н, то
|– ( )v
xR¬ Φ ∈Н;
якщо –|
,
, ( )z v
z xR¬ Φ ∈Н, то –| ( )v
xR¬ Φ ∈Н.
НRR) якщо |– ( ( )v w
x yR R Φ )∈Н, то
|– ( )v w
x yR Φo ∈Н;
якщо –| ( ( )v w
x yR R Φ )∈Н, то –
| ( )v w
x yR Φo ∈Н.
Н¬RR) якщо |– ( ( )v w
x yR R )¬ Φ ∈Н, то
|– ( )v w
x yR¬ Φo ∈Н;
якщо –| ( ( )v w
x yR R )¬ Φ ∈Н, то
–| ( )v w
x yR¬ Φo ∈Н.
НR¬) якщо |– (v
xR )¬Φ ∈Н, то
|– ¬ ( )v
xR Φ ∈Н;
якщо –| (v
xR )¬Φ ∈Н, то –| ¬ ( )v
xR Φ ∈Н.
Н¬R¬) Якщо |– (v
xR )¬ ¬Φ ∈Н, то
|– ( )v
xR Φ ∈Н;
якщо –| (xR )v¬ ¬Φ ∈Н, то –| ( )xR Φv ∈Н.
НR∨) якщо |– v
xR (Φ∨Ψ)∈Н, то
|–
v
xR (Φ)∨ v
xR (Ψ)∈Н;
якщо –|
v
xR (Φ∨Ψ)∈Н, то –|
v
xR (Φ)∨ v
xR (Ψ)∈Н.
Н¬R∨) якщо |– (xR )v¬ Φ∨Ψ ∈Н, то
43
Теоретичні та методологічні основи програмування
|– ( )v
xR¬ Φ ∈Н та |– ( )v
xR¬ Ψ ∈Н;
якщо –| (v
xR¬ Φ∨Ψ)∈Н, то
–| ( )v
xR¬ Φ ∈Н або –| ( )v
xR¬ Ψ ∈Н.
НΦN) якщо |– ,
, ( )y v
z xR Φ ∈Н та у∈ν(Φ),
то |– ( )v
xR Φ ∈Н;
якщо –|
,
, ( )y v
z xR Φ ∈Н та у∈ν(Φ), то
–| ( )v
xR Φ ∈Н.
Н¬ΦN) якщо |– ,
, ( )y v
z xR¬ Φ ∈Н та у∈ν(Φ), то
|– ( )v
xR¬ Φ ∈Н;
якщо –|
,
, ( )y v
z xR¬ Φ ∈Н та у∈ν(Φ), то
–| ( )v
xR¬ Φ ∈Н.
НR∃) якщо |– (v
xR y∃ Φ)∈Н та y∉{ ,v x }, то
|– ( )v
xyR∃ Φ ∈Н;
якщо –| (xR y∃ Φ)v ∈Н тa y∉{ ,v x }, то
–| ( )xyR∃ Φv ∈Н.
Н¬R∃) якщо |– (xR y¬ ∃ Φ)v ∈Н та y∉{ ,v x },
то |– ( )xyR¬∃ Φv ∈Н;
якщо –| (xR y¬ ∃ Φ)v ∈Н тa y∉{ ,v x }, то
–| ( )xyRv Φ¬∃ ∈Н.
НR∃S) якщо |– ( )vR y∃ Φx ∈Н та y∈{ ,v x }, то
|– ( )v yzR ox z∃ Φ ∈Н;
якщо –| ( )vR y∃ Φx ∈Н та y∈{ , xv }, то
–| ( )v yzR ox z∃ Φ ∈Н.
Н¬R∃S) якщо |– ( )vR y¬ ∃ Φx ∈Н та y∈{ ,v x },
то |– ( )v yzR¬∃ Φox z ∈Н;
якщо –| ( )v
xR y¬ ∃ Φ ∈Н та y∈{ , xv }, то
–| ( )v y
x zzR Φo¬∃ ∈Н.
Для НR∃S та Н¬R∃S z строго тота-
льно неістотне та z∉ ( ( ))vnm R y∃ Φ
( )xR Φ
( )xR Φ
( )xR Φ
( )xR Φ
x .
Н∃) якщо |–∃хΦ∈Н, то існує у∈W таке, що
|– y ∈Н;
якщо –|∃хΦ∈Н, то для всіх у∈W маємо
–| y ∈Н.
Н¬∃) якщо |–¬∃хΦ∈Н, то для всіх у∈W
маємо |– y¬ ∈Н;
якщо –|¬∃хΦ∈Н, то існує у∈W таке, що
–| y¬ ∈Н.
Числення QEqL. Множина Н спе-
цифікованих формул із виділеними мно-
жинами W ⊆ nm(Н) означених імен та
U = nm(Н) \ W неозначених імен EqL-мо-
дельна, якщо виконуються вищенаведені
умови для L-модельної множини та додат-
кові умови коректності:
НCEqT) не існує пари формул |–
,
, ( )x u
y vR Φ ∈Н
та –|
,
, ( )x u
z vR Φ ∈Н таких: z∈W та y∈U;
НCEq¬T) не існує пари формул
|–
,
, ( )x u
y vR¬ Φ ∈Н та –|
,
, ( )x u
z vR¬ Φ ∈Н таких:
z∈W та y∈U.
Числення QR. Множина Н специфі-
кованих формул із виділеними множинами
W ⊆ nm(Н) означених імен та U = nm(Н) \ W
неозначених імен R-модельна, якщо вико-
нуються умови НС, НСU, Н¬¬, Н∨, Н¬∨,
НRT, НRR, НR¬, НR∨, НΦN, Н¬RT,
Н¬RR, Н¬R¬, Н¬R∨, Н¬ΦN, НR∃, Н¬R∃,
НR∃S, Н¬R∃S, Н∃, Н¬∃, а також НСR:
НСR) не існує формули Φ такої, що –|Φ∈Н
та –|¬Φ∈Н.
Тут НС та НСR – умови коректності
R-модельної можини.
Числення QEqR. Множина Н специ-
фікованих формул із виділеними множи-
нами W ⊆ nm(Н) означених імен та
U = nm(Н) \ W неозначених імен EqR-мо-
дельна, якщо виконуються вищенаведені
умови для R-модельної множини та додат-
кові умови коректності:
НCEqF) не існує пари формул
|–
,
, ( )x u
z vR Φ ∈Н та –|
,
, ( )x u
y vR Φ ∈Н таких:
z∈W та y∈U;
НCEq¬F) не існує пари формул
|–
,
, ( )x u
z vR¬ Φ ∈Н та –|
,
, ( )x u
y vR¬ Φ ∈Н таких:
z∈W та y∈U.
Числення QLR. Множина Н специ-
фікованих формул із виділеними множи-
нами W ⊆ nm(Н) означених імен та
U = nm(Н) \ W неозначених імен LR-моде-
льна, якщо виконуються умови Н¬¬, Н∨,
Н¬∨, НRT, НRR, НR¬, НR∨, НΦN, Н¬RT,
Н¬RR, Н¬R¬, Н¬R∨, Н¬ΦN, НR∃, Н¬R∃,
НR∃S, Н¬R∃S, Н∃, Н¬∃, а також наступні
умови коректності LR-модельної множини:
НС, НСL або НСR, НСU.
44
Теоретичні та методологічні основи програмування
Замість умови "НСL або НСR" тут
можна брати рівносильну умову:
НСLR) не існують формули Φ та Ψ такі, що
|–Φ∈Н, |–¬Φ∈Н та –|Ψ∈Н, –|¬Ψ∈Н.
Секвенційне числення QEqLR. Мно-
жина Н специфікованих формул із виділе-
ними множинами W ⊆ nm(Н) означених
імен та U = nm(Н) \ W неозначених імен
EqLR-модельна, якщо виконуються вище-
наведені умови для LR-модельної мно-
жини з наступними умовами коректності:
НС, НСL, НСU, НCEqT, НCEq¬T; або НС,
НСR, НСU, НCEqF, НCEq¬F.
Числення QCl. Множина Н специфі-
кованих формул із виділеними множинами
W ⊆ nm(Н) означених імен та U = nm(Н) \ W
неозначених імен C-модельна, якщо вико-
нуються умови НС, НСU, Н∨, НRT, НRR,
НR¬, НR∨, НΦN, НR∃, НR∃S, Н∃ та Н¬:
Н¬) якщо |–¬Φ∈Н, то –|Φ∈Н;
якщо –|¬Φ∈Н, то |–Φ∈Н.
НС та НСU – це умови коректності
C-модельної можини.
Зауважимо, що визначення L-мо-
дельної, EqL-модельної, R-модельної, EqR-
модельної, LR-модельної, EqLR-модельної
множини відрізняються тільки різними
умовами їх коректності.
5. Повнота секвенційних числень
Теорема 2. Нехай ℘ – незамкнений
шлях у секвенційному дереві, Н – множи-
на всіх специфікованих формул секвенцій
цього шляху. Тоді Н – модельна множина
відповідного типу (C-модельна, L-модель-
на, EqL-модельна, R-модельна, EqR-мо-
дельна, LR-модельна, EqLR-модельна).
Справді, для переходу від нижчої
вершини шляху до вищої використовуєть-
ся одна з базових секвенційних форм від-
повідного числення. Переходи згідно з та-
кими формами узгодженні з однойменни-
ми пунктами визначення модельної мно-
жини відповідного типу. Кожна формула,
яка не є примітивною чи її запереченням,
що зустрічається на шляху ℘, рано чи піз-
но буде розкладена чи спрощена згідно з
відповідною секвенційною формою. Усі
секвенції шляху ℘ незамкнені, тому вико-
нані відповідні умови коректності модель-
ної множини відповідного типу:
– НС та НСU для C-модельної;
– НС, НСL та НСU для L-модельної;
– НС, НСL, НCEqT, НCEq¬T та НСU
для EqL-модельної;
– НС, НСR та НСU для R-модельної;
– НС, НСR, НCEqF, НCEq¬F та НСU
для EqR-модельної;
– НС, НСLR та НСU для LR-модель-
ної;
– НС, НСL, НСU, НCEqT, НCEq¬T або
НС, НСR, НСU, НCEqF, НCEq¬F для
EqLR-модельної.
Наступні твердження фактично за-
дають побудову контрмоделей при відсут-
ності логічного наслідку. Вони формулю-
ються для різних типів модельних множин.
Теорема 3. Нехай Н – модельна
множина, яка може бути L-модельною,
EqL-модельною, R-модельною, EqR-моде-
льною, LR-модельною, EqLR-модельною.
Тоді існують моделі мови АС A = (A, I) і
BB = (A, I) та δ, η∈ A такі: V
1) |–Φ∈Н ⇒ δ∈T(ΦA) та –|Φ∈Н ⇒ δ∉T(ΦA);
2) |–Φ∈Н ⇒ η∉F(ΦB) та B –|Φ∈Н ⇒ η∈F(ΦBB).
Пари (A, δ) та (B, η) із такими влас-
тивостями відповідно назвемо T-контрмо-
деллю та F-контрмоделлю.
Доведення теореми 3 не залежить
від умови однозначності предикатів, це
враховано при виборі позначень. Ми пи-
шемо d∈T(P), d∈F(P), d∉T(P), d∉F(P), що
для однозначних предикатів можна записа-
ти P(d) = T, P(d) = F, невірно P(d) = T, неві-
рно P(d) = F. Тут T(P) = {d∈VA | T∈P(d)} та
F(P) = {d∈VA | F∈P(d)} – області істиннос-
ті та хибності квазіарного предиката Р.
Нехай W – множина всіх означених
предметних імен, що фігурують у Н.
Візьмемо деяку множину А таку, що
|А| = |W|, та деякі ін'єктивні δ, η∈VA з
im(δ) = W. Така А дублює множину W.
Доведення теореми проведемо ін-
дукцією за складністю формули згідно з
побудовою модельної множини.
Спочатку задамо значення базових
предикатів та їх заперечень на δ та η, а та-
кож на ІМ вигляду r v
x (δ) та r v
x (η):
– якщо |– р∈Н, то задамо δ∈T(рA);
– якщо –| р∈Н, то задамо δ∉T(рB); B
45
Теоретичні та методологічні основи програмування
– якщо |– р∈Н, то задамо η∉F(рB); B
– якщо –| р∈Н, то задамо η∈F(рA);
– якщо |–¬р∈Н, то δ∈F(pA) = T(¬pA);
– якщо –|¬p∈Н, то δ∉F(pA) = T(¬pA);
– якщо |–¬p∈Н, то η∉T(pB) = F(¬pB BB);
– якщо –|¬p∈Н, то η∈T(pB) = F(¬pB BB);
– якщо |– ( )v
xR p ∈Н, то задамо r v
x (δ)∈T(рA);
– якщо –| ( )v
xR p ∈Н, то задамо r v
x (δ)∉T(рA);
– якщо |– ( )v
xR p ∈Н, то задамо r v
x (η)∉F(рB); B
– якщо –| ( )v
xR p ∈Н, то задамо r v
x (η)∈F(рB); B
– якщо |– ( )v
xR p¬ ∈Н, то задамо
r v
x (δ)∈F(pA) = T(¬pA);
– якщо –| ( )v
xR p¬ ∈Н, то задамо
r v
x (δ)∉F(pA) = T(¬pA);
– якщо |– ( )v
xR p¬ ∈Н, то задамо
r v
x (η)∉T(pB) = F(¬pB BB);
– якщо –| ( )v
xR p¬ ∈Н, то задамо
r v
x (η)∈T(pB) = F(¬pB BB).
В усіх інших випадках значення ба-
зових предикатів та їх заперечень можна
задавати довільно, беручи до уваги обме-
ження щодо строго неістотності: для всіх
d, h∈VA таких, що d║-ν(p) = h║-ν(p), необ-
хідно рA(d) = рA(h), ¬рA(d) = ¬рA(h), рB(d) =
= р
B
BB(h), ¬рB(d) = ¬рB BB(h). Це враховує стро-
го неістотність імен у∈ν(p) для рA та рB .
Для випадків EqL-модельної, EqR-
модельної чи EqLR-модельної множини ви-
щезадані значення базових предикатів та їх
заперечень продовжимо, ураховуючи умови
еквітонності та строго неістотності імен, на
відповідні h∈VA. В усіх інших випадках зна-
чення базових предикатів та їх заперечень
задаємо довільно, беручи до уваги обмежен-
ня щодо еквітонності та строго неістотнос-
ті. Таким чином, значення базових преди-
катів та їх заперечень визначені коректно.
Для атомарних формул і формул ви-
гляду ( )v
xR p та їх заперечень твердження
теореми випливають з вищенаведеного ви-
значення значень базових предикатів та їх
заперечень.
Доведемо крок індукції.
Нехай |–¬¬Φ∈Н. Згідно Н¬¬ маємо
|–Φ∈Н. За припущенням індукції для δ ма-
ємо δ∈T(ΦA), звідки δ∈T(¬¬ΦA). За при-
пущенням індукції для η маємо η∉F(ΦB),
звідки η∉F(¬¬Φ
B
BB).
Нехай –|¬¬Φ∈Н. Згідно Н¬¬ маємо
–|Φ∈Н. За припущенням індукції для δ ма-
ємо δ∉T(ΦA), звідки δ∉T(¬¬ΦA). За при-
пущенням індукції для η маємо η∈F(ΦB),
звідки η∈F(¬¬Φ
B
BB).
Нехай |–Φ∨Ψ∈Н. Згідно Н∨ маємо
|–Φ∈Н або |–Ψ∈Н. За припущенням індук-
ції для δ маємо δ∈T(ΦA) або δ∈T(ΨA), звід-
ки δ∈T(ΦA)∪T(ΨA) = T(Φ∨ΨA). За припу-
щенням індукції для η маємо η∉F(ΦB) або
η∉F(Ψ
B
BB), тому η∉F(ΦB)∩F(ΨB BB) = F(Φ∨ΨB). B
Нехай –|Φ∨Ψ∈Н. Згідно Н∨ маємо
–|Φ∈Н та –|Ψ∈Н. За припущенням індукції
для δ маємо d∉T(ΦA) та d∉T(ΨA), звідки
d∉T(ΦA)∪T(ΨA) = T(Φ∨ΨA). За припущен-
ням індукції для η тоді η∈F(ΦB) і η∈F(ΨB BB),
звідки η∈F(ΦB)∩F(ΨB BB) = F(Φ∨ΨB). B
Нехай |–¬(Φ∨Ψ)∈Н. Згідно Н¬∨ ма-
ємо |–¬Φ∈Н та |–¬Ψ∈Н. За припущенням
індукції для δ тоді δ∈T(¬ΦA) та δ∈T(¬ΨA),
звідки δ∈F(ΦA) та δ∈F(ΨA), тому
δ∈F(ΦA)∩F(ΨA) = F(Φ∨ΨA) = T(¬(Φ∨Ψ)A).
За припущенням індукції для η маємо
η∉F(¬ΦB) та η∉F(¬ΨB BB), звідки η∉T(ΦB)
та η∉T(Ψ
B
BB), тому η∉T(ΦB)∪T(ΨB BB) =
= T(Φ∨ΨB) = F(¬(Φ∨Ψ)B BB).
Нехай –|¬(Φ∨Ψ)∈Н. Згідно Н¬∨ ма-
ємо –|¬Φ∈Н або –|¬Ψ∈Н. За припущенням
індукції для δ маємо δ∉T(¬ΦA) або
δ∉T(¬ΨA), звідки δ∉F(ΦA) або δ∉F(ΨA),
тому маємо δ∉F(ΦA)∩F(ΨA) = F(Φ∨ΨA) =
= T(¬(Φ∨Ψ)A). За припущенням індукції
для η маємо η∈F(¬ΦB) або η∈F(¬ΨB BB), зві-
дки η∈T(ΦB) або η∈T(ΨB BB), тому
η∈T(ΦB)∪T(ΨB BB) = T(Φ∨ΨB) = F(¬(Φ∨Ψ)B BB).
Нехай |–
,
, ( )z v
z xR Φ ∈Н. Згідно НRT ма-
ємо |– ( )v
xR Φ ∈Н. За припущенням індукції
для δ маємо δ∈T( ( )v
x AR Φ ), звідки
δ∈T( ,
, (z v
z x AR )Φ ). За припущенням індукції
для η маємо η∉F( ( )v
x BR Φ ), звідки
η∉F( ,
, ( )z v
z x BR Φ ).
Нехай –|
,
, ( )z v
z xR Φ ∈Н. Згідно НRT ма-
46
Теоретичні та методологічні основи програмування
ємо –| ( )v
xR Φ ∈Н. За припущенням індукції
для δ маємо δ∉T( ( )v
x AR Φ ), звідки
δ∉T( ,
, (z v
z x AR Φ ) ). За припущенням індукції
для η маємо η∈F( ( )v
x BR Φ ), звідки
η∈F( ,
, (z v
z x BR Φ ) ).
Нехай |– ( ( )v w
x yR R Φ )∈Н. Згідно НRR
маємо |– ( )v w
x yR Φo ∈Н. За припущенням ін-
дукції для δ маємо δ∈T( ( )v w
x yR Φo A ), звідки
δ∈T( ( ( ))v w
x yR R Φ A ). За припущенням індук-
ції для η маємо η∉F( ( )v w
x yR Φo B ), звідки
η∉F( ( ( ))v w
x y BR R Φ ).
Нехай –| ( ( )v w
x yR R Φ )∈Н. Згідно НRR
маємо –| ( )v w
x yR Φo ∈Н. За припущенням ін-
дукції для δ маємо δ∉T( ( )v w
x yR Φo A ), звідки
δ∉T( ( ( ))v w
x yR R Φ A ). За припущенням індук-
ції для η маємо η∈F( ( )v w
x yR Φo B ), звідки
η∈F( ( ( ))v w
x y BR R Φ ).
Нехай |– (v
xR ¬Φ)∈Н. Згідно НR¬
маємо |– ( )v
xR¬ Φ ∈Н. За припущенням ін-
дукції для δ маємо δ∈T( ( )v
x AR ¬Φ ), звідки
δ∈T( ( )v
x AR¬ Φ ). За припущенням індукції
для η маємо η∉F( ( )v
x BR ¬Φ ), звідки
η∉F( ( )v
x BR¬ Φ ).
Нехай –| (v
xR ¬Φ)∈Н. Згідно НR¬
маємо –| ( )v
xR¬ Φ ∈Н. За припущенням ін-
дукції для δ маємо δ∉T( ( )v
x AR ¬Φ ), звідки
δ∉T( ( )v
x AR¬ Φ ). За припущенням індукції
для η маємо η∈F( ( )v
x BR ¬Φ ), звідки
η∈F( ( )v
x BR¬ Φ ).
Нехай |– (v
xR Φ∨Ψ)∈Н. Згідно НR∨
маємо |– ( ) ( )x xR RΦ ∨ Ψv v ∈Н. За припущен-
ням індукції для δ маємо
δ∈T( ( ) ( )v v
x xR RΦ ∨ Ψ A ), звідки отримуємо
δ∈T( ( )v
x AR Φ∨Ψ ). За припущенням індук-
ції для η маємо η∉F( ( ) ( )v v
x x BR RΦ ∨ Ψ ),
звідки η∉F( ( )v
x BR Φ∨Ψ ).
Нехай –| (xR Φ∨Ψ)v ∈Н. Згідно НR∨
маємо –| ( ) ( )v v
x xR RΦ ∨ Ψ ∈Н. За припущен-
ням індукції для δ маємо
δ∉T( ( ) ( )v v
x xR R AΦ ∨ Ψ ), звідки отримуємо
δ∉T( (v )x AR Φ∨Ψ ). За припущенням індук-
ції для η маємо η∈F( ( ) ( )v v
x x BR RΦ ∨ Ψ ),
звідки η∈F( ( )v
x BR Φ∨Ψ ).
Нехай |–
,
, ( )y v
z xR Φ ∈Н та у∈ν(Φ). Згід-
но НΦN маємо |– ( )v
xR Φ ∈Н. За припущен-
ням індукції для δ маємо δ∈T( ( )v
x AR Φ ),
звідки δ∈T( ,
, ( )y v
z x AR Φ ). За припущенням ін-
дукції для η маємо η∉F( (v )x BR Φ ), звідки
η∉F( ,
, ( )y v
z x BR Φ ).
Нехай –|
,
, ( )y v
z xR Φ ∈Н та у∈ν(Φ). Згід-
но НΦN маємо –| ( )v
xR Φ ∈Н. За припущен-
ням індукції для δ маємо δ∉T( ( )v
x AR Φ ),
звідки δ∉T( ,
, ( )y v
z x AR Φ ). За припущенням ін-
дукції для η маємо η∈F( (v )x BR Φ ), звідки
η∈F( ,
, ( )y v
z x BR Φ ).
Нехай |–
,
, ( )z v
z xR¬ Φ ∈Н. Згідно Н¬RT
|– ( )xRv¬ Φ ∈Н. За припущенням індукції
для δ маємо δ∈T( ( )v
x AR¬ Φ ). Але
T( ( )v
x AR¬ Φ ) = F( ( )v
x AR Φ ) = F( , )z v
, (z x AR Φ ) =
= T( ,z v
, ( )z x AR¬ Φ ), звідки δ∈T( ,z v
, ( )z x AR¬ Φ ).
За припущенням індукції для η маємо
η∉F( ( )v
x BR¬ Φ ). Але F( ( )v
x BR¬ Φ ) =
= T( ( )v
x BR Φ ) = T( , )z v
, (z x BR Φ ) = F( ,z v
, ( )z x BR¬ Φ ),
звідки η∉F( ,z v
, ( )z x BR¬ Φ ).
Нехай –|
,z v
, ( )z xR¬ Φ ∈Н. Згідно Н¬RT
–| ( )xRv¬ Φ ∈Н. За припущенням індукції
для δ маємо δ∉T( ( )v
x AR¬ Φ ). Але
T( ( )v
x AR Φ ) = F( ( )v
x AR Φ ) = F(¬ , )z v
, (z x AR Φ ) =
= T( ,z v
, ( )z x AR¬ Φ ), звідки δ∉T( ,z v¬ Φ, ( )z x AR ).
За припущенням індукції для η маємо
η∈F( ( )v
x BR Φ ). Але F( ( )v
x BR¬ ¬ Φ ) =
= T( ( )v
x BR Φ ) = T( , )z v Φ, (z x BR ) = F( ,z v
, ( )z x BR¬ Φ ),
звідки η∈F( , ( )z vR ,z x BΦ ). ¬
Нехай |– ( ( ))v wR Rx y Φ ∈Н. Згідно ¬
47
Теоретичні та методологічні основи програмування
Н¬RR тоді |– ( )v w
x yR¬ o Φ ∈Н. За припущен-
ням індукції для δ δ∈T( ( )v w
x yR¬ Φo A ). Але
T( ( )v w
x yR¬ Φo A ) = T( ( ( ))v w
x yR R¬ Φ A ), звідки
δ∈T( ( ( ))v w
x yR R¬ Φ A ). За припущенням ін-
дукції для η маємо η∉F( ( )v w
x yR¬ Φo B ). Але
F( ( )v w
x yR¬ Φo B ) = F( ( ( ))v w
x yR R¬ Φ B ), звідки
η∉F( ( ( ))v w
x y BR R¬ Φ ).
Нехай –| ( ( )v w
x yR R¬ Φ )∈Н. Згідно
Н¬RR тоді –| ( )v w
x yR¬ o Φ ∈Н. За припущен-
ням індукції для δ δ∉T( ( )v w
x yR¬ Φo A ). Але
T( ( )v w
x yR¬ Φo A ) = T( ( ( ))v w
x yR R¬ Φ A ), звідки
δ∉T( ( ( ))v w
x yR R¬ Φ A ). За припущенням ін-
дукції для η маємо η∈F( ( )v w
x yR¬ Φo B ). Але
F( ( )v w
x yR¬ Φo B ) = F( ( ( ))v w
x yR R¬ Φ B ), звідки
η∈F( ( ( ))v w
x y BR R¬ Φ ).
Нехай |– (v
xR¬ ¬Φ)∈Н. Згідно Н¬R¬
маємо |– ( )v
xR Φ ∈Н. За припущенням інду-
кції для δ маємо δ∈T( ( )v
x AR Φ ). Але
T( ( )v
x AR Φ ) = T( ( )v
x AR¬ ¬Φ ), звідки маємо
δ∈T( ( )v
x AR¬ ¬Φ ). За припущенням індук-
ції для η маємо η∉F( ( )v
x BR Φ ). Але
F( ( )v
x BR Φ ) = F( ( )v
x BR¬ ¬Φ ), звідки маємо
η∉F( ( )v
x BR¬ ¬Φ ).
Нехай –| (v
xR¬ ¬Φ)∈Н. Згідно Н¬R¬
маємо –| ( )v
xR Φ ∈Н. За припущенням індук-
ції для δ маємо δ∉T( ( )v
x AR Φ ). Але
T( ( )v
x AR Φ ) = T( ( )v
x AR¬ ¬Φ ), звідки маємо
δ∉T( ( )v
x AR¬ ¬Φ ). За припущенням індук-
ції для η маємо η∈F( ( )v
x BR Φ ). Але
F( ( )v
x BR Φ ) = F( ( )v
x BR¬ ¬Φ ), звідки маємо
η∈F( ( )v
x BR¬ ¬Φ ).
Нехай |– ( )xR¬ Φ∨Ψv ∈Н. Згідно
Н¬R∨ маємо |– ( )xR¬ Φv ∈Н та |–
( )xR¬ Ψv ∈Н. За припущенням індукції для δ
маємо δ∈T( ( )v
x AR¬ Φ ) та δ∈T( ( )v
x AR¬ Ψ ),
звідки δ∈T( ( ) & ( )v v
x x AR R¬ Φ ¬ Ψ ) =
T( ( ( ) ( )) )v v
x xR R¬ Φ ∨¬ Ψ A =T( ( )v ).x AR¬ Φ∨Ψ
За припущенням індукції для η маємо
η∉F( ( )v
x BR¬ Φ ) та η∉F( ( )v
x BR¬ Ψ ), звідки
η∉F( ( )v
x BR¬ Φ )∪F( ( )v
x BR¬ Ψ ). Врахову-
ючи, що F( ( )v
x BR¬ Φ )∪F( ( )v
x BR¬ Ψ ) =
= F( ( ) & ( )v v
x xR R B¬ Φ ¬ Ψ ) = F( ( )v
x BR¬ Φ∨Ψ ),
звідси η∉F( ( )v
x BR¬ Φ∨Ψ ).
Нехай –| ( )v
xR¬ Φ∨Ψ ∈Н. Згідно
Н¬R∨ тоді –| ( )v
xR¬ Φ ∈Н або –| ( )v
xR¬ Ψ ∈Н.
За припущенням індукції для δ маємо
δ∉T( ( )v
x AR¬ Φ ) або δ∉T( ( )v
x AR¬ Ψ ), звідки
δ∉T( ( )v
x AR¬ Φ )∩T( ( )v
x AR¬ Ψ ). Але маємо
T( ( )v
x AR¬ Φ )∩T( ( )v
x AR¬ Ψ ) =
= T( ( ) & ( )v v
x xR R A¬ Φ ¬ Ψ ) = T( ( )v
x AR¬ Φ∨Ψ ),
тому δ∉T( (v )x AR¬ Φ∨Ψ ). За припущенням
індукції для η маємо η∈F( ( )v
x BR¬ Φ ) або
η∈F( ( )v
x BR¬ Ψ ), звідки η∈F( ( )v
x BR¬ Φ )∪
∪F( ( )v
x BR¬ Ψ ). Враховуючи, що
F( ( )v
x BR¬ Φ )∪F( ( )v
x BR¬ Ψ ) =
= F( ( ) & ( )v v
x xR R B¬ Φ ¬ Ψ ) = F( ( )v
x BR¬ Φ∨Ψ ),
звідси η∈F( ( )v
x BR¬ Φ∨Ψ ).
Нехай |–
,
, ( )y v
z xR¬ Φ ∈Н та у∈ν(Φ).
Згідно Н¬ΦN маємо |– ( )v
xR¬ Φ ∈Н. За при-
пущенням індукції для δ маємо
δ∈T( (v )x AR¬ Φ ). Проте T( (v )x AR¬ Φ ) =
= T( ,
, ( )y v
z x AR¬ Φ ), звідки δ∈T( ,
, ( )y v
z x AR¬ Φ ).
За припущенням індукції для η маємо
η∉F( ( )v
x BR¬ Φ ). Водночас F( ( )v
x BR¬ Φ ) =
= F( ,
, ( )y v
z x BR¬ Φ ), звідки η∉F( ,
, ( )y v
z x BR¬ Φ ).
Нехай –|
,
, ( )y v
z xR¬ Φ ∈Н та у∈ν(Φ).
Згідно Н¬ΦN маємо –| ( )v
xR¬ Φ ∈Н. За при-
пущенням індукції для δ маємо
δ∉T( ( )v
x AR¬ Φ ). Проте T( (v )x AR¬ Φ ) =
= T( ,
, ( )y v
z x AR¬ Φ ), звідки δ∉T( ,
, ( )y v
z x AR¬ Φ ).
За припущенням індукції для η маємо
η∈F( ( )v
x BR¬ Φ ). Водночас F( ( )v
x BR¬ Φ ) =
48
Теоретичні та методологічні основи програмування
= F( ,
, ( )y v
z x BR¬ Φ ), звідки η∈F( ,
, ( )y v
z x BR¬ Φ ).
Нехай |–∃хΦ∈Н. Згідно Н∃ тоді існує
у∈W таке, що |– ( )x
yR Φ ∈Н. За припущен-
ням індукції для δ маємо δ∈T( ( )x
y AR Φ ).
Звідси δ∇хaδ(у)∈T(ΦA). Однак δ(у)↓ згідно
з δ∈WА та у∈W, тому для а = δ(у) маємо
δ∇хaа∈T(ΦA), звідки δ∈T(∃хΦA). За при-
пущенням індукції для η маємо
η∉F( ). Звідси η∇хaη(у)∉F(Φ( )x
yR Φ B B).
Однак η(у)↓ згідно з η∈ А та у∈W, тому
для а = η(у) маємо η∇хaа∉F(Φ
B
W
BB), звідки
η∉F(∃хΦB). B
A
B
Нехай –|∃хΦ∈Н. Згідно Н∃ тоді для
всіх у∈W маємо –| ( )x
yR Φ ∈Н. За припущен-
ням індукції для δ маємо δ∉T( ) для
всіх у∈W. Звідси δ∇хaδ(у)∉T(Φ
( )x
yR Φ
A) для всіх
у∈W. Згідно з δ∈АW маємо δ(у)↓ для всіх
у∈W. Позаяк δ є бієкцією W→А, то кожне
b∈А має вигляд b = δ(у) для деякого у∈W.
Отже, δ∇хab∉T(ΦA) для всіх b∈А, звідки
δ∉T(∃хΦA). За припущенням індукції для η
маємо η∈F( ) для всіх у∈W. Звідси
η∇хaη(у)∈F(Φ
( )x
yR Φ
B) для всіх у∈W. Згідно з
η∈А маємо η(у)↓ для всіх у∈W. Позаяк η
є бієкцією W→А, то кожне b∈А має вигляд
b = η(у) для деякого у∈W. Отже,
η∇хab∈F(Φ
B
W
BB) для всіх b∈А, звідки
η∈F(∃хΦB). B
A
B
Нехай |–¬∃хΦ∈Н. Згідно Н¬∃ тоді
для всіх у∈W маємо |– ( )x
yR¬ Φ ∈Н. За при-
пущенням індукції для δ маємо
δ∈T( ( ) для всіх у∈W. Звідси
δ∇хaδ(у)∈F(Φ
)x
yR¬ Φ
A) для всіх у∈W. Згідно з
δ∈АW маємо δ(у)↓ для всіх у∈W. Позаяк δ є
бієкцією W→А, то кожне b∈А має вигляд
b = δ(у) для деякого у∈W. Отже,
δ∇хab∈F(ΦA) для всіх b∈А, звідки
δ∈F(∃хΦA), тому δ∈T(¬∃хΦA). За припу-
щенням індукції для η маємо
η∉F( ( ) для всіх у∈W. Звідси
η∇хaη(у)∉T(Φ
)x
yR¬ Φ
B) для всіх у∈W. Згідно з
η∈А маємо η(у)↓ для всіх у∈W. Позаяк η
є бієкцією W→А, то кожне b∈А має вигляд
b = η(у) для деякого у∈W. Отже,
η∇хab∉T(Φ
B
W
BB) для всіх b∈А, звідки
η∉T(∃хΦB), тому η∉F(¬∃хΦB BB
A
).
Нехай –|¬∃хΦ∈Н. Згідно Н¬∃ тоді
існує у∈W таке, що –| ( )x
yR¬ Φ ∈Н. За при-
пущенням індукції для δ маємо
δ∉T( ( )x
yR¬ Φ ). Звідси δ∇хaδ(у)∉F(ΦA).
Однак δ(у)↓ згідно з δ∈WА та у∈W, тому
для а = δ(у) маємо δ∇хaа∉F(ΦA), звідки
δ∉F(∃хΦA), тому δ∉T(¬∃хΦA). За припу-
щенням індукції для η тоді маємо
η∈F( ( )x
yR B¬ Φ ). Звідси η∇хaη(у)∈T(ΦB).
Однак η(у)↓ згідно з η∈ А та у∈W, тому
для а = η(у) маємо η∇хaа∈T(Φ
B
W
BB), звідки
η∈T(∃хΦB), тому η∈F(¬∃хΦB BB).
Аналогічним чином доводимо для
пп. НR∃, Н¬R∃, НR∃S, Н¬R∃S визначення
модельної множини.
Теорема 4. Нехай Н – C-модельна
множина. Тоді існують модель мови АС
A = (A, I) та δ∈VA такі:
|–Φ∈Н ⇒ δ∈T(ΦA) та –|Φ∈Н ⇒ δ∈F(ΦA).
Пару (A, δ) із вищенаведеними вла-
стивостями назвемо Cl-контрмоделлю.
Доведення теореми 4 подібне до до-
ведення теореми 3, воно наведене в [3].
Теорема повноти для різних варіан-
тів секвенційних числень та логічних нас-
лідків формулюється однаково.
Теорема 5. Нехай Γ |=Cl Δ. Тоді сек-
венція |–Γ–|Δ вивідна в численні QCl.
Припустимо супротивне: Γ |=Cl Δ та
|–Γ–|Δ невивідна. Якщо Σ = |–Γ–|Δ невивідна,
то секвенційне дерево для |–Γ–|Δ незамкнене,
тому в ньому існує незамкнений шлях. Згі-
дно з теоремою 2, множина Н усіх специ-
фікованих формул секвенцій цього шляху
– C-модельна. При цьому |–Γ–|Δ ⊆ Н.
Згідно з теоремою 4 існує Cl-контр-
модель (A, δ) така: |–Φ∈Н ⇒ δ∈T(ΦA) та
–|Φ∈Н ⇒ δ∈F(ΦA). Згідно з |–Γ–|Δ ⊆ Н для
всіх Φ∈Γ маємо δ∈T(ΦA), для всіх Ψ∈Δ
δ∈F(ΨA). Звідси δ∈T(ΓA)∩F(ΔA), звідки
T(ΓA)∩F(ΔA) ≠ ∅. Це заперечує Γ |=Cl Δ.
Розглянемо теореми повноти чис-
лень QL, QEqL, QR, QEqR, QLR, QEqLR
для відношень |=T , |=F та |=TF. Зробимо пе-
вні зауваження щодо вибору числень та
контрмоделей.
49
Теоретичні та методологічні основи програмування
У загальному випадку логіки одно-
значних предикатів:
– формалізуємо |=T численням QL
та беремо T-контрмодель;
– формалізуємо |=F численням QR
та беремо F-контрмодель.
Для логіки однозначних еквітонних
предикатів:
– формалізуємо |=T численням
QEqL та беремо T-контрмодель;
– формалізуємо |=F численням
QEqR та беремо F-контрмодель.
Зауважимо, що для T-контрмоделі δ
невиконання умови НСL, тобто наявність
формули Φ такої, що |–Φ∈Н та |–¬Φ∈Н, дає
δ∈T(ΦA) та δ∈T(¬ΦA) = F(ΦA), звідки має-
мо неоднозначність ΦA . Для F-контрмо-
делі η невиконання умови НСR, тобто на-
явність Φ такої, що –|Φ∈Н та –|¬Φ∈Н, дає
η∈F(ΦB) та η∈F(¬ΦB BB) = T(ΦB), звідки ма-
ємо неоднозначність Φ
B
B .
Теорема 6. Нехай Γ |=T Δ. Тоді сек-
венція |–Γ–|Δ вивідна в численні QL.
Припустимо супротивне: Γ |=T Δ та
|–Γ–|Δ невивідна. Якщо Σ = |–Γ–|Δ невивідна,
то в секвенційному дереві для Σ існує не-
замкнений шлях. Згідно з теоремою 2,
множина Н усіх специфікованих формул
секвенцій цього шляху – L-модельна. Тоді
|–Γ–|Δ ⊆ Н.
Згідно з теоремою 3 існує T-контр-
модель (A, δ) така: |–Φ∈Н ⇒ δ∈T(ΦA) та
–|Φ∈Н ⇒ δ∉T(ΦA). Згідно з |–Γ–|Δ ⊆ Н для
всіх Φ∈Γ маємо δ∈T(ΦA), для всіх Ψ∈Δ
маємо δ∉T(ΨA). Звідси δ∈T(ΓA) та δ∉T(ΔA),
звідки невірно T(ΓA) ⊆ T(ΔA). Це заперечує
Γ |=T Δ.
Теорема 7. Нехай Γ |=T Δ. Тоді сек-
венція |–Γ–|Δ вивідна в численні QEqL.
Припустимо супротивне: Γ |=T Δ та
|–Γ–|Δ невивідна. Якщо Σ = |–Γ–|Δ невивідна,
то в дереві для Σ існує незамкнений шлях.
Згідно з теоремою 2, множина Н усіх спе-
цифікованих формул секвенцій цього шля-
ху – EqL-модельна. Тоді |–Γ–|Δ ⊆ Н.
Далі доводимо так, як в теоремі 6.
Теорема 8. Нехай Γ |=F Δ. Тоді сек-
венція |–Γ–|Δ вивідна в численні QR.
Припустимо супротивне: Γ |=T Δ та
|–Γ–|Δ невивідна. Якщо Σ = |–Γ–|Δ невивідна,
то в секвенційному дереві для Σ існує незам-
кнений шлях. Згідно з теоремою 2, множи-
на Н усіх специфікованих формул секвен-
цій цього шляху – R-модельна. Тоді
|–Γ–|Δ ⊆ Н.
Згідно з теоремою 3 існує F-контр-
модель (B, η) така: |–Φ∈Н ⇒ η∉F(ΦB) та B
–|Φ∈Н ⇒ η∈F(ΦBB). Згідно з |–Γ–|Δ ⊆ Н для
всіх Φ∈Γ маємо η∉F(ΦB), для всіх Ψ∈Δ
маємо η∈F(Ψ
B
BB). Звідси η∉F(ΓB) та
η∈F(Δ
B
BB), звідки невірно F(ΔB)B ⊆ F(ΓBB). Це
заперечує Γ |=F Δ.
Теорема 9. Нехай Γ |=F Δ. Тоді сек-
венція |–Γ–|Δ вивідна в численні QEqR.
Припустимо супротивне: Γ |=F Δ та
|–Γ–|Δ невивідна. Якщо Σ = |–Γ–|Δ невивідна,
то в секвенційному дереві для Σ існує не-
замкнений шлях. Згідно з теоремою 2,
множина Н усіх специфікованих формул
секвенцій цього шляху – EqR-модельна.
Тоді |–Γ–|Δ ⊆ Н.
Далі доводимо так, як в теоремі 8.
Для вибору T-контрмоделі чи F-контр-
моделі в QLR-численні чи QEqLR-численні
беремо до уваги наступні обставини.
Якщо при виконанні НСLR не вико-
нується НСL (тоді маємо НСR), то для T-
контрмоделі отримуємо неоднозначний
предикат, тому беремо F-контрмодель.
Якщо при виконанні НСLR не вико-
нується НСR (тоді маємо НСL), то для F-
контрмоделі отримуємо неоднозначний
предикат, тому беремо T-контрмодель.
Якщо виконуються НСL та НСR, то
можна брати як T-контрмодель, так і F-
контрмодель.
Теорема 10. Нехай Γ |=TF Δ. Тоді сек-
венція |–Γ–|Δ вивідна в численні QLR.
Припустимо супротивне: Γ |=TF Δ та
|–Γ–|Δ невивідна. Якщо Σ = |–Γ–|Δ невивідна,
то в секвенційному дереві для Σ існує не-
замкнений шлях. Згідно з теоремою 2,
множина Н усіх специфікованих формул
секвенцій цього шляху – LR-модельна. То-
ді |–Γ–|Δ ⊆ Н.
Згідно з теоремою 3 існують T-контр-
модель (A, δ) та F-контрмодель (B, η) такі:
|–Φ∈Н ⇒ δ∈T(ΦA) та –|Φ∈Н ⇒ δ∉T(ΦA);
|–Φ∈Н ⇒ η∉F(ΦB) та B –|Φ∈Н ⇒ η∈F(ΦBB).
50
Теоретичні та методологічні основи програмування
Для T-контрмоделі згідно з |–Γ–|Δ ⊆ Н
для всіх Φ∈Γ маємо δ∈T(ΦA), для всіх Ψ∈Δ
маємо δ∉T(ΨA). Звідси δ∈T(ΓA) та δ∉T(ΔA),
звідки невірно T(ΓA) ⊆ T(ΔA).
Це заперечує Γ A|=T Δ, тому й запере-
чує Γ |=TF Δ.
Для F-контрмоделі згідно з |–Γ–|Δ ⊆ Н
для всіх Φ∈Γ маємо η∉F(ΦB), для всіх
Ψ∈Δ маємо η∈F(Ψ
B
BB). Звідси η∉F(ΓB) та
η∈F(Δ
B
BB), звідки невірно F(ΔB)B ⊆ F(ΓBB). Це
заперечує Γ B|=F Δ, тому й заперечує Γ |=TF Δ.
Теорема 11. Нехай Γ |=TF Δ. Тоді сек-
венція |–Γ–|Δ вивідна в численні QEqLR.
Припустимо супротивне: Γ |=TF Δ та
|–Γ–|Δ невивідна. Якщо Σ = |–Γ–|Δ невивідна,
то в дереві для Σ існує незамкнений шлях.
Згідно з теоремою 2, множина Н усіх спе-
цифікованих формул секвенцій цього шля-
ху – EqLR-модельна. Тоді |–Γ–|Δ ⊆ Н.
Далі доводимо так, як в теоремі 10.
Висновки
На основі властивостей відношень ло-
гічного наслідку для першопорядкових ком-
позиційно-номінативних логік однозначних
квазіарних предикатів кванторного рівня
побудовано числення секвенційного типу.
Такі числення збудовано як для логік екві-
тонних, так і для загального випадку логік
однозначних квазіарних предикатів. Для
пропонованих числень наведено базові
секвенційні форми та умови замкненості
секвенцій, описано процедуру побудови
секвенційного дерева, визначено поняття
модельної множини. Для побудованих чис-
лень доведено теореми коректності та пов-
ноти.
В наступній роботі планується побу-
дова числень секвенційного типу для пер-
шопорядкових композиційно-номінативних
логік тотальних неоднозначних та частко-
вих неоднозначних квазіарних предикатів.
1. Никитченко Н.С. Композиционно-номина-
тивный подход к уточнению понятия
программы // Проблеми програмування. –
1999. – № 1. – С. 16–31.
2. Шкільняк С.С. Відношення логічного наслі-
дку в композиційно-номінативних логіках //
Проблеми програмування. – 2010. – № 1. –
C. 15–38.
3. Шкильняк С.С. Логики квазиарных предика
тов первого порядка // Кибернетика и сис-
темный анализ. – 2010. – № 6 – С. 32–49.
4. Шкільняк С.С. Спеціальні відношення логіч-
ного наслідку в логіках квазіарних преди-
катів // Проблеми програмування. – 2011. –
№ 4. – C. 36–48.
5. Смирнова Е.Д. Логика и философия – М.,
1996. – 304 с.
6. Нікітченко М.С., Шкільняк С.С. Математич-
на логіка та теорія алгоритмів. – К., 2008. –
528 с.
7. Клини С. Математическая логика. – М.,
1973. – 480 с.
Отримано 14.07.2011
Про автора:
Шкільняк Степан Степанович,
доктор фізико-математичних наук,
доцент кафедри теорії та технології
програмування.
Місце роботи автора:
Київський національний університет
імені Тараса Шевченка,
01601, Київ,
вул. Володимирська, 60.
Тел.: (044) 259-0519, (044) 522-0640 (д)
e-mail: sssh@unicyb.kiev.ua
UDC 004.42:510.69
51
|