Секвенційні числення композиційно-номінотивних логік квазіарних предикатів
Збережено в:
| Дата: | 2015 |
|---|---|
| Автор: | |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
PROBLEMS IN PROGRAMMING
2015
|
| Теми: | |
| Онлайн доступ: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/50 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Репозитарії
Problems in programming| id |
pp_isofts_kiev_ua-article-50 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/e1/db81803fa6f6328235f03f53469e29e1.pdf |
| spelling |
pp_isofts_kiev_ua-article-502018-10-02T21:08:19Z Секвенційні числення композиційно-номінотивних логік квазіарних предикатів Shkilniak, S.S. композиційно-номінативні логіки Побудовано секвенційні числення першопорядкових композиційно-номінативних логік часткових однозначних, тотальних неоднозначних та часткових неоднозначних квазіарних предикатів кванторного рівня. Такі числення запропоновано для загального випадку логік квазіарних предикатів, для логік однозначних еквітонних та логік тотальних антитонних предикатів. Для побудованих числень доведено теореми коректності та повноти.We construct sequent calculi for first-order composition-nominative logics of partial single-valued, total multiple-valued and partial multiple-valued quasiary predicates of quantifier level. The defined calculi are proposed for a general case of logics of quasiary predicates, for logics of single-valued equitone predicates and for logics of total multiple-valued antytone predicates. For the introduced calculi soundness and completeness theorems are proved. PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2015-09-10 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/50 PROBLEMS IN PROGRAMMING; No 2-3 (2012) ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2-3 (2012) ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2-3 (2012) 1727-4907 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/50/51 Copyright (c) 2015 ПРОБЛЕМИ ПРОГРАМУВАННЯ |
| institution |
Problems in programming |
| baseUrl_str |
https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| datestamp_date |
2018-10-02T21:08:19Z |
| collection |
OJS |
| language |
Ukrainian |
| topic |
|
| spellingShingle |
Shkilniak, S.S. Секвенційні числення композиційно-номінотивних логік квазіарних предикатів |
| topic_facet |
композиційно-номінативні логіки |
| format |
Article |
| author |
Shkilniak, S.S. |
| author_facet |
Shkilniak, S.S. |
| author_sort |
Shkilniak, S.S. |
| title |
Секвенційні числення композиційно-номінотивних логік квазіарних предикатів |
| title_short |
Секвенційні числення композиційно-номінотивних логік квазіарних предикатів |
| title_full |
Секвенційні числення композиційно-номінотивних логік квазіарних предикатів |
| title_fullStr |
Секвенційні числення композиційно-номінотивних логік квазіарних предикатів |
| title_full_unstemmed |
Секвенційні числення композиційно-номінотивних логік квазіарних предикатів |
| title_sort |
секвенційні числення композиційно-номінотивних логік квазіарних предикатів |
| description |
|
| publisher |
PROBLEMS IN PROGRAMMING |
| publishDate |
2015 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/50 |
| work_keys_str_mv |
AT shkilniakss sekvencíjníčislennâkompozicíjnonomínotivnihlogíkkvazíarnihpredikatív |
| first_indexed |
2025-07-17T10:06:58Z |
| last_indexed |
2025-07-17T10:06:58Z |
| _version_ |
1850412851659800576 |
| fulltext |
Теоретичні та методологічні основи програмування
УДК 004.42:510.69
СЕКВЕНЦІЙНІ ЧИСЛЕННЯ КОМПОЗИЦІЙНО-НОМІНАТИВНИХ
ЛОГІК КВАЗІАРНИХ ПРЕДИКАТІВ
С.С. Шкільняк
Київський національний університет імені Тараса Шевченка
01601, Київ, вул. Володимирська, 60
тел.: (044) 259 0511
e-mail: sssh@unicyb.kiev.ua
Побудовано секвенційні числення першопорядкових композиційно-номінативних логік часткових однозначних, тотальних неодно-
значних та часткових неоднозначних квазіарних предикатів кванторного рівня. Такі числення запропоновано для загального випад-
ку логік квазіарних предикатів, для логік однозначних еквітонних та логік тотальних антитонних предикатів. Для побудованих чис-
лень доведено теореми коректності та повноти.
We construct sequent calculi for first-order composition-nominative logics of partial single-valued, total multiple-valued and partial multi-
ple-valued quasi-ary predicates of quantifier level. The defined calculi are proposed for a general case of logics of quasi-ary predicates, for
logics of single-valued equitone predicates and for logics of total multiple-valued antytone predicates. For the introduced calculi soundness
and completeness theorems are proved.
Вступ
Програмно-орієнтовані логічні формалізми, будовані на основі cпільного для логіки й програмування
композиційно-номінативного підходу [1], називаються композиційно-номінативними логіками (КНЛ). Такі ло-
гічні формалізми вивчались, зокрема, в [2]. Різноманітність семантик та відношень логічного наслідку в КНЛ
квазіарних предикатів [3] індукує побудову для них низки різновидностей секвенційних числень. Для традицій-
ного відношення |=Cl КНЛ однозначних квазіарних предикатів такі числення побудовано в [2, 4]. Першопоряд-
кові секвенційні числення КНЛ однозначних квазіарних предикатів для відношень |=T, |=F, |=TF збудовано в [5].
Пропонована стаття є безпосереднім продовженням роботи [5]. Метою статті є побудова спектру секвен-
ційних числень для відношень |=Cl, |=Cm, |=T, |=F, |=TF (їх визначення див. [3, 6]) в логіках часткових однозначних,
тотальних неоднозначних та часткових неоднозначних квазіарних предикатів. Основну увагу приділено побу-
дові секвенційних числень першопорядкових КНЛ кванторного рівня (КНЛК). Такі числення пропонуються як
для загального випадку квазіарних предикатів, так і для логік еквітонних однозначних, та, дуально, для логік
антитонних тотальних предикатів. Характерною особливістю цих числень є використання спеціальних секвен-
ційних форм елімінації кванторів під реномінацією, що робить зайвим використання секвенційних форм для
пронесення кванторів через реномінації. Для побудованих числень доведено теореми коректності й повноти.
Для логік тотальних однозначних предикатів (класична семантика) відношення логічного наслідку |=Cl,
|=Cm, |=T, |=F, |=TF збігаються. Маємо традиційні секвенційні числення класичної логіки предикатів (див. [7, 8]).
Для логік часткових однозначних предикатів (неокласична семантика) можна розглядати відношення
|=Cl, |=T, |=F, |=TF (відношення |=Cm порожнє). Першопорядкові секвенційні числення відомі [2] для відношення
|=Cl неокласичних логік еквітонних квазіарних предикатів. Побудовано також [4] секвенційне числення для від-
ношення |=Cl в загальному випадку логік однозначних квазіарних предикатів кванторного рівня.
Для логік тотальних неоднозначних предикатів (пересичена семантика) можна розглядати |=Cm, |=T, |=F,
|=TF (відношення |=Cl порожнє). Відношення |=Cm тут дає секвенційні числення, ідентичні відповідним числен-
ням для відношення |=Cl логіки однозначних часткових предикатів. Для випадку пропозиційної логіки отримує-
мо числення, яке збігається з класичним пропозиційним секвенційним численням. Останнє означає, що класич-
не пропозиційне секвенційне числення допускає набагато ширші порівнянно з класичними класи семантичних
моделей, до яких належать, зокрема, класи часткових однозначних і тотальних неоднозначних предикатів.
Для інших відношень розглядались [8] пропозиційні секвенційні числення. Відношення |=T дає числення
дуальної логіки Хао Вана, |=F – числення логіки Хао Вана, |=TF – числення фрагмента логіки Лукасєвича.
Для логік часткових неоднозначних предикатів (загальна семантика) відношення |=T, |=F, |=TF збігаються,
відношення |=Cl та |=Cm порожні. Тому для цих логік розглядаємо секвенційні числення лише для відношення
|=TF. На пропозиційному рівні для |=TF маємо відоме [8] пропозиційне секвенційне числення логіки де Моргана.
Поняття, які в статті не визначаються, тлумачимо в сенсі робіт [2–4, 6].
1. Основні властивості відношень логічного наслідку для множин формул
Наведемо властивості відношень логічного наслідку для множин формул пропозиційного рівня. Тут |= оз-
начає: для неокласичної семантики – |=Cl, |=T, |=F, |=TF; для пересиченої – |=Cm, |=T, |=F, |=TF; для загальної – |=TF .
U) Нехай Γ ⊆ Λ та Δ ⊆ Σ, тоді Γ |= Δ ⇒ Λ |= Σ.
С) Φ, Γ |= Δ, Φ.
¬¬|– ) ¬¬Φ, Γ |= Δ ⇔ Φ, Γ |= Δ.
33
© С.С. Шкільняк, 2012
ISSN 1727-4907. Проблеми програмування. 2012. № 2-3. Спеціальний випуск
Теоретичні та методологічні основи програмування
¬¬–| ) Γ |= Δ, ¬¬Φ ⇔ Γ |= Δ, Φ.
∨|– ) Φ∨Ψ, Γ |= Δ ⇔ Φ, Γ |= Δ та Ψ, Γ |= Δ.
∨–| ) Γ |= Δ, Φ∨Ψ ⇔ Γ |= Δ, Φ, Ψ.
¬∨|– ) ¬(Φ∨Ψ), Γ |= Δ ⇔ ¬Φ, ¬Ψ, Γ |= Δ.
¬∨–| ) Γ |= Δ, ¬(Φ∨Ψ) ⇔ Γ |= Δ, ¬Φ та Γ |= Δ, ¬Ψ.
Для відношень |=Cl (неокласична семантика) та |=Cm (пересичена семантика) також справджуються:
¬|– ) ¬Φ, Γ |= Δ ⇔ Γ |= Δ, Φ.
¬–| ) Γ |= Δ, ¬Φ ⇔ Φ, Γ |= Δ.
У відповідних семантиках маємо властивості, які додатково гарантують наявність логічного наслідку:
СL) Φ, ¬Φ, Γ |= Δ (для неокласичної семантики |= – це |=T, |=Cl ; для пересиченої – |=F, |=Cm );
СR) Γ |= Δ, Φ, ¬Φ (для неокласичної семантики |= – це |=F, |=Cl ; для пересиченої – |=T, |=Cm ).
СLR) Φ, ¬Φ, Γ |=TF Δ, Ψ, ¬Ψ (неокласична семантика чи пересичена семантика).
Зрозуміло, що для |=TF маємо: СLR ⇔ СL & СR. Для |=Cl та |=Cm властивості СL, СR, СLR зводяться до С.
До основних властивостей реномінативного рівня віднесемо наведені в [5] RT|–, RT–|, ΦN|–, ΦN–|, RR|–,
RR–|, R¬|–, R¬–|, R∨|–, R∨–|, ¬RT|–, ¬RT–|, ¬ΦN|–, ¬ΦN–|, ¬RR|–, ¬RR–|, ¬R¬|–, ¬R¬–|, ¬R∨|–, ¬R∨–|. Ці властивості
справджуються для |=TF, у відповідних семантиках вони вірні також для |=T, |=F, |=Cl, |=Cm.
До основних властивостей кванторного рівня належать властивості елімінації кванторів та властивості,
пов’язані зі згорткою за квантифікованим верхнім іменем реномінації. Останні мають вигляд (тут { }x u∉ ):
R∃R|–) ,
, ( Φ),u x
v yR x∃ Γ |=∗ Δ ⇔ ( Φ),u
vR x∃ Γ |=∗ Δ Зокрема, Γ |=( Φ),x
yR x∃ ∗ Δ ⇔ ∃хΦ, Γ |=∗ Δ.
R∃R–|) Γ |=∗ Δ, ,
, ( Φ)u x
v yR x∃ ⇔ Γ |=∗ Δ, ( Φ)u
vR x∃ . Зокрема, Γ |=∗ Δ, ⇔ Γ |=( Φ)x
yR x∃ ∗ Δ, ∃хΦ.
¬R∃R|–) ,
, ( Φ),u x
v yR x¬ ∃ Γ |=∗ Δ ⇔ ( Φ),u
vR x¬ ∃ Γ |=∗ Δ. Зокрема, Γ |=( Φ),x
yR x¬ ∃ ∗ Δ ⇔ ¬∃хΦ, Γ |=∗ Δ.
¬R∃R–|) Γ |=∗ Δ, ,
, ( Φ)u x
v yR x¬ ∃ ⇔ Γ |=∗ Δ, ( Φ)u
vR x¬ ∃ . Зокрема, Γ |=∗ Δ, ⇔ Γ |=( Φ)x
yR x¬ ∃ ∗ Δ, ¬∃хΦ.
Тут і надалі, якщо інше явно не вказано, ∗ – це одне з Cl, Cm, T, F, TF (для відповідних семантик).
Розглянемо властивості Х–Y-означених відношень логічного наслідку. До наведених в [4, 6] властивостей
тут додамо властивості елімінації кванторів під реномінацією.
Нехай z тотально строго неістотне та z∉пт(Γ, Δ, ∃хΦ), тоді при z∈X маємо:
∃Х–Y |– ) ∃хΦ, Γ Х –Y |=∗ Δ ⇔ ∃хΦ, Γ {z}∪Х –Y |=∗ Δ ⇔ Γ(Φ),x
zR {z}∪Х–Y |=∗ Δ;
¬∃Х–Y –| ) Γ Х–Y |=∗ Δ, ¬∃хΦ ⇔ Γ {z}∪Х–Y |=∗ Δ, ¬∃хΦ ⇔ Γ {z}∪Х–Y |=∗ Δ, . (Φ)x
zR¬
Нехай z тотально строго неістотне, z∉пт(Γ, Δ, ( Φ)u
vR x∃ ) та { }x u∉ . Тоді при z∈X маємо:
∃R Х–Y |– ) ( Φ),u
vR x∃ Γ Х –Y |=∗ Δ ⇔ ( Φ),u
vR x∃ Γ {z}∪Х –Y |=∗ Δ ⇔ ,
, (Φ),u x
v zR Γ {z}∪Х–Y |=∗ Δ.
¬∃R Х–Y –| ) Γ Х–Y |=∗ Δ, ( Φ)u
vR x¬ ∃ ⇔ Γ {z}∪Х–Y |=∗ Δ, ( Φ)u
vR x¬ ∃ ⇔ Γ {z}∪Х–Y |=∗ Δ, ,
, (Φ)u x
v zR¬ .
Наведемо властивості елімінації кванторів з розгалуженням.
Нехай Z, W, U ⊆ V – диз’юнктні множини. Тоді маємо (тут { }x u∉ ):
Br∃) Γ A, W–U |=∗ Δ, ∃хΦ ⇔ для кожної Y ⊆ Z Γ A, W∪Y–U∪(Z\Y) |=∗ Δ, ∃хΦ, 1
(Φ),..., (Φ),...,
n
x x
y yR R де всі yi∈W∪Y.
Br∃R) Γ A, W–U |=∗ Δ, ( Φ)u
vR x∃ ⇔ для кожної Y ⊆ Z
Γ A, W∪Y–U∪(Z\Y) |=∗ Δ, ( Φ),u
vR x∃
1
, ,
, ,(Φ),..., (Φ),...,
n
u x u x
v y v 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.
Br¬∃R) ( Φ),u
vR x¬ ∃ Γ A, W–U |=∗ Δ ⇔ для кожної Y ⊆ Z
( Φ),u
vR x¬ ∃
1
, ,
, ,(Φ),..., (Φ),...,
n
u x u x
v y v yR R¬ ¬ Γ A, W∪Y–U∪(Z\Y) |=∗ Δ, де всі yi∈W∪Y.
Нехай Z ⊆ V. Тоді маємо (тут { }x u∉ ):
Br∃f) Γ A |=∗ Δ, ∃хΦ ⇔ для кожної непорожньої Y ⊆ Z Γ A, Y–(Z\Y) |=∗ Δ, ∃хΦ, де всі y
1
(Φ),..., (Φ),...,
n
x x
y yR R i∈Y,
та Γ A, {t}–Z |=∗ Δ, ∃хΦ, де t тотально строго неістотне, t∉пт(Γ,(Φ),x
tR Δ, ∃хΦ).
Br∃Rf) Γ A |=∗ Δ, ( Φ)u
vR x∃ ⇔ для кожної непорожньої Y ⊆ Z `
Γ A, Y–(Z\Y) |=∗ Δ, ( Φ),u
vR x∃
1
, ,
, ,(Φ),..., (Φ),...,
n
u x u x
v y v yR R де всі yi∈Y,
та Γ A, {t}–Z |=∗ Δ, ( Φ),u
vR x∃ ,
, (Φ),u x
v tR де t тотально строго неістотне, t∉пт(Γ, Δ, ( Φ)u
vR x∃ ).
Br¬∃f) ¬∃хΦ, Γ A |=∗ Δ ⇔ для кожної непорожньої Y ⊆ Z ¬∃хΦ, Γ
1
(Φ),..., (Φ),...,
n
x x
y yR R¬ ¬ A, Y–(Z\Y) |=∗ Δ, де всі yi∈Y,
та ¬∃хΦ, Γ(Φ),x
tR¬ A, {t}–Z |=∗ Δ, де t тотально строго неістотне, t∉пт(Γ, Δ, ∃хΦ).
34
Теоретичні та методологічні основи програмування
Br¬∃Rf) ( Φ),u
vR x¬ ∃ Γ A |=∗Δ ⇔ для кожної непорожньої Y ⊆ Z
( Φ),u
vR x¬ ∃
1
, ,
, ,(Φ),..., (Φ),...,
n
u x u x
v y v yR R¬ ¬ Γ A, Y–(Z\Y) |=∗ Δ, де всі yi∈Y,
та ( Φ),u
vR x¬ ∃ ,
, (Φ),u x
v tR¬ Γ A, {t}–Z |= ∗Δ, де t тотально строго неістотне, t∉пт(Γ, Δ, ( Φ)u
vR x∃ ).
Властивості елімінації кванторів з розгалуженням базуються на основі наступних. При умові z∈X маємо:
∃Х–Y –| ) Γ A, Х–Y |=∗ Δ, ∃хΦ ⇔ Γ A, Х–Y |=∗ Δ, ∃хΦ, ; (Φ)x
zR
∃R Х–Y –| ) Γ A, Х–Y |=∗ Δ, ( Φ)u
vR x∃ ⇔ Γ A, Х–Y |=∗ Δ, ( Φ),u
vR x∃ ,
, (Φ)u x
v yR ;
¬∃Х–Y |– ) Γ, ¬∃хΦ Х–Y |=∗ Δ ⇔ Γ, ¬∃хΦ, (Φ)x
zR¬ Х–Y |=∗ Δ;
¬∃R Х–Y |– ) Γ, ( Φ)u
vR x¬ ∃ Х–Y |=∗ Δ ⇔ Γ, ( Φ),u
vR x¬ ∃ ,
, (Φ)u x
v yR¬ Х–Y |=∗ Δ.
Для |=Cl в неокласичній семантиці логіки еквітонних предикатів та |=Cт в пересиченій семантиці логіки
антитонних предикатів маємо (тут { }x u∉ , C – це одне з Cl, Cт):
∃ |– ) ∃хΦ, Γ |=C Δ ⇔ Γ(Φ),x
zR |=C Δ, де z тотально строго неістотне, z∉пт(Γ, Δ, ∃хΦ).
∃R|– ) ( Φ),u
vR x∃ Γ |=C Δ ⇔ ,
, (Φ),u x
v yR Γ |=C Δ, де z тотально строго неістотне, z∉пт(Γ, Δ, ( Φ)u
vR x∃ ).
∃–| ) Γ |=C Δ, ∃хΦ ⇔ Γ |=C Δ, ∃хΦ, . (Φ)x
zR
∃R–| ) Γ |=C Δ, ( Φ)u
vR x∃ ⇔ Γ |=C Δ, ( Φ),u
vR x∃ ,
, (Φ)u x
v yR .
Наведемо спеціальні властивості Х–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.
Дуально, для логіки антитонних предикатів у пересиченій семантиці:
CAnF) ,
, (Φ),x u
y vR Γ A, Х–Y |=F
,
, (Φ),x u
z vR Δ при умові z∈X та y∈Y;
CAn¬F) ,
, (Φ),x u
y vR¬ Γ A, Х–Y |=F
,
, (Φ),x u
z vR¬ Δ при умові z∈X та y∈Y;
CAnT) ,
, (Φ),x u
z vR Γ A, Х–Y |=T
,
, (Φ),x u
y vR Δ при умові z∈X та y∈Y;
CAn¬T) ,
, (Φ),x u
z vR¬ Γ A, Х–Y |=T
,
, (Φ),x u
y vR¬ Δ при умові z∈X та y∈Y.
Нехай Φv
xR та Φz
yR мають однакові U-неозначувані [4, 6] форми. Тоді маємо:
UnD) Φ,v
xR Γ A, –U |=∗ Φ,z
yR Δ.
Зазначені умови наявності логічного наслідку індукують відповідні умови замкненості секвенції.
2. Різновидності секвенційних числень КНЛ квазіарних предикатів
Залежно від відношення логічного наслідку та семантики для КНЛ квазіарних предикатів можна отрима-
ти низку різновидностей секвенційних числень. Для числень логік однозначних предикатів вводимо такі ж на-
зви, як для відповідних числень роботи [5], хоча тут ми використовуємо секвенційні форми елімінації кванторів
під реномінацією, щ робить зайвим використання форм для пронесення кванторів через реномінації.
Числення QCl формалізує:
– відношення |=Cl (неокласична семантика) для КНЛК однозначних предикатів;
– відношення |=Cm (пересичена семантика) для КНЛК тотальних предикатів.
Числення QEqCl формалізує:
– відношення |=Cl (неокласична семантика) для КНЛК однозначних еквітонних предикатів;
– відношення |=Cm (пересичена семантика) для КНЛК тотальних антитонних предикатів.
Числення QCl – це різновидність числення QG, побудованого в [4].
Числення QEqCl – це різновидність відомого [2] неокласичного секвенційного числення.
Числення QL (назва пов’язана із умовою СL замкненості секвенції) формалізує:
– відношення |=T (неокласична семантика) для КНЛК однозначних предикатів;
– відношення |=F (пересичена семантика) для КНЛК тотальних предикатів.
Числення QEqL формалізує:
– відношення |=T (неокласична семантика) для КНЛК однозначних еквітонних предикатів;
– відношення |=F (пересичена семантика) для КНЛК тотальних антитонних предикатів.
Числення QR (назва пов’язана із умовою СR замкненості секвенції) формалізує:
35
Теоретичні та методологічні основи програмування
– відношення |=F (неокласична семантика) для КНЛК однозначних предикатів;
– відношення |=T (пересичена семантика) для КНЛК тотальних предикатів.
Числення QEqR формалізує:
– відношення |=F (неокласична семантика) для КНЛК однозначних еквітонних предикатів;
– відношення |=T (пересичена семантика) для КНЛК тотальних антитонних предикатів.
Числення QLR (назва пов’язана із умовами СL та СR) формалізує відношення |=TF для КНЛК однознач-
них предикатів (неокласична семантика) та для КНЛК тотальних предикатів (пересичена семантика).
Числення QEqLR формалізує відношення |=TF для КНЛК однозначних еквітонних предикатів (неокласич-
на семантика) та для КНЛК тотальних антитонних предикатів (пересичена семантика):
Числення QGS формалізує |=TF у випадку загальної семантики часткових неоднозначних предикатів.
Окремими випадками першопорядкових числень QCl, QL, QR, QLR, QGS для реномінативних логік є від-
повідно числення RnCl, RnL, RnR, RnLR, RnGS.
На пропозиційному рівні маємо числення PrCl, PrL, PrR, PrLR, PrGS, які є окремими випадками числень
RnCl, RnL, RnR, RnLR, RnGS. Числення PrCl – це, фактично, відоме [7, 2] класичне пропозиційне числення.
Базова умова замкненості секвенції Σ в усіх численнях – умова С:
С) існує формула Φ така, що |–Φ∈Σ та –|Φ∈Σ.
Згідно відповідної властивості С відношення логічного наслідку, якщо секвенція |–Γ–|Δ замкнена, то Γ |=∗ Δ.
Додаткова умова UnD замкненості секвенції в даній вершині секвенційного дерева опирається на власти-
вість UnD. Умова UnD індукована розподілом імен секвенції-вершини дерева на означені й неозначені.
Нехай U – множина всіх неозначених імен в даній вершині-секвенції Σ. Секвенція Σ U-замкнена, якщо:
UnD) існує пара формул |– Φv
xR ∈Σ та –| Φz
yR ∈Σ таких, що Φv
xR та Φz
yR мають однакові U-неозначувані форми.
Якщо секвенція |–Γ–|Δ U-замкнена, то Γ A, Х–U |=∗ Δ для довільних A та Х ⊆ V: Х ∩ U = ∅.
Опишемо тепер введені числення детальніше.
Числення QGS. Замкненість секвенції визначається умовою C ∨ UnD. Отже, секвенція Σ замкнена, якщо
виконується С або Σ U-замкнена згідно UnD, де U – множина всіх неозначених імен в цій вершині дерева Σ.
Базові секвенційні форми числення QGS записуються згідно відповідних властивостей відношень |=TF .
|−¬¬ |
|
, Σ
, Σ
A
A
−
−¬¬
−|¬¬ |
|
, Σ
, Σ
A
A
−
− ¬¬
|−∨ | |
|
, Σ , Σ
, Σ
A B
A B
− −
− ∨
−|∨ | |
|
, , Σ
, Σ
A B
A B
− −
− ∨
|−¬∨ | |
|
, , Σ
( ), Σ
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
−
−
|–¬RT |
,
| ,
( ),Σ
( ),Σ
v
x
z v
z x
R A
R A
−
−
¬
¬
–|¬RT |
,
| ,
( ),Σ
( ),Σ
v
x
z v
z x
R A
R A
−
−
¬
¬
|–ΦN |
,
| ,
( ),Σ
( ),Σ
v
u
y v
z u
R A
R A
−
−
при у∈ν(A) –|ΦN |
,
| ,
( ),Σ
( ),Σ
v
u
y v
z u
R A
R A
−
−
при у∈ν(A)
|–¬ΦN |
,
| ,
( ),Σ
( ),Σ
v
u
y v
z u
R A
R A
−
−
¬
¬
при у∈ν(A) –|¬ΦN |
,
| ,
( ),Σ
( ),Σ
v
u
y v
z u
R A
R A
−
−
¬
¬
при у∈ν(A)
Тут ν(A) – множина строго неістотних [2] предметних імен формули 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
|–¬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
x
v
x
R A
R A
−
−¬ ¬
–|¬R¬ |
|
( ),Σ
( ),Σ
v
x
v
x
R A
R A
−
− ¬ ¬
36
Теоретичні та методологічні основи програмування
|–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
−
−
∨
∨
|–¬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
− −
−
¬ ¬
¬ ∨
|–R∃R |
,
| ,
( ),Σ
( ),Σ
u
v
u x
v y
R xA
R xA
−
−
∃
∃
при { }x u∉ –|R∃R |
,
| ,
( ),Σ
( ),Σ
u
v
u x
v y
R xA
R xA
−
−
∃
∃
при { }x u∉
|–¬R∃R |
,
| ,
( ),Σ
( ),Σ
u
v
u x
v y
R xA
R xA
−
−
¬ ∃
¬ ∃
при { }x u∉ –|¬R∃R |
,
| ,
( ),Σ
( ),Σ
u
v
u x
v y
R xA
R xA
−
−
¬ ∃
¬ ∃
при { }x u∉
|–R∃p |
|
,Σ
( ),Σx
y
xA
R xA
−
−
∃
∃
–|R∃p |
|
,Σ
( ),Σx
y
xA
R xA
−
−
∃
∃
|–¬R∃p |
|
,Σ
( ),Σx
y
xA
R xA
−
−
¬∃
¬ ∃
–|¬R∃p |
|
,Σ
( ),Σx
y
xA
R xA
−
−
¬∃
¬ ∃
|–∃R
,
| ,
|
( ),Σ
( ),Σ
u x
v z
u
v
R A
R xA
−
− ∃
–|∃R
,
| , |
|
( ), ( ), Σ
( ),Σ
u x u
v y v
u
v
R A R xA
R xA
− −
−
∃
∃
|–¬∃R
,
| | ,
|
( ), ( ), Σ
( ),Σ
u u x
v v y
u
v
R xA R A
R xA
− −
−
¬ ∃ ¬
¬ ∃
–|¬∃R
,
| ,
|
( ),Σ
( ),Σ
u x
v z
u
v
R A
R xA
−
−
¬
¬ ∃
Для |–∃R та –|¬∃R ім’я { }x u∉ , ім’я z тотально строго неістотне та z∉пт(Σ, ( Φ))u
vR x∃ .
|–∃ |
|
( ),Σ
,Σ
x
yR A
xA
−
−∃
–|∃ | |
|
( ), ,Σ
,Σ
x
zR A xA
xA
− −
−
∃
∃
|–¬∃ | |
|
, ( ) Σ
,Σ
x
yxA R A
xA
− −
−
¬∃ ¬
¬∃
,
–|¬∃ |
|
( ),Σ
,Σ
x
zR A
xA
−
−
¬
¬∃
Для |–∃ та –|¬∃ у тотально строго неістотне та у∉пт(Σ, А).
Секвенційні форми типів RT, ¬RT, ΦN, ¬ΦN, R∃R, ¬R∃R, R∃p, ¬R∃p назвемо допоміжними, інші ба-
зові секвенційні форми віднесемо до основних.
Форми |–∃R, |–∃, –|¬∃R, –|¬∃ назвемо ∃T-формами. Форми |–¬∃R, |–¬∃, –|∃R, –|∃ назвемо ∃F-формами.
Форми |−¬¬, −|¬¬, |−∨, −|∨, |−¬∨, −|¬∨, |–RT, –|RT, |–¬RT, –|¬RT, |–RR, –|RR, |–¬RR, –|¬RR, |–R¬, –|R¬,
|–¬R¬, –|¬R¬, |–R∨, –|R∨, |–¬R∨, –|¬R∨, |–ΦN, |–ΦN, |–¬ΦN, |–¬ΦN – базові секвенційні форми числення RnGS.
Форми |−¬¬, −|¬¬, |−∨, −|∨, |−¬∨, −|¬∨ є базовими секвенційними формами числення PrGS.
Замкненість секвенції в численнях RnGS та PrGS задається умовою С.
Числення QL. Замкненість секвенції Σ дається умовою C ∨ CL ∨ UnD. Умова СL така:
СL) Σ замкнена, якщо існує формула Φ така, що |–Φ∈Σ та |–¬Φ∈Σ.
Базові секвенційні форми числення QL записуються згідно відповідних властивостей відношень |=T (нео-
класична семантика) та |=F (пересичена семантика). Вони такі ж, як і для числення QGS.
Базові секвенційні форми числень RnL та PrL такі ж, як для числень RnGS та PrGS відповідно.
Замкненість секвенції в численнях RnL та PrL задається умовою C ∨ CL.
Числення QEqL. Базові секвенційні форми числення QEqL такі ж, як для числення QL.
Замкненість секвенції визначається умовою C ∨ CL ∨ CEqT ∨ CEq¬T ∨ UnD.
Додаткові умови CEqT та CEq¬T замкненості секвенції індуковані властивістю еквітонності (неокласич-
на семантика) чи властивістю антитонності (пересичена семантика). При побудові секвенційного дерева вздовж
незамкненого шляху кожна формула секвенції рано чи пізно буде розкладена до кінця – до примітивних фор-
мул чи їх заперечень. Тому властивості еквітонності та антитонності достатньо враховувати лише для формул
вигляду ,
, (Φ)x u
y vR чи ,
, (Φ)x u
y vR¬ . При цьому властивості CEqT та CEq¬T (неокласична семантика) і властивості
CAnF та CAn¬F (пересичена семантика) дають одні й ті ж умови CEqT та CEq¬T для секвенції-вершини Σ:
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.
Тут Х та Y – множини всіх означених та неозначених імен в даній вершині Σ.
Якщо виконується одна з умов CEqT чи CEq¬T, то секвенцію Σ назвемо TХ–Y -замкненою у випадку нео-
класичної семантики, та FХ–Y -замкненою у випадку пересиченої семантики.
Якщо |–Γ–|Δ TХ–Y -замкнена, то Γ A, Х–Y |=T Δ; якщо ж |–Γ–|Δ FХ–Y -замкнена, то Γ A, Х–Y |=F Δ (для довільної A).
37
Теоретичні та методологічні основи програмування
Числення QR. Базові секвенційні форми числення QR записуються згідно відповідних властивостей від-
ношень |=F (неокласична семантика) та |=T (пересичена семантика). Вони такі ж, як і для числення QGS.
Замкненість секвенції визначається умовою C ∨ CR∨ UnD. Умова СR така:
СR) Σ замкнена, якщо існує формула Φ така, що –|Φ∈Σ та –|¬Φ∈Σ.
Базові секвенційні форми числень RnR та PrR такі ж, як для числень RnGS та PrGS відповідно.
Замкненість секвенції в численнях RnR та PrR задається умовою C ∨ CR.
Числення QEqR. Базові секвенційні форми числення QEqR такі ж, як для числення QR.
Замкненість секвенції визначається умовою C ∨ CR ∨ CEqF ∨ CEq¬F ∨ UnD.
Додаткові умови CEqF та CEq¬F замкненості секвенції індуковані властивістю еквітонності (неокласич-
на семантика) чи властивістю антитонності (пересичена семантика), їх достатньо враховувати лише для формул
вигляду ,
, (Φ)x u
y vR чи ,
, (Φ)x u
y vR¬ . При цьому властивості CEqF та CEq¬F (неокласична семантика) і властивості
CAnT та CAn¬T (пересичена семантика) дають одні й ті ж умови CEqF та CEq¬F для секвенції-вершини Σ:
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.
Тут Х та Y – множини всіх означених та неозначених імен в даній вершині Σ.
Якщо виконується одна з умов CEqF чи CEq¬F, то секвенцію Σ назвемо FХ–Y -замкненою у випадку нео-
класичної семантики, та TХ–Y -замкненою у випадку пересиченої семантики.
Якщо |–Γ–|Δ FХ–Y -замкнена, то Γ A, Х–Y |=F Δ; якщо ж |–Γ–|Δ TХ–Y -замкнена, то Γ A, Х–Y |=T Δ.
Числення QLR. Базові секвенційні форми числення QLR такі ж, як і для числення QGS.
Замкненість секвенції визначається умовою C ∨ CL & CR ∨ UnD.
Одночасне виконання умов СL та СR рівносильне виконанню такої умови:
СLR) Σ замкнена, якщо існують формули Φ та Ψ: |–Φ∈Σ, |–¬Φ∈Σ, –|Ψ∈Σ, –|¬Ψ∈Σ.
Базові секвенційні форми числень RnLR та PrLR такі ж, як для числень RnGS та PrGS відповідно.
Замкненість секвенції в численнях RnLR та PrLR задається умовою С ∨ СLR.
Числення QEqLR. Базові секвенційні форми числення QEqLR такі ж, як для числення QLR.
Замкненість секвенції визначається умовою C ∨ (CL ∨ EqT ∨ CEq¬T) & (CR ∨ CEqF ∨ CEq¬F) ∨ UnD.
Числення QCl. Замкненість секвенції Σ дається умовою C ∨ UnD.
Базовими секвенційними формами числення QCl є |− ¬, −| ¬, |−∨, −|∨, |–RT, –|RT, |–RR, –|RR, |–R¬, –|R¬, |–R∨,
–|R∨, |–ΦN, |–ΦN, |–R∃R, –|R∃R, |–R∃p, –|R∃p, |–∃, –|∃, |–∃R, –|∃R. Ці форми записуються згідно відповідних власти-
востей |=Cl (неокласична семантика) та |=Cm (пересичена семантика). Форми |− ¬ та −| ¬ мають традиційний вигляд:
|− ¬ |
|
, Σ
, Σ
A
A
−
−¬
−| ¬ |
|
, Σ
, Σ
A
A
−
− ¬
Форми |−¬, −|¬, |−∨, −|∨, |–RT, –|RT, |–RR, –|RR, |–R¬, –|R¬, |–R∨, –|R∨, |–ΦN, |–ΦN є базовими формами відо-
мого [2] реномінативного числення RnCl. Базовими формами пропозиційного числення PrCl є |−¬, −|¬, |−∨, −|∨.
Замкненість секвенції в численнях RnCl та PrCl задається умовою С.
Числення QEqCl. Базові секвенційні форми числення QEqCl такі ж, як для числення QCl.
Замкненість секвенції визначається умовою С.
3. Побудова секвенційного дерева. Коректність секвенційних числень
Процедура побудови секвенційного дерева для заданої секвенції Σ фактично однакова для числень QGS,
QL, QEqL, QR, QEqR, QLR, QEqLR. Подібна процедура описана в [5]. Для числення QG, яке є різновидністю
числення QCl, процедура побудови секвенційного дерева описана в [4], для неокласичного числення, яке є різ-
новидністю числення QEqCl, подібна, але істотно простіша процедура, наведена в [2]. Ускладнення процедури
побудови секвенційного дерева в численнях QGS, QL, QEqL, QR, QEqR, QLR, QEqLR зумовлене тим, що в за-
гальному випадку значення предиката P(d) може бути різним залежно від того, входить чи не входить до d ком-
понента з певним предметним іменем. Тому при застосуванні ∃F-форм приклади можуть формуватися лише для
означених імен. Отже, при застосуванні ∃F-форм треба перебирати всі можливі розподіли наявних предметних
імен на означені й неозначені. Це можна реалізувати за допомогою побудови відповідних розгалужень секвен-
ційного дерева: якщо ∃F-форма застосовується вперше на етапі, нехай це буде у вершині Ξ до формули вигляду
–|∃xΦ, –| ( Φ),u
vR x∃ |–¬∃xΦ, |– ( Φ),u
vR x¬ ∃ то для Ξ будується не одна, а багато вершин-"сестер", які є безпосередніми
предками Ξ, мають одну й ту ж множину наявних імен і відрізняються лише різними множинами означених імен та
відповідними множинами прикладів вигляду –| (Φ),x
yR –|
,
, (Φ),u x
v yR |– (Φ),x
yR¬ |– ,
, (Φ),u x
v yR¬ де ім’я у – означене.
Процедура побудови дерева для секвенції Σ починається з кореня дерева. Таку процедуру розіб’ємо на
етапи. Кожне застосування секвенційної форми проводиться до скінченної множини доступних на даний мо-
мент формул. На початку кожного етапу виконується крок доступу. Це означає, що до списку доступних фор-
мул додаємо по одній формулі зі списку |–-формул та списку –|-формул. Якщо в секвенції недоступних |–-формул
38
Теоретичні та методологічні основи програмування
чи –|-формул немає (відповідний список вичерпано), то на подальших кроках доступу додаємо по одній формулі
невичерпаного списку. На початку побудови дерева доступна лише пара перших формул списків (або єдина
|–-формула чи –|-формула, якщо один зі списків порожній). Перед побудовою дерева для секвенції Σ зафіксуємо
деякий список TN (нескінченний) тотально строго неістотних "нових" імен таких, що nm(Σ)∩TN = ∅.
Із кожною вершиною дерева пов’язуємо множину наявних та множину означених предметних імен.
Множина наявних імен – це множина імен усіх формул, які доступні на шляху від кореня до даної вершини.
Множина означених імен явно виділяється лише на шляхах, де були хоч раз застосовані ∃F-форми чи ∃T-форми
(до такого застосування явне виділення множини означених імен непотрібне), при цьому гарантовано означеними
є тотально строго неістотні імена, введені ∃T-формами на шляху від кореня до даної вершини.
Нехай виконано k етапів процедури. На етапі k+1 перевіряємо, чи буде кожен з листів дерева замкненою
секвенцією (беремо до уваги тільки доступні формули секвенцій). Якщо всі листи замкнені, то процедура завер-
шена позитивно, ми отримали замкнене секвенційне дерево. Якщо ні, то для кожного незамкненого листа ξ ро-
бимо наступний крок доступу, після чого добудовуємо скінченне піддерево з вершиною ξ наступним чином.
1. Активізуємо всі доступні (окрім примітивних) формули ξ.
2. До кожної активної формули застосовуємо відповідну основну секвенційну форму.
Перед застосуванням основних секвенційних форм усуваємо, у разі наявності, тотожні перейменування
та пари імен реномінацій за неістотним чи квантифікованим верхнім іменем, застосовуючи належну кількість
разів форми типів RT, ¬RT, ΦN, ¬ΦN, R∃R, ¬R∃R, R∃p, ¬R∃p.
Спочатку виконуємо (якщо це можливо) всі ∃T-форми. Кожне застосування такої форми додає нове то-
тально неістотне у до множини означених імен вершини, таке у беремо як перше незадіяне на даному шляху від
кореня ім’я зі списку TN. Ім’я у гарантовано означене, додаємо його до множин наявних та означених імен.
Після цього до кожної з решти активних формул застосовуємо відповідну форму – одну з форм типів RR,
¬RR, R¬, ¬R¬, R∨, ¬R∨, ¬¬, ∨, ¬∨. Вони не змінюють множини наявних та означених імен.
Далі застосовуємо ∃F-форми. Це робимо таким чином.
1. Якщо першим застосуванням форми елімінації квантора на шляху від кореня дерева до даної вершини
була саме ∃F-форма, то на цьому шляху ще не було виділення означених та неозначених імен. Нехай в даній вер-
шині маємо множину Z наявних імен (імена доступних формул). Тоді, застосовуючи цю форму (–|∃R до
–| ( Φ)u
vR x∃ , –|∃ до –|∃xΦ, |–¬∃R до |– ( Φ),u
vR x¬ ∃ |–¬∃ до |–¬∃xΦ), із даної вершини будуємо скінченне розгалуження
дерева. Для цього розглядаємо всеможливі розподіли імен Z на означені (утворюють множину Y ⊆ Z) та неозначені
(утворюють множину Z\Y). Для кожної Y ⊆ Z будуємо безпосереднього предка даної вершини-секвенції, додаючи
приклади (вигляду –| (Φ),x
yR –|
,
, (Φ),u x
v yR |– (Φ),x
yR¬ |–
,
, (Φ)u x
v yR¬ ) для кожного z∈Y. Для вершини-предка із Y = ∅ бе-
ремо (зі списку TN) нове тотально строго неістотне ім’я t та додаємо приклад вигляду –| (Φ),x
tR –|
,
, (Φ),u x
v tR |– (Φ),x
tR¬
|–
,
, (Φ)u x
v tR¬ ; для такої вершини-предка t – означене, Z – множина неозначених, {t}∪Z – множина наявних імен.
2. Нехай на шляху від кореня дерева до даної вершини ∃F-форма застосовується вперше, проте на шляху
вже були застосування ∃T-форм. Це означає, що в даній вершині вже виділено множину W означених імен (вони
тотально неістотні гарантовано означені). Нехай X – множина всіх інших наявних імен, вони ще не розподілені
на означені та неозначені (W∪X – множина наявних імен вершини). Тоді розглядаємо всеможливі розподіли імен X
на означені (утворюють Y ⊆ X) та неозначені (утворюють X\Y). Для кожної Y ⊆ Z будуємо безпосереднього предка да-
ної вершини-секвенції, додаючи приклади для кожного z∈ W∪Y.
3. Нехай ∃F-форма застосовується вперше на етапі, проте на шляху від кореня дерева до даної вершини
вже були застосування ∃F-форм. Це означає, що в даній вершині вже виділено множини W означених та U не-
означених імен. Нехай на початку етапу після виконання кроку доступу до множини наявних імен було додано
множину X імен нових доступних формул; до першого виконання на даному етапі ∃F-форми імена із X не роз-
поділяються на означені й неозначені (водночас від початку етапу можливе розширення множини означених
імен ∃T-формами); тоді W∪U∪X – множина наявних імен вершини. Розглядаючи всеможливі розподіли імен X на
означені й неозначені, для кожної Y ⊆ X будуємо безпосереднього предка даної вершини-секвенції, додаючи в ньому
приклади для кожного z∈W∪Y.
4. Нехай застосування ∃F-форми – це не перше застосування на етапі форми такого типу. Це означає, що в
даній вершині виділено множини W означених та U неозначених імен, а нерозподілених імен немає, тобто
W∪U – множина наявних імен вершини. Тоді добудовуємо єдиного безпосереднього предка даної вершини-секвен-
ції, додаючи приклади для кожного z∈W. Зауважимо, що при повторному застосуванні ∃F-форми до формули Φ
(застосування ∃F-форми вже були на попередніх етапах) фактично додаємо лише приклади для нових означених
на даному етапі імен, адже для означених на попередніх етапах імен такі приклади вже додані попередніми за-
стосуваннями ∃F-форм до Φ, а повтори формул неможливі (секвенції – це множини специфікованих формул).
Після виконання основної секвенційної форми утворені нею формули на даному етапі пасивні. До таких
формул на даному етапі секвенційні форми вже не застосовуються (це не стосується допоміжних форм).
Всі повтори специфікованих формул у секвенції усуваємо.
Секвенції-вершини, в яких вже немає активних формул, перевіряємо на замкненість. При появі замкненої
секвенції до неї вже незастосовна жодна форма, і процес побудови дерева на цьому шляху обривається.
39
Теоретичні та методологічні основи програмування
При побудові секвенційного дерева можливі такі випадки:
1) Процедуру завершено позитивно, маємо скінченне замкнене дерево.
2) Процедуру завершено негативно, маємо скінченне незамкнене дерево.
3) Процедура не завершується, маємо нескінченне секвенційне дерево. За лемою Кеніга [7] нескінченне
дерево зі скінченним розгалуженням має хоча б один нескінченний шлях.
Отже, у випадках 2) і 3) у дереві існує скінченний або нескінченний незамкнений шлях ℘, всі його вер-
шини – незамкнені секвенції. Кожна з формул секвенції Σ зустрінеться на шляху℘ і стане доступною.
Нехай секвенція |–Γ–|Δ вивідна, тоді для неї побудоване замкнене секвенційне дерево. Із наведеної проце-
дури побудови секвенційного дерева випливає, що для кожної його вершини |–Λ–|Κ з множинами означених імен
W та неозначених імен U для кожної моделі мови A у відповідній семантиці справджується Λ A, W–U |=∗ Κ.
Для листів дерева це випливає з виконання в кожному із числень відповідних умов замкненості секвенції.
Збереження секвенційними формами зазначеного вище відношення логічного наслідку (від засновків до висно-
вків) виконується для допоміжних форм типу RT, ¬RT, ΦN, ¬ΦN, R∃R, ¬R∃R, R∃p, ¬R∃p та основних форм
типу RR, ¬RR, R¬, ¬R¬, R∨, ¬R∨, ¬¬, ∨, ¬∨. Це випливає з однойменних властивостей цього відношення.
Для форм |–∃R, |–∃, –|¬∃R, –|¬∃ збереження відповідних відношень логічного наслідку від засновку до виснов-
ку випливає з властивостей ∃R Х–Y |– , ∃Х–Y |– , ¬∃R Х–Y –| , ¬∃Х–Y –| .
Для форм –|∃R, –|∃, |–¬∃R, |–¬∃ збереження відповідних відношень логічного наслідку при русі до вершини Σ,
яка містить активну формулу вигляду –| ( Φ),u
vR x∃ –|∃xΦ, |– ( Φ),u
vR x¬ ∃ |–¬∃xΦ, від вершин, які є її безпосередніми
предками та містять відповідні приклади вигляду –|
,
, (Φ),u x
v yR –| (Φ),x
yR |– ,
, (Φ),u x
v yR¬ |– (Φ),x
yR¬ гарантується властиво-
стями Br∃R, Br∃Rf, Br∃, Br∃f, Br¬∃R, Br¬∃Rf, Br¬∃, Br¬∃f, а також ∃R Х–Y –|, ∃Х–Y –|, ¬∃R Х–Y |–, ¬∃Х–Y |– .
Для форм |–∃R, |–∃, –|∃R, –|∃ в QEqCl-численнях збереження |=Cl та |=Cт гарантується ∃|–, ∃R|–, ∃–|, ∃R–| .
Таким чином, для побудованих секвенційних числень справджується теорема коректності. Для різних чис-
лень та логічних наслідків вона формулюється однаково, згідно наведеного на початку розділу 2 зв’язку між чис-
леннями певних класів та відношеннями логічного наслідку, які цими численнями формалізуються.
Теорема 1 (коректності). Нехай |–Γ–|Δ вивідна в численні певного класу. Тоді Γ |=* Δ для відповідного від-
ношення |=* у відповідній семантиці.
4. Модельні множини. Повнота секвенційних числень
Для доведення повноти збудованих секвенційних числень використовується метод модельних (хінтікків-
ських) множин [8]. Надалі Н – це множина формул, специфікованих символами |– та –| , із виділеною множиною
W ⊆ nm(Н) означених імен; тоді U = nm(Н) \ W – множина її неозначених імен.
Числення QGS. Множина Н – GS-модельна, якщо виконуються такі умови:
НС) Не існує формули Φ такої, що |–Φ∈Н та –|Φ∈Н.
НСU) Не існує пари формул |–
v
xR A∈Н та –|
u
yR A∈Н таких, що v
xR A та u
yR A мають однакові U-неозна-
чувані форми.
Н¬¬) Якщо |–¬¬Φ∈Н, то |–Φ∈Н; якщо –|¬¬Φ∈Н, то –|Φ∈Н.
Н∨) Якщо |–Φ∨Ψ∈Н, то |–Φ∈Н або |–Ψ∈Н; якщо –|Φ∨Ψ∈Н, то –|Φ∈Н та –|Ψ∈Н.
Н¬∨) Якщо |–¬(Φ∨Ψ)∈Н, то |–¬Φ∈Н та |–¬Ψ∈Н; якщо –|¬(Φ∨Ψ)∈Н, то –|¬Φ∈Н або –|¬Ψ∈Н.
Н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¬ ∈Н.
НΦ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¬ ∈Н.
Н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 ∈Н; якщо –| ( Φ)v
xR¬ ¬ ∈Н, то –| (Φ)v
xR ∈Н.
НR∨) Якщо |– v
xR (Φ∨Ψ)∈Н, то |– v
xR (Φ)∨ v
xR (Ψ)∈Н; якщо –|
v
xR (Φ∨Ψ)∈Н, то –|
v
xR (Φ)∨ v
xR (Ψ)∈Н.
Н¬R∨) Якщо |– (Φ Ψ)v
xR¬ ∨ ∈Н, то |– (Φ)v
xR¬ ∈Н та |– (Ψ)v
xR¬ ∈Н;
якщо –| (Φ Ψ)v
xR¬ ∨ ∈Н, то –| (Φ)v
xR¬ ∈Н або –| (Ψ)v
xR¬ ∈Н.
НR∃R) Якщо |– ,
, ( Φ)u x
v yR x∃ ∈Н, то |– ( Φ)u
vR x∃ ∈Н; якщо –|
,
, ( Φ)u x
v yR x∃ ∈Н, то –| ( Φ)u
vR x∃ ∈Н.
Н¬R∃R) Якщо |– ,
, ( Φ)u x
v yR x¬ ∃ ∈Н, то |– ( Φ)u
vR x¬ ∃ ∈Н; якщо –|
,
, ( Φ)u x
v yR x¬ ∃ ∈Н, то –| ( Φ)u
vR x¬ ∃ ∈Н.
НR∃p) Якщо |– ( Φ)x
yR x∃ ∈Н, то |–∃хΦ∈Н; якщо –| ( Φ)x
yR x∃ ∈Н, то –|∃хΦ∈Н.
40
Теоретичні та методологічні основи програмування
Н¬R∃p) Якщо |– ( Φ)x
yR x¬ ∃ ∈Н, то |–¬∃хΦ∈Н; якщо –| ( Φ)x
yR x¬ ∃ ∈Н, то –|¬∃хΦ∈Н.
Н∃) Якщо |–∃хΦ∈Н, то існує у∈W таке, що |– (Φ)x
yR ∈Н; якщо –|∃хΦ∈Н, то –| (Φ)x
yR ∈Н для всіх у∈W.
Н¬∃) Якщо |–¬∃хΦ∈Н, то |– (Φ)x
yR¬ ∈Н для всіх у∈W;
якщо –|¬∃хΦ∈Н, то існує у∈W таке, що –| (Φ)x
yR¬ ∈Н.
Н∃R) Якщо |– ( Φ)u
vR x∃ ∈Н, то існує у∈W таке, що |– ,
, (Φ)u x
v yR ∈Н;
якщо –| ( Φ)u
vR x∃ ∈Н, то –|
,
, (Φ)u x
v yR ∈Н для всіх у∈W.
Н¬∃R) Якщо |– ( Φ)u
vR x¬ ∃ ∈Н, то |– ,
, ( Φ)u x
v yR x¬ ∃ ∈Н для всіх у∈W;
якщо –| ( Φ)u
vR x¬ ∃ ∈Н, то існує у∈W таке, що –|
,
, (Φ)u x
v yR¬ ∈Н.
НС та НСU – це умови коректності GS-модельної множини.
Числення QL. Множина Н – L-модельна, якщо виконуються наведені вище умови для GS-модельної мно-
жини, а також умова НСL:
НСL) Не існує формули Φ такої, що |–Φ∈Н та |–¬Φ∈Н.
НС НСL та НСU – це умови коректності L-модельної можини.
Числення QEqL. Н – 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. Н – R-модельна, якщо виконуються умови для GS-модельної множини, а також умова НСR:
НСR) Не існує формули Φ такої, що –|Φ∈Н та –|¬Φ∈Н.
НС, НСR та НСU – це умови коректності R-модельної можини.
Числення QEqR. Н – 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. Н – LR-модельна, якщо виконуються умови для GS-модельної множини, а також НСLR:
НСLR) Не існують формули Φ та Ψ такі, що |–Φ∈Н, |–¬Φ∈Н та –|Ψ∈Н, –|¬Ψ∈Н.
НС, НСLR та НСU – це умови коректності LR-модельної множини.
Числення QEqLR. Н – EqLR-модельна, якщо виконуються умови для GS-модельної множини, а також
умови коректності НСL, НCEqT, НCEq¬T, або умови коректності НСR, НCEqF, НCEq¬F.
Числення QCl. Н – C-модельна, якщо виконуються умови НС, НСU, Н∨, НRT, НΦN, НRR, НR¬, НR∨,
НR∃R, НR∃p, Н∃, Н∃R, а також умова Н¬:
Н¬) Якщо |–¬Φ∈Н, то –|Φ∈Н; якщо –|¬Φ∈Н, то |–Φ∈Н.
НС та НСU – це умови коректності C-модельної можини.
Числення QEqCl. Множина Н – EqC-модельна, якщо виконуються умови НС, Н¬, Н∨, НRT, НΦN, НRR,
НR¬, НR∨, НR∃R, НR∃p, Н∃, Н∃R. НС – це умова коректності EqC-модельної можини.
Незамкнений шлях в секвенційному дереві індукує модельну множину.
Теорема 2. Нехай ℘ – незамкнений шлях у секвенційному дереві, Н – множина всіх специфікованих фо-
рмул секвенцій цього шляху. Тоді Н – модельна множина відповідного типу (GS-модельна, L-модельна, EqL-
модельна, R-модельна, EqR-модельна, LR-модельна, EqLR-модельна, C-модельна).
Для переходу від нижчої вершини шляху до вищої використовується одна з базових секвенційних форм
відповідного числення. Переходи згідно з цими формами узгодженні з однойменними пунктами визначення
модельної множини відповідного типу. Кожна формула на шляху ℘, яка не є примітивною чи її запереченням,
рано чи пізно буде розкладена чи спрощена згідно з відповідною секвенційною формою. Усі секвенції шляху ℘
незамкнені, тому виконані умови коректності модельної множини відповідного типу.
За модельною множиною можна побудувати контрмодель.
Теорема 3. Нехай Н – модельна множина, яка може бути GS-, L-, EqL-, R-, EqR-, LR-, EqLR-модельною.
Тоді існують моделі мови A = (A, I), BB = (A, I) та δ, η∈ A такі: V
1) |–Φ∈Н ⇒ δ∈T(ΦA) та –|Φ∈Н ⇒ δ∉T(ΦA);
2) |–Φ∈Н ⇒ η∉F(ΦB) та –|Φ∈Н ⇒ η∈F(ΦB).
Пари (A, δ) та (B, η) із наведеними вище властивостями назвемо T-контрмоделлю та F-контрмоделлю.
Зауважимо, що теорема 3 роботи [5] – це окремий випадок теореми 3 для логік однозначних предикатів.
Нехай W – множина усіх означених предметних імен, що фігурують у Н. Візьмемо деяку множину А та-
ку, що |А| = |W|, та деякі ін’єктивні δ, η∈VA з im(δ) = W. Така А дублює множину W.
Доведення теореми ведеться індукцією за складністю формули згідно з побудовою модельної множини.
41
Теоретичні та методологічні основи програмування
Задамо значення базових предикатів та їх заперечень на δ та η, а також на ІМ вигляду r v
x (δ) та r v
x (η):
– якщо |– р∈Н, то задамо δ∈T(рA); – якщо –| р∈Н, то задамо δ∉T(рA);
– якщо |– р∈Н, то задамо η∉F(рB); – якщо –| р∈Н, то задамо η∈F(рB);
– якщо |–¬р∈Н, то задамо δ∈F(pA) = T(¬pA); – якщо –|¬p∈Н, то задамо δ∉F(pA) = T(¬pA);
– якщо |–¬p∈Н, то задамо η∉T(pB) = F(¬pB); – якщо –|¬p∈Н, то задамо η∈T(pB) = F(¬pB);
– якщо |– ( )v
xR p ∈Н, то задамо r v
x (δ)∈T(рA); – якщо –| ( )v
xR p ∈Н, то задамо r v
x (δ)∉T(рA);
– якщо |– ( )v
xR p ∈Н, то задамо r v
x (η)∉F(рB); – якщо –| ( )v
xR p ∈Н, то задамо r v
x (η)∈F(р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); – якщо –| ( )v
xR p¬ ∈Н, то задамо r v
x (η)∈T(pB)B = F(¬pBB).
В усіх інших випадках значення базових предикатів та їх заперечень задаємо довільно, беручи до уваги
обмеження щодо строго неістотності: для всіх d, h∈VA таких, що d║-ν(p) = h║-ν(p), необхідно рA(d) = рA(h),
¬рA(d) = ¬рA(h), рB(d) = рB(h), ¬рB(d) = ¬рB(h). Це враховує строго неістотність імен у∈ν(p) для рA та рB . Для
випадків EqL-, EqR-, EqLR-модельної множини так задані значення базових предикатів та їх заперечень продо-
вжуємо, ураховуючи також умови еквітонності (антитонності), на відповідні h∈VA. В усіх інших випадках зна-
чення базових предикатів та їх заперечень задаємо довільно, беручи до уваги обмеження щодо еквітонності (ан-
титонності) та строго неістотності. Отже, значення базових предикатів та їх заперечень визначені коректно.
Для атомарних формул і формул вигляду ( )v
xR p та їх заперечень твердження теореми випливають з ви-
щенаведеного визначення значень базових предикатів та їх заперечень.
Доведення кроку індукції аналогічне відповідному доведенню теореми 3 роботи [5]. Наведемо для при-
кладу доведення для п. Н¬∃R визначення модельної множини.
Нехай |– ( Φ)u
vR x¬ ∃ ∈Н. Згідно Н¬∃R тоді для всіх у∈W маємо |–
,
, (Φ)u x
v yR¬ ∈Н. За припущенням індукції
для δ маємо δ∈T ,
,( (Φ)u x
v y AR¬ ) для всіх у∈W. Звідси δ δ( ) δ( )u v x y∇ ∇a a ∈F(ΦA) для всіх у∈W. Згідно з δ∈АW
маємо δ(у)↓ для всіх у∈W. Позаяк δ є бієкцією W→А, то кожне b∈А має вигляд b = δ(у) для деякого у∈W. Отже,
δ δ( )u v x∇ ∇a a b ∈F(ΦA) для всіх b∈А, звідки δ∈F ( ( Φ)u
v AR x∃ ) = T ( ( Φ)u
vR x¬ ∃ A ). За припущенням індукції
для η маємо η∉F ,
,( (Φ)u x
v y BR¬ для всіх у∈W. Звідси η η( ) η( )u v x y∇ ∇a a ∉T(ΦB) для всіх у∈W. Згідно з η∈АW
маємо η(у)↓ для всіх у∈W. Позаяк η є бієкцією W→А, то кожне b∈А має вигляд b = η(у) для деякого у∈W. Отже,
η η( )u v x∇ ∇a a b ∉T(ΦB) для всіх b∈А, звідки η∉T ( ( Φ)u
v BR x∃ ) = F ( ( Φ)u
v BR x¬ ∃ ).
Нехай –| ( Φ)u
vR x¬ ∃ ∈Н. Згідно Н¬∃R тоді існує у∈W таке, що –|
,
, (Φ)u x
v yR¬ ∈Н. За припущенням індукції
для δ маємо δ∉T ,
,( (Φ)u x
v y AR¬ ). Звідси δ δ( ) δ( )u v x∇ ∇a a y ∉F(ΦA). Однак δ(у)↓ згідно з δ∈WА та у∈W, тому
δ δ( )u v x∇ ∇a a a ∉F(ΦA) для а = δ(у), звідки δ∉F ( ( Φ)u
v AR x∃ ) = T ( ( Φ)u
vR x¬ ∃ A ). За припущенням індукції для
η маємо η∈F ,
,( (Φ)u x
v y BR¬ ). Звідси η η( ) η( )u v x∇ ∇a a y ∈T(ΦB). Однак η(у)↓ згідно з η∈WА та у∈W, тому для
а = η(у) маємо η η( )u v x∇ ∇a a a ∈T(ΦB), звідки η∈T ( ( Φ)u
v BR x∃ ) = F ( ( Φ)u
v BR x¬ ∃ ).
Теорема 4. Нехай Н – C-модельна множина. Тоді існують моделі мови A = (A, I), BB = (A, I) та δ, η∈ A такі: V
1) |–Φ∈Н ⇒ δ∈T(ΦA) та –|Φ∈Н ⇒ δ∈F(ΦA);
2) |–Φ∈Н ⇒ η∉F(ΦB) та –|Φ∈Н ⇒ η∉T(ΦB).
Пари (A, δ) та (B, η) із наведеними вище властивостями назвемо Cl-контрмоделлю та Cm-контрмоделлю.
Нехай W – множина усіх означених предметних імен, що фігурують у Н. Візьмемо деяку множину А та-
ку, що |А| = |W|, та деякі ін’єктивні δ, η∈VA з im(δ) = W.
Теорема доводиться індукцією за складністю формули згідно з побудовою C-модельної множини.
Задамо значення базових предикатів на δ та η, а також на ІМ вигляду r v
x (δ) та r v
x (η):
– якщо |– р∈Н, то задамо δ∈T(рA); – якщо –| р∈Н, то задамо δ∈F(рA);
– якщо |– р∈Н, то задамо η∉F(рB); – якщо –| р∈Н, то задамо η∉T(рB);
– якщо |– ( )v
xR p ∈Н, то задамо r v
x (δ)∈T(рA); – якщо –| ( )v
xR p ∈Н, то задамо r v
x (δ)∈F(рA);
– якщо |– ( )v
xR p ∈Н, то задамо r v
x (η)∉F(рB); – якщо –| ( )v
xR p ∈Н, то задамо r v
x (η)∉T(рB).
В усіх інших випадках значення базових предикатів задаємо довільним чином, беручи до уваги обмеження
щодо строго неістотності імен: для всіх d, h∈VA таких, що d║-ν(p) = h║-ν(p), необхідно рA(d) = рA(h), рB(d) = рB(h).
Це враховує строго неістотність імен у∈ν(p) для рA і рB . Отже, значення базових предикатів визначені коректно.
Для атомарних формул і формул вигляду ( )v
xR p твердження теореми випливають із визначення значень
базових предикатів. Наведемо для прикладу доведення кроку індукції для п. НR∃p визначення модельної множини.
Нехай |– ( Φ)x
yR x∃ ∈Н. Згідно умови НR∃p маємо |–∃хΦ∈Н. За припущенням індукції для δ маємо
42
Теоретичні та методологічні основи програмування
δ∈T(∃хΦА) = T ( ( ). За припущенням індукції для η маємо η∉F(∃хΦΦ)x
yR x∃ A
A
B) = F ). ( ( Φ)x
y BR x∃
Нехай –| ( Φ)x
yR x∃ ∈Н. Згідно умови НR∃p маємо –|∃хΦ∈Н. За припущенням індукції для δ маємо
δ∈F(∃хΦА) = F ). За припущенням індукції для η маємо η∉T(∃хΦ( ( Φ)x
yR x∃ B) = T ( ( ). Φ)x
y BR x∃
Теорема повноти для різних варіантів секвенційних числень та логічних наслідків формулюється одна-
ково. Розглядаємо випадок першопорядкових числень КНЛК (для реномінативних та пропозиційних числень
формулювання й доведення теорем аналогічні). Зауважимо, що коректність та повнота першопорядкових чис-
лень логіки однозначних еквітонних предикатів, різновидністю яких є QEqCl-числення, доведена в [2].
Поєднуючи теореми повноти та відповідні теореми коректності, отримуємо наступне твердження.
Теорема 5. 1) Γ |=Cl Δ в неокласичній семантиці ⇔ секвенція |–Γ–|Δ вивідна в численні QCl;
2) Γ |=Cm Δ в пересиченій семантиці ⇔ секвенція |–Γ–|Δ вивідна в численні QCl;
3) Γ |=Cl Δ в неокласичній семантиці логіки еквітонних предикатів ⇔ |–Γ–|Δ вивідна в численні QEqCL;
4) Γ |=Cm Δ в пересиченій семантиці логіки антитонних предикатів ⇔ |–Γ–|Δ вивідна в численні QEqCL;
5) Γ |=T Δ в неокласичній семантиці ⇔ секвенція |–Γ–|Δ вивідна в численні QL;
6) Γ |=F Δ в пересиченій семантиці ⇔ секвенція |–Γ–|Δ вивідна в численні QL;
7) Γ |=T Δ в неокласичній семантиці логіки еквітонних предикатів ⇔ |–Γ–|Δ вивідна в численні QEqL;
8) Γ |=F Δ в пересиченій семантиці логіки антитонних предикатів ⇔ |–Γ–|Δ вивідна в численні QEqL;
9) Γ |=F Δ в неокласичній семантиці ⇔ секвенція |–Γ–|Δ вивідна в численні QR;
10) Γ |=T Δ в пересиченій семантиці ⇔ секвенція |–Γ–|Δ вивідна в численні QR;
11) Γ |=F Δ в неокласичній семантиці логіки еквітонних предикатів ⇔ |–Γ–|Δ вивідна в численні QEqR;
12) Γ |=T Δ в пересиченій семантиці логіки антитонних предикатів ⇔ |–Γ–|Δ вивідна в численні QEqR;
13) Γ |=TF Δ в неокласичній семантиці чи пересиченій семантиці ⇔ |–Γ–|Δ вивідна в численні QLR;
14) Γ |=TF Δ в неокласичній семантиці логіки еквітонних предикатів чи пересиченій семантиці логіки ан-
титонних предикатів ⇔ секвенція |–Γ–|Δ вивідна в численні QEqLR;
15) Γ |=TF Δ в загальній семантиці ⇔ секвенція |–Γ–|Δ вивідна в численні QGS.
Наведемо для прикладу доведення п. 15. Припустимо супротивне: Γ |=TF Δ та |–Γ–|Δ невивідна. Якщо Σ = |–Γ–|Δ
невивідна, то в секвенційному дереві для Σ існує незамкнений шлях. Згідно з теоремою 2, множина Н усіх спе-
цифікованих формул секвенцій цього шляху – GS-модельна. Тоді |–Γ–|Δ ⊆ Н.
Згідно з теоремою 3 існують T-контрмодель (A, δ) та F-контрмодель (B, η) такі:
|–Φ∈Н ⇒ δ∈T(ΦA) та –|Φ∈Н ⇒ δ∉T(ΦA); |–Φ∈Н ⇒ η∉F(ΦB) та B –|Φ∈Н ⇒ η∈F(ΦBB).
Для T-контрмоделі згідно з |–Γ–|Δ ⊆ Н для всіх Φ∈Γ маємо δ∈T(ΦA), для всіх Ψ∈Δ маємо δ∉T(ΨA). Звідси
δ∈T(ΓA) та δ∉T(ΔA), звідки невірно T(ΓA) ⊆ T(ΔA). Це заперечує Γ A|=T Δ, тому й заперечує Γ |=TF Δ.
Для F-контрмоделі згідно з |–Γ–|Δ ⊆ Н для всіх Φ∈Γ маємо η∉F(ΦB), для всіх Ψ∈Δ маємо η∈F(ΨB). Звідси
η∉F(ΓB) та η∈F(ΔB), звідки невірно F(ΔB) ⊆ F(ΓB). Це заперечує Γ B|=B F Δ, тому й заперечує Γ |=TF Δ.
Висновки
Для першопорядкових композиційно-номінативних логік часткових однозначних, тотальних неоднознач-
них та часткових неоднозначних квазіарних предикатів кванторного рівня побудовано числення секвенційного
типу. Основою такої побудови є досліджені в попередніх роботах властивості відношень логічного наслідку для
множин формул. Характерною особливістю пропонованих числень є використання спеціальних секвенційних
форм елімінації кванторів під реномінацією Розмаїття цих відношень дає низку різновидностей секвенційних
числень. Такі числення збудовано як для загального випадку логік квазіарних предикатів, так і для логік одно-
значних еквітонних та логік тотальних антитонних предикатів. Для пропонованих числень наведено базові
секвенційні форми та умови замкненості секвенцій, визначено поняття модельної множини. Для побудованих
числень доведено теореми коректності та повноти.
1. Никитченко Н.С. Композиционно-номинативный подход к уточнению понятия программы // Проблеми програмування. – 1999. – № 1. –
С. 16–31.
2 Нікітченко М.С., Шкільняк С.С. Математична логіка та теорія алгоритмів. – К., 2008. – 528 с.
3. Шкільняк С.С. Відношення логічного наслідку в композиційно-номінативних логіках // Проблеми програмування. – 2010. –№ 1. – C. 15–38.
4. Шкильняк С.С. Логики квазиарных предикатов первого порядка // Кибернетика и системный анализ. – 2010. – № 6. – С. 32–49.
5. Шкільняк С.С. Секвенційні числення першопорядових логік однозначних квазіарних предикатів // Проблеми програмування. – 2012. – № 1.
– C. 34–51.
6. Шкільняк С.С. Спеціальні відношення логічного наслідку в логіках квазіарних предикатів // Проблеми програмування. – 2011. – № 4. –
C. 36–48.
7. Клини С. Математическая логика. – М., 1973. – 480 с.
8. Смирнова Е.Д. Логика и философия. – М., 1996. – 304 с.
43
|