Spectrum of sequential number pershopordinal compositional-nominative logics
Prombles in programming 2013; 3: 22-37
Збережено в:
| Дата: | 2025 |
|---|---|
| Автор: | |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
Інститут програмних систем НАН України
2025
|
| Теми: | |
| Онлайн доступ: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/750 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Problems in programming |
Репозитарії
Problems in programming| id |
pp_isofts_kiev_ua-article-750 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/1b/776c32de66c585bdc96caefa12ee621b.pdf |
| spelling |
pp_isofts_kiev_ua-article-7502025-06-21T15:30:49Z Spectrum of sequential number pershopordinal compositional-nominative logics Спектр секвенційних числень першопорядкових композиційно-номінативних логік Shkilnyak, S.S. UDC 004.42:510.69 УДК 004.42:510.69 Prombles in programming 2013; 3: 22-37 Досліджено чисті першопорядкові композиційно-номінативні логіки часткових однозначних, тотальних неоднозначних та часткових неоднозначних квазіарних предикатів. Для різних відношень логічного наслідку в таких логіках побудовано спеціальні секвенційні числення. При цій побудові використано спеціальні предикати-індикатори наявності значення для змінних. Для пропонованих числень доведено теореми коректності й повноти.Prombles in programming 2013; 3: 22-37 Інститут програмних систем НАН України 2025-06-21 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/750 PROBLEMS IN PROGRAMMING; No 3 (2013); 22-37 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 3 (2013); 22-37 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 3 (2013); 22-37 1727-4907 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/750/802 Copyright (c) 2025 PROBLEMS IN PROGRAMMING |
| institution |
Problems in programming |
| baseUrl_str |
https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| datestamp_date |
2025-06-21T15:30:49Z |
| collection |
OJS |
| language |
Ukrainian |
| topic |
UDC 004.42:510.69 |
| spellingShingle |
UDC 004.42:510.69 Shkilnyak, S.S. Spectrum of sequential number pershopordinal compositional-nominative logics |
| topic_facet |
UDC 004.42:510.69 УДК 004.42:510.69 |
| format |
Article |
| author |
Shkilnyak, S.S. |
| author_facet |
Shkilnyak, S.S. |
| author_sort |
Shkilnyak, S.S. |
| title |
Spectrum of sequential number pershopordinal compositional-nominative logics |
| title_short |
Spectrum of sequential number pershopordinal compositional-nominative logics |
| title_full |
Spectrum of sequential number pershopordinal compositional-nominative logics |
| title_fullStr |
Spectrum of sequential number pershopordinal compositional-nominative logics |
| title_full_unstemmed |
Spectrum of sequential number pershopordinal compositional-nominative logics |
| title_sort |
spectrum of sequential number pershopordinal compositional-nominative logics |
| title_alt |
Спектр секвенційних числень першопорядкових композиційно-номінативних логік |
| description |
Prombles in programming 2013; 3: 22-37 |
| publisher |
Інститут програмних систем НАН України |
| publishDate |
2025 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/750 |
| work_keys_str_mv |
AT shkilnyakss spectrumofsequentialnumberpershopordinalcompositionalnominativelogics AT shkilnyakss spektrsekvencíjnihčislenʹperšoporâdkovihkompozicíjnonomínativnihlogík |
| first_indexed |
2025-07-17T09:53:42Z |
| last_indexed |
2025-07-17T09:53:42Z |
| _version_ |
1838410124579831808 |
| fulltext |
Теоретичні та методологічні основи програмування
© C.С. Шкільняк, 2013
22 ISSN 1727-4907. Проблеми програмування. 2013. № 3
УДК 004.42:510.69
С.С. Шкільняк
СПЕКТР СЕКВЕНЦІЙНИХ ЧИСЛЕНЬ ПЕРШОПОРЯДКОВИХ
КОМПОЗИЦІЙНО-НОМІНАТИВНИХ ЛОГІК
Досліджено чисті першопорядкові композиційно-номінативні логіки часткових однозначних, тотальних
неоднозначних та часткових неоднозначних квазіарних предикатів. Для різних відношень логічного на-
слідку в таких логіках побудовано спеціальні секвенційні числення. При цій побудові використано спе-
ціальні предикати-індикатори наявності значення для змінних. Для пропонованих числень доведено те-
ореми коректності й повноти.
Вступ
Апарат математичної логіки дово-
дить свою ефективність при розв'язанні
широкого кола задач інформатики й про-
грамування. Створено багато різноманіт-
них логічних систем (див., напр., [1]), які
успішно застосовуються в програмуванні.
Такі системи зазвичай базуються на класи-
чній логіці предикатів. Проте ця логіка має
принципові обмеження, що ускладнює її ви-
користання. Вона базується на структурах
однозначних тотальних скінченно-арних
предикатів, водночас для програмування
характерне використання часткових неод-
нозначних відображень над складними да-
ними. Тому вельми актуальною стає проб-
лема побудови нових, програмно-орієнто-
ваних логічних формалізмів. Такими є ком-
позиційно-номінативні логіки (КНЛ) – ло-
гічні формалізми, збудовані [2] на основі
композиційно-номінативного підходу.
Для розв'язання низки задач, що ви-
никають в інформаційних і програмних
системах, необхідний ефективний пошук
виведень. Потужним апаратом побудови
виведень є числення секвенційного (ґенце-
нівського) типу. Такі числення формалізу-
ють фундаментальне поняття логічного
слідування. Уточнення цього поняття для
КНЛ за допомогою відношень логічного
наслідку запропоновано в [3]. Введено "не-
спростовнісний" |=Cl, "насичений" |=Cm, "іс-
тиннісний" |=T, "хибнісний" |=F, "сильний"
|=TF логічні наслідки. Побудовано (див.,
напр., [4–8]) низку секвенційних числень
для різних класів КНЛ, які формалізують
ці відношення. Зазначимо, що пропозицій-
ні числення для таких відношень розгля-
дались у [9]. Спеціальні секвенційні чис-
лення для чистих першопорядкових КНЛ
однозначних часткових предикатів запро-
поновано в [7, 8], їх особливістю є викори-
стання введених в [10] спеціальних преди-
катів, які визначають наявність значення
для предметних імен (змінних).
Метою даної роботи є побудова сек-
венційних числень для різних відношень
логічного наслідку в чистих першопоряд-
кових КНЛ (ЧКНЛ) часткових однознач-
них, тотальних неоднозначних і часткових
неоднозначних предикатів. При побудові
використовуємо спеціальні предикати-ін-
дикатори наявності значення для змінних.
Поняття, які тут не визначаються,
тлумачимо в сенсі робіт [2, 3, 6].
1. Основні поняття і визначення
Для полегшення читання наведемо
основні визначення та позначення.
V-іменна множина (V-ІМ) над A – це
однозначна функція вигляду
:
V A. По-
даємо V-ІМ у вигляді [v1a1,...,vnan,...].
Клас всіх V-ІМ над A позначимо
V
A.
Вводимо функцію asn :
V
A2
V
так:
asn() = {vV | va для деякого aA}.
Визначимо ║Х = {va | vXV}.
Замість ║(V \{x}) пишемо ║–x .
Задамо 12 = 2 (1 ||(V \ asn(2)));
r 1
1
,...,
,...,
n
n
v v
x x
() = [v1(x1),...,vn(xn)]
(║(V\{v1,...,vn})).
Замість y1,…, yn пишемо також y .
Під V-квазіарним предикатом на
множині А розуміємо довільну часткову не-
однозначну функцію вигляду P :
V
А Bool.
Теоретичні та методологічні основи програмування
23
Тут Bool = {T, F} – множина істин-
нісних значень.
Зауважимо, що в цій роботі, як і в
[3, 6], ми беремо найпростіше математичне
уточнення складного і багатоаспектного
поняття неоднозначної функції, трактуючи
неоднозначні предикати як відношення між
V
A та Bool. Тому такі предикати можна на-
звати предикатами реляційного типу. При
цьому ми трактуємо P(d) як множину зна-
чень, які предикат P може прийняти на
d
V
A. Зрозуміло, що, клас однозначних V-
квазіарних предикатів реляційного типу
ізоморфний класу традиційних [2] V-квазі-
арних предикатів – однозначних функцій
типу
V
А Bool.
Для V-квазіарного предиката Р за-
даємо області істинності та хибності:
T(P) = {d
V
A | TP(d)};
F(P) = {d
V
A | FP(d)}.
V-квазіарний предикат P:
– однозначний, якщо T(P)F(P) = ;
– тотальний, якщо T(P)F(P) =
V
A.
Фундаментальною властивістю ві-
дображень, які використовуються в прог-
рамуванні, є монотонність щодо розши-
рення даних новими компонентами.
Предикат P :
V
А
{T, F} монотон-
ний, якщо d d' P(d) P(d').
Окремим випадком монотонності є
еквітонність – збереження прийнятого зна-
чення при розширенні даних.
Предикат P еквітонний, якщо з умо-
ви P(d) та d d випливає P(d) = P(d).
Для однозначних часткових преди-
катів визначення монотонності й еквітон-
ності рівносильні. Для цих предикатів мо-
нотоність можна трактувати як збереження
їх інформативності при збільшенні інфор-
мативності вхідних даних. Проте для тота-
льних монотонних предикатів при розши-
ренні вхідних даних інформативність може
лише зменшуватися. Для тотальних преди-
катів змістовно прийнятною є дуальна до
монотонності властивість антитонності.
Предикат P :
V
А
{T, F} антитон-
ний, якщо d d' P(d) P(d').
Базовими композиціями ЧКНЛ є ,
, R ,v
x x. Для їх визначення задаємо пре-
дикати P, PQ, R ( ),v
x P xP :
T(P) = F(P);
F(P) = T(P);
T(PQ) = T(P)T(Q);
F(PQ) = F(P)F(Q);
T( Rv
x (P)) = r v
x (T(P));
F( Rv
x (P)) = r v
x (F(P));
T(xP) = {d
V
A | TР(dxa) для
деякого aA};
F(xP) = {d
V
A | FР(dxa) для
всіх aA}.
Композиції , , R ,v
x x зберігають
властивості монотонності та антитонності.
Ім'я xV (строго) неістотне для V-ква-
зіарного предиката P, якщо для довільних
d
V
A та aA маємо P(dxa) = P(d║–x).
Семантичними моделями ЧКНЛ є
композиційні системи (КС) квазіарних пре-
дикатів (
V
А, Pr
A
, C), де Pr
A
– клас V-ква-
зіарних предикатів на A, C визначається ба-
зовими композиціями , , R ,v
x x. Терми
композиційної алгебри (Pr
A
, C) трактуємо
як формули мови ЧКНЛ.
Алфавіт мови: символи , , ,v
xR x
базових композицій, множина Ps предика-
тних символів (сигнатура мови), множина
V предметних імен. Множина Fr формул
мови ЧКНЛ визначається індуктивно:
1) кожний рPs є формулою; такі
формули атомарні;
2) нехай та – формули; тоді
, Ф, v
xR , x – формули.
Формули вигляду v
xR називати-
мемо R-формулами.
На основі тотального однозначного
відображення I : Ps Pr
A
, яке позначає
символами Рs базові предикати, задаємо
відображення інтерпретації J : FrPr
A
:
1) J(р) = I(p) для кожного рPs;
2) J() = (J()),
J() = (J(), J()),
J ( )v
xR = Rv
x (J()), J(x) = x(J()).
Предикат J() позначаємо A .
Відображення J пов'язує алгебру да-
них (А, Pr) із мовою ЧКНЛ. Тому моделя-
ми мови є об'єкти вигляду A = ((A, Pr
A
), I) –
алгебраїчні системи з доданою сигнатурою
Теоретичні та методологічні основи програмування
24
(мовою) [2], які скорочено позначатимемо
(A, I). Кожна така A задає КС (
V
A, Pr
A
, C).
Ім'я xV строго неістотне для фор-
мули , якщо для кожної моделі мови A
ім'я x строго неістотне для A.
Формула примітивна, якщо вона
атомарна або має вигляд v
xR p , причому
відсутні тотожні перейменування та не
містить строго неістотних для p імен.
Для кожного рPs множину (стро-
го) неістотних предметних імен задаємо за
допомогою тотальної функції : Ps2
V
,
яка продовжується [3] до : Fr2
V
. Для
ЧКНЛ постулюємо нескінченність множи-
ни ( )T
p Ps
V p
тотально неістотних імен.
Характерною ознакою логік квазі-
арних предикатів є те, що значення преди-
ката P(d) може бути різним залежно від
того, входить чи не входить до d компоне-
нта з певним предметним іменем. Тому
для цих логік невірні [3, 4] деякі важливі
закони класичної логіки. Отже, при інтер-
претаціях формул варто явно вказувати оз-
начені та неозначені предметні імена. Це
можна робити [3–6] за допомогою спеціа-
льних Х–Y-означених відношень логічного
наслідку. В даній роботі використовуємо
запропоновані в [10] спеціальні 0-арні ком-
позиції – параметризовані за предметними
іменами предикати-індикатори x. Вони
визначають наявність в даних компоненти
з таким x, тобто наявність значення для x.
ЧКНЛ, мови яких розширені множи-
ною {x | xV} символів предикатів-інди-
каторів x, названо [7, 8] -ЧКНЛ. Такі роз-
ширені логіки утворюють окремий підрі-
вень кванторного рівня із базовими компо-
зиціями , , R ,v
x x, x.
Предикати x задамо так:
F(x) = {d | d(x)} = {d
V
A | xasn(d)};
T(x) = {d | d(x)} = {d
V
A | xasn(d)}.
Теорема 1. Маємо
T
,
,(R ( ))u x
v y P F(y) T (R ( ))u
v xP та
F (R ( ))u
v xP F(y) F
,
,(R ( ))u x
v y P .
Звідси T (R ( ))x
y P F(y) T(xР) та
F(xР) F(y) F (R ( ))x
y P . Водночас умо-
ви T (R ( ))x
y P T(xР) і F(xР) F (R ( ))x
y P
невірні [4] навіть для однозначних квазіар-
них предикатів.
Семантичні властивості КНЛ част-
кових однозначних, тотальних неоднозна-
чних і часткових неоднозначних квазіар-
них предикатів досліджено в [3].
2. Відношення логічного наслідку
Відношення A|=T, A|=F, A|=TF, A|=Cl,
A|=Cm наслідку для множин формул при ін-
терпретації на моделі мови A задаємо так.
Нехай Fr та Fr. Визначаємо:
A|=Cl , якщо
( ) ( )A AT F
;
A|=Cm , якщо
( ) ( ) V
A AF T A
;
A|=T , якщо
( ) ( )A AT T
;
A|=F , якщо
( ) ( )A AF F
;
A|=TF , якщо A|=F та A|=T .
Відношення логічного наслідку для
множин формул |=T, |=F, |=TF, |=Cl, |=Cm ви-
значаємо за такою схемою:
|= , якщо A|= для кожної мо-
делі мови A (тут – одне з T, F, TF, Cl, Cm).
Для логік однозначних часткових
предикатів (неокласична семантика) відно-
шення |=Cm порожнє [3], тому можна роз-
глядати відношення |=Cl, |=T, |=F, |=TF .
Для логік неоднозначних тотальних
предикатів (пересичена семантика) відно-
шення |=Cl порожнє [3], тому можна роз-
глядати відношення |=Cm, |=T, |=F, |=TF .
Для логік неоднозначних часткових
предикатів (загальна семантика) відношен-
ня |=Cl та |=Cm порожні, відношення |=T та
|=F збігаються, тому маємо єдине природне
змістовне відношення |=TF .
Теорема 2. 1) |=Cl в неокласич-
ній семантиці |=Cm в пересиченій;
2) |=T в неокласичній семантиці
|=F в пересиченій;
3) |=F в неокласичній семантиці
|=T в пересиченій;
4) у випадку загальної семантики
|=T |=F |=TF .
Теоретичні та методологічні основи програмування
25
Співвідношення між різними відно-
шеннями логічного наслідку в різних се-
мантиках наведено в [3].
Надалі, якщо інше окремо не зазна-
чено, |= позначає:
– |=TF для загальної семантики;
– одне із |=Cl, |=T, |=F, |=TF для нео-
класичної семантики;
– одне із |=Cm, |=T, |=F, |=TF для пе-
ресиченої семантики.
Наведемо основні властивості від-
ношень |=T, |=F, |=TF, |=Cl, |=Cm .
Властивості пропозиційного рівня:
U) якщо |= та , то |= |= ;
С) , |= , ;
|–) , |= , |= ;
–|) |= , |= , ;
|–) , |= , |= та , |= ;
–|) |= , |= , , ;
|–) (), |= , , |= ;
–|) |= , () |= , та
|= , .
Для |=Cl та |=Cm також маємо:
|– ) , |= |= , ;
–| ) |= , , |= .
Це означає, що для |=Cl та |=Cm мож-
на знімати зовнішнє заперечення, перено-
сячи формулу з лівої частини у праву і на-
впаки. Водночас для |=T , |=F, |=TF власти-
вості |– та –| невірні, адже для |=T , |=F,
|=TF знімати зовнішнє заперечення вже не
можна (див. [2, 9]).
Отже, для |=T , |=F, |=TF, необхідно
виділяти додаткові властивості для випадку
зовнішнього заперечення на реномінацію.
Властивість С гарантує наявність
кожного із логічних наслідків у відповід-
них семантиках. Додатково гарантують на-
явність логічного наслідку властивості:
СL) , , |=
(для неокласичної семантики |= – це |=T
або |=Cl ; для пересиченої – |=F або |=Cm );
СR) |= , ,
(для неокласичної семантики |= – це |=F
або |=Cl ; для пересиченої – |=T або |=Cm );
СLR) , , |=TF , ,
(для неокласичної семантики або для пере-
сиченої семантики).
Для |=Cl та |=Cm властивості СL, СR,
СLR зводяться до С.
Властивості кванторного рівня:
RT|–)
,
, ( ),z v
z xR |= ( ),v
xR |= ;
RT–|) |= , ,
, ( )z v
z xR |= , ( );v
xR
RT|–)
,
, ( )z v
z xR , |= ( )v
xR , |= ;
RT–|) |= , ,
, ( )z v
z xR |= , ( );v
xR
N|–)
,
, ( ),y v
z xR |= ( ),v
xR |= ;
N–|) |= , ,
, ( )y v
z xR |=TF , ( );v
xR
N|–)
,
, ( ),y v
z xR |= ( ),v
xR |= ;
N–|) |= , ,
, ( )y v
z xR |= , ( ).v
xR
Для властивостей N|–, N–|, N|–,
N–| умова: у().
RR|–)
,
, ( ),u x
v yR x |= ( ),u
vR x |= ;
RR–|) |= , ,
, ( )u x
v yR x |= , ( );u
vR x
RR|–)
,
, ( ),u x
v yR x |=
( ),u
vR x |= ;
RR–|) |= , ,
, ( )u x
v yR x
|= , ( );u
vR x
Rp|–) ( ),x
yR x |= х, |= ;
Rp–|) |= , ( )x
yR x |= , х;
Rp|–) ( ),x
yR x |= х, |= ;
Rp–|) |= , ( )x
yR x |= , х;
RR|–) ( ( )),v w
x yR R |= ( ),v w
x yR |= ;
RR–|) |= , ( ( ))v w
x yR R |= , ( );v w
x yR
RR|–) ( ( )),v w
x yR R |=
( ),v w
x yR |= ;
RR–|) |= , ( ( ))v w
x yR R
|= , ( );v w
x yR
R|–) ( ),v
xR |= ( ),v
xR |= ;
R–|) |= , ( )v
xR |= , ( );v
xR
R|–) ( ),v
xR |= ( ),v
xR |= ;
R–|) |= , ( )v
xR |= , ( );v
xR
R|–) ( ),v
xR |=
( ) ( ),v v
x xR R |= ;
R–|) |= , ( )v
xR
|= , ( ) ( );v v
x xR R
R|–) ( ),v
xR |=
( ), ( ),v v
x xR R |= ;
Теоретичні та методологічні основи програмування
26
R–|) |= , ( )v
xR
|= , ( )v
xR та |= , ( ).v
xR
Властивості елімінації кванторів за-
писуємо з використанням символів спеці-
альних предикатів-індикаторів z:
R|–) ( ),u
vR x |= ,
, ( ),u x
v zR |= , z;
|–) х, |= ( ),x
zR |= , z;
R–|) |= , ( )u
vR x
|= , ,
, ( ),u x
v zR z;
–|) |= , х |= , ( ),x
zR z;
Rf–|) |= , ( )u
vR x
|= , ( ),u
vR x ,
, ( ),u x
v zR z;
f–| ) |= , х |= , х, ( ),x
zR z;
Rf|–) ( ),u
vR x |=
( ),u
vR x ,
, ( ),u x
v zR |= , z;
f|–) х, |=
х, ( ),x
zR |= , z.
Для R|–, R–|, Rf–|, Rf|– умови:
zVT та znm(, , ( ))u
vR x ; для |–, –|,
f–|, f|– умови: zVT та znm(, , х)).
Rv–|) |= , ( ),u
vR x y
|= , ( ),u
vR x ,
, ( ),u x
v yR y;
v–|) |= , х, y |= , х, ( ),x
yR y;
Rv|– ) ( ),u
vR x |= , y
( ),u
vR x ,
, ( ),u x
v yR |= , y;
v|–) х, |= , y
х, ( ),x
yR |= , y;
Rd–|) |= , ( )u
vR x
y, |= , ( )u
vR x та
|= , ( ),u
vR x ,
, ( ),u x
v yR y;
d–|) |= , х y, |= , х та
|= , х, ( ),x
yR y;
Rd|–) ( ),u
vR x |=
y, ( ),u
vR x |= та
( ),u
vR x ,
, ( ),u x
v yR |= , y;
d|–) х, |= y, х, |= та
х, ( ),x
yR |= , y.
Для символів y спеціальних преди-
катів-індикаторів можна знімати зовнішнє
заперечення навіть у випадку |=T , |=F, |=TF :
Теорема 3. y, |= |= , y
та |= , y y, |= .
Доведення теореми 3 зводиться до
перевірки наявності усіх відповідних нас-
лідків |=T , |=F, |=TF, що безпосередньо ро-
бимо на основі визначень.
У випадку монотонних (еквітонних)
предикатів маємо наступні властивості:
Теорема 4. Маємо:
1) ,
, ( ), ,u x
v yR y |=T
,
, ( ),u x
v zR та
,
, ( ), ,u x
v yR y |=T
,
, ( ),u x
v zR ;
2) ,
, ( ), ,u x
v zR y |=F
,
, ( ),u x
v yR та
,
, ( ), ,u x
v zR y |=F
,
, ( ),u x
v yR .
Теорема 4 безпосередньо доводить-
ся на основі визначень.
3. Секвенційні числення чистих
першопорядкових логік
Семантичною основою побудови чи-
слень секвенційного типу для ЧКНЛ є вла-
стивості відношень логічного наслідку для
множин формул. Секвенційні числення фо-
рмалізують такі відношення.
Секвенції ми трактуємо як множини
формул, специфікованих (відмічених) спе-
ціальними символами |– та –| , які не входять
до алфавіту мови. Формули секвенції, від-
мічені |–, називають T-формулами, а відмі-
чені –| – F-формулами. Позначаємо секвен-
ції як |––|, або, не деталізуючи, як .
Секвенційне числення будуємо так:
секвенція |––| має виведення |= .
Виведення в секвенційних числен-
нях має вигляд дерева, вершинами якого є
секвенції. Такі дерева – секвенційні.
Аксіомами секвенційного числення
є замкнені секвенції. Замкненість секвенції
|––| означає, що |= .
Секвенційне дерево замкнене, якщо
кожний його лист – замкнена секвенція.
Правилами виведення секвенційних
числень є секвенційні форми. Вони є син-
таксичними аналогами семантичних влас-
тивостей відношення |=.
Секвенція вивідна, якщо існує за-
мкнене секвенційне дерево з коренем .
Залежно від відношення логічного
наслідку та семантики отримуємо різнома-
нітні секвенційні числення. Низку секвен-
Теоретичні та методологічні основи програмування
27
ційних числень для різних класів КНЛ по-
будовано в [4–6]. Такі числення запропо-
новано для загального випадку логік квазі-
арних предикатів, для логік однозначних
еквітонних предикатів (ЕП) та логік тота-
льних антитонних предикатів (АП). Їх по-
будова базується на властивостях Х–Y-оз-
начених відношень логічного наслідку.
Наведемо спектр секвенційних чис-
лень чистих першопорядкових КНЛ квазі-
арних предикатів, збудованих в [4–6]
(табл. 1).
Таблиця 1. Секвенційні числення чистих
першопорядкових КНЛ
|=Cl |=Cm |=T |=F |=TF
Н QCl – QL QR QLR
Е QEqCl – QEqL QEqR QEqLR
П – QCl QR QL QLR
А – QEqCl QEqR QEqL QEqLR
З – – QGS QGS QGS
Тут і далі використано скорочення:
– Н – неокласична семантика;
– Е – неокласична семантика ЕП;
– П – пересичена семантика;
– А – пересичена семантика АП;
– З – загальна семантика.
Числення QCl – це різновидність
числення QG, побудованого в [4]. Числен-
ня QEqCl – це різновидність відомого [2]
неокласичного секвенційного числення.
Спеціальні секвенційні числення
ЧКНЛ. Секвенційні числення, пропоновані
в даній роботі, використовують, на відміну
від [4–6], не Х–Y-означені відношення логі-
чного наслідку, а спеціальні предикати-ін-
дикатори наявності значення для предмет-
них імен. При їх побудові також викорис-
товуємо спеціальні секвенційні форми елі-
мінації кванторів під реномінацією.
Зауважимо, що тут ми будуємо сек-
венційні числення для класів ЧКНЛ, а не
-ЧКНЛ. В наших численнях предикати-ін-
дикатори y є допоміжним інструментом
побудови виведень. Початкова секвенція,
для якої будуємо дерево, не містить спеціа-
льних символів y. Ці символи можуть фі-
гурувати в секвенціях лише в складі специ-
фікованих формул |–y та –|y; такі формули
індукуються формами елімінації кванторів.
Числення QSC формалізує:
– відношення |=Cl (неокласична се-
мантика) для ЧКНЛ однозначних частко-
вих предикатів;
– відношення |=Cm (пересичена се-
мантика) для ЧКНЛ неоднозначних тоталь-
них предикатів.
Числення QMSC ідентичне числен-
ню QEqCl (див. [5, 6]), воно є різновидніс-
тю неокласичного секвенційного числення
[2], по суті відрізняючись лише викорис-
танням форм елімінації кванторів під ре-
номінацією. Числення QMSC формалізує:
– відношення |=Cl (неокласична се-
мантика) для ЧКНЛ однозначних ЕП;
– відношення |=Cm (пересичена сема-
нтика) для ЧКНЛ тотальних АП.
Числення QSL формалізує:
– відношення |=T (неокласична се-
мантика) для ЧКНЛ однозначних частко-
вих предикатів;
– відношення |=F (пересичена семан-
тика) для ЧКНЛ неоднозначних тотальних
предикатів.
Числення QMSL формалізує:
– відношення |=T (неокласична се-
мантика) для ЧКНЛ однозначних ЕП;
– відношення |=F (пересичена се-
мантика) для ЧКНЛ тотальних АП.
Числення QSR формалізує:
– відношення |=F (неокласична се-
мантика) для ЧКНЛ однозначних частко-
вих предикатів;
– відношення |=T (пересичена семан-
тика) для ЧКНЛ неоднозначних тотальних
предикатів.
Числення QMSR формалізує:
– відношення |=F (неокласична се-
мантика) для ЧКНЛ однозначних ЕП;
– відношення |=T (пересичена се-
мантика) для ЧКНЛ тотальних АП.
Числення QSLR формалізує відно-
шення |=TF для ЧКНЛ однозначних частко-
вих предикатів (неокласична семантика) та
неоднозначних тотальних предикатів (пе-
ресичена семантика).
Числення QMSLR формалізує відно-
шення |=TF для ЧКНЛ однозначних ЕП
Теоретичні та методологічні основи програмування
28
(неокласична семантика) та для ЧКНЛ то-
тальних АП (пересичена семантика).
Числення QSG формалізує відно-
шення |=TF для загальної семантики ЧКНЛ
неоднозначних часткових предикатів.
Розглянемо умови замкненості сек-
венції в різних численнях.
Базова умова замкненості |––|:
С) існує формула : та .
Додаткова умова замкненості сек-
венції в усіх численнях – unv-замкненість.
Для секвенції введемо множини
означених та неозначених предметних імен,
або множини val-змінних та unv-змінних:
val() = {xV | –|x};
unv() = {xV | |–x}.
Нехай Un = unv(), нехай R-формула
1 1 1
1 1 1
,... , ,... , ,...
,... , ,... , ,...
k n m
k n m
r r x x u u
s s y y v v
R така:
{r1,…, rk, s,…, sk, y1,…, yn} Un,
{x1,…, xn}Un = , {v1,…, vm}Un = .
Вираз 1 1
1
,... , ,...,
,..., , ,...,
n m
m
x x u u
v v
R
, де позначає
невизначене значення, назвемо Un-unv-
формою формули 1 1 1
1 1 1
,... , ,... , ,...
,... , ,... , ,...
k n m
k n m
r r x x u u
s s y y v v
R .
R-формули та unv-еквівалентні
відносно Un, або Un-unv-еквівалентні, якщо
та мають однакові Un-unv-форми.
Якщо та Un-unv-еквівалентні,
то A(d) = A(d) для кожних моделі мови A
та d
V
A, для яких uA(d) = T для всіх uUn.
Секвенцію |––| із множиною unv-
змінних Un назвемо unv-замкненою, якщо:
UnС) існують Un-unv-еквівалентні
R-формули та такі, що та .
Якщо |––| unv-замкнена, то |= .
Властивості СL, СR, СLR, які істотні
для відношень |=T, |=F, |=TF, індукують до-
даткові умови СL, СR, СLR замкненості
секвенції |––|:
СL) існує формула : та ;
СR) існує формула : та ;
СLR) існують формули та такі:
, , , .
Зрозуміло, що СLR СL та СR.
Для логіки ЕП у неокласичній се-
мантиці та, дуально, для логіки АП у пере-
сиченій семантиці, маємо додаткові умови
замкненості секвенції |––|.
СMT) існують yV та формули ви-
гляду ,
, ( )u x
v yR і ,
, ( )u x
v zR такі, що y та
виконується наступна умова:
( ,
, ( )u x
v yR та ,
, ( )u x
v zR ) або
( ,
, ( )u x
v yR та ,
, ( )u x
v zR ).
СMF) існують yV та формули ви-
гляду ,
, ( )u x
v yR і ,
, ( )u x
v zR такі, що y та
виконується наступна умова:
( ,
, ( )u x
v zR та ,
, ( )u x
v yR ) або
( ,
, ( )u x
v zR та ,
, ( )u x
v yR ).
Згідно теорем 2 та 4, умова СMT га-
рантує наявність |=T для логіки ЕП у
неокласичній семантиці та |=F для логі
ки АП у пересиченій семантиці; умова
СMF гарантує наявність |=F для логіки
ЕП у неокласичній семантиці та |=T для
логіки АП у пересиченій семантиці; умова
СMT & СMF гарантує наявність |=TF
для логіки ЕП у неокласичній семантиці та
для логіки АП у пересиченій семантиці.
Підсумовуючи, наведемо умови за-
мкненості секвенції в різних численнях.
Числення QSC: умова C UnС;
числення QMSC: умова C.
Числення QSL: C CL UnС;
числення QMSL: C CL UnС СMT.
Числення QSR: C CR UnС;
числення QMSR: C CR UnС СMF.
Числення QSLR: C CLR UnС;
QMSLR: C CLR UnС СMT & СMF.
Числення QSG: умова C UnС.
Базовими секвенційними формами
числень QSL, QMSL, QSR, QMSR, QSLR,
QMSLR, QSG є наступні:
|–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
; –|N
|
,
| ,
( ),
( ),
v
u
y v
z u
R A
R A
;
|–N
|
,
| ,
( ),
( ),
v
u
y v
z u
R A
R A
; –|N
|
,
| ,
( ),
( ),
v
u
y v
z u
R A
R A
.
Для форм типу N та N у(A).
Теоретичні та методологічні основи програмування
29
|–RR
|
,
| ,
( ),
( ),
u
v
u x
v y
R xA
R xA
; –|RR
|
,
| ,
( ),
( ),
u
v
u x
v y
R xA
R xA
;
|–RR
|
,
| ,
( ),
( ),
u
v
u x
v y
R xA
R xA
;
–|RR
|
,
| ,
( ),
( ),
u
v
u x
v y
R xA
R xA
;
|–Rp
|
|
,
( ),x
y
xA
R xA
; –|Rp
|
|
,
( ),x
y
xA
R xA
;
|–Rp
|
|
,
( ),
x
y
xA
R xA
; –|Rp
|
|
,
( ),
x
y
xA
R xA
;
|
|
|
,
,
A
A
; |
|
|
,
,
A
A
;
|
| |
|
, ,
,
A B
A B
; |
| |
|
, ,
,
A B
A B
;
|
| |
|
, ,
( ),
A B
A B
;
|
| |
|
, ,
( ),
A B
A B
;
|–RR
|
|
( ),
( ( )),
v w
x y
v w
x y
R A
R R A
; –|RR
|
|
( ),
( ( )),
v w
x y
v w
x y
R A
R R A
;
|–RR
|
|
( ),
( ( )),
v w
x y
v w
x y
R A
R R A
;
–|RR
|
|
( ),
( ( )),
v w
x y
v w
x y
R A
R 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
; –|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
;
|–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, на відміну від
однойменних форм в роботах [2, 4–8], тут
фактично поєднані з формами | та |.
Зауважимо, що подібну будову мають та-
кож форми |–R, –|R, |–R, –|R.
Наведемо форми елімінації кванто-
рів; ці форми використовують символи z:
|–
| |
|
( ), ,
,
x
zR A z
xA
;
–|
| |
|
( ), ,
,
x
zR A z
xA
;
|–R
,
| , |
|
( ), ,
( ),
u x
v z
u
v
R A z
R xA
;
–|R
,
| , |
|
( ), ,
( ),
u x
v z
u
v
R A z
R xA
;
–|f
| | |
|
, ( ), ,
,
x
zxA R A z
xA
;
|–f
| | |
|
, ( ), ,
,
x
zxA R A z
xA
;
–|Rf
,
| | , |
|
( ), ( ), ,
( ),
u u x
v v z
u
v
R xA R A z
R xA
;
|–Rf
,
| | , |
|
( ), ( ), ,
( ),
u u x
v v z
u
v
R xA R A z
R xA
.
Для форм |–, –|, –|f, |–f умо-
ва: zVT, znm(, xА). Для |–R, –|R,
–|Rf, |–Rf умова: znm(, ( ))u
vR xA , zVT.
Для –|f, |–f, –|Rf, |–Rf додаткова
умова: не містить формул вигляду –|z.
–|v
| | |
| |
, ( ), ,
, ,
x
yxA R A y
xA y
;
|–v
| | |
| |
, ( ), ,
, ,
x
yxA R A y
xA y
;
–|Rv
,
| | , |
| |
( ), ( ), ,
( ), ,
u u x
v v y
u
v
R xA R A y
R xA y
;
|–Rv
,
| | , |
| |
( ), ( ), ,
( ), ,
u u x
v v y
u
v
R xA R A y
R xA y
.
Форми –|f, |–f, –|Rf, |–Rf – це
форми типу f; –|v, |–v, –|Rv, |–Rv –
це форми типу v.
2-засновкові форми –|d та |–d:
Теоретичні та методологічні основи програмування
30
| | | | |
|
, , , ( ), ,
,
x
yy xA xA R A y
xA
;
| | | | |
|
, , , ( ), ,
.
,
x
yy xA xA R A y
xA
2-засновкові форми –|Rd та |–Rd:
,
| | | | , |
|
, ( ), ( ), ( ), ,
;
( ),
u u u x
v v v y
u
v
y R xA R xA R A y
R xA
,
| | | | , |
|
ε , ( ),Σ ( ), ( ), ε ,Σ
.
( ),Σ
u u u x
v v v y
u
v
y R xA R xA R A y
R xA
–|d, |–d, –|Rd, |–Rd – це форми
типу d. Для цих форм умова: y не вхо-
дить до та містить символи вигляду z.
Форми |–R, –|R, |–, –| на-
звемо T-формами, а форми типів f, v, d
назвемо F-формами.
Форми типів RT, RT, N, N,
RR, RR, Rp Rp – допоміжні, інші
базові секвенційні форми – основні.
Базовими секвенційними формами
числення QSC є |–RT, –|RT, |–N, |–N,
|–RR, –|RR, |–Rp, –|Rp, | , | , |, |,
|–RR, –|RR, |–R, –|R, |–R, –|R, |–, |–R,
–|f, –|Rf, –|v, –|Rv, –|d, –|Rd.
Для |=Cl та |=Cm можна знімати запе-
речення, переносячи формулу з лівої части-
ни наслідку в праву і навпаки, тому в чис-
ленні QSC форми для зовнішнього запере-
чення не потрібні. Форми | та | такі:
|
|
|
,
,
A
A
; |
|
|
,
,
A
A
.
Базовими секвенційними формами
числення QMSC є |–RT, –|RT, |–N, |–N,
|–RR, –|RR, |–Rp,–|Rp, | , | , |, |,
|–RR, –|RR, |–R, –|R, |–R, –|R, а також фор-
ми елімінації кванторів |–, |–R, –|, –|R.
Традиційні форми елімінації кванто-
рів |–, –| та форми |–R, –|R не використо-
вують символи z предикатів-індикаторів:
|–
|
|
( ),
,
x
zR A
xA
; |–R
,
| ,
|
( ),
( ),
u x
v z
u
v
R A
R xA
;
–|
| |
|
, ( ),
,
x
yxA R A
xA
;
–|R
,
| | ,
|
( ), ( ),
( ),
u u x
v v y
u
v
R xA R A
R xA
.
Нехай
| |
| |
та
| | | |
| |
–
базові секвенційні форми. На основі влас-
тивостей відношень |= тоді маємо:
Теорема 5. 1) |= |= ;
|= та |= |= ;
2) | | ;
| | або | .
Побудова секвенційного дерева.
Процедура побудови секвенційного дерева
розбита на етапи, вона починається з коре-
ня дерева. Кожне застосування секвенцій-
ної форми проводиться до скінченної мно-
жини доступних на даний момент формул.
Перед побудовою дерева зафіксуємо де-
який нескінченний список TN тотально не-
істотних імен такий, що nm()TN = . На
початку кожного етапу виконується крок
доступу. Це означає, що до списку доступ-
них формул додаємо по одній формулі зі
списків T-формул та F-формул. На початку
побудови доступна лише пара перших фо-
рмул списків (єдина T-формула чи F-фор-
мула, якщо один зі списків порожній).
Якщо всі листи замкнені, то проце-
дура завершена позитивно, отримано замк-
нене секвенційне дерево. Якщо ні, то у ви-
падку виведення скінченної секвенції пе-
ревіряємо, чи буде хоч один із листів фі-
нальною секвенцією. Незамкнена верши-
на-секвенція – фінальна, якщо до неї не-
застосовна жодна форма, або кожне засто-
сування форми до не вводить нових фо-
рмул (відмінних від формул секвенцій на
шляху від кореня до ).
Якщо процедура не завершена, то
для кожного незамкненого листа робимо
наступний крок доступу, після чого добу-
довуємо скінченне піддерево з вершиною
таким чином. Активізуємо всі доступні
(окрім примітивних) формули . Далі до
кожної активної формули застосовуємо
відповідну основну форму (як описано
нижче). За потреби застосовуємо належну
кількість разів допоміжні форми типів RT,
RT, N, N, RR, RR, Rp, Rp.
Після застосування основної форми утво-
рені нею формули на даному етапі пасивні.
До таких формул на даному етапі основні
форми вже не застосовуються.
Спочатку виконуємо (за можливос-
Теоретичні та методологічні основи програмування
31
ті) всі T-форми. При кожному застосуванні
такої форми беремо зі списку TN нове то-
тально неістотне ім'я z як перше незадіяне
на даному шляху від кореня до даної вер-
шини. Потім застосовуємо форми типу RR,
RR, R, R, R, R, , , . Далі
застосовуємо F-форми. Це робимо так.
Якщо в момент застосування F-фор-
ми до певної F-формули секвенції ма-
ємо val() = , то застосовуємо відповідну
форму типу f; якщо ж val() , то засто-
совуємо відповідну форму типу v, що ро-
бимо для кожного zval(). Нехай після та-
кого застосування форми типу f чи форм
типу v отримана секвенція . Далі до цієї
багатократно застосовуємо відповідну 2-
засновкову форму типу d, добудовуючи
скінченне піддерево з вершиною . Це ро-
бимо для всіх уnm(0) \ (val() unv()),
де 0 – множина доступних на даний мо-
мент формул секвенції . Зауважимо, що
val() = val(0) та unv() = unv(0), адже
специфіковані формули вигляду |–x та –|x
індукуються формами елімінації кванторів,
тому вони не можуть бути серед недоступ-
них формул секвенції.
Після виконання кожної форми пе-
ревіряємо на замкненість секвенції-верши-
ни. При появі замкненої секвенції до неї
незастосовна жодна форма, процес побудо-
ви дерева на цьому шляху обривається.
Повтори формул у секвенціях усуваємо.
Якщо процедура побудови дерева
для секвенції завершена позитивно, то
отримано скінченне замкнене дерево.
Якщо процедура завершена негати-
вно (маємо скінченне незамкнене дерево)
або процедура не завершується (маємо не-
скінченне дерево), то у дереві існує незам-
кнений шлях , всі його вершини – неза-
мкнені секвенції. Кожна з формул секвен-
ції зустрінеться на і стане доступною.
3. Теореми коректності та повноти
Для побудованих секвенційних чи-
слень справджується:
Теорема 6 (коректності). 1) |––| ви-
відна в QSC-численні |=Cl в неокла-
сичній семантиці та |=Cm в пересиченій;
2) |––| вивідна в QMSC-численні
|=Cl в неокласичній семантиці логіки
ЕП та |=Cm в пересиченій семантиці ло-
гіки АП;
3) |––| вивідна в QSL-численні
|=T в неокласичній семантиці та |=F
в пересиченій;
4) |––| вивідна в QMSL-численні
|=T в неокласичній семантиці логіки
ЕП та |=F в пересиченій семантиці ло-
гіки АП;
5) |––| вивідна в QSR-численні
|=F в неокласичній семантиці та |=T
в пересиченій;
6) |––| вивідна в QMSR-численні
|=F в неокласичній семантиці логіки
ЕП та |=T в пересиченій семантиці ло-
гіки АП;
7) |––| вивідна в QSLR-численні
|=TF в неокласичній семантиці та в пе-
ресиченій семантиці;
8) |––| вивідна в QMSLR-численні
|=TF в неокласичній семантиці логіки
ЕП та в пересиченій семантиці логіки АП;
9) |––| вивідна в QSG-численні
|=TF в загальній семантиці.
Доведення. Нехай |––| вивідна, то-
ді для неї побудоване замкнене секвенцій-
не дерево. Із процедури побудови випли-
ває, що |= для кожної його вершини
|––|. Для листів дерева це випливає з їх
замкненості. Збереження секвенційними
формами відповідних відношень |=Cl, |=Cm,
|=T, |=F, |=TF (від засновків до висновків)
випливає із теореми 5.
Повнота побудованих секвенційних
числень випливає із відповідних теорем
про існування контрмоделі для множини
формул незамкненого шляху секвенційно-
го дерева. Доведення цих теорем опира-
ється на метод модельних множин [9, 2].
Числення QSG. Сформулюємо тео-
рему про контрмоделі для числення QSG.
Теорема 7. Нехай – незамкнений
шлях у секвенційному дереві, збудованому
для секвенції |––|, нехай Н – множина
всіх специфікованих формул секвенцій
цього шляху. Тоді існують моделі мови
A = (A, I), B = (A, I) та ,
V
A такі:
1) |–Н T(A) та –|Н T(A);
2) |–Н F(B) та –|Н F(B).
Теоретичні та методологічні основи програмування
32
Пари (A, ) та (B, ) із такими влас-
тивостями називатимемо T-контрмоделлю
та F-контрмоделлю для секвенції |––|.
Множини W = {ynm(Н) | –|yН} та
Un = {ynm(Н) | |–yН} назвемо відповід-
но множиною означених імен та множи-
ною неозначених імен множини Н.
Доведення. Застосування секвенцій-
них форм до секвенцій шляху відбува-
ється до тих пір, поки це можливо, тому
кожна непримітивна формула чи її запере-
чення, що зустрічається на шляху , рано
чи пізно буде розкладена чи спрощена.
Усі секвенції шляху незамкнені,
тому для них не виконується умова зам-
кненості C UnС. Отже, для множини Н
виконуються такі умови коректності:
НС) не існує примітивної формули
такої, що |–Н та –|Н;
НСU) не існує примітивних Un-unv-
еквівалентних формул v
xR A та u
yR A таких,
що |
v
xR A Н та |
u
yR A Н.
Переходи від нижчої вершини шля-
ху до вищої відбуваються згідно з від-
повідною секвенційною формою, тому для
Н виконуються такі умови переходу:
Н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) ,
| , ( )u x
v yR x Н
| ( )u
vR x Н;
,
| , ( )u x
v yR x Н | ( )u
vR x Н;
НRR) ,
| , ( )u x
v yR x Н
| ( )u
vR x Н;
,
| , ( )u x
v yR x Н | ( )u
vR x Н;
НRp) | ( )x
yR x Н |–хН;
| ( )x
yR x Н –|хН;
НRp) | ( )x
yR x Н
|–хН;
| ( )x
yR x Н –|хН;
Н) |–Н |–Н;
–|Н –|Н;
Н) |–Н |–Н або |–Н;
–|Н –|Н та –|Н;
Н) |–()Н
|–Н та |–Н;
–|()Н –|Н або –|Н;
НRR) | ( ( ))v w
x yR R Н
| ( )v w
x yR Н;
| ( ( ))v w
x yR R Н | ( )v w
x yR Н;
НRR) | ( ( ))v w
x yR R Н
| ( )v w
x yR Н;
| ( ( ))v w
x yR R Н | ( )v w
x yR Н;
Н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 Н;
Н) |–хН існує уW таке, що
| ( )x
yR Н;
–|хН | ( )x
yR Н для всіх уW;
Н) |–хН | ( )x
yR Н
для всіх уW;
–|хН існує уW таке, що
Теоретичні та методологічні основи програмування
33
| ( )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 Н для всіх уW;
| ( )u
vR x Н існує уW таке, що
,
| , ( )u x
v yR Н.
Виконання для Н умов переходу
очевидне майже для всіх цих умов. Дове-
демо для прикладу Н та НR.
Н). Нехай |–()Н, тоді на
деякому кроці виведення на шляху до
T-формули () була застосована |–-
форма, яка дала T-формули та , зві-
дки отримуємо |–Н та |–Н. Нехай
–|()Н, тоді на деякому кроці виве-
дення на шляху до F-формули ()
була застосована –|-форма, яка дала F-
формулу або F-формулу , звідки
–|Н або –|Н.
НR). Нехай | ( )u
vR x Н, тоді на
деякому кроці виведення на шляху до
T-формули ( )u
vR x була застосована
|–R-форма, яка дала приклад – T-формулу
( )u
vR x . Тоді ,
| , ( )u x
v yR Н та –|yН, то-
му уW. Отже, для деякого уW маємо
,
| , ( )u x
v yR Н. Нехай | ( )u
vR x Н; тоді
при кожній активізації цієї F-формули до
відповідної вершини-секвенції додають-
ся, згідно відповідної F-форми, її приклади
– F-формули
,
, ( )u x
v yR – для кожного у та-
кого, що –|y0, де 0 – множина доступ-
них формул . Отже, якщо | ( )u
vR x Н
то ,
| , ( )u x
v yR Н для всіх уW.
Mножинy специфікованих формул
Н, для якої виконуються вищенаведені
умови, назвемо G-модельною.
Перейдемо до побудови контрмоде-
лі за G-модельною множиною Н.
Візьмемо деяку множину А таку, що
|А| = |W|, та деякі ін’єктивні ,
V
A з
asn() = W. Така А дублює множину W.
Задамо значення базових предика-
тів та їх заперечень на і та на іменних
множинах вигляду r v
x () і r v
x ():
– |–yН T(yА) та F(yB);
– –|yН T(yА) та F(yB);
– |– рН T(рA) та F(рB);
– –| рН T(рA) та F(рB);
– |–рН T(pA) та F(pB);
– –|pН T(pA) та F(pB);
– | ( )v
xR p Н r v
x ()T(рA) та r v
x ()F(рB);
– | ( )v
xR p Н r v
x ()T(рA) та r v
x ()F(рB);
– | ( )v
xR p Н r v
x ()T(pA) та
r v
x ()F(pB);
– | ( )v
xR p Н r v
x ()T(pA) та
r v
x ()F(pB).
В усіх інших випадках значення ба-
зових предикатів і їх заперечень задаємо
довільно, враховуючи обмеження щодо не-
істотності предметних імен: для всіх d, h
V
A
таких, що d║-(p) = h║-(p), маємо
рA(d) = рA(h), рA(d) = рA(h), рB(d) = рB(h),
рB(d) = рB(h). Це гарантує, що всі у(p)
строго неістотні для рА та pB.
Для атомарних формул і формул
вигляду ( )v
xR p та їх заперечень тверджен-
ня теореми випливає з визначення базових
предикатів. Далі доводимо (див. [5, 6]) тра-
диційно: індукцією за складністю формули
згідно з пунктами визначення множини Н.
Наведемо як приклад доведення для
пунктів НR та НR визначення Н
Нехай |– ( )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 v
x x AR R T( ( )v
x AR ). За
припущенням індукції для тепер маємо
F ( ( ) )v
x BR або F ( ( ) )v
x BR , звідки
отримуємо F ( ( ) )v
x BR F ( ( ) )v
x BR =
= F ( ( ) ( ) ) v v
x x BR R F( ( )v
x BR ).
Нехай –| ( )v
xR Н. Згідно НR
маємо | ( )v
xR Н та | ( )v
xR Н. За при-
Теоретичні та методологічні основи програмування
34
пущенням індукції для тоді маємо
T ( ( ) )v
x AR ) та T ( ( ) )v
x AR ), звідки
отримуємо T ( ( ) )v
x AR T ( ( ) )v
x AR =
= T ( ( ) ( ) )v v
x x AR R T( ( )v
x AR ). За
припущенням індукції для тепер маємо
F ( ( ) )v
x BR ) та F ( ( ) )v
x BR ), звідки
отримуємо F ( ( ) ) v
x BR F ( ( ) )v
x BR =
= F ( ( ) ( ) ) v v
x x BR R F( ( )v
x BR ).
Нехай | ( )u
vR x Н. Згідно НR
існує уW: ,
| , ( )u x
v yR Н. За припущенням
індукції для маємо T
,
,( ( )u x
v y AR ). Звід-
си ( ) ( )u v x y T(A). Однак
(у) згідно з
W
А та уW, звідки для
а = (у) маємо ( )u v x a T(A)
тому T ( ( )u
v AR x ). Тепер за припущен-
ням індукції для маємо F
,
,( ( )u x
v y BR ).
Звідси ( ) ( )u v x y F(B). Од-
нак (у) згідно з
W
А та уW, тому для
а = (у) маємо ( )u v x a F(B),
звідки F ( ( )u
v BR x ).
Нехай | ( )u
vR x Н. Згідно НR
для всіх уW маємо ,
| , ( )u x
v yR Н. За при-
пущенням індукції для тоді для всіх уW
маємо T
,
,( ( )u x
v y AR ). Звідси для всіх уW
маємо ( ) ( )u v x y T(A). Згід-
но з А
W
маємо (у) для всіх уW. Поза-
як є бієкцією WА, то кожне bА має
вигляд b = (у) для деякого уW. Отже,
( )u v x b T(A) для всіх bА,
звідки T ( ( )u
v AR x ). Тепер за припу-
щенням індукції для для всіх уW маємо
F
,
,( ( )u x
v y BR . Звідси для всіх уW маємо
( ) ( )u v x y F(B). Згідно з
А
W
маємо (у) для всіх уW. Позаяк
є бієкцією WА, то кожне bА має вигляд
b = (у) для деякого уW. Отже, для всіх
bА маємо ( )u v x b F(B),
звідки F ( ( )u
v BR x ).
Числення QSL, QSR, QSLR, QMSL,
QMSR, QMSLR. Для цих числень теорема
про контрмоделі формулюється аналогіч-
но. Відмінність полягає у різних умовах
коректності модельної множини, а для чи-
слень QMSL, QMSR, QMSLR при заданні
значення базових предикатів та їх запере-
чень ураховуємо еквітонність.
Із умов СL, СR, СLR замкненості
секвенції отримуємо відповідні умови ко-
ректності для модельних множин:
НСL) не існує примітивної формули
такої, що |–Н та |–Н;
НСR) не існує примітивної формули
такої, що –|Н та –|Н;
НСLR) не існує примітивних фор-
мул та таких, що виконуються наступні
умови: |–Н, |–Н, –|Н, –|Н.
Зрозуміло, що НСLR НСL НСR.
Для числень логік ЕП у неокласич-
ній семантиці та логік АП у пересиченій
семантиці маємо додаткові умови корект-
ності модельних множин (випливають із
умов СMT і СMF замкненості секвенції):
НСMT) не існує примітивних фор-
мул ,
, ( )u x
v yR і ,
, ( )u x
v zR таких, що yUn та
виконується умова:
( ,
| , ( )u x
v yR Н та ,
| , ( )u x
v zR Н) або
( ,
| , ( )u x
v yR Н та ,
| , ( )u x
v zR Н).
НСMF) не існує примітивних фор-
мул ,
, ( )u x
v yR і ,
, ( )u x
v zR таких, що yUn та
виконується умова:
( ,
| , ( )u x
v zR Н та ,
| , ( )u x
v yR Н) або
( ,
| , ( )u x
v zR Н та ,
| , ( )u x
v yR Н).
Таким чином, приходимо до наступ-
них визначень.
Mножина специфікованих формул
Н, для якої виконуються умови переходу
G-модельної множини:
– L-модельна, якщо для Н викону-
ються умови коректності НС, НСL, НСU;
– R-модельна, якщо для Н викону-
ються умови коректності НС, НСR, НСU;
– LR-модельна, якщо для Н викону-
ються умови коректності НС, НСLR, НСU;
– ML-модельна, якщо для Н вико-
нуються умови НС, НСL, НСU, НСMT;
– MR-модельна, якщо для Н вико-
нуються умови НС, НСR, НСU, НСMF;
– MLR-модельна, якщо для Н вико-
нуються умови коректності НС, НСLR,
НСU, НСMT НСMF.
Теоретичні та методологічні основи програмування
35
Доведення теореми про контрмоде-
лі для числень QSL, QSR, QSLR, QMSL,
QMSR, QMSLR аналогічне доведенню цієї
теореми для числень QSG.
Зауважимо, що для T-контрмоделі
невиконання умови НСL, тобто наявність
формули такої, що |–Н та |–Н, дає
T(A) та T(A) = F(A), звідки має-
мо неоднозначність A . Для F-контрмо-
делі невиконання умови НСR, тобто на-
явність такої, що –|Н та –|Н, дає
F(B) та F(B) = T(B), звідки ма-
ємо неоднозначність B .
Числення QSС. Сформулюємо тео-
рему про контрмоделі для числення QSС.
Теорема 8. Нехай – незамкнений
шлях у секвенційному дереві, збудованому
для секвенції |––|, нехай Н – множина
всіх специфікованих формул секвенцій
цього шляху. Тоді існують моделі мови
A = (A, I), B = (A, I) та ,
V
A такі:
1) |–Н T(A) та –|Н F(A);
2) |–Н F(B) та –|Н T(B).
Пари (A, ) та (B, ) із такими влас-
тивостями назвемо Cl-контрмоделлю та
Cm-контрмоделлю для секвенції |––|.
Доведення. Вводимо множини озна-
чених імен W = {ynm(Н) | –|yН} та не-
означених імен Un = {ynm(Н) | |–yН}.
Усі секвенції шляху незамкнені,
тому для них не виконується умова зам-
кненості C UnС. Застосування форм до
секвенцій шляху відбувається до тих
пір, поки це можливо, тому кожна непри-
мітивна формула на шляху буде розкла-
дена чи спрощена згідно з відповідною
секвенційною формою числення QSС.
Отже, для множини Н виконуються
умови коректності НС і НСU та умови пе-
реходу Н, Н, НRT, НN, НRR, НRp,
НRR, НR, НR, Н, НR. Тут умова Н:
Н) |–Н –|Н;
–|Н |–Н.
Множину Н із такими властивостя-
ми назвемо C-модельною.
Доведення теореми 8 аналогічне до-
веденню теореми 7. Спочатку задаємо зна-
чення базових предикатів на і та на
іменних множинах вигляду r v
x () і r v
x ():
– |–yН T(yА) та F(yB);
– –|yН T(yА) та F(yB);
– |– рН T(рA) та F(рB);
– –| рН F(рA) та T(рB);
– | ( )v
xR p Н r v
x ()T(рA) та r v
x ()F(рB);
– | ( )v
xR p Н r v
x ()F(рA) та r v
x ()T(рB).
В усіх інших випадках значення ба-
зових предикатів задаємо довільно, врахо-
вуючи обмеження щодо неістотності імен:
рA(d) = рA(h) і рB(d) = рB(h) для всіх d, h
V
A
таких, що d║-(p) = h║-(p). Це гарантує,
що всі у(p) строго неістотні для рА та pB.
Для атомарних формул і формул
вигляду ( )v
xR p твердження теореми ви-
пливає з визначення базових предикатів.
Далі доводимо індукцією за склад-
ністю формули згідно з пунктами визна-
чення C-модельної множини. Наведемо для
прикладу доведення для пп. НRR та Н.
Нехай ,
| , ( )u x
v yR x Н. Згідно НRR
| ( )u
vR x Н; За припущенням індукції
для тоді T ( ( ) )u
v AR x = T
,
,( ( ) )u x
v y AR x .
За припущенням індукції для отримуємо
F ( ( ) )u
v BR x = F
,
,( ( ) )u x
v y BR x .
Нехай ,
| , ( )u x
v yR x Н. Згідно НRR
| ( )u
vR x Н. За припущенням індукції
для тоді F ( ( ) )u
v AR x = F
,
,( ( ) )u x
v y AR x .
За припущенням індукції для отримуємо
T ( ( ) )u
v BR x = T
,
,( ( ) )u x
v y BR x .
Нехай |–Н. Згідно Н маємо
–|Н. За припущенням індукції для ма-
ємо F(A) = T(A). За припущенням
індукції для маємо T(B) = F(B).
Нехай –|Н. Згідно Н маємо
|–Н. За припущенням індукції для ма-
ємо T(A) = F(A). За припущенням
індукції для маємо F(B) = T(B).
Повнота першопорядкових числень
логіки ЕП, різновидністю яких є числення
QMSC, доведена в [2]. Для цих числень те-
орему про контрмоделі тут не розглядаємо.
Теореми повноти. Для різних чис-
лень та логічних наслідків ці теореми фор-
мулюються однотипно. Вони доводяться
на основі теорем про контрмоделі.
Теоретичні та методологічні основи програмування
36
Теорема 9. 1) |=Cl в неокласичній
семантиці |––| вивідна в численні QSC;
2) |=Cm в пересиченій семантиці
|––| вивідна в численні QSC.
Доводимо п.1. Припустимо супро-
тивне: |=Cl та |––| невивідна. Тоді в сек-
венційному дереві для |––| існує незамкне-
ний шлях. Множина Н усіх специфікова-
них формул секвенцій цього шляху – C-
модельна. Зрозуміло, що |––| Н. За тео-
ремою 8 існує Cl-контрмодель (A, ) така:
|–Н T(A) та –|Н F(A).
Згідно з |––| Н маємо T(A) для всіх
та F(ΨA) для всіх Ψ. Звідси
T(A)F(A). Отже, T(A)F(A) .
Це заперечує |=Cl .
Доводимо п.2. Припустимо супроти-
вне: |=Cm та |––| невивідна. Міркуючи,
як в доведенні п.1, маємо C-модельну Н. Зa
теоремою 8 існує Cm-контрмодель (B, ):
|–Н F(B) та –|Н T(B).
Згідно з |––| Н для всіх маємо
F(B), для всіх Ψ маємо T(ΨB).
Звідси F(B)T(B), тому отримуємо
F(B)T(B)
V
A. Це заперечує |=Cm .
Теорема 10. 1) |=T в неокласичній
семантиці |––| вивідна в численні QSL;
2) |=F в пересиченій семантиці
|––| вивідна в численні QSL.
3) |=F в неокласичній семантиці
|––| вивідна в численні QSR;
4) |=T в пересиченій семантиці
|––| вивідна в численні QSR.
5) |=TF в неокласичній семантиці
чи |=TF в пересиченій семантиці
|––| вивідна в численні QSLR.
Наведемо доведення п. 5. Пп. 1–4 до-
водяться аналогічно (див. також [5, 6]).
Припустимо супротивне: |=TF та
|––| невивідна. Тоді в секвенційному де-
реві для |––| існує незамкнений шлях.
Множина Н усіх специфікованих формул
секвенцій цього шляху – LR-модельна,
|––| Н. За теоремою 7 існують T-контр-
модель (A, ) і F-контрмодель (B, ):
|–Н T(A) та –|Н T(A);
|–Н F(B) та –|Н F(B).
Якщо за умови НСLR невірна НСL
(тоді маємо НСR), то для T-контрмоделі
отримуємо неоднозначний предикат, а для
F-контрмоделі – нетотальний предикат; то-
му для логіки однозначних предикатів бе-
ремо F-контрмодель, а для логіки тоталь-
них предикатів – T-контрмодель.
Якщо за умови НСLR невірна НСR
(тоді маємо НСL), то для F-контрмоделі
отримуємо неоднозначний предикат, а для
T-контрмоделі – нетотальний предикат; то-
му для логіки однозначних предикатів бе-
ремо T-контрмодель, а для логіки тоталь-
них предикатів – F-контрмодель.
Якщо вірні НСL i НСR, то можна бра-
ти як T-контрмодель, так і F-контрмодель.
Для 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|=F та |=TF .
Подібним чином доводиться
Теорема 11. 1) |=T в неокласич-
ній семантиці логіки ЕП |––| вивідна в
численні QMSL;
2) |=F в пересиченій семантиці ло-
гіки АП |––| вивідна в численні QMSL;
3) |=F в неокласичній семантиці
логіки ЕП |––| вивідна в численні QMSR;
4) |=T в пересиченій семантиці ло-
гіки АП |––| вивідна в численні QMSR;
5) |=TF в неокласичній семантиці
логіки ЕП чи |=TF в пересиченій се-
мантиці логіки АП |––| вивідна в чис-
ленні QMSLR.
Теорема 12. |=TF в загальній се-
мантиці |––| вивідна в численні QSG.
Доведення. Нехай маємо супротивне:
|=TF та |––| невивідна. Тоді в дереві для
|––| існує незамкнений шлях. Множина Н
усіх специфікованих формул секвенцій
цього шляху – G-модельна, причому маємо
|––| Н. За теоремою 7 існують T-контр-
модель (A, ) та F-контрмодель (B, ) такі:
|–Н T(A) та –|Н T(A);
|–Н F(B) та –|Н F(B).
Теоретичні та методологічні основи програмування
37
Тут можна брати як T-контрмодель,
так і F-контрмодель.
Далі доводимо як в п. 5 теореми 10.
Підсумовуючи, наведемо спектр по-
будованих секвенційних числень чистих
першопорядкових КНЛ (табл. 2). Для по-
значення семантик тут використано скоро-
чення із табл. 1.
Таблиця 2. Спеціальні секвенційні числення
чистих першопорядкових КНЛ
|=Cl |=Cm |=T |=F |=TF
Н QSC – QSL QSR QSLR
Е QMSC – QMSL QMSR QMSLR
П – QSC QSR QSL QSLR
А – QMSC QMSR QMSL QMSLR
З – – QSG QSG QSG
Використовуючи табл. 2, поєднаємо
теореми коректності та повноти:
Теорема 13. Для семантики маємо:
|= |––| вивідна в численні .
Тут – одне з T, F, TF, Cl, Cm; –
одна з семантик, скорочене позначення якої
є іменем рядка таблиці. Назву числення
читаємо на перетині стовпця |= та рядка .
Висновки
В роботі досліджено чисті першо-
порядкові композиційно-номінативні логі-
ки часткових однозначних, тотальних не-
однозначних та часткових неоднозначних
квазіарних предикатів. На основі різних
формалізацій відношення логічного нас-
лідку для цих логік побудовано спектр чи-
слень секвенційного типу. Низка таких чи-
слень була раніше збудована на базі Х–Y-
означених відношень логічного наслідку.
В даній роботі при побудові чис-
лень використано спеціальні предикати-ін-
дикатори наявності значення для змінних.
Такі числення запропоновано як для зага-
льного випадку квазіарних предикатів, так
і для логік еквітонних та логік антитонних
предикатів. Для пропонованих числень до-
ведено теореми коректності й повноти.
Побудову подібних числень секвен-
ційного типу планується продовжити для
логік кванторно-екваційного рівня.
1. Handbook of Logic in Computer Science. Ed-
ited by S. Abramsky, Dov M. Gabbay and
T. S. E. Maibaum. – Oxford Univ. Press. –
Vol. 1–5, 1993–2000.
2. Нікітченко М.С., Шкільняк С.С. Математи-
чна логіка та теорія алгоритмів. – К., 2008. –
528 с.
3. Шкільняк С.С. Відношення логічного нас-
лідку в композиційно-номінативних логі-
ках // Проблеми програмування. – 2010. –
№ 1. – C. 15–38.
4. Шкильняк С.С. Логики квазиарных преди-
катов первого порядка // Кибернетика и сис-
темный анализ. – 2010. – № 6. – С. 32–49.
5. Шкільняк С.С. Секвенційні числення пер-
шопорядrових логік однозначних квазіар-
них предикатів // Проблеми програмування.
– 2012. – № 1. – C. 34–51.
6. Шкільняк С.С. Секвенційні числення ком-
позиційно-номінативних логік квазіарних
предикатів // Проблеми програмування. –
2012. – № 2–3. – C. 33–43.
7. Шкільняк С.С. Спеціальні секвенційні чис-
лення логік однозначних квазіарних преди-
катів // Вісник Київського ун-ту. Серія: фіз.-
мат. науки. – 2012. – Вип. 3. – С. 287–292.
8. Нікітченко М.С., Шкільняк С.С. Спеціаль-
ні секвенційні числення чистих компози-
ційно-номінативних логік першого поряд-
ку // Вісник Київського ун-ту. Серія: кібе-
рнетика. – К., 2012. – Вип. 12. – C. 38–45.
9. Смирнова Е.Д. Логика и философия – М.,
1996. – 304 с.
10. Nikitchenko M., Tymofieiev V. Satisfability and
Validity Problems in Many-sorted Composi-
tion-Nominative Pure Predicate Logics //
Comm. in Comp. and Inf. Science. – V. 347. –
P. 89–110. – Springer, 2012.
Одержано 24.10.2012
Про автора:
Шкільняк Степан Степанович,
доктор фізико-математичних наук,
професор кафедри теорії та технології
програмування.
Місце роботи автора:
Київський національний університет
імені Тараса Шевченка,
01601, Київ, вул. Володимирська, 60.
Тел.: (044) 259 0519,
(044) 522 0640 (д).
E-mail: sssh@unicyb.kiev.ua
mailto:sssh@unicyb.kiev.ua
|