Досліджено чисті першопорядкові логіки часткових і тотальних, однозначних і неоднозначних квазіарних предикатів. Описано семантичні моделі та мови таких логік, особливу увагу приділено вивченню композиційних предикатних алгебр та класів інтерпретацій (семантик), відношень логічного наслідку для множин формул. Для таких відношень побудовано низку числень секвенцій ного типу, характерною особливістю цих числень є розширені умови замкненості секвенції та оригінальні форми елімінації кванторів. Ключові слова: логіка, предикат, семантика, логічний наслідок, секвенційне числення. Исследованы чистые первопорядковые логики частичных и тотальных, однозначных и неоднозначных квазиарных предикатов. Описаны семантические модели и языки таких логик, особое внимание уделено изучению композиционных предикатных алгебр и классов интерпретаций (семантик), отношений логического следствия для множеств формул. Для таких отношений построен ряд исчислений секвенциального типа, характерными особенностями этих исчислений являются расширенные условия замкнутости секвенции и оригинальные формы элиминации кванторов. Ключевые слова: логика, предикат, семантика, логическое следствие, секвенциальное исчисление. Pure first-order logics of partial and total, single-valued and multi-valued quasiary predicates are investigated. For these logics we describe semantic models and languages, giving special attention in our research to composition algebras of predicates and interpretation classes (sematics), and logical consequence relations for sets of formulas. For the defined relations a number of sequent type calculi is constructed; their characteristic features are extended conditions for sequent closure and original forms for quantifier elimination.
ємо у вигляді [ v1 a a1,..., vn a an, ...], де vі∈V, aі∈A, vі ≠ vj при і ≠ j. Клас всіх V-A-ІМ позначаємо VA. Параметричну операцію реномінації rxv11,,......,,xvnn : VА → VA задаємо так: rxv11,,......,,xvnn (d ) = d ∇ [ v1 a d(x1),..., vn a (xn)]. Якщо параметри реномінації відсутні, маємо тотожну реномінацію r, вона діє як тотожне відображення: r(d) = d.
В подальшому викладі використаємо скорочення y для y1,..., yn . Замість rxv11,,......,,xvnn тоді можна писати rvx .
Послідовне застосування двох операцій rvx (зовнішня) та ruy (внутрішня) можна подати [
Під V-A-квазіарним предикатом будемо розуміти часткову неоднозначну, взагалі кажучи, функцію вигляду P : VA ® {T, F}. Тут {T, F} – множина істиннісних значень.
Ми трактуємо часткові неоднозначні квазіарні предикати як відношення між VA та {T, F}, такі предикати
названо [
T(P) = {d∈VA | T∈P(d)} та F(P) = {d∈VA | F∈P(d)}. Ім’я z∈V неістотне для V-A-квазіарного предиката P, якщо з умови d1║–х = d2║–х випливає P(d1) = P(d2). V-A-квазіарний предикат P: – однозначний, якщо T(P)∩F(P) = ∅; – тотальний, якщо T(P)∪F(P) = VA; – неспростовний (частково істинний), якщо F(P) = ∅; – виконуваний, якщо T(P) ≠ ∅; – тотально істинний, якщо T(P) = VА, тотально хибний, якщо F(P) = VА; – тотожно істинний, якщо T(P) = VА та F(P) = ∅, тотожно хибний, якщо T(P) = ∅ та F(P) = VА; – всюди невизначений, якщо T(P) = ∅ та F(P) = ∅; – тотально насичений (повне бінарне відношення), якщо T(P) = VА та F(P) = VА. Кожний неспростовний та кожний невиконуваний предикат є однозначними.
Часткові однозначні V-A-квазіарні предикати назвемо P-предикатами, тотальні – T-предикатами, тотальні однозначні – TS-предикатами. Класи таких предикатів відповідно позначаємо PrRVA , PrPAV , PrTAV , PrTSVA .
Всюди невизначений V-A-квазіарний предикат позначаємо як ⊥VA , тотожно істинний – як TAV , тотожно хибний – як FAV , тотально насичений – як
VA . Якщо V і А маються на увазі, ці предикати позначаємо ⊥, T, F, . Предикат P : VА→{T, F} монотонний, якщо з d ⊆ d' випливає P(d) ⊆ P(d'). Предикат P : VА → {T, F} антитонний, якщо з d ⊆ d' випливає P(d) ⊇ P(d'). Константні предикати ⊥, T, F, є монотонними й антитонними. Для однозначних предикатів монотонність стає еквітонністю. Однозначний предикат P : VА → {T, F} еквітонний, якщо з умови P(d)↓ та d ⊆ d' випливає P(d')↓ = P(d). Монотонні R-предикати, антитонні R-предикати, еквітонні P-предикати, антитоннi T-предикати будемо називати RM-предикатами, RА-предикатами, PE-предикатами, TА-предикатами. Класи V-A-квазіарних RM-предикатів, RА-предикатів, PE-предикатів, TА-предикатів позначимо відповідно PrRM VA , PrRAVA , PrPEVA , PrTAVA .
~ Предикат P назвемо дуальним до предиката P, якщо T (P% ) = F (P) та F (P%) = T (P) . доповнення до P як до реляції. Тоді T (P ) = T (P) та F (P ) = F (P) . Звідси T (P~) = F (P ); F (P~) = T (P ) . Для V-A-квазіарного предиката P, трактованого як реляція P ⊆ VА × Bool, можна розглядати предикат P – Прикладом пари взаємно дуальних та взаємно доповнених предикатів є ⊥ та .
~ ~ Твердження 1. Q монотонний ⇒ Q та Q антитонні; Q антитонний ⇒ Q та Q монотонні. Твердження 2. Q ∈ PrPAV ⇔ Q~ ∈ PrTAV ⇔ Q ∈ PrTAV ; Q ∈ PrTAV ⇔ Q~ ∈ PrPAV ⇔ Q ∈ PrPAV ; Q ∈ PrTSVA ⇔ Q ∈ PrTSVA ; Q ∈ PrTSVA ⇒ Q~ = Q . ~ Задамо відображення дуалізації δ : PrRVA → PrRVA наступним чином: δ (P) = P для кожного P ∈ PrRVA . Відображення дуалізації інволютивне: δ (δ (P)) = P для кожного P ∈ PrRVA .
Твердження 3. δ(T) = T, δ(F) = F, δ(⊥) = , δ( ) = ⊥, δ (PrPAV ) = PrTAV , δ (PrTAV ) = PrPAV , δ (PrTSVA ) = = PrTSVA , δ (PrPEVA ) = PrTAVA , δ (PrTAVA ) = PrTAVA , δ (PrRM VA ) = PrRAVA , δ (PrRM VA ) = PrRAVA . 2. Композиційні алгебри квазіарних предикатів Опишемо композиції квазіарних предикатів.
На пропозиційному рівні композиції працюють лише з виробленими предикатами істиннісними значеннями, їх називають логiчними зв’язками. Основними є 1-арна композиція заперечення ¬ та 2-арні композиції диз’юнкція ∨, кон’юнк ція &, імплікація →, еквіваленція ↔. Предикати ¬(P), ∨(P, Q), →(P, Q), &(P, Q), ↔(P, Q) далі традиційно позначаємо ¬P, P∨Q, P→Q, P&Q, P↔Q. Як базові пропозиційні композиції візьмемо ¬ та ∨. Предикати ¬P та P∨Q задамо через області істинності й хибності відповідних предикатів:
T(¬P) = F(P); T(P∨Q) = T(P)∪T(Q);
F(¬P) = T(P);
F(P∨Q) = (P)∩F(Q). Композиції →, &, ↔ є похідними, вони виражаються через ¬ та ∨: Твердження 4. Маємо P = ¬P% та P% = ¬P . Твердження 5. Для предикатів ⊥, , T, F маємо: 1) ¬ ⊥ = ⊥, ⊥ ∨ ⊥ = ⊥; ¬ = ,
∨ = ; 2) ¬T = F, ¬F = T, T ∨ T = T, T ∨ F = F ∨ T = T, F ∨ F = F;
P→Q = ¬P∨Q; P&Q = ¬(¬P ∨ ¬Q); P↔Q = (P→Q)&(Q→P). 3) T ∨ ⊥ = ⊥ ∨ T = T, F ∨ ⊥ = ⊥ ∨ F = ⊥; T ∨ = ∨ T = , F ∨ = ∨ F = ; ⊥ ∨ = ∨ ⊥ = T. На рівні ЧКНЛ до логiчних зв’язок додаємо композиції реномінації та квантифікації.
Параметричну композицію реномінації R vx : PrА → PrА задамо так: R vx (P)(d ) = P(rvx (d )) для кожного d∈VА.
Композиція R з відсутніми параметрами – тотожна реномінація, – діє як тотожне відображення: R(P) = P. Параметричну композицію квантифікації ∃x: PrА → PrА візьмемо як базову; задамо її через області істинності та хибності відповідного предиката ∃xP:
T(∃xP) = {d∈VA | d ∇ x a a ∈T(Р) для деякого a∈A};
F(∃xP) = {d∈VA | d ∇ x a a ∈F(Р) для всіх a∈A}. Композиція ∀х є похідною, вона задається такою умовою: ∀хР = ¬∃х¬Р. Композиції ¬, ∨, R vx , ∃x назвемо базовими композиціями ЧКНЛ. Твердження 6. 1) Для предикатів ⊥ та маємо: R vx (⊥) = ⊥, ∃x(⊥) = ⊥; R x ( ) = v , ∃x( =) ; 2) для предикатів T та F маємо: Rvx (T) = T, ∃x(T) = T; Rvx (F) = F, ∃x(F) = F . Теорема 1. Композиції ¬, ∨, R v , ∃x зберігають:
x 1) однозначність та тотальність квазіарних предикатів; 2) монотонність та антитонність квазіарних предикатів. Наслідок 1. 1) Mножини {⊥}, { }, {T, F}, {⊥, , T, F} замкнені відносно ¬, ∨, →, &, ↔, R vx , ∃x, ∀x; 2) класи P-предикатів, T-предикатів, TS-предикатів замкнені відносно ¬, ∨, →, &, ↔, R vx , ∃x, ∀x; 3) класи монотонних, антитонних, еквітонних предикатів замкнені відносно ¬, ∨, →, &, ↔, R vx , ∃x, ∀x. Композиційну алгебру QRVA = (PrRVA ,CQ) , де CQ = {¬, ∨, R vx , ∃x}, назвемо чистою першопорядковою алгеброю квазіарних предикатів.
Необхідна умова, щоб певний клас квазіарних предикатів утворив алгебру – його замкненість щодо операцій алгебри, у нашому випадку – щодо ¬, ∨, R vx , ∃x. Те, що ℵ є підалгеброю алгебри ℜ, позначатимемо ℵ p ℜ. Таким чином, можна виділити низку підалгебр алгебри QRVA : QPAV = (PrPAV ,CQ) – алгебра P-предикатів; QTAV = (PrTAV ,CQ) – алгебра T-предикатів; QTSVA = (PrTSVA ,CQ) – алгебра TS-предикатів; маємо QTSVA p QPAV та QTSVA p QTAV ; QRM VA = (PrRM VA ,CQ) – алгебра монотонних R-предикатів; QRAVA = (PrRAVA ,CQ) – алгебра антитонних R-предикатів; QPEVA = (PrPEVA ,CQ) – алгебра еквітонних P-предикатів; маємо QPEVA p QPAV та QPEVA p QRM VA ; QTAVA = (PrTAVA ,CQ) – алгебра антитонних T-предикатів; маємо QTAVA p QTAV та QTAVA p QRAVA ; сингулярні алгебри ⊥V-A = ({⊥VA},CQ) та V-A = ({ VA},CQ); для них маємо ⊥V-A p QPEVA та V-A p QTAVA ; алгебра BV-A = ({TAV , FAV },CQ); маємо BV-A p QTSVA , BV-A p QPEVA , BV-A p QTAVA ; алгебра BLV-A = ({⊥VA, VA,TAV , FAV },CQ); тоді BLV-A p QRM VA , BLV-A p QRAVA , а також ⊥V-A, V-A, BV-A p BLV-A . Нехай δ – відображення дуалізації. Алгебри (Pr1, CQ) і (Pr2 ,CQ) дуальні, якщо δ(Pr1) = Pr2 та δ(Pr2) = Pr1. Отже, маємо пари дуальних алгебр QPAV та QTAV , QPEVA та QTAVA , QRM VA та QRAVA , ⊥V-A та V-A . Алгебри QRVA , QTSVA , BV-A , BLV-A автодуальні.
Властивості квазіарних предикатів та їх композицій описано в [
R) R(P) = P – тотожна реномінація.
RI) R zz,,vx (P) = R vx (P) – згортка пари тотожних імен.
RU) Нехай z∈V неістотне для предиката P. Тоді R zy,,vx (P) = R vx (P) . Згортку R vx owy композицій R vx і R wy задаємо так: R vx (R wy (P))(d ) = R vx owy (P)(d ) = P(r wy •vx (d )) . Звідси: RR) R vx (R wy (P)) = R vx owy (P) . Опишемо взаємодію реномінацій та логічних зв’язок і кванторів.
Ren) ∃yP = ∃zR zy (P) за умови z неістотне для P – перейменування кванторного імені.
R¬) R vx (¬P) = ¬R vx (P) – R¬-дистрибутивність.
R∨) R vx (P ∨ Q) = R vx (P) ∨ R vx (Q) – R∨-дистрибутивність. R∃s) R vx (∃yP) = ∃yR vx (P), якщо y ∉{v, x} – проста (обмежена) R∃-дистрибутивність.
R∃) R vx (∃yP) = ∃zR vx o zy (P), якщо z неістотне для P та z ∉{v, x} – R∃-дистрибутивність. T (R uv,,yx (P)) ∩ T(Ey) ⊆ T (R uv (∃xP)) ; зокрема, T (R xy (P)) ∩ T(Ey) ⊆ T(∃xР); F (R uv (∃xP)) ∩ T(Ey) ⊆ F (R uv,,yx (P)) ; зокрема, F(∃xР) ∩ T(Ey) ⊆ F (R xy (P)); T (R uv,,yx (P)) ⊆ F(Ey) ∪ T (R uv (∃xP)) ; зокрема, T (R xy (P)) ⊆ F(Ey) ∪ T(∃xР);
F (R uv (∃xP)) ⊆ F(Ey) ∪ F (R uv,,yx (P)) ; зокрема, F(∃xР) ⊆ F(Ey) ∪ F (R xy (P)) . 3. Мови та семантичні моделі ЧКНЛ
Семантичними моделями ЧКНЛ є [
Алфавiт мови ЧКНЛ: множина V предметних імен (змінних), в якій виділена множина U ⊆ V тотально
неістотних [
Для зручності далі використовуємо скоро чення формул (див. [
Позначимо nm(Φ) множину тих x∈V, які фігурують у символах реномінації та квантифікації формули Φ. Інтерпретуємо мову на композицій них системах (VA, Pr, CQ). Iмена x∈V позначають елементи множини базових даних A, символи композицій – композиції із CQ. Символи Рs позначають базові предикати в множині Pr, для опису цього позначення задамо тотальне однозначне відображення I : Ps → Pr. Із базових предикатів за допомогою композицій будуємо складніші, які позначаються формулами. Відображення інтерпретації формул I : Fr → Pr задамо як розширення I : Ps → Pr згідно побудови формул із простіших за допомогою символів Cs:
IF) I(¬Φ) = ¬(I(Φ)), I(∨ΦΨ) = ∨(I(Φ), I(Ψ)), I (Rxv (Φ)) = R vx (I (Φ)); I(∃xΦ) = ∃x(I(Φ)).
Трійку J = (CS, Σ, I) назвемо інтерпретацією мови ЧКНЛ сигнатури Σ. Iнтерпретації будемо скорочено
позначати (A, I). Предикат J(Φ) – значення формули Φ при інтерпретації J – позначимо ΦJ.
Ім’я x∈V неістотне для формули Φ, якщо для кожної інтерпретації J ім’я x неістотне для предиката ΦJ.
Визначимо для формул множини гарантовано неістотних імен за допомогою відображення ν : Fr→2V так.
Для р∈Ps візьмемо ν(р) = U, а далі [
Φ∈Γ Виділення підалгебр квазіарних предикатів виділяє відповідні класи інтерпретацій. Можна говорити про загальний клас R-інтерпретацій та підкласи P-інтерпретацій, T-інтерпретацій, TS-інтерпретацій, а також Теорема 3. TS ⊂ P ⊂ R, TS ⊂ T ⊂ R, PE ⊂ RM ⊂ R, TA ⊂ RA ⊂ R, PE ⊂ P, TA ⊂ T . Відображення дуалізації δ продовжимо на класи інтерпретацій.
Інтерпретацію δ(J) = (A, Iδ) назвемо дуальною до інтерпретації J = (A, I), якщо для кожного p∈Ps маємо
тиннiсна оцiнка мови – це тотальне відображення τ : Fr0 →{T, F}. Продовжимо τ до відображення τ : Fr →{T, F}
згідно дії ¬ та ∨ на предикати (див. [
Нехай Φ утворена із пропозиційно нерозкладних формул ϕ1, …, ϕn. Нехай TS|≠id Φ, тоді Φ(d) = F для деяких J = (A, I) ∈TS та d∈VA. Візьмемо істиннiсну оцiнку τ: τ(ϕi) = ϕiJ(d). Тоді τ(Φ) = F, тому Φ не тавтологія. Наслідок 2. Пропозиційна формула Φ є тавтологія ⇔ TS|=id Φ ⇔ P|= Φ ⇔ T|≡ Φ. 1) Істиннісний, або T-наслідок J|=T : Φ J|=T Ψ ⇔ T(ΦJ) ⊆ T(ΨJ). 2) Хибнісний, або F-наслідок J|=F : Φ J|=F Ψ ⇔ F(ΨJ) ⊆ F(ΦJ). 3) Cильний, або TF-наслідок J|=TF : Φ J|=TF Ψ ⇔ T(ΦJ) ⊆ T(ΨJ) та F(ΨJ) ⊆ F(ΦJ). 4) Неспростовнісний, або IR-наслідок J|=IR : Φ J|=IR Ψ ⇔ T(ΦJ)∩F(ΨJ) = ∅. 5) Дуальний до IR, або DI-наслідок J|=DI : Φ J|=DI Ψ ⇔ F(ΦJ)∪T(ΨJ) = VA. Відповідні відношення логічного наслідку в семантиці α визначаємо за схемою:
Φ α|=∗ Ψ, якщо Φ J|=∗ Ψ для кожної J∈α.
Зазначені відношення описано в [
Вони продукують відповідні відношення логічного наслідку, нетривіальними та відмінними від інших є
P|=T∨F та R|=С . Проте P|=T∨F та R|=С нетранзитивні, для них невірні деякі властивості декомпозиції формул (про це
нижче). С-наслідок для пропозиційної логіки розглядався в [
У випадках класичної логіки та логіки TS-предикатів усі наведені відношення логічного наслідку
втрачають відмінності, вони збігаються і стають єдиним відношенням, яке позначимо TS|= . Отже:
Твердження 10. TS|=TF = TS|=T = TS|=F = TS|=IR = TS|=DI = TS|=C = TS|=T∨F = TS|=.
Для запропонованих відношень маємо такі властивості (доведення див. [
P|=IR, P|=T∨F, P|=T, P|=F, P|=TF, R|=С, R|=TF.
Розглянемо питання, пов’язані з транзитивністю розглянутих відношень.
Твердження 11. Відношення J|=T, J|=F, J|=TF та відношення P|=T, P|=F, P|=TF, R|=TF є транзитивними.
Відношення наслідку A|=IR нетранзитивне. Справді, маємо
Приклад 1. Нехай A∈P, p, q, s∈Ps. Задамо pA як T, qA як ⊥, sA як F. Тоді p A|=IR q, q A|=IR s, проте p A|≠IR s.
Водночас для відношення логічного наслідку P|=IR ситуація нормалізується (див. [
Теорема 14. Нехай Φ' отримано з формули Φ заміною деяких входжень Φ1, ..., Φn на Ψ1, ..., Ψn. Якщо Φ1 α∼∗ Ψ1, ..., Φn α∼∗ Ψn, то Φ α∼∗ Φ'.
Властивості квазіарних предикатів індукують відповідні семантичні властивості формул (див. [
RU) Ryz,,vx (Φ) ∼ Rxv (Φ) за умови z∈ν(Φ).
RR) Rxv (Ryw (Φ)) ∼ Rxv o wy (Φ) .
R¬) Rxv (¬Φ) ∼ ¬Rxv (Φ) .
R∨) Rxv (Φ ∨ Ψ) ∼ Rxv (Φ) ∨ Rxv (Ψ) .
R∃s) Ruv (∃xΦ) ∼ ∃xRuv (Φ) за умови x ∉{v ,u} – проста (обмежена) R∃-дистрибутивність. R∃) Rxv (∃yΦ) ∼ ∃zRxv ozy (Φ) за умови z ∈ fu(Rxv (∃xΦ)) . 5. Відношення логічного наслідку для множин формул
Відношення логічного наслідку поширимо на пари множин формул. Спочатку задамо відношення наслідку між двома множинами формул при фіксованій інтерпретації J. Нехай Γ⊆ Fr, Δ ⊆ Fr. Введемо позначення IT (Φ J ) як T∧(ΓJ), I F (ΨJ ) як F∧ΔJ), UT (ΨJ ) як T∨(ΔJ), U F (Φ J ) як F∨(ΓJ). Φ∈Γ Ψ∈Δ Ψ∈Δ Φ∈Γ Δ є T-наслідком Γ при J (позн. Γ J|=T Δ), якщо T∧(ΓJ) ⊆ T∨(ΔJ). Δ є F-наслідком Γ при J (позн. Γ J|=F Δ), якщо F∧(ΔJ) ⊆ F∨(ΓJ). Δ є TF-наслідком Γ при J (позн. Γ J|=TF Δ), якщо T∧(ΓJ) ⊆ T∨(ΔJ) та F∧(ΔJ) ⊆ F∨(ΓJ). Δ є IR-наслідком Γ при J (позн. Γ J|=ID Δ), якщо T∧(ΓJ) ∩ F∧(ΔJ) = ∅. Δ є DI-наслідком Γ при J (позн. Γ J|=DI Δ), якщо F∨(ΓJ) ∪ T∨(ΔJ) = VA. Δ є С-наслідком Γ при J (позн. Γ J|=С Δ), якщо T∧(ΓJ) ∩ F∧(ΔJ) ⊆ F∨(ΓJ) ∪ T∨(ΔJ). Δ є T∨F-наслідком Γ при J (позн. Γ J|=TF Δ), якщо T∧(ΓJ) ⊆ T∨(ΔJ) або F∧(ΔJ) ⊆ F∨(ΓJ). Відповідні відношення логічного наслідку для множин формул в семантиці α визначаємо за схемою: Γ α|=∗ Δ, якщо Γ J|=∗ Δ для кожної J∈α. Наведемо характерні властивості відношень логічного наслідку для множин формул. Теорема 15 Нехай інтерпретації J та ϑ дуальні. Тоді: 1) Γ J|=IR Δ ⇔ Γ ϑ|=DI Δ та Γ J|=DI Δ ⇔ Γ ϑ|=IR Δ; 2) Γ J|=T Δ ⇔ Γ ϑ|=F Δ та Γ J|=F Δ ⇔ Γ ϑ|=T Δ; 3) Γ J|=TF Δ ⇔ Γ ϑ|=TF Δ; 4) Γ J|=С Δ ⇔ Γ ϑ|=С Δ; Γ J|=T∨F Δ ⇔ Γ ϑ|=T∨F Δ; Із наведених відношень логічного наслідку для множин формул лише 7 різних. Виділимо ці відношення:
P|=IR, P|=T∨F, P|=T, P|=F, P|=TF, R|=С, R|=TF .
Відношення наслідку та логічного наслідку для множин формул рефлексивні й нетранзитивні [
Теорема 16. ∅ P|=C Φ ⇔ ∅ P|=IR Φ ⇔ ∅ P|=F Φ ⇔ ∅ T|=C Φ ⇔ ∅ T|=DI Φ ⇔ ∅ T|=T Φ ⇔ P|= Φ ⇔ T|≡ Φ; Φ P|=C ∅ ⇔ Φ P|=IR ∅ ⇔ Φ P|=F ∅ ⇔ Φ T|=C ∅ ⇔ Φ T|=DI ∅ ⇔ Φ T|=T ∅ ⇔ P|= ¬Φ ⇔ T|≡ ¬Φ. Розглянемо можливість перенесення формули з лівої частини логічного наслідку в праву і навпаки. Теорема 17. 1) Γ P|=IR Δ, Φ ⇔ ¬Φ, Γ P|=IR Δ та Γ P|=IR Δ, ¬Φ ⇔ Φ, Γ P|=IR Δ; 2) Γ R|=С Δ, Φ ⇔ ¬Φ, Γ R|=С Δ та Γ R|=С Δ, ¬Φ ⇔ Φ, Γ R|=С Δ; Теорема 18. Можливі такі ситуації: 1) ¬Φ, Γ P|=T Δ та Γ P|≠T Δ, Φ; Φ, Γ P|=T Δ та Γ P|≠T Δ, ¬Φ; 2) Γ P|=F Δ, ¬Φ та Φ, Γ P|≠F Δ; Γ P|=F Δ, Φ та ¬Φ, Γ P|≠F Δ; 3) ¬Φ, Γ P|=TF Δ та Γ P|≠TF Δ, Φ; Γ P|=TF Δ, ¬Φ та Φ, Γ P|≠TF Δ; 4) ¬Φ, Γ R|=TF Δ та Γ R|≠TF Δ, Φ; Γ R|=TF Δ, ¬Φ та Φ, Γ R|≠TF Δ; 5) ¬Φ, Γ P|=T∨F Δ та Γ P|≠T∨F Δ, Φ; Γ P|=T∨F Δ, ¬Φ та Φ, Γ P|≠T∨F Δ.
Отже, для P|=IR та R|=С можна робити перенесення формули з лівої частини логічного наслідку в праву і навпаки; для P|=T, P|=F, P|=TF, P|=T∨F, R|=TF – не можна.
Теорема 19. 1) ¬Φ, Φ, Γ P|=T Δ, Γ P|=F Δ, ¬Ψ, Ψ, ¬Φ, Φ, Γ P|=TF Δ, ¬Ψ, Ψ;
2) ¬Φ, Φ, Γ P|≠F Δ; Γ P|≠T Δ, ¬Ψ, Ψ; ¬Φ, Φ, Γ R|≠TF Δ, ¬Ψ, Ψ.
У випадку відношень для множин формул R|=С зводиться до R|=TF (тут позначення ¬Σ для {¬Φ | Φ∈Σ}).
Теорема 20. Маємо Γ R|=С Δ ⇔ ¬Δ, Γ R|=TF Δ, ¬Γ.
Аналогом теореми еквівалентності для множин формул є теорема заміни еквівалентних.
Теорема 21. Нехай Φ α∼∗ Ψ, тоді маємо: Φ, Γ α|=∗ Δ ⇔ Ψ, Γ α|=∗ Δ; Γ α|=∗ Δ, Φ ⇔ Γ α|=∗|= Δ, Ψ.
Тут α∼∗ та α|=∗ – це відповідно R∼TF, P∼TF, P∼IR та R|=∼TF, P|=∼TF, P|=∼IR .
Розглянемо властивості відношень логічного наслідку для множин формул на пропозиційному рівні.
Маємо [
Для всіх зазначених відношень маємо монотонність: якщо Γ ⊆ Λ та Δ ⊆ Σ, то Γ |= Δ ⇒Λ |= Σ. Розглянемо властивості, які гарантують наявність логічного наслідку. Для кожного з відношень маємо: С) Φ, Γ |= Δ, Φ. Додатково гарантують наявність відповідного відношення логічного наслідку такі властивості СL) Φ, ¬Φ, Γ P|=T Δ; СR) Γ P|=F Δ, Φ, ¬Φ; СLR) Φ, ¬Φ, Γ P|=TF Δ, Ψ, ¬Ψ.
B силу ¬L та ¬R явне виділення таких властивостей зайве для відношень P|=IR та R|=С .
Наведемо властивості, пов'язані з реномінацією та кванторами. Вони отримуються на основі наведених вище властивостей R, RI, RU, RR, R¬, R∨, R∃s, R∃. Кожна така властивість R∗ продукує 4 відповідні властивості R∗L, R∗R, ¬R∗L, ¬R∗R для відношення логічного наслідку, коли виділена формула чи її заперечення знаходиться у лівій чи правій частині цього відношення. Наведемо для прикладу властивості, індуковані R∃s та R∃.
R∃sR) Γ |= Δ, Rxv (∃yΦ) ⇔ Γ |= Δ, ∃yRxv (Φ) за умови у∉{ v , x }. ¬R∃sL) ¬Rxv (∃yΦ), Γ |= Δ ⇔ ¬∃yRxv (Φ), Γ |= Δ за умови у∉{ v , x }. ¬R∃sR) Γ |= Δ, ¬Rxv (∃yΦ) ⇔ Γ |= Δ, ¬∃yRxv (Φ) за умови у∉{ v , x }.
R∃L) Rxv (∃yΦ), Γ |= Δ ⇔ ∃zRxv ozy (Φ), Γ |= Δ за умови z ∈ fu(Rxv (∃xΦ)) .
R∃R) Γ |= Δ, Rxv (∃yΦ) ⇔ Γ |= Δ, ∃zRxv ozy (Φ) за умови z ∈ fu(Rxv (∃xΦ)) . ¬R∃L) ¬Rxv (∃yΦ), Γ |= Δ ⇔ ¬∃zRxv ozy (Φ), Γ |= Δ за умови z ∈ fu(Rxv (∃xΦ)) . ¬R∃R) Γ |= Δ, ¬Rxv (∃yΦ) ⇔ Γ |= Δ, ¬∃zRxv ozy (Φ) за умови z ∈ fu(Rxv (∃xΦ)) . Наведемо властивості елімінації кванторів. Такі властивості базуються на теоремі 2. ∃L) ∃хΦ, Γ |= Δ ⇔ Rzx (Φ), Ez, Γ |= Δ за умови z∈fu(Γ, Δ, ∃хΦ)). ¬∃R) Γ |= ¬∃хΦ, Δ ⇔ Γ, Ez |= ¬Rzx (Φ), Δ за умови z∈fu(Γ, Δ, ∃хΦ)). ∃vR) Γ, Ey |= ∃хΦ, Δ ⇔ Γ, Ey |= ∃xΦ, Ryx (Φ), Δ . ¬∃vL) ¬∃хΦ, Ey, Γ |= Δ ⇔ ¬∃xΦ, ¬Ryx (Φ), Ey, Γ |= Δ. Для |=IR в силу ¬L та ¬R властивості вигляду ¬∗ із запереченням виділеної формули є похідними. Bластивості E-розподілу та первісного означення: Ed) Γ |= Δ ⇔ Ey, Γ |= Δ та Γ |= Δ, Ey.
Ev) Γ |= Δ ⇔ Ez, Γ |= Δ за умови z∈fu(Γ, Δ). 6. Секвенційні числення ЧКНЛ
Секвенційні числення формалізують відношення логічного наслідку для множин формул. Як і в роботах
[
В цій роботі не розглядаємо секвенційні числення логік еквітонних і антитонних предикатів, такі
числення описано в [
Секвенція Σ вивідна (має виведення), якщо існує замкнене секвенційне дерево з коренем Σ. Таке дерево називають виведенням секвенції Σ. Секвенційне дерево замкнене, якщо кожний його лист – замкнена секвенція.
Замкнені секвенції є аксіомами секвенційного числення. Правилами виведення секвенційних числень є секвенційні форми, вони є синтаксичними аналогами властивостей відношень логічного наслідку.
Замкненість секвенції |–Γ–|Δ означає, що Γ |= Δ. Тому умови, які гарантують наявність логічного наслідку, індукують відповідні умови замкненості секвенції. Для опису таких умов введемо наступні визначення.
Для множини специфікованих формул (секвенції) |–Γ–|Δ задамо множини означених та неозначених предметних імен, або множини val-змінних та unv-змінних: val(|–Γ–|Δ) = {x∈V | Ex∈Γ}; unv(|–Γ–|Δ) = {x∈V | Ex∈Δ}. Множину нерозподілених для |–Γ–|Δ імен введемо так: ud(|–Γ–|Δ) = nm(Γ∪Δ) \ (val(|–Γ–|Δ) ∪ unv(|–Γ–|Δ)). Формули вигляду Ryx (Φ) назвемо R-формулами. Rs-формою R-формули Rxx,,yu,,zv (Φ), де {u} ⊆ ν(Φ) , назвемо R-формулу Rzv (Φ) , утворену із Rxx,,yu,,zv (Φ) всеможливими спрощенням зовнішньої реномінації на основі вла стивостей R, RI, RU (застосування R дає Rs-форму Φ, яка може не бути R-формулою). Властивості R, RI, RU гарантують: якщо Ψ та ϑ мають однакові Rs-форми, то T(ΨJ) = T(ϑJ) та F(ΨJ) = F(ϑJ) для всіх інтерпретацій J.
Нехай Un ⊆ V – множина імен, трактованих як неозначені, а символ ε∉V позначає відсутність значення. Нехай R-формула Rsr,,yx,,vu Φ така: {r , s , y} ⊆ Un, {x, v}∩Un = ∅ . Un-форма формули Rsr,,yx,,vu Φ – це вираз Rεx,,vu Φ . Для формули Ψ, яка не є R-формулою, її Un-форма збігається із Ψ.
R-формули Ψ та Ξ назвемо Rs-Un-еквівалентними, якщо Ψ та Ξ мають однакові Rs-форми або ці Rsформи мають однакові Un-форми. Кожна R-формула Rs-Un-еквівалентна сама собій (рефлексивність). Якщо R-формули Ψ та Ξ Rs-Un-еквівалентні, то ¬Ψ та ¬Ξ теж назвемо Rs-Un-еквівалентними. Твердження 13. Якщо формули Ψ та Ξ Rs-Un-еквівалентні, то для кожнoї інтерпретації J маємо: T(ΨJ) ∩ V\UnA = T(ΞJ) ∩ V\UnA та F(ΨJ) ∩ V\UnA = F(ΞJ) ∩ V\UnA. (тут |= – одне з P|=IR, P|=T, P|=F, P|=TF, R|=TF ); 2) нехай формули Ψ та Ξ – Rs-Un-еквівалентні, тоді Ψ, ¬Ξ, Γ P|=T Δ; зокрема, Φ, ¬Φ, Γ P|=T Δ; 3) нехай формули Ψ та Ξ – Rs-Un-еквівалентні, тоді Γ P|=F Ψ, ¬Ξ, Δ; зокрема, Γ P|=F Φ, ¬Φ, Δ;
Теорема 23 обґрунтовує наведені нижче умови замкненості секвенції |–Γ–|Δ із множиною unv-змінних Un. Базова умова замкненості індукована властивістю С: С) існують Rs-Un-еквівалентні формули Ψ та Ξ такі: Ψ∈Γ та Ξ∈Δ; зокрема, якщо існує Φ: Φ∈Γ та Φ∈Δ. Властивості СL, СR, СLR, які істотні для відношень P|=T, P|=F, P|=TF, індукують додаткові умови СL, СR, СLR замкненості секвенції |–Γ–|Δ: СL) існують Rs-Un-еквівалентні R-формули Ψ та Ξ такі: Ψ∈Γ та ¬Ξ∈Δ; зокрема, якщо існує формула Φ: Φ∈Γ та ¬Φ∈Γ; СR) існують Rs-Un-еквівалентні R-формули Ψ та Ξ такі: Ψ∈Δ та ¬Ξ∈Δ; зокрема, якщо існує формула Φ: Φ∈Δ та ¬Φ∈Δ; СLR) існують Rs-Un-еквівалентні R-формули ϕ, ξ та Rs-Un-еквівалентні R-формули θ, ω такі: ϕ∈Γ, ¬ξ∈Γ, θ∈Δ, ¬ω∈Δ; зокрема, якщо існують формули Φ та Ψ такі: Φ∈Γ, ¬Φ∈Γ, Ψ∈Δ, ¬Ψ∈Δ. Зрозуміло, що СLR ⇔ СL та СR. У випадку числень для відношення P|=IR умови СL, СR, СLR зводяться до С. Секвенційне числення задається базовими секвенційними формами і умовами замкненості секвенції. Опишемо числення, які будемо називати базовими секвенційними численнями ЧКНЛ. Числення QBG формалізує відношення R|=TF. Умова замкненості секвенції: C. Числення QBLR формалізує відношення |=TF. Умова замкненості секвенції: C ∨ CLR. Числення QBL формалізує відношення |=T. Умова замкненості секвенції: C ∨ CL. Числення QBR формалізує відношення |=F. Умова замкненості секвенції: C ∨ CR. Числення QBC формалізує відношення |=IR. Умова замкненості секвенції: C. Числення QBG, QBLR, QBL, QBR мають однакові базові секвенційні форми. Опишемо ці форми. Форми еквівалентних перетворень |–RR, –|RR, |–¬RR, –|¬RR, |–R¬, –|R¬, |–¬R¬, –|¬R¬, |–R∨, –|R∨, |–¬R∨, –|¬R∨, |–R∃s, –|R∃s, |–¬R∃s, –|¬R∃s, |–R∃, –|R∃, |–¬R∃, –|¬R∃ індукуються відповідними властивостями відношення логічного наслідку RRL, RRR, ¬RRL, ¬RRR, R¬L, R¬R, ¬R¬L, ¬R¬R, R∨L, R∨R, ¬R∨L, ¬R∨R, R∃sL, R∃sR, ¬R∃sL, ¬R∃sR, R∃L, R∃R, ¬R∃L, ¬R∃R, які в свою чергу продукуються властивостями RR, R¬, R∨, R∃s, R∃. Наведемо для прикладу форми |–RR, –|¬R∨, |–R∃s, –|R∃: Форми декомпозиції індукуються відповідними властивостями ¬¬L, ¬¬R, ∨L, ∨R, ¬∨L, ¬∨R : |–RR |− Rxv owy (Φ),Σ ;
|− Rxv (Ryw (Φ)),Σ |–R∃s |− ∃yRxv (Φ),Σ , де у∉{ v , x };
|− Rxv (∃yΦ),Σ |−¬¬ Форми елімінації кванторів та E-розподілу: |−¬∨ |− ¬Φ, |−¬Ψ, Σ ;
|− ¬(Φ ∨ Ψ), Σ |−∃ |− Rzx (Φ), |− Ez, Σ
; |− ∃xΦ, Σ |−¬∃v |− ¬∃xΦ, |− Ey, |− Ryx (Φ), Σ
; |− ¬∃xΦ, |− Ey, Σ |–RI |− Rxv (Φ),Σ ;
|− Rzz,,xv (Φ),Σ |−¬
Базовими формами числення QBС є |–RR, –|RR, |–R¬, –|R¬, |–R∨, –|R∨, |–R∃s, –|R∃s, |–R∃, –|R∃, |−∨, −|∨, |−∃, −|∃v, Ed, до яких додаємо |−¬ та −| ¬. Допоміжнi форми спрощення: |–R, –|R, |–RI, –|RI, |–RU, –|RU. Форми |−¬ та −| ¬ такі: −|¬∨ −|¬Φ, Σ −|¬(Φ ∨ Ψ), Σ −|¬Ψ, Σ
. −|¬∃ −|¬Rzx (Φ), |− Ez, Σ
; −|¬∃xΦ, Σ −|∃v −|∃xΦ,| − Ey, −| Ryx (Φ), Σ
.
−|∃xΦ, |− Ey, Σ –|¬RU −| ¬Ruv (Φ),Σ −| ¬Rzy,,uv (Φ),Σ
, де у∈ν(Φ); −| ¬ Теорема 24. 1. Нехай |− Λ−|Κ – базова форма; тоді: a) Λ |= Κ ⇔ Γ |= Δ; b) Γ |≠ Δ ⇔ Λ |≠ Κ.
|− Γ−|Δ 2. Нехай |− Λ−|Κ |− Γ−|Δ |−Χ−|Ζ
– базова форма; тоді: a) Λ |=∗ Κ та Χ |=∗ Ζ ⇔ Γ |=∗ Δ; b) Γ |≠∗ Δ ⇔ Λ |≠∗ Κ або Χ |≠∗ Ζ.
Для кожного з пропонованих числень, що формалізує відповідне відношення логічного наслідку, вірні
теореми коректності та повноти. Для доведення повноти пропонованих секвенційних числень використовуємо
метод модельних множин (подібні доведення див., напр., [
Теорема 25 (коректності та повноти). Γ |= Δ ⇔ секвенція |– Γ–| Δ вивідна. Висновки
Досліджено семантичні та синтаксичні аспекти композиційно-номінативних логік. Розглянуто класи чистих першопорядкових логік часткових і тотальних, однозначних і неоднозначних квазіарних предикатів. Описа но семантичні моделі та мови таких логік, особливу увагу приділено вивченню композиційних предикатних алгебр та класів інтерпретацій (семантик). Виділено низку підалгебр першопорядкової алгебри квазіарних предикатів, описано відповідні семантики. Розглянуто відношення логічного наслідку для множин формул, досліджено їх властивості. Для таких відношень запропоновано низку числень секвенційного типу. Характерна осо бливість цих числень – розширені умови замкненості секвенції та оригінальні форми елімінації кванторів. По дібні дослідження планується продовжити для першопорядкових композиційнономінативних логік з рівністю. 4. Нікітченко М.С. , Шкільняк С.С. Композиційно-номінативні логіки квазіарних предикатів: семантичні аспекти // Вісник Київського національного університету імені Тараса Шевченка. – Серія: фіз.-мат. науки. – 2012. – Вип. 4. – C. 165–172. 5. Нікітченко М.С. , Шкільняк О.С. , Шкільняк С.С. Першопорядкові композиційно-номінативні логіки із узагальненими реномінаціями // Проблеми програмування. – 2014. – № 2–3. – C. 17–28. 6. Nikitchenko М., Shkilniak S. Semantic Properties of Logics of Quasiary Predicates // Workshop on Foundations of Informatics: Proceedings FOI2015. – Chisinau, Moldova. – P. 180–197. 7. Нікітченко М.С., Шкільняк С.С. Алгебри квазіарних та бі-квазіарних реляцій // Проблеми програмування. – 2016. – № 1. – C. 17–28. 8. Шкільняк С.С. Спектр секвенційних числень першопорядкових композиційно-номінативних логік // Проблеми програмування. – 2013, № 3. – C. 22–37. 9. Шкільняк С.С. Секвенційні системи логічного виведення першопорядкових логік часткових предикатів // Компьютерная математика. – 2013, Вып. 2. – C. 88–96. 10. Нікітченко М.С. , Шкільняк О.С. , Шкільняк С.С. Відношення логічного наслідку в логіках квазіарних предикатів // Проблеми програмування. – 2016. – № 1. – C. 13–25. 11. Смирнова Е.Д. Логика и философия. – М.: РОССПЕН, 1996. – 304 с.