Logics of local equitone predicates: semantic properties and sequential calculuses

Composition nominative logics of local equitone predicates are proposed. Such logics preserve the main deductive properties of classical logic, but have more rich class of models. Semantic properties and consequence relation for sets of formulas of such logics are studied and сorresponding sequentia...

Ausführliche Beschreibung

Gespeichert in:

Bibliographische Detailangaben
Datum:	2015
Hauptverfasser:	Nikitchenko, M.S., Shkilniak, S.S.
Format:	Artikel
Sprache:	Ukrainian
Veröffentlicht:	Інститут програмних систем НАН України 2015
Schlagworte:
Online Zugang:	https://pp.isofts.kiev.ua/index.php/ojs1/article/view/9
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!
Назва журналу:	Problems in programming
Завантажити файл:

Institution

Problems in programming

id	pp_isofts_kiev_ua-article-9
record_format	ojs
resource_txt_mv	ppisoftskievua/a8/2104e0323a9e4f90d57c9e3c591e0ba8.pdf
spelling	pp_isofts_kiev_ua-article-92018-10-02T13:30:20Z Logics of local equitone predicates: semantic properties and sequential calculuses Логики локально-эквитонных предикатов: семантические свойства и секвенциальные исчисления Логіки локально-еквітонних предикатів: семантичні властивості та секвенційні числення Nikitchenko, M.S. Shkilniak, S.S. Composition nominative logics of local equitone predicates are proposed. Such logics preserve the main deductive properties of classical logic, but have more rich class of models. Semantic properties and consequence relation for sets of formulas of such logics are studied and сorresponding sequential calculuses are constructed. The soundness and completeness theorems are proved on this base. Предложены композиционно-номинативные логики локально-эквитонных предикатов. Такие логики сохраняют основные дедуктивные свойства классических логик, но имеют более богатый класс моделей. Изучаются семантические свойства этих логик, отношение логического следования для множеств формул, строятся соответствующие секвенциальные исчисления, на их основе доказываются теоремы корректности и полноты. Пропонуються композиційно-номінативні логіки локально-еквітонних предикатів. Такі логіки зберігають основні дедуктивні властивості класичних логік, але мають значно багатший клас моделей. Вивчаються семантичні властивості цих логік, відношення логічного наслідку для множин формул, будуються відповідні секвенційні числення, на їх основі доводяться теореми коректності та повноти. Інститут програмних систем НАН України 2015-07-01 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/9 PROBLEMS IN PROGRAMMING; No 2 (2003) ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2 (2003) ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2 (2003) 1727-4907 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/9/15 Copyright (c) 2015 ПРОБЛЕМИ ПРОГРАМУВАННЯ
institution	Problems in programming
baseUrl_str	https://pp.isofts.kiev.ua/index.php/ojs1/oai
datestamp_date	2018-10-02T13:30:20Z
collection	OJS
language	Ukrainian
topic
spellingShingle	Nikitchenko, M.S. Shkilniak, S.S. Logics of local equitone predicates: semantic properties and sequential calculuses
topic_facet
format	Article
author	Nikitchenko, M.S. Shkilniak, S.S.
author_facet	Nikitchenko, M.S. Shkilniak, S.S.
author_sort	Nikitchenko, M.S.
title	Logics of local equitone predicates: semantic properties and sequential calculuses
title_short	Logics of local equitone predicates: semantic properties and sequential calculuses
title_full	Logics of local equitone predicates: semantic properties and sequential calculuses
title_fullStr	Logics of local equitone predicates: semantic properties and sequential calculuses
title_full_unstemmed	Logics of local equitone predicates: semantic properties and sequential calculuses
title_sort	logics of local equitone predicates: semantic properties and sequential calculuses
title_alt	Логики локально-эквитонных предикатов: семантические свойства и секвенциальные исчисления Логіки локально-еквітонних предикатів: семантичні властивості та секвенційні числення
description	Composition nominative logics of local equitone predicates are proposed. Such logics preserve the main deductive properties of classical logic, but have more rich class of models. Semantic properties and consequence relation for sets of formulas of such logics are studied and сorresponding sequential calculuses are constructed. The soundness and completeness theorems are proved on this base.
publisher	Інститут програмних систем НАН України
publishDate	2015
url	https://pp.isofts.kiev.ua/index.php/ojs1/article/view/9
work_keys_str_mv	AT nikitchenkoms logicsoflocalequitonepredicatessemanticpropertiesandsequentialcalculuses AT shkilniakss logicsoflocalequitonepredicatessemanticpropertiesandsequentialcalculuses AT nikitchenkoms logikilokalʹnoékvitonnyhpredikatovsemantičeskiesvojstvaisekvencialʹnyeisčisleniâ AT shkilniakss logikilokalʹnoékvitonnyhpredikatovsemantičeskiesvojstvaisekvencialʹnyeisčisleniâ AT nikitchenkoms logíkilokalʹnoekvítonnihpredikatívsemantičnívlastivostítasekvencíjníčislennâ AT shkilniakss logíkilokalʹnoekvítonnihpredikatívsemantičnívlastivostítasekvencíjníčislennâ
first_indexed	2025-07-17T09:37:55Z
last_indexed	2025-07-17T09:37:55Z
_version_	1838499778979168256
fulltext	Теоретические и методологические основы программирования © М.С. Нікітченко, С.С. Шкільняк, 2003 28 ISSN 1727-4907. Проблемы программирования. 2003. № 2 УДК 510.6, 681.3.06 М.С. Нікітченко, С.С. Шкільняк ЛОГІКИ ЛОКАЛЬНО-ЕКВІТОННИХ ПРЕДИКАТІВ: СЕМАНТИЧНІ ВЛАСТИВОСТІ ТА СЕКВЕНЦІЙНІ ЧИСЛЕННЯ∗ Пропонуються композиційно-номінативні логіки локально-еквітонних предикатів. Такі логіки зберігають основні дедуктивні властивості класичних логік, але мають значно багатший клас моделей. Вивчаються семантичні властивості цих логік, відно- шення логічного наслідку для множин формул, будуються відповідні секвенційні чис- лення, на їх основі доводяться теореми коректності та повноти. ∗ Робота виконана в рамках проекту INTAS 2000-447 Вступ Методи математичної логіки зна- ходять широке застосування в інфор- матиці, програмуванні, обчислювальній математиці, лінгвістиці, інших сферах людської діяльності. Це привело до по- яви великої кількості логічних форма- лізмів, які орієнтовані на відображення особливостей тих чи інших прикладних областей. Таких формалізмів стало на- стільки багато, що навіть поверхневий їх опис вимагає багатьох томів (тут до- сить пригадати 18-томне! видання з фі- лософської логіки видавництва Kluwer Academic Publishers, редактори Dov M. Gabbay та F. Guenther). Таке розмаїття логік робить актуальною проблему їх інтеграції. Тому не дивною є поява рі- зноманітних підходів до уніфікації ло- гічних формалізмів. До таких належить і композиційно-номінативний підхід [1], який має метою побудову логік предикатів різного рівня абстракції на єдиній методологічний основі з теорією програмування та теорією алгоритмів. Побудова відповідної ієрархії логік різ- ного рівня абстракції є дуже складною проблемою, вона вимагає багатьох ро- ків напруженої праці. Проте вже зараз можна окреслити певні логічні форма- лізми, які займають в цій ієрархії особ- ливе місце. До таких формалізмів в пе- ршу чергу належить класична логіка предикатів. Особливе місце класичної логіки визначається тим, що, по-перше, вона є основою багатьох спеціальних логік (модальних, темпоральних, реле- вантних та інших), а по-друге, вона де- тально досліджена і для неї побудовано багато різноманітних систем автомати- зованого доведення. В той же час класична логіка предикатів, незважаючи на численні позитивні якості, не дозволяє адекват- но виразити нові задачі, які з’являють- ся у програмуванні та моделюванні. Вона має низку обмежень [1], які ускладнюють її застосування в зазна- чених областях. Викликано це тим, що класична логіка орієнтується на класи- чні математичні структури тотальних (всюди визначених) n-арних функцій та предикатів. Така орієнтація веде до обмежень при побудові формул та мо- делей класичної логіки. Проте якщо подивитись на аксіоми та правила ви- ведення різних числень класичної логі- ки, то неважко переконатись, що в них n-арні функції та предикати безпосере- дньо не використовуються. Це спосте- реження дає підставу для побудови ло- гіки, яка орієнтується на істотно зага- льніший клас функцій та предикатів. Проведений аналіз класичної ло- гіки [2, 3] дозволяє стверджувати, що такими більш загальними функціями та предикатами повинні бути квазіарні відображення, які задаються на довіль- них наборах іменованих предметних значень. Прийняття такого рішення ве- де до кількох наслідків. По-перше, пе- рехід до квазіарних відображень зму- шує відмовитись від їх тотальності. Це означає перехід до логік часткових предикатів. По-друге, робота з квазіар- ними предикатами вимагає нових за- собів, пов’язаних з перейменуванням значень, що спонукає явне введення Теоретические и методологические основы программирования 29 оператора (композиції) реномінації. По-третє, клас квазіарних предикатів є надзвичайно потужним, тому для збе- реження властивостей класичної логіки його варто обмежити. Таке обмеження природно задається властивістю екві- тонності. Ця властивість говорить про те, що значення відображення не змі- нються при розширенні даних. Наве- дені властивості реалізовані в неокла- сичних логіках часткових предикатів, які орієнтовані на клас еквітонних ві- дображень [2, 3]. Зважаючи на те, що неокласичні логіки предикатів зберігають основні дедуктивні властивості класичної логі- ки, але розширюють клас її моделей, природно поставити питання про побу- дову неокласичних логік з максималь- ним класом моделей. Побудова такого максимального класу вимагає попере- днього уточнення та спеціального до- слідження. Крім того, вже зараз можна стверджувати, що опис такого класу не буде простим. Тому темою даної статті є побудова неокласичної логіки, орієн- тованої на відносно простий, зате по- тужний клас відображень. Таким є клас локально-еквітонних предикатів. Цей клас є узагальненням класу екві- тонних предикатів, для якого допуска- ється розширення даних лише на скін- ченну кількість іменованих значень (зауважимо, що достатньо розглядати розширення лише на одне значення – 1-еквітонність). Побудовані композиційно-номі- нативні логіки локально-еквітонних предикатів (ЛЕ-логіки) зберігають ос- новні закони класичної логіки при іс- тотному розширенні класу моделей. Це дозволяє використовувати в програму- ванні та моделюванні теоретичні ре- зультати і багатий досвід застосування класичної логіки. В статті викладаються семантичні властивості ЛЕ-логік, зо- крема відношення логічного наслідку для множин формул. Стосовно синтак- сичного аспекту для таких логік буду- ються аксіоматичні системи секвенцій- ного типу — реномінативні та кванто- рні секвенційні ЛЕ-числення. На базі таких числень розглядаються теореми повноти для ЛЕ-логік реномінативного та кванторного рівнів. 1. Основні поняття та семантичні властивості ЛЕ-логік Будемо дотримуватись позначень робіт [2, 4]. Для зручності нагадаємо основні поняття та визначення. Потужність множини М познача- тимемо \|M\|. Те, що значення f(d) деякої функції f : D → R визначене, позначаємо f(d)↓. Якщо f(d) невизначене, то пишемо f(a)↑. Для функцій f та g вводимо по- значення f(a) ≅ g(b), якщо з f(a)↓ та g(b)↓ випливає f(a) = g(b). Нехай A – множина базових да- них, V – множина предметних імен (предметних змінних). V-іменною мно- жиною (V-ІМ) над A назвемо довільну однозначну функцію із V в A. Множи- ну всіх V-IM над A позначаємо VA. V-ІМ будемо звичайно задавати у вигляді [v1 а1, ..., vn аn, ...] (тут vi∈V, ai∈A, причому vi ≠ vj при i ≠ j). V-повна ІМ над A — це тотальна однозначна функція із V в A. Множину всіх V-повних ІМ над A позначаємо AV. Множину всіх скінчен- них V-ІМ над A позначаємо VAF. Для V-ІМ вводимо операції ∩, \ та операцію звуження за множиною Х ⊆ V, задану так: δ║Х = [v a ∈ δ \| v∈X]. Вводимо функцію im: VA → 2V, визначену умовою im(δ) = pr1(δ). Замість δ║(V \{х}) для спрощення будемо писати δ║-х. Операція ║Х для множин імен- них множин визначається так: Μ║Х = { δ║X \| δ∈Μ}. Замість Μ║(V \{х}) для спрощення будемо писати Μ║-х. Визначимо операцію ∇ накладки V-ІМ δ2 на V-ІМ δ1: δ1∇ δ2 = δ2 ∪ (δ1║(V \ \ im(δ2))). Безпосередньо із визначення операції ∇ випливає: якщо α ⊆ β, то α ∇ δ ⊆ β ∇ δ. Твердження 1. Нехай α ⊆ δ, β ⊆ δ та α \ β і β \ α скінченні. Тоді існує ІМ Теоретические и методологические основы программирования 30 ϕ ⊆ δ така, що α ⊆ ϕ, β ⊆ ϕ та ϕ \ α і ϕ \ β скінченні. Справді, ІМ ϕ = (α ∩ β) ∪ (α \ β) ∪ ∪ (β \ α) – шукана. Операцію реномінації r: VA×VVF → → VA визначимо наступним чином: r([v1 x1, ..., vn xn], δ) = [v1 δ(x1), ..., vn δ(xn)] ∪ (δ║(V \ {v1, ..., vn})). Операція r v x монотонна в насту- пному смислі: із d' ⊇ d випливає r v x (d') ⊇ ⊇ r v x (d). Довільну функцію вигляду VA→R назвемо V-квазіарною функцією. Не- хай FпА – множина таких функцій. Під композицією реномінації в загаль- ному випадку розуміємо композицію R : FпА × VVF → FпА, яка задається так: R(f, [v1 x1, ..., vn xn])(δ) = = f(r([v1 x1, ..., vn xn], δ)). При фіксуванні множини пар імен [v1 x1, ..., vn xn] говоримо про параметричну операцію реномінації r ],...,[ 11 nn xvxv : VА → VA та параметричну композицію реномінації R ],...,[ 11 nn xvxv : FпА → FпА, які традиційно позначаються [2] r n n vv xx ,..., ,..., 1 1 та R n n vv xx ,..., ,..., 1 1 . Ввівши позначення вигляду y для y1, ..., yn, замість r n n vv xx ,..., ,..., 1 1 та R n n vv xx ,..., ,..., 1 1 також пишемо r v x та R v x . Довільний предикат вигляду Р : VA → {T, F} назвемо V-квазіарним предикатом на A. Предикат P (частково) істинний, якщо для довільних d∈VA із P(d)↓ ви- пливає P(d) = T. Ім'я x неiстотне для V-квазі- арнoго предикату Р, якщо для довіль- них d∈VA та для довільних a, b∈A маємо Р(d ∇ x a) ≅ Р(d ∇ x b). V-квазіарний предикат Р на A на- звемо 1-еквітонним, якщо для довіль- них d, d' ∈ VA із умов Р(d)↓, d' ⊃ d та \|d' \ d\| = 1 випливає Р(d')↓ = Р(d). V-квазіарний предикат Р на A на- звемо скінченно-еквітонним, або лока- льно-еквітонним, якщо для довільних d, d'∈VA із умов Р(d)↓, d' ⊇ d та d' \ d скін- ченна, випливає Р(d')↓ = Р(d). Неважко переконатись, що має місце Твердження 2. Предикат Р 1-ек- вітонний ⇔ Р локально-еквітонний. V-квазіарний предикат Р на A на- звемо еквітонним, якщо для довільних d, d' ∈VA із умови Р(d)↓ та d' ⊇ d випли- ває Р(d')↓ = Р(d). Кожний еквітонний предикат є локально-еквітонним, але зворотне не- обов'язкове: Твердження 3. Існують неекві- тонні локально-еквітонні предикати. Таким є, зокрема, предикат, іс- тинний на всіх скінченних ІМ та хиб- ний на всіх нескінченних ІМ. V-квазіарний предикат P повно- тотальний, якщо P(d)↓ для всіх d∈AV. Eквітонні повнототальні V-квазі- арні предикати назвемо V-повними. Семантичною основою компози- ційно-номінативної логіки локально- еквітонних предикатів (скорочено ЛЕ- логіки) реномінативного та кванторно- го рівнів є композиційні алгебри лока- льно-еквітонних квазіарних предикатів (LEРrА, C). Тут LEРrА – множина лока- льно-еквітонних V-квазіарних предика- тів на A, множина C задається базови- ми композиціями першого порядку ∨, ¬, R v x для логік реномінативного рівня та ∨, ¬, R v x , ∃x для логік кванторного рівня. Такі композиції зберігають [2] властивості еквітонності, фінарності та повнототальності. Теорема 1. Композиції ¬, ∨, R v x , ∃x зберігають властивість локально-ек- вітонності V-квазіарних предикатів. Нехай d' ⊇ d та d' \ d скінченна. Нехай предикати Р та Q локально-екві- тонні. Із умови Р(d)↓ та Q(d)↓ маємо Р(d')↓ = Р(d) та Q(d')↓ = Q(d). Якщо ¬(Р)(d)↓, то ¬(Р)(d')↓ = ¬(Р)(d). Якщо Теоретические и методологические основы программирования 31 ∨(Р, Q)(d)↓, то Р(d) = Т, або Q(d) = Т, або Р(d) = Q(d) = F. За локально-еквітон- ністю Р та Q маємо, що Р(d') = Т, або Q(d') = Т, або Р(d) = Q(d) = F. Звідси ∨(Р, Q)(d')↓ = ∨(Р, Q)(d). Нехай R v x (Р)(d)↓. За монотонніс- тю операції r v x із d' ⊇ d маємо r v x (d') ⊇ ⊇ r v x (d). Якщо d' \ d скінченна, то r v x (d') \ \ r v x (d) теж скінченна. За локально-екві- тонністю Р маємо Р(r v x (d'))↓ = Р(r v x (d)), тобто R v x (Р)(d')↓ = R v x (Р)(d). Нехай ∃x(Р)(d)↓. Це означає, що Р(d ∇ x b) = T для деякого b∈A або Р(d ∇ x a) = F для всіх a∈A. Із d' ⊇ d маємо d' ∇ x a ⊇ d ∇ x a. Якщо d' \ d скінченна, то зрозуміло, що (d' ∇ x a) \ \ (d ∇ x a) теж скінченна. Звідси за локально-еквітонністю предикату Р ма- ємо Р(d' ∇ x b)↓ = Р(d ∇ x b) = T для деякого b∈A або Р(d' ∇ x a)↓ = = Р(d ∇ x a) = F для всіх a∈A. Тому ∃x(Р)(d')↓ = ∃x(Р)(d). Наслідок 1. Клас LEРrА замкне- ний відносно композицій ¬, ∨, R v x , ∃x. Беручи до уваги похідні компо- зиції →, &, ↔, ∀x, дістаємо: Наслідок 2. Клас LEРrА замкне- ний відносно композицій ¬, ∨, →, &, ↔, R v x , ∃x, ∀x. Побудова композиційної алгебри локально-еквітонних предикатів дає змогу визначити мову ЛЕ-логіки. Алфа- віт мови складається з множини V предметних імен (предметних змінних), множини Ps предикатних символів, а також символів базових композицій ¬, ∨, R v x , ∃x. Множина Fr формул мови ЛЕ-ло- гіки визначається індуктивно: 1. Кожний предикатний символ є формулою. Такі формули назвемо атомарними. 2. Нехай Φ та Ψ – формули. Тоді ¬Φ, ∨ΦΨ, R v x Φ, ∃xΦ – формули. Для кожної формули вигляду ∃xΦ чи R v x Φ формулу Φ назвемо областю дії кванторного префікса ∃x чи символа реномінації R v x . Для запису формул бу- демо також використовувати інфіксну форму та символи похідних компози- цій →, &, ↔, ∀x. При фіксуванні множини базо- вих композицій композиційна алгебра (LEРrА, C) визначається алгебраїчною системою (АС) (А, LЕРrА). Для визна- чення значення формул ЛЕ-логіки за- дамо відображення I : Рs → LЕРrА. Пару ((А, LЕРrА), I) будемо називати алгебраї- чною системою локально-еквітонних предикатів з доданою сигнатурою. На- далі такі АС будемо позначати у вигля- ді A = (А, I). Відображення I продовжимо до відображення J : Fr → ЕРrА : 1) J(р) = I(р) для кожного р∈Ps. 2) J(¬Φ) = ¬J(Φ  , J(∨ΦΨ) = ∨(J(Φ), J(Ψ)), J(R v x Φ) = R v x (J(Φ)), J(∃xΦ) = ∃x(J(Φ)). Предикат J(Φ), який є значенням формули Φ при інтерпретації A = (А, I), позначаємо ΦA. Таким чином, з синтаксичної то- чки зору мови ЛЕ-логіки та неокласич- ної логіки (НКЛ) не відрізняються. Різ- ниця – в семантичних моделях. Для ЛЕ-логіки клас таких моделей ширший. У той же час основні закони класичної логіки [9, 10] справджуються і для ЛЕ- логіки. Формула Φ істинна при інтер- претації A = (A, I) або A-істинна, якщо ΦA – частково істинний предикат. Це позначаємо A \|= Φ. Формула Φ всюди істинна, якщо A \|= Φ при кожній інтерпретації A. Це позначаємо \|= Φ. Формула Ψ є логічним наслідком формули Φ, що позначаємо Φ \|= Ψ, як- що \|=Φ→Ψ. Теоретические и методологические основы программирования 32 Формули Φ та Ψ логічно еквіва- лентні, що позначаємо Φ∼Ψ, якщо Φ \|= Ψ та Ψ \|= Φ. Формула Ψ є логічним наслідком множини формул {Φ1, ..., Φn}, що по- значаємо {Φ1, ..., Φn} \|= Ψ, якщо Φ1& …& & Φn \|= Ψ. Семантичні властивості ЛЕ-логік в основному аналогічні відповідним властивостям НКЛ, які розглядались в [2—6]. Важливе місце серед таких вла- стивостей займає теорема семантичної еквівалентності. Теорема 2. Нехай формула Φ' отримана із формули Φ заміною де- яких входжень формул Φ1, ..., Φn на Ψ1, ..., Ψn відповідно. Якщо \|= Φ1 ↔ Ψ1, ..., \|= Φn ↔ Ψn, то \|= Φ ↔ Φ'. Предметне ім'я x∈V неістотне для формули Φ, якщо для кожної A = (A, I) ім'я x неістотне для предикату ΦA. Критерії неістотності предметних імен, що мають місце для НКЛ, справ- джуються і для ЛЕ-логік. Теорема 3. Ім'я x∈V неістотне для формули Φ ⇔ для кожного v∈V \|= Φ ↔ )(Φx vR . Теорема 4. Ім'я x∈V неістотне для формули Φ ⇔ \|= Φ ↔ ∀xΦ ⇔ \|= Φ → → ∀xΦ ⇔ \|= ∃xΦ → Φ ⇔ \|= ∃xΦ ↔ Φ. Для кожного p∈Ps постулюємо множину синтетично неістотних [6] імен. Таку множину визначаємо за до- помогою тотальної функції µ : Ps → 2V. Зазначену функцію продовжуємо так, як це зроблено для НКЛ [6], до функції µ : Fr → 2V. Кожне х∈µ(Φ) неістотне для формули Φ. Ім'я x∈V тотально неістотне, якщо воно неістотне для кожного p∈Ps. Додатковою вимогою до семан- тичних моделей ЛЕ-логік, подібно до семантичних моделей НКЛ, є наявність нескінченної множини тотально неіс- тотних імен. Це необхідно [6] для ви- конання еквівалентних перетворень довільних формул. Семантичні властивості ЛЕ-логік RТ, RR, R¬, R∃, PsN, ΦN формулюються цілком аналогічно відповідним власти- востям неокласичних логік, які наведе- ні в [2—6]. Позначимо σ(Φ) множину всіх тих р∈Рs, які входять до складу фор- мули Φ. Позначимо nm(Φ) множину всіх імен із V, які фігурують у символах ре- номінації та квантифікації, що входять до складу Φ. Таку nm(Φ) назвемо мно- жиною імен формули Φ. Позначимо q(Φ) множину всіх імен із V, які фігурують у символах квантифікації, що входять до складу Φ. Таку q(Φ) назвемо множиною квантор- них імен формули Φ. Множину nm(Φ) \ q(Φ) позначимо пq(Φ). Розширимо пт, σ, q та nq на мно- жини формул: пт(Γ) = ∪ Γ∈Ф )Ф(nm ; σ(Γ) = ∪ Γ∈ σ Ф )Ф( ; q(Γ) = ∪ Γ∈Ф )Ф(q ; пq(Γ) = nm(Γ)\q(Γ). Формула примітивна, якщо во- на атомарна або має вигляд v xR р, де { v } ∩ µ(p) = ∅. Формула Ψ знаходиться в різно- кванторній, або субнормальній формі, якщо всі входження кванторних пре- фіксів у Ψ, за їх наявності, – по різних тотально неістотних іменах, причому кожне ім'я у∈q(Ψ) не може лежати в області дії символа R v x такого, що у∈{ v , x }. Формулу в різнокванторній фо- рмі назвемо різнокванторною, або суб- нормальною. Кожну формулу ЛЕ-логіки можна звести до субнормальної форми: Теорема 5. Для кожної формули Φ можна збудувати різнокванторну формулу Ξ таку, що \|= Φ ↔ Ξ. Доведення цілком аналогічне до- веденню [8] відповідної теореми нео- класичної логіки. Різнокванторну фор- мулу Ξ, отриману із Φ описаним в та- кому доведенні способом, назвемо суб- нормалізантою формули Φ. Теоретические и методологические основы программирования 33 Формула Ψ знаходиться в норма- льній формі [2, 4], якщо вона в різно- кванторній формі, та всі її символи ре- номінації, за їх наявності, застосовані тільки до предикатних символів. Фор- мулу в нормальній формі назвемо нор- мальною. Теорема 6. Для кожної формули Φ можна збудувати нормальну форму- лу Ψ таку, що \|= Φ ↔ Ψ. Доведення теореми 6 аналогічне доведенню [2, 4] відповідної теореми неокласичної логіки. Нормальну фор- мулу Ξ, отриману із Φ описаним у та- кому доведенні способом, назвемо нор- малізантою формули Φ. Надалі вважаємо зафіксованою мову ЛЕ-логіки та відповідну сигнату- ру АС. Для довільних d∈VA та X ⊆ V множину ∪ F AX d ∈ ∇ κ κ позначимо XFd. При X = V множину VFd позначимо Fd. Таким чином, Fd – множина всіх ІМ, утворе- них накладками скінченних ІМ на d. Теорема 7. Нехай A = (А, IА) і В = (А, IВ) – АС одної сигнатури та d∈VA. Нехай формула Φ із nm(Φ) = X та- ка, що для всіх р∈σ(Φ) для всіх δ∈XFd із умови рA(δ)↓ випливає рВ(δ)↓ = рA(δ). То- ді для всіх δ∈XFd з умови ΦA(δ)↓ випли- ває ΦВ(δ)↓ = ΦA(δ). Доводимо індукцією за побудо- вою формули Φ. Нехай Φ атомарна, тобто Φ суть р∈Ps. Тоді ΦA(δ)↓ означає рA(δ)↓. Згідно умови теореми звідси рВ(δ)↓ = рA(δ), тоб- то ΦВ(δ)↓ = ΦA(δ). Нехай Φ має вигляд ¬Ψ. Тоді ΦA(δ)↓ означає (¬Ψ)A(δ)↓. Із (¬Ψ)A(δ)↓ випливає ΨA(δ)↓, звідки за припущен- ням індукції ΨВ(δ)↓ = ΨA(δ). Звідси (¬Ψ)В(δ)↓ = (¬Ψ)A(δ), тобто ΦВ(δ)↓ = ΦA(δ). Нехай Φ має вигляд ∨ΨΞ. Тоді ΦA(δ)↓ означає (∨ΨΞ)A(δ)↓. Можливі два випадки: 1) ΨА(δ) = ΞA(δ) = F; 2) ΨА(δ) = Т або ΞA(δ) = Т. У випадку 1) за припущенням ін- дукції ΨВ(δ)↓ = ΨA(δ) = F та ΞВ(δ)↓ = ΞA(δ) = = F, звідси (∨ΨΞ)В(δ)↓ = (∨ΨΞ)A(δ) = F. У випадку 2) за припущенням індукції ΨВ(δ)↓ = ΨA(δ) = Т або ΞВ(δ)↓ = ΞA(δ) = Т, звідки (∨ΨΞ)В(δ)↓ = (∨ΨΞ)A(δ) = Т. В обох випадках ΦВ(δ)↓ = ΦA(δ). Нехай Φ має вигляд Ψn n vv xxR ,..., ,..., 1 1 . Тоді ΦA(δ)↓ означає ( Ψn n vv xxR ,..., ,..., 1 1 )A(δ)↓, зві- дси ΨA(δ ∇ v1 δ(x1) ∇…∇ vn δ(xn))↓. Якщо δ∈XFd, то δ ∇ v1 δ(x1) ∇…∇ vn (xn)∈XFd. Тепер за припущенням ін- дукції ΨВ(δ ∇ v1 δ(x1) ∇…∇ vn δ(xn))↓ = = ΨA(δ ∇ v1 δ(x1) ∇…∇ vn δ(xn)), тому ( Ψn n vv xxR ,..., ,..., 1 1 )В(δ)↓ = ( Ψn n vv xxR ,..., ,..., 1 1 )A(δ). Отже ΦВ(δ)↓ = ΦA(δ). Нехай Φ має вигляд ∃хΨ. Тоді ΦA(δ)↓ означає (∃хΨ)A(δ)↓. Можливі два випадки: 1) ΨА(δ ∇ х а) = Т для деяко- го а∈A; 2) ΨА(δ ∇ х с) = F для всіх с∈A. Якщо δ∈XFd , то для всіх b∈A δ ∇ х b ∈XFd . У випадку 1) за припущенням ін- дукції ΨВ(δ ∇ х а)↓ = ΨA(δ ∇ х а) = Т для деякого а∈A, звідки (∃хΨ)В(δ)↓ = = (∃хΨ)A(δ). У випадку 2) за припущен- ням індукції для всіх с∈A маємо ΨВ(δ ∇ х с)↓ = ΨA(δ ∇ х с) = F, звідси (∃хΨ)В(δ)↓ = (∃хΨ)A(δ). Отже ΦВ(δ)↓ = = ΦA(δ). Наслідок. Нехай АС одної сигна- тури A = (А, IА) і В = (А, IВ) та формула Φ такі, що для всіх р∈σ(Φ) для всіх δ∈VA із умови рA(δ)↓ випливає рВ(δ)↓ = = рA(δ). Тоді для довільного δ∈VA із умо- ви ΦA(δ)↓ випливає ΦВ(δ)↓ = ΦA(δ). Теорема 8. Нехай Φ – формула, у∈V тотально неістотне та у∉пт(Φ), A = (А, IА) – АС. Тоді існує АС В = (А, IВ) така, що з умови ΦA(d)↓ випливає ΦВ(d║-у)↓ = ΦВ(d)↓ = ΦA(d). Для кожного р∈σ(Φ) визначимо рВ наступним чином. Для кожного δ∈VA║-у при умові рA(δ)↓ покладемо Теоретические и методологические основы программирования 34 рB(δ) = рA(δ) та рB(δ ∇ y а) = рA(δ) для всіх а∈A. Якщо рA(δ)↑ та рА(δ ∇ y a)↑ для всіх a∈A, то покладемо рB(δ)↑ та рB(δ ∇ y a)↑ для всіх a∈A. Якщо рA(δ)↑ та рA(δ ∇ y b)↓ для деякого b∈A, то покладемо рB(δ) = рA(δ) та рB(δ ∇ y a) = = рA(δ ∇ х b) для всіх a∈A. Коректність такого визначення випливає із умов локально-еквітонності рA та рB і тоталь- ної неістотності імені у. Далі доводимо індукцією за по- будовою формули Φ. Наслідок. Нехай Σ – множина формул, у тотально неістотне та у∉ пт(Σ), A = (А, IА) – АС. Тоді існує АС В = (А, IВ) така, що для довільної Φ∈Σ з умови ΦA(d)↓ випливає ΦВ(d║-у)↓ = = ΦВ(d)↓ = ΦA(d). Справді, достатньо для кожного р∈σ(Σ) визначити рВ так, як описано в теоремі. Теорема 9. Нехай Σ – множина формул, Ψ ∼ Φ. Нехай АС A = (А, IА) та d∈VA такі, що для всіх Ξ∈Σ ΞA(d)↓, ΨA(d)↓ та ΦA(d)↑. Тоді існують АС В = (А, IВ) та δ∈AV такі, що для всіх Ξ∈Σ ΞB(δ)↓ = ΞA(d), ΨB(δ)↓ = ΨA(d) та ΦB(δ)↓ = = ΨB(δ). Нехай Ed = ∪ dF VA ∈α ∈δα⊇δ } та{ – множина всіх V-повних розширень ІМ із Fd . Для кожного р∈σ(Σ∪{Φ, Ψ}) та кож- ної δ∈Ed визначимо рВ(δ) таким чином. 1. Нехай існує α∈Fd таке, що α ⊆ δ та рA(δ)↓. Тоді покладемо рВ(δ) = рA(α). Таке визначення коректне: неможливе існування β ⊆ δ та η ⊆ δ таких, що β∈Fd, η∈Fd та рA(β) ≠ рA(η). Справді, якщо β∈Fd та η∈Fd, то β\η та η\β скінченні, тому, за твердженням 1, існує ІМ ϕ ⊆ δ така, що β ⊆ ϕ, η ⊆ ϕ та ϕ\β і ϕ\η скінченні. За локально-еквітонністю рA(ϕ)↓ = рA(β) та рA(ϕ)↓ = рA(η), що неможливо в силу рA(β) ≠ рA(η). 2. Нехай для кожного α∈Fd тако- го, що α ⊆ δ, маємо рA(δ)↑. Тоді значен- ня рВ(δ) визначаємо довільним чином. Оскільки неможливо одночасно 1 та 2, то для випадку 2 неможливо одночасно визначити рВ(δ) як рA(α) для деякого α∈Fd такого, що α ⊆ δ. Візьмемо довільне α∈Fd. Нехай рA(δ)↓. Згідно 1 для кожного δ∈Ed тако- го, що α ⊆ δ, маємо рВ(δ) = рA(α)↓. При обчисленні ΘВ для довільної Θ∈Σ∪{Φ, Ψ} на d∈VA обчислюються тільки рВ(β) для р∈σ(Θ) на певних β∈Fd. Згідно теореми 7, звідси при δ ⊇ d для всіх Ξ∈Σ маємо ΞB(δ)↓ = ΞA(d) та ΨB(δ)↓ = = ΨA(d). Але рВ(ϕ)↓ для кожних р∈σ(Φ) та ϕ∈Ed , тому ΦB(δ)↓. В силу Ψ ∼ Φ ма- ємо ΦB(δ) = ΨB(δ). 2. Відношення логічного наслідку для множин формул Нехай Γ та ∆ – множини фор- мул певної мови сигнатури Ps; A = (А, I) – АС A = (А, I) сигнатури Ps. Скажемо, що в АС A із Γ випли- ває ∆, або ∆ є логічним наслідком Γ в АС A, якщо для всіх d∈VA з того, що ΦА(d) = T для всіх Φ∈Γ, випливає наступ- не: неможливо ΨА(d) = F для всіх Ψ∈∆. Те, що ∆ є логічним наслідком Γ в АС A, позначаємо Γ \|=А ∆. Скажемо, що із Γ випливає ∆, або ∆ є логічним наслідком Γ, якщо Γ \|=А ∆ для всіх АС A = (А, I) сигнатури Ps. Те, що ∆ є логічним наслідком Γ, позначаємо Γ \|= ∆. Отже, Γ \|≠ ∆ ⇔ існують АС A = (А, I) та d∈VA такі, що для всіх Φ∈Γ маємо ΦА(d) = T та для всіх Ψ∈∆ маємо ΨА(d) = F. Для спрощення запису замість {Φ}∪Γ будемо звичайно писати Φ, Γ або Γ, Φ. Зауважимо, що відношення логі- чного наслідку для множин формул рефлексивне, але нетранзитивне. Справді, очевидно ∆ \|= ∆, але з Γ \|= ∆ та ∆ \|= Σ не мусить випливати Γ \|= Σ. Остан- Теоретические и методологические основы программирования 35 нє засвідчує такий приклад. Маємо {x = 0 ∨ x = 1 ∨ x = 2}\|={x = 0 ∨ x = 1, x = 1 ∨ ∨ x = 2} та {x = 0 ∨ x = 1, x = 1 ∨ x = 2}\|={x = 1}, але {x = 0 ∨ x = 1 ∨ x = 2}\|≠{ x = 1}. Розглянемо властивості логічного наслідку для множин формул на про- позиційному рівні. Вказані властивості цілком аналогічні відповідним власти- востям відношення \|= класичної логіки предикатів [11]. Для їх доведення ви- користовуються визначення пропози- ційних композицій [2] та наведене ви- ще визначення відношення \|=. G1) Якщо Γ∩∆ ≠ ∅, то Γ \|= ∆ . G2) Нехай Γ \|= ∆ та ∆ ⊆ Σ. Тоді Γ \|= Σ. ¬\|− ) ¬Φ, Γ \|= ∆ ⇔ Γ \|= ∆, Φ. ¬−\| ) Γ \|= ∆, ¬Φ ⇔ Φ, Γ \|= ∆. ∨\|− ) Φ∨Ψ, Γ \|= ∆ ⇔ Φ, Γ \|= ∆ та Ψ, Γ \|= ∆. ∨−\| ) Γ \|= ∆, Φ ∨ Ψ ⇔ Γ \|= ∆, Φ, Ψ. &\|− ) Φ & Ψ, Γ \|= ∆ ⇔ Φ, Ψ, Γ \|= ∆. &−\| ) Γ \|= ∆, Φ & Ψ ⇔ Γ \|= ∆, Φ та Γ \|= ∆, Ψ. →\|− ) Φ → Ψ, Γ \|= ∆ ⇔ Γ \|= ∆, Φ та Ψ, Γ \|= ∆. →−\| ) Γ \|= ∆, Φ → Ψ ⇔ Φ, Γ \|= ∆, Ψ. ↔\|− ) Φ ↔ Ψ, Γ \|= ∆ ⇔ Φ, Ψ, Γ \|= ∆ та Γ \|= ∆, Φ, Ψ. ↔−\| ) Γ \|= ∆, Φ ↔ Ψ ⇔ Φ, Γ \|= ∆, Ψ та Ψ, Γ \|= ∆, Φ. Теорема 10. Нехай Φ ∼ Ψ. Тоді Φ, Γ \|= ∆ ⇔ Ψ, Γ \|= ∆ та Γ \|= ∆, Φ ⇔ Γ \|= ∆, Ψ. Доведемо Φ, Γ \|= ∆ ⇔ Ψ, Γ \|= ∆. Аналогічно доводиться Γ \|= ∆, Φ ⇔ ⇔ Γ \|= ∆, Ψ. Припустимо супротивне: Φ, Γ \|= ∆ та Ψ, Γ \|≠ ∆. Останнє означає, що існу- ють АС A = (А, I) та d∈VA такі: ΨA(d) = T і ΞA(d) = T для всіх Ξ∈Γ, та ΘА(d) = F для всіх Θ∈∆ (1) Якщо ΦA(d)↓, то в силу Φ ∼ Ψ ма- ємо ΦA(d) = ΨA(d) = T, звідки ΦA(d) = T і ΞA(d) = T для всіх Ξ∈Γ та ΘA(d) = F для всіх Θ∈∆. Це суперечить Φ, Γ \|= ∆. От- же, необхідно ΦA(d)↑. В силу теореми 9 існують АС В = (А, IВ) та δ∈AV такі, що для всіх Ξ∈Γ ΞB(δ)↓ = ΞA(d) = T, для всіх Θ∈∆ ΘB(δ)↓ = ΘA(d) = F, ΨB(δ)↓ = ΨA(d) = T, ΦB(δ)↓ = ΨB(δ) = T. Але тоді Φ, Γ \|≠ ∆. Вкажемо властивості відношення \|= на реномінативному та кванторному рівнях. Вони безпосередньо відтворю- ють відповідні властивості формул, пов'язані з композицією реномінації. Згідно теореми 10, кожна така власти- вість розщеплюється на дві відповідні властивості для \|=, коли еквівалентні формули знаходяться зліва від \|= та справа від \|=. RT\|−) )(, , Φv x z zR , Γ \|= ∆ ⇔ )(Φv xR , Γ \|= ∆. RT−\|) Γ \|= ∆, )(, , Φv x z zR ⇔ Γ \|= ∆, )(Φv xR . RR\|−) v xR ( w yR (Φ)), Γ \|= ∆ ⇔ v xR w y (Φ), Γ \|= ∆. RR−\|) Γ \|= ∆, v xR ( w yR (Φ)) ⇔ Γ \|= ∆, v xR w y (Φ). R¬\|−) v xR (¬Φ), Γ \|= ∆ ⇔ ¬ v xR (Φ), Γ \|= ∆. R¬−\|) Γ \|= ∆, v xR (¬Φ) ⇔ Γ \|= ∆, ¬ v xR (Φ). R∨\|−) v xR (Φ∨Ψ), Γ \|= ∆ ⇔ v xR (Φ) ∨ v xR (Ψ), Γ \|= ∆. R∨−\|) Γ \|= ∆, v xR (Φ ∨ Ψ) ⇔ Γ \|= ∆, v xR (Φ) ∨ ∨ v xR (Ψ). PsN\|−) )(, , pR y z v x , Γ \|= ∆ ⇔ v xR (р), Γ \|= ∆. PsN−\|) Γ \|= ∆, )(, , pR y z v x ⇔ Γ \|= ∆, v xR (р). ΦN\|−) )(, , Φv x y zR , Γ \|= ∆ ⇔ )(Φv xR , Γ \|= ∆. ΦN−\|) Γ \|= ∆, )(, , Φv x y zR ⇔ Γ \|= ∆, )(Φv xR . R∃\|−) v xR (∃yΦ), Γ \|= ∆ ⇔ ∃y )(Φv xR , Γ \|= ∆. R∃−\|) Γ \|= ∆, v xR (∃yΦ) ⇔ Γ \|= ∆, ∃y )(Φv xR . ∃∃R \|−) ∃хΦ, Γ \|= ∆ ⇔ ∃у )(Φx уR , Γ \|= ∆. ∃∃R −\|) Γ \|= ∆, ∃хΦ ⇔ Γ \|= ∆, ∃у )(Φx уR . Для PsN\|− та PsN−\| умова у∈µ(р), де р∈Ps. Для ΦN\|− та ΦN−\| умова у∈µ(Φ). Для R∃\|− та R∃−\| умова у∉{ v , x }. Для ∃∃R \|− та ∃∃R −\| умова у∈µ(Φ), яку можна ослабити до умови \|=Φ → ∀уΦ. Властивості R∃\|−, R∃−\|, ∃∃R \|−, ∃∃R −\| нескладно переформулювати для ∀х. Теоретические и методологические основы программирования 36 Якщо формула v xR (∃yΦ) різно- кванторна, то вже за визначенням у∉{ v , x }. Тому для різнокванторних та нормальних формул R∃\|− і R∃−\| форму- люються без обмежень. Для довільної множини формул Σ позначимо Σр множину субнормалізант всіх формул множини Σ та позначимо Σн множину нормалізант всіх формул множини Σ. Враховуючи теореми 5, 6 та 10, отримуємо такий результат: Теорема 11. Γ \|= ∆ ⇔ Γр \|= ∆р та Γ \|= ∆ ⇔ Γн \|= ∆н . В подальшому викладі Γ, ∆ – множини формул, A = (А, I) – АС такої ж сигнатури. Теорема 12. Γ \|=A ∆, )( 1 Φx yR ,…, )(Φx yn R , ∃хΦ ⇔ Γ \|=A ∆, ∃хΦ. Теорема 13. З умови ∃хΦ, Γ \|=A ∆ випливає )(Φx yR , Γ \|=A ∆. Теорема 14. Нехай у тотально не- істотне та у∉пт(Γ, ∆, Φ). Тоді з )(Φx yR , Γ \|= ∆ випливає ∃хΦ, Γ \|= ∆. Доведення відповідних тверд- жень для випадку неокласичних логік наведені в [7]. При доведенні по суті використовується тільки умова лока- льної еквітонності, тому зазначені до- ведення переносяться на випадок ЛЕ- логік. На основі теорем 12—14 отриму- ємо наступні властивості відношення \|=: ∃−\|) Γ \|= ∆, )( 1 Φx yR , …, )(Φx yn R , ∃хΦ ⇔ ⇔ Γ \|= ∆, ∃хΦ. ∃\|−) ∃хΦ, Γ \|= ∆ ⇔ )(Φx yR , Γ \|= ∆ (тут у тотально неістотне та у∉пт(Γ, ∆, Φ). Властивості ¬\|−, ¬−\|, ∨\|−, ∨−\|, RT\|−, RТ−\|, RR\|−, RR−\|, R¬\|−, R¬−\|, R∨\|−, R∨−\|, PsN\|−, PsN−\| назвемо базовими властивостями відношення \|= на реномінативному рів- ні. Додавши R∃\|−, R∃−\|, ∃−\|, ∃\|−, отримуємо базові властивості відношення \|= на кванторному рівні. Базові властивості відношення \|= дозволяють звести логічний наслідок складної формули (разом з множиною інших формул) до логічних наслідків простіших формул, що утворюють складнішу. Тому питання про відно- шення логічного наслідку між двома множинами формул, в одну з яких входить складна формула, зводиться до питання про відношення логічного нас- лідку між двома множинами формул, в які вже входять компоненти складної формули (з точністю до перейменуван- ня предметних імен). 3. Секвенційні числення ЛЕ-логік Формально-аксіоматичні систе- ми, які формалізують відношення логі- чного наслідку між двома множинами формул ЛЕ-логік реномінативного та кванторного рівнів, назвемо реноміна- тивними та кванторними секвенцій- ними ЛЕ-численнями. В класичному, генценівському варіанті [9], секвенціями називають об'єкти вигляду Γ→ ∆, де Γ та ∆ – множини формул, → – новий символ, що не входить до алфавіту мови логіки. Секвенційне числення будується так, що секвенція Γ→ ∆ вивідна ⇔ Γ \|= ∆. Тому базовим властивостям відношен- ня \|= співставимо їх синтаксичні анало- ги – секвенційні форми. Секвенційні форми є правилами виведення секвен- ційних числень. Секвенції Γ → ∆ такі, що Γ ∩ ∆ ≠ ∅, називають замкненими. Але з умови Γ ∩ ∆ ≠ ∅ випливає Γ \|= ∆. Тому якщо се- квенція Γ → ∆ замкнена, то Γ \|= ∆. Зам- кнені секвенції грають роль аксіом секвенційних числень. Секвенційні форми традиційно записують у вигляді Ω Σ або Ω ΛΣ . Тут Σ, Λ, Ω – секвенції. Секвенції над рис- кою – засновки, під рискою – ви- сновки. В нашому випадку засновки – це секвенції, співставлені лівим ча- стинам відповідних семантичних влас- тивостей, висновки – це секвенції, співставлені їх правим частинам. Мо- жна вважати, що секвенційні форми застосовуються незалежно від порядку входження формул. Теоретические и методологические основы программирования 37 Форма запису секвенцій з вико- ристанням символу → традиційна [9], вона відповідає записам логічного нас- лідку для множин формул. Проте для нас зручнішою є модифікована форма запису секвенцій, подібна до форми за- пису семантичних таблиць Бета [11, 12]. Кожну формулу секвенції відмі- тимо (специфікуємо) зліва одним з двох символів: \|− чи −\|. Якщо формула знаходиться зліва від →, відмічаємо її символом \|− , якщо справа – символом −\|. Тепер кожна формула секвенції на- буває вигляду \|−Φ або −\|Φ, причому від- мітка однозначно вказує на місце фор- мули в секвенції – зліва чи справа від →. Тому в записі секвенції символ → можна опустити. Секвенцію, утворену з секвенції Γ→ ∆ описаною вище відміткою фор- мул, позначимо \|−Γ−\| ∆. Не деталізуючи, секвенції відмічених формул будемо також позначати Σ . Секвенція Σ замкнена, якщо іс- нує формула Φ така, що \|−Φ∈Σ та −\|Φ∈Σ. Відповідно до базових властивос- тей відношення \|= вводимо такі базові секвенційні форми реномінативного рівня (зліва записуємо назву форми): \|−¬ Σ Σ , ,\| A A \| ¬− − −\|¬ Σ Σ , , \| A A\| ¬− − \|−∨ Σ ΣΣ , ,, BA B A \| \|\| ∨− −− −\|∨ Σ Σ , ,, \| \|\| BA BA ∨− −− \|−RT Σ Σ ),( ),( , , AR AR z z\| \| v x v x − − −\|RT Σ Σ ),( ),( , ,\| \| AR AR z z v x v x − − \|−RR Σ Σ )),(( ),( ARR AR \| \| w y v x w y v x − − −\|RR Σ Σ )),(( ),( \| \| ARR AR w y v x w y v x − − \|−R¬ Σ Σ ),( ),( AR AR \| \| ¬ ¬ − − v x v x −\|R¬ Σ Σ ),( ),( \| \| AR AR ¬ ¬ − − v x v x \|−R∨ Σ Σ ),( ),()( BAR BRAR \| \| ∨ ∨ − − v x v x v x −\|R∨ Σ Σ ),( ),()( \| \| BAR BRAR ∨ ∨ − − v x v x v x \|−PsN Σ Σ ),( ),( , , pR pR y z\| \| v x v x − − при у∈µ(р) −\|PsN Σ Σ ),( ),( , ,\| \| pR pR y z v x v x − − при у∈µ(р) На кванторному рівні додаємо такі базові секвенційні форми: \|−R∃ Σ Σ ),( ),( yAR AyR \| \| ∃ ∃ − − v x v x при y∉{ xv , } −\|R∃ Σ Σ ),( ),( \| \| yAR AyR ∃ ∃ − − v x v x при y∉{ xv , } \|−∃ Σ Σ , ),( \| \| xA AR x y ∃− − при умові у тотально −\|∃ Σ Σ , ,),(),...,( \| \|\|\| 1 xA xAARAR x z x z m ∃ ∃ − −−− , де {z1,…, zт}= неістотне та у∉пт(Σ, А) = nq(Σ, ∃xА) Для різнокванторних формул властивості R∃\|− та R∃−\| формулюються без обмежень, тому в секвенційних формах \|−R∃ та −\|R∃ виконання умови y∉{ xv , } гарантоване. Враховуючи семантичні власти- вості ¬\|− , ¬−\| , ∨\|− , ∨−\| , RT\|−, RТ−\|, RR\|−, RR−\|, R¬\|−, R¬−\|, R∨\|−, R∨−\|, PsN\|−, PsN−\| , R∃\|−, R∃−\|, ∃−\| , ∃\|− отримуємо наступний результат: Теорема 15. Нехай Ω Σ та Ω ΥΣ – секвенційні форми, Σ = \|−Λ−\| Κ, Υ = = \|−Χ−\| Ζ та Ω = \|−Γ−\| ∆. Тоді 1) якщо Теоретические и методологические основы программирования 38 Λ \|= Κ, то Γ \|= ∆; 2) якщо Λ \|= Κ та Χ \|= Ζ, то Γ \|= ∆. Секвенційні числення ЛЕ-логік з наведеними вище базовими секвенцій- ними формами реномінативного/кван- торного рівня назвемо реномінативни- ми/кванторними ЛЕ-численнями. Поняття виведення для секвен- ційних ЛЕ-числень введемо традицій- ним чином, аналогічно класичним сек- венційним численням [9, 11, 12]. Виве- дення в секвенційних численнях має вигляд дерева, вершинами якого є сек- венції. Такі дерева називають секвен- ційними. Наведемо індуктивне визна- чення секвенційного дерева. 1. Секвенція Σ утворює тривіаль- не секвенційне дерево з єдиною вер- шиною Σ, яка є коренем дерева. 2. Нехай α – секвенційне дерево з коренем Σ; β – секвенційне дерево з коренем Υ; Ω Σ та Ω ΥΣ – секвенційні форми. Тоді Ω α \| та Ω βα /\ – секвенційні дерева з коренем Ω. Секвенційне дерево з коренем Σ називають секвенційним деревом сек- венції Σ. Тривіальне секвенційне дерево замкнене, якщо це замкнена секвенція. Нетривіальне секвенційне дерево за- мкнене, якщо кожний його лист (кін- цева вершина, відмінна від кореня) – замкнена секвенція. Секвенція Σ виві- дна (має виведення), якщо існує за- мкнене секвенційне дерево з коренем Σ. Таке дерево назвемо виведенням секвенції Σ. Сформулюємо теорему корект- ності для ЛЕ-числень. Теорема дово- диться індукцією за побудовою за- мкненого секвенційного дерева для секвенції \|−Γ−\| ∆. Теорема 16. Нехай секвенція \|− Γ−\| ∆ вивідна. Тоді Γ \|= ∆. Для доведення повноти секвен- ційних ЛЕ-числень природно викорис- тати метод модельних (хінтікківських) множин. Доведення теореми повноти з використанням модельних множин для неокласичних секвенційних числень реномінативного та кванторного рівнів наведені в [7, 8]. Враховуючи розгляну- ті вище семантичні властивості та той факт, що з синтаксичної точки зору мови ЛЕ-логіки та НКЛ не відрізня- ються, такі доведення переносяться на випадок реномінативних та кванторних ЛЕ-числень. Множину Н відмічених формул кванторної неокласичної логіки із W = nq(Н) назвемо модельною, якщо ви- конуються наступні умови: 1) для кожної примітивної Φ ли- ше одна з формул \|−Φ чи −\|Φ може на- лежати до Н; 2) якщо у∈µ(p) та \|− )(, , pR y z v x ∈Н, то \|− )( pRv x ∈Н; якщо −\| )(, , pR y z v x ∈Н, то −\| )( pRv x ∈Н; 3) якщо \|−¬Φ∈Н, то −\|Φ∈Н; якщо −\|¬Φ∈Н, то \|−Φ∈Н; 4) якщо \|−Φ ∨ Ψ∈Н, то \|−Φ∈Н або \|−Ψ∈Н; якщо −\|Φ∨Ψ∈Н, то −\|Φ∈Н та −\|Ψ∈Н; 5) якщо \|− )(, , Φv x z zR ∈Н, то \|− )(Φv xR ∈Н; якщо −\| )(, , Φv x z zR ∈Н, то −\| )(Φv xR ∈Н; 6) якщо \|− v xR ( w yR (Φ))∈Н, то \|− v xR w y (Φ)∈Н; якщо −\| v xR ( w yR (Φ))∈Н, то −\| v xR w y (Φ)∈Н; 7) якщо \|− v xR (¬Φ)∈Н, то \|−¬ v xR (Φ)∈ ∈Н; якщо −\| v xR (¬Φ)∈Н, то −\| ¬ v xR (Φ)∈Н; 8) якщо \|− v xR (Φ ∨ Ψ)∈Н, то \|− v xR (Φ) ∨ ∨ v xR (Ψ)∈Н; якщо −\| v xR (Φ ∨ Ψ)∈Н, то −\| v xR (Φ) ∨ v xR (Ψ)∈Н; 9) при y∉{ xv , } якщо \|− v xR (∃yΦ)∈ ∈Н, то \|− ∃y v xR (Φ)∈Н; якщо −\| v xR (∃yΦ)∈Н, то −\| ∃y v xR (Φ)∈Н; 10) якщо \|−∃хΦ∈Н, то існує у∈nq(Н) таке, що \|− )(Φx yR ∈Н; якщо −\|∃хΦ∈Н, то для всіх у∈nq(Н) маємо −\| )(Φx yR ∈Н. Теоретические и методологические основы программирования 39 Якщо формули множини Н різ- нокванторні, то умова y∉{ xv , } із п.9 виконується гарантовано, тому її мож- на не вказувати. Для кожної формули ЛЕ-логіки можна збудувати (теорема 5) еквівале- нтну їй різнокванторну формулу. До- водиться [7], що застосування базових секвенційних форм зберігає умову різ- нокванторності. Згідно теореми 10, не обмежуючи загальності, будемо надалі вважати, що формули в секвенціях знаходяться в різнокванторній формі. Процедура пошуку виведення для секвенції Σ – це процедура побудови секвенційного дерева для Σ. Такі про- цедури для неокласичних секвенційних числень описані в [7, 8]. Розглянемо в загальних рисах процедуру побудови дерева для секвенції Σ з різноквантор- них формул, наведену в [8]. Вона при- датна як для скінченних, так і для злі- ченно-нескінченних секвенцій ЛЕ-логі- ки. Кожне застосування секвенційної форми проводиться до скінченної множини доступних формул. На поча- тку кожного етапу виконується крок доступу: до списку доступних формул додається по одній формулі з \|−-списку та −\|-списку. Якщо недоступних \|−-фор- мул чи −\|-формул немає (відповідний список вичерпаний), то на подальших кроках доступу додаємо по одній фор- мулі з невичерпаного списку. Зафіксу- ємо деякий нескінченний список TN тотально неістотних імен такий, що TN ∩ nm(Σ) = ∅. На початку побудови доступна лише пара перших формул списків (або єдина формула, якщо один із спи- сків порожній). Нехай виконано k ета- пів процедури. На етапі k+1 перевіряє- мо, чи буде кожен з листів дерева за- мкненою секвенцією. Якщо всі листи замкнені, то процедура завершена по- зитивно, отримане замкнене секвен- ційне дерево. Якщо ні, то для кожного незамкненого листа ξ робимо наступ- ний крок доступу, після чого добудову- ємо скінченне піддерево з вершиною ξ так. Активізуємо всі доступні непримі- тивні формули ξ. По черзі до кожної активної формули застосовуємо відпо- відну секвенційну форму. Перед засто- суванням однієї з форм \|−RR, \|−R¬, \|−R∨, \|−R∃ чи −\|RR, −\|R¬, −\|R∨, −\|R∃ усуваємо в разі наявності тотожні перейменуван- ня, застосовуючи допоміжні форми \|−RT та −\|RТ. При застосуванні −\|∃ мно- жина {z1, …, zт} складається з усіх не- кванторних імен доступних формул листа. При застосуванні \|−∃ беремо у як перше незадіяне на шляху від кореня до даного листа ім'я списку TN. Після застосування недопоміжної форми фо- рмула дезактивується. При побудові секвенційного де- рева можливі такі випадки: 1. Процедура завершена позити- вно, маємо скінченне замкнене дерево. 2. Процедура завершена негати- вно, маємо скінченне незамкнене де- рево. Тоді дерево має незамкнений лист, до якого жодна секвенційна фо- рма незастосовна, він складається тіль- ки з примітивних формул. Отже, в де- реві існує скінченний шлях Σ = Σ1, Σ2, …, Σп, всі вершини якого – незамкнені секвенції. Такий шлях назвемо неза- мкненим. 3. Процедура не завершується, маємо нескінченне дерево. За лемою Кеніга [9], в дереві існує нескінченний шлях Σ = Σ1, Σ2, …, Σп, …, всі вершини якого – незамкнені секвенції (при по- яві замкненої секвенції побудова шля- ху обривається). Такий шлях теж на- звемо незамкненим. Кожна з формул секвенції Σ зустрінеться на цьому шля- ху і стане доступною. Теорема 17. Нехай ℘ – незамк- нений шлях в секвенційному дереві, Н – множина всіх відмічених формул секвенцій цього шляху. Тоді Н – мо- дельна множина. Для переходу від нижчої верши- ни шляху до вищої використовується одна з базових секвенційних форм, але переходи згідно таких форм точно відповідають визначенню модельної множини. Теоретические и методологические основы программирования 40 Теорема 18. Нехай Н – модельна множина, W = nq(Н). Тоді існують АС А = (А, І) з \|А\| = \|W\| та ін'єктивна δ∈VA з im(δ) = W такі, що 1) з умови \|−Φ∈Н ви- пливає ΦА(δ) = Т; 2) з умови −\|Φ∈Н ви- пливає ΦА(δ) = F. Доведення теореми для випадку ЛЕ-числень аналогічне доведенню відпо- відної теореми для неокласичних чис- лень [7]. Візьмемо деяку множину А та- ку, що \|А\| = \|W\|, та ін'єктивну δ∈VA з im(δ) = W. Фактично А продубльовує множину W всіх предметних імен, що фігурують в Н. Задамо значення базо- вих предикатів на d∈WA, які продовжи- мо за еквітонністю на довільні h∈VA та- кі, що d ⊂ h. Якщо \|−р∈Н, то покладемо рА(δ) = Т ; якщо −\| р∈Н, то покладемо рА(δ) = F. Якщо \|− )( pRv x ∈Н, то покладемо рА(r )(δv x ) = Т; якщо −\| )( pRv x ∈Н, то покла- демо рА(r )(δv x ) = F. В усіх інших випад- ках d∈WA значення рА(d) задаємо довіль- ним чином, враховуючи обмеження: для всіх d, h∈WA таких, що d\|\|µ(p) = h\|\|µ(p), необхідно рА(d) = рА(h). Тоді значення рА задані однозначно, враховано неістот- ність для рА імен у∈µ(p). Отже, значен- ня базових предикатів визначені коре- ктно. Далі доводимо індукцією за скла- дністю формули згідно побудови моде- льної множини. Використовуючи теорему 18, отримаємо теореми повноти для секве- нційних ЛЕ-числень. Формулювання теорем повноти однакове для числень реномінативного та кванторного рівнів. Теорема 19. Нехай Γ \|= ∆. Тоді секвенція \|− Γ−\| ∆ вивідна. Припустимо супротивне: Γ \|= ∆ та секвенція \|− Γ−\| ∆ невивідна. Тоді секвен- ційне дерево для Σ = \|− Γ−\| ∆ незамкне- не. Отже, в ньому існує (скінченний чи нескінченний) незамкнений шлях ℘. Нехай Н – це множина всіх відміче- них формул секвенцій цього шляху. За теоремою 17, Н – модельна множина. За теоремою 18, існують АС А = (А, І) та δ∈VA такі: з \|−Φ∈Н випливає ΦА(δ) = Т та з −\|Φ∈Н випливає ΦА(δ) = F. Це, зокре- ма, вірно і для формул з Σ = \|− Γ−\| ∆ , бо Σ ⊆Н. Але це суперечить умові Γ \|= ∆. Для випадку ЛЕ-логік, як і для неокласичних логік, справджуються важливі властивості, що випливають з теореми повноти, зокрема принцип компактності. Доведення цих властиво- стей, проведені [8] для НКЛ, перено- сяться на випадок ЛЕ-логік. Висновки. Досліджені семантичні та синтаксичні властивості ЛЕ-логік реномінативного та кванторного рівнів. Вивчаються семантичні властивості відношення логічного наслідку для множин формул таких логік, пропону- ються та досліджуються аксіоматичні системи секвенційного типу – секвен- ційні ЛЕ-числення. На основі цих чис- лень пропонуються теореми повноти ЛЕ-логік реномінативного та квантор- ного рівнів. 1. Никитченко Н.С. Композиционно-номина- тивный подход к уточнению понятия про- граммы // Проблемы программирования. – 1999. – №1. – С. 16—31. 2. Нікітченко М.С., Шкільняк С.С. Компози- ційно-номінативні логіки еквітонних пре- дикатів // Вісник Київського ун-ту. Сер.: фіз.-мат. науки. – 2000. – Вип. 2. – С. 300—314. 3. Никитченко Н.С., Шкильняк С.С. Неоклас- сические логики предикатов // Проблемы программирования. – 2000. – № 3—4. – С. 3—17. 4. Шкільняк С.С. Нормальні форми в неокла- сичній логіці // Там же. – 2001, № 3—4. – С. 14—22. 5. Шкільняк С.С. Безкванторні неокласичні логіки // Вісник Київського ун-ту. Сер.: фіз.-мат. науки. – 2001. – Вип. 4. – С. 323—331. 6. Нікітченко М.С., Шкільняк С.С. Семантич- ні аспекти посткласичних логік // Про- блемы программирования. – 2001. – № 1—2. – С. 3—12. 7. Нікітченко М.С., Шкільняк С.С. Неокласич- ні логіки та секвенційні числення // Деп. в ДНТБ України 22.07.2002, № 114-Ук2002. – 46 с. 8. Шкільняк С.С. Неокласичні секвенційні чи- слення // Вісник Київського ун-ту. Сер.: фіз.-мат. науки. – 2002. – Вип. 4. – С. 261—274. Теоретические и методологические основы программирования 41 9. Клини С. Математическая логика. – М.: Наука, 1973. – 480 с. 10. Шенфилд Дж. Математическая логика. – М.: Наука, 1975. – 527 с. 11. Смирнова Е.Д. Логика и философия. – М.: РОССПЕН, 1996. – 304 с. 12. Непейвода Н.Н. Прикладная логика. – Но- восибирск: НГУ, 2000. – 521 с. Отримано 14.05.03 Про авторів Нікітченко Микола Степанович доктор фіз.-мат. наук, зав. кафедрою теорії програмування Шкільняк Степан Степанович канд. фіз.-мат. наук, доцент кафедри теорії програмування Місце роботи авторів: Київський національний університет ім. Тараса Шевченка вул. Володимирська, 60, Київ, Україна Тел. (044) 259 0519 E-mail: nikitchenko@unicyb.kiev.ua sssh@unicyb.kiev.ua

Logics of local equitone predicates: semantic properties and sequential calculuses

Institution

Ähnliche Einträge