Досліджено безкванторні композиційно-номінативні логіки часткових квазіарних предикатів. Виділено такі рівні цих логік: реномінативний, реномінативний з предикатами слабкої рівності, реномінативний з предикатами строгої рівності, безкванторно-функціональний, безкванторно-функціональний з композицією слабкої рівності, безкванторно-функціональний з композицією строгої рівності. Основна увага приділена логікам безкванторно-функціональних рівнів з рівністю. Описано мови та семантичні моделі безкванторних логік, досліджено їх семантичні властивості, зокрема, властивості відношень логічного наслідку для множин формул. Ключові слова: безкванторна логіка, предикат, реномінація, суперпозиція, рівність, логічний наслідок. Исследованы бескванторные композиционно-номинативные логики частичных квазиарных предикатов. Выделены такие уровни этих логик: реноминативный, реноминативный с предикатами слабого равенства, реноминативный с предикатами строгого равенства, бескванторно-функциональный, бескванторно-функциональный с композицией слабого равенства, бескванторно-функциональный с композицией строгого равенства. Основное внимание уделено логикам бескванторно-функциональных уровней с равенством. Описаны язики и семантические модели бескванторных логик, исследованы их семантические свойства, в частности, свойства отношений логического следствия для множеств формул. Ключевые слова: бескванторная логика, предикат, реноминация, суперпозиция, равенство, логическое следствие. Free-quantifier composition nominative logics of partial quasiary predicates are considered. We specify the following levels of these logics: renominative, renominative with predicates of weak equality, renominative with predicates of strong equality, free-quantifier, free-quantifier with composition of weak equality, free-quantifier with composition of strong equality. The paper is mainly dedicated to investigation of logics of free-quantifier levels with equality. Languages and semantic models of such logics are described, their semantic properties are studied, in particular the properties of relations of logical consequence.
Можна виділити такі рівні безкванторних логік квазіарних предикатів: Для V-A-ІМ операцію ||−Х , де X ⊆ V , задаємо так: d ||− Х = {v a a ∈ d | v ∉ X } . Операцію ∇ накладки V-A-ІМ h на V-A-ІМ d визначаємо так: d∇h = d ||−asn(h) ∪h . Операцію реномінації rxv11,,......,,xvnn : VА→VA задаємо так: rxv11,,......,,xvnn (d ) = d ∇ [v1ad(x1),...,vnad(xn)]. Замість y1,..., yn зазвичай будемо скорочено писати y . Тоді замість rxv11,,......,,xvnn також пишемо rvx . Функції вигляду VA→А назвемо V-А-квазіарними функціями. Клас цих функцій позначимо Fn A . Функції вигляду VA→{T, F} назвемо V-А-квазіарними предикатами. Клас цих предикатів позначимо Pr A . Область істинності та область хибності V-А-квазіарного предиката P – це множини
T (P) = {d∈VА | P(d) = T} та F (P) = {d∈VА | P(d ) = F }. Предикат P : VА → {T, F} назвемо: − неспростовним (частково істинним), якщо F (P) = ∅; − − − тотожно істинним, якщо T (P) = VА та F (P) = ∅; виконуваним, якщо T (P) ≠ ∅; всюди невизначеним, якщо T (P) = F (P) = ∅. Предикат P : VА → {T , F} еквітонний (монотонний), якщо: P(d ) ↓ та d ⊆ d ′ ⇒ P(d ′) ↓= P(d ) . Предметне ім’я x ∈V неістотне для квазіарнoї функції (предиката) g , якщо
d1||− x = d2||− x ⇒ g(d1) = g(d2 ) . 1. Композиційні системи логік реномінативних та безкванторно-функціональних рівнів Семантичною основою КНЛ є композиційні предикатні системи. Для реномінативних логік такі системи мають вигляд (VА, Pr A , C ), для безкванторно-функціональних – (VА А, Fn A ∪ Pr A , C ). Тут Fn A та Pr A – це множини V-А-квазіарних функцій та V-А-квазіарних предикатів, C – множина композицій відповідного рівня.
Будемо розглядати КНЛ, розширені шляхом виділення підмножини U ⊆ V тотально неістотних предметних імен (неістотних для всіх базових функцій та предикатів). Будемо вважати, що така U розв’язна відносно V .
На рівні РНЛ можна перейменовувати компоненти вхідних даних, що дає змогу ввести композицію реномінації. Базовими композиціями РНЛ є логічні зв’язки ¬, ∨ та реномінація Rvx .
Композиція Rvx : Pr A → Pr A визначається так: для кожного d∈VА маємо Rvx (P)(d ) = P(rvx (d )) . Дамо визначення логічних зв’язок ¬ та ∨ через області істинності й хибності відповідних предикатів: T(¬P) = F(P); T(P∨Q) = T(P)∪T(Q);
F(¬P) = T(P);
F(P∨Q) = F(P)∩F(Q);
Подібним чином можна визначити похідні логічні зв’язки →, &, ↔ (див. [
На рівнях РНЛР та РНЛРС можна ототожнювати й розрізняти значення предметних імен за допомогою спеціальних 0-арних композицій – параметризованих за іменами предикатів рівності. Можна розглядати дві різновидності цих предикатів: слабкої (з точністю до визначеності) рівності =xy та строгої (точної) рівності ≡xy .
Предикати =xy та ≡xy задаються їх областями істинності й хибності наступним чином: T( =xy ) = {d∈VA | d(x)↓, d(y)↓ та d(x) = d(y)}, F( =xy ) = {d∈VA | d(x)↓, d(y)↓ та d(x) ≠ d(y)}; T( ≡xy ) = {d∈VA | d(x)↓, d(y)↓ та d(x) = d(y)} ∪ {d∈VA | d(x)↑ та d(y)↑}, F( ≡xy ) = {d∈VA | d(x)↓, d(y)↓ та d(x) ≠ d(y)} ∪ {d∈VA | d(x)↓, d(y)↑ або d(x)↑, d(y)↓}. Предикати =xy є частковими еквітонними, предикати ≡xy тотальні немонотонні (нееквітонні). Базовими композиціями РНЛР є ¬, ∨, Rvx , =ху. Базовими композиціями РНЛРС є ¬, ∨, Rvx , ≡ху. На функціональних рівнях можна формувати нові базові значення для вхідних даних. Це дає змогу ввести композицію суперпозиції. Нехай FА – клас квазіарних функцій вигляду f : VA→R.
Параметрична (n+1)-арна композиція суперпозиції Sv1,...vn : F A × (FnA )n → F A визначається так. Для кожного d∈VА задаємо
Sv1,...vn ( f , g1,..., gn )(d ) = f (d∇[v1 a g1(d ),..., vn a gn (d )]) . Розглядатимемо суперпозиції двох типів: – суперпозиції вигляду (Fn A )n+1 → Fn A функцій у функції (результатом є функція); – суперпозиції вигляду Pr A × (Fn A )n → Pr A функцій у предикати (результатом є предикат). Для роботи з окремими компонентами даних доцільно ввести спеціальні 0-арні композиції – функції деномінації (розіменування) 'v, де v∈V. Ці функції задаємо так: 'v(d) = d(v).
При наявності функцій деномінації композиції реномінації можна промоделювати за допомогою композицій суперпозиції: для кожної f ∈ Fn A ∪ Pr A маємо
Ruv11,,......,,vunn ( f ) = Su1,...,un ( f ,'v1,...,'vn ) . Отримуємо рівень безкванторно-функціональних логік – БКФЛ. Базові композиції БКФЛ: ¬, ∨, Sx , 'v. На функціональних рівнях з рівністю можна ототожнювати й розрізняти предметні значення, що дає змогу ввести спеціальну композицію рівності. Розглядаємо дві її різновидності: слабкої (з точністю до визначеності) рівності = та строгої (точної) рівності ≡ . Ці композиції задаються так. Для кожних f , g ∈ Fn A та d∈VА маємо:
⎧⎪T , якщо f (d ) ↓, g(d ) ↓, f (d ) = g(d ),
= ( f , g)(d ) = ⎨F, якщо f (d ) ↓, g(d ) ↓, f (d ) ≠ g(d ),
⎪⎩невизначене, якщо f (d ) ↑ або g(d ) ↑;
⎧ T , якщо f (d ) ↓, g(d ) ↓, f (d ) = g(d ) або f (d ) ↑, g(d ) ↑;
≡ ( f , g)(d ) = ⎨⎩F, якщо f (d ) ↓, g(d ) ↓, f (d ) ≠ g(d ) або f (d ) ↓, g(d ) ↑ або f (d ) ↑, g(d ) ↓ .
Отже, композиція ≡ в усіх випадках має результатом тотальний предикат.
На функціональних рівнях з рівністю наявність функцій розіменування є цілком природною.
Таким чином, отримуємо рівні БКФЛР та БКФЛРС безкванторно-функціональних логік з рівністю.
Базові композиції БКФЛР: ¬, ∨, Sx , 'v, = . Базові композиції БКФЛРС: ¬, ∨, Sx , 'v, ≡ .
Властивості композицій реномінації та предикатів рівності розглянуто в [
Таким чином, на рівні БКФЛРС логіки еквітонних предикатів не розглядаємо. Розглянемо основні властивості композицій суперпозиції.
S¬) Дистрибутивність суперпозиції щодо ¬: Sv (¬P, f ) = ¬Sv (P, f ) .
S∨) Дистрибутивність суперпозиції щодо ∨: Sv (P ∨ Q, f ) = Sv (P, f ) ∨ Sv (Q, f ) .
SS) Згортка суперпозицій: (тут ϕ∈ Fn A ∪ Pr A та введені позначення: u для u1,..., un ; t для t1,..., tn ; x для x1,..., xk ; r для r1,..., rk ; w для w1,..., wk ; v для v1,..., vm ; s для s1,..., sm ):
Su ,x (Sx,v (ϕ, r , s ), t , w) = Su ,x,v (ϕ, t ,Su ,x (r1, t , w), ...,Su ,x (rk , t , w),Su ,x (s1, t , w),...,Su ,x (sm , t , w)) . CN) Згортка імен (тут ϕ∈ Fn A ∪ Pr A ):
Sx1,...,xm ,v (ϕ,'x1,...,'xm , g ) = Sv (ϕ, g ) ; зокрема, Sx1,...,xm (ϕ,'x1,...,'xm ) = ϕ .
SD) Згорткa неістотних імен для функцій 'x: Sv ('x, g ) = 'x за умови x ∉{v} .
SF) Cпрощення для функцій 'x: Sx,v ('x, f , g ) = f ; зокрема, Sx ('x, f ) = f .
CU) Згортка за неістотним іменем (тут ϕ∈ Fn A ∪ Pr A ):
за умови x неістотне для ϕ маємо Sx,v (ϕ, f , g ) = Sv (ϕ, , g ) , зокрема, Sx (ϕ, f ) = ϕ .
Зауважимо, що властивості SS, CN, CU формулюються для квазіарних функцій та предикатів, а властивості SD, SF – лише для квазіарних функцій.
Укажемо основні властивості композицій рівності. Вважаємо, що P ∈ Pr A та h, f , f1,..., fn , g, g1,..., gn ∈ ∈ Fn A .
Rf) (рефлективність) кожний предикат вигляду = ( f , f ) є неспростовним; кожний предикат вигляду ≡ ( f , f ) є тотожно істинним.
Sm) (симетричність) для кожного d∈VA маємо = ( f , g)(d ) = = (g, f )(d ) та ≡ ( f , g)(d ) = ≡ (g, f )(d ) ; це означає, що предикати ≡ ( f , g) і ≡ (g, f ) рівні та предикати = ( f , g) і = (g, f ) рівні;
Tr) (транзитивність) для кожного d∈VA маємо: якщо = ( f , g)(d ) = T = ( f , h)(d ) = T ; якщо ≡ ( f , g)(d ) = T та ≡ (g, h)(d ) = T , то ≡ ( f , h)(d ) = T . Як наслідок маємо: кожний предикат вигляду = ( f , g) & = (g, h) → = ( f , h) неспростовний; кожний предикат вигляду ≡ ( f , g) & ≡ (g, h) → ≡ ( f , h) тотожно істинний (адже він тотальний). та = (g, h)(d ) = T , то Твердження 1. Якщо ≡ ( f , g) та ≡ (g, h) тотожно істинні, то ≡ ( f , h) тотожно істинний. Водночас для композиції = аналогічне твердження невірне. Приклад. Якщо = ( f , g) та = (g, h) неспростовні, то = ( f , h) може бути спростовним. Справді, візьмемо f (d ) ≠ h(d ) для деякого d∈VA, та нехай функція g – всюди невизначена. Наведемо властивості, пов’язані з заміною рівних.
EF) кожний предикат вигляду = ( f , g) → = (Sz,v (h, f , r ), Sz,v (h, g, r )) є неспростовним; кожний предикат вигляду ≡ ( f , g) → ≡ (Sz,v (h, f , r ), Sz,v (h, g, r )) є тотожно істинним; EP) кожний предикат вигляду = ( f , g) → (Sz,v (P, f , r ) ↔ Sz,v (P, g, r )) є неспростовним; кожний предикат вигляду ≡ ( f , g) → (Sz,v (P, f , r ) ↔ Sz,v (P, g, r )) є неспростовним. Дистрибутивність суперпозиції щодо рівності:
SЕ) Sv ( = ( f , g), r ) = = (Sv ( f , r ), Sv (g, r )) ; Sv ( ≡ ( f , g), r ) = ≡ (Sv ( f , r ), Sv (g, r )) . 2. Мови логік безкванторно-функціональних рівнів. Відношення логічного наслідку На безкванторно-функціональних рівнях композиційна система (А, Fn A ∪ Pr A, C ) визначає композиційну алгебру квазіарних функцій і предикатів ( Fn A ∪ Pr A, C ) та алгебру (алгебраїчну систему) даних (А, Fn A ∪ Pr A ). Побудова композиційної алгебри дає змогу визначити мову логіки: терми такої алгебри є формулами мови. Опишемо мову БКФЛ. Алфавіт мови: множини предметних імен (змінних) V та тотально неістотних імен U ⊆ V; множина Dns = {'v | v∈V} деномінаційних символів (ДНС) – імен функцій розіменування; множини Fns та Ps функціональних (ФНС) та предикатних (ПС) символів; множина {¬, ∨, S v , 'v} символів базових композицій. Множину σ = Fns∪Ps назвемо сигнaтурою мови. Множини термів Тr і формул Fr вводимо так. Т0) Кожний ФНС та кожний ДНС є термом, такі терми – атомарні. Т1) Нехай τ, t1,..., tn ∈Tr ; тоді S v1,...vn τt1...tn ∈Tr . Ф0) Кожний ПС є формулою (атомарною), такі формули – атомарні. Ф1) Нехай Φ, Ψ∈Fr, t1,..., tn ∈Tr ; тоді S v1,...vn Φt1...tn ∈ Fr , ¬Φ∈Fr, ∨ΦΨ∈Fr.
При зафіксованій множині базових композицій мови БКФЛ істотно відрізняються сигнaтурами. Неістотні відмінності – це способи запису термів і формул. Ми використовуємо префіксну форму.
Для бінарних композицій зазвичай використовують не префіксну, а інфіксну форму (див. [
У випадку БКФЛР множина базових композицій {¬, ∨, S v , 'v, =}. Визначення множини Тr термів таке ж, як для мови БКФЛ. Індуктивне визначення множини Fr формул задається пп. Ф0, Ф1, до якого додаємо: ФЕ) t, s ∈Tr ⇒ =ts∈ Fr . ФЕS) t, s ∈Tr ⇒ ≡ts∈ Fr .
У випадку БКФЛРС множина базових композицій {¬, ∨, Sx , 'v, ≡}. Визначення множини Тr термів таке ж, як для мови БКФЛ. Індуктивне визначення множини Fr формул задається пп. Ф0, Ф1, до якого додаємо: Замість =ts та ≡ts також писатимемо t = s та t ≡ s.
Інтерпретуємо мови БКФЛ, БКФЛР, БКФЛРС на відповідних композиційних системах квазіарних функцій та предикатів. Символи сигнатури σ = Fns∪Ps позначають (виділяють) базові функції та базові предикати в множинах Fn A та Pr A , символи 'v позначають відповідні функції деномінації 'v. Для такого позначення задаємо тотальне однозначне відображення I : Dns∪Fns∪Ps → Fn A ∪ Pr A . При цьому I('v) = 'v для кожного 'v∈Dns, кожне z∈U неістотне для кожного g∈I(σ). Далі продовжимо I до відображення інтерпретації I : Tr∪Fr→ Fn A ∪ Pr A згідно побудови термів та формул із простіших за допомогою символів композицій: ІТ) I (S v1,...vn τt1...tn ) = Sv1,...vn (I (τ), I (t1),..., I (tn )) ; ІΦ) I (S v1,...vn Φt1...tn ) = Sv1,...vn (I (Φ), I (t1),..., I (tn )) ; I(¬Φ) = ¬(I(Φ)), I(∨ΦΨ) = ∨(I(Φ), I(Ψ)). У випадках мови БКФЛР та мови БКФЛРС відповідно додаємо: IΦЕ) I(t = s =ts) = =(I(t), I(s)).
IΦS) I(t ≡ s) = ≡(I(t), I(s)). Трійку J = (CS, σ, I) назвемо інтерпретацією мови БКФЛ (БКФЛР, БКФЛРС) сигнатури σ. Cкорочено інтерпретації мови також позначаємо як (A, σ, I) чи (A, I). Функцію I(t), яка є значенням терма t при інтерпретації J, позначаємо tJ . Предикат I(Φ), який є значенням формули Φ при інтерпретації J, позначаємо Φ J . Ім’я x∈V неістотне для термa t, якщо при кожній інтерпретації J ім’я x неістотне для функції tJ . Ім’я x∈V неістотне для формули Φ, якщо при кожній інтерпретації J ім’я x неістотне для предиката Φ J . Формула Φ виконувана при інтерпретації J, якщо предикат ΦJ – виконуваний. Формула Φ виконувана, якщо Φ виконувана при деякій інтерпретації J.
Формула Φ неспростовна (частково істинна) при інтерпретації J, що позначаємо J |= Φ, якщо предикат Φ J – неспростовний. Формула Φ неспростовна, що позначаємо |= Φ, якщо J |= Φ при кожній інтерпретації J. Формула Φ тотожно істинна при інтерпретації J, що позначаємо J =id Φ , якщо предикат Φ J – тотожно істинний. Формула Φ тотожно істинна, що позначаємо =id Φ , якщо J =id Φ при кожній інтерпретації J.
Поняття тотожно істинної формули змістовне лише для БКФЛРС, тому що їх побудова неможлива без використання ≡ . Зокрема, =id t ≡ t та =id t ≡ s ↔ s ≡ t. Водночас: Твердження 2. У випадках БКФЛ та БКФЛР множина тотожно істинних формул порожня. Справді, розглянемо таку інтерпретацію J, на якій кожний ПС інтерпретується як всюди невизначений предикат, а кожний ФНС інтерпретується як всюди невизначена функція.
На множині формул можна ввести [
Φ∈Γ Ψ∈Δ Ψ∈Δ Φ∈Γ Δ є IR-наслідком Γ при J (позн. Γ J =ID Δ), якщо T∧(Γ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). Відповідні відношення логічного наслідку визначаємо за схемою: Γ =* Δ , якщо Γ J =* Δ для кожної J. Твердження 3. Маємо такі співвідношення: =TF = =T ∩ =F ; =TF ⊂ =T ⊂ =IR , =TF ⊂ =F ⊂ =IR . Окремим випадком розглянутих відношень для множин формул є відповідні відношення для пари формул: відношення наслідку при фіксованій J та відношення логічного наслідку; для них вводимо традиційні позначення Φ J =* Ψ та Φ J =* Ψ , де Φ, Ψ∈Fr.
Відношення логічного наслідку для пари формул індукують відношення логічної еквівалентності. Відношення еквівалентності при інтерпретації J визначаємо за схемою: Φ J∼∗ Ψ, якщо Φ J =* Ψ та ΨJ =*Φ . Відношення логічної еквівалентності ∼IR, ∼T, ∼F, ∼TF визначаємо за схемою: Φ ∼∗ Ψ, якщо Φ =* Ψ та Ψ =*Φ .
Із визначень випливає: Φ ∼∗ Ψ ⇔ Φ J∼∗ Ψ для кожної інтерпретації J.
Властивості описаних вище відношень вивчались в [
Особливу роль мають відношення =IR та ∼IR , вони традиційно позначаються [
Φ =IR Ψ ⇔ = Φ → Ψ ; Φ ∼IR Ψ ⇔ |= Φ ↔ Ψ . Важливим є також відношення J ∼TF : Φ J∼TF Ψ ⇔ T (Φ J ) = T (ΨJ ) та F (Φ J ) = F (ΨJ ) ⇔ Φ J = ΨJ . Розглянемо співвідношення між =id Φ → Ψ і Φ =TF Ψ та між =id Φ ↔ Ψ і Φ ∼TF Ψ. Для БКФЛ та БКФЛР множина тотожно істинних формул порожня (твердження 2), проте для БКФЛРС це питання нетривіальне.
Теорема 2. 1) =id Φ → Ψ ⇒ Φ =TF Ψ , водночас зворотне невірне; 2) =id Φ ↔ Ψ ⇒ Φ ∼TF Ψ, водночас зворотне невірне. Доводимо п. 1. =id Φ → Ψ
⇔ для кожних J = (A, I) маємо F (Φ J ) ∪ T (ΨJ ) = VA. Звідси, враховуючи диз’юнктність множини та її доповнення, із F (Φ J ) ∪ T (ΨJ ) = VA, маємо T (Ψ J ) ⊆ F (ΦJ ) та F (ΦJ ) ⊆ T (Ψ J ) . Враховуючи F (Φ J ) ∩ T (ΨJ ) = ∅ та
F (ΨJ ) ∩ T (ΨJ ) = ∅, отримуємо F (Ψ J ) ⊆ T (Ψ J ) та T (ΦJ ) ⊆ F (ΦJ ) . Звідси F (Ψ J ) ⊆ F (ΦJ ) та T (Φ J ) ⊆ T (ΨJ ) , що дає Φ J =TF Ψ . Це вірно для кожної J, звідки Φ =TF Ψ . Отже, =id Φ → Ψ ⇒ Φ =TF Ψ .
Водночас зворотне невірне: завжди маємо Φ =TF Φ , проте =id Φ → Φ вимагає, щоб для кожної J предикат Φ → Φ J , тобто ¬Φ∨ Φ J , був тотальним, звідки для кожної J предикат Φ J має бути тотальним. Така ситуація можлива для БКФЛРС, проте неможлива для БКФЛ та БКФЛР. 3. Семантичні властивості логік безкванторно-функціональних рівнів
Виділення тим чи іншим способом (див. [
I {i|vi∉ν(τ)} ν(S x1,...xn τt1...tn ) =(ν(τ)∪{x1,..., xn})∩ ν(ti ) ; ν(S x1,...xn Φt1...tn ) = (ν(Φ)∪{x1,..., xn})∩
I {i|vi∉ν(Φ)} ν(ti ) ; ν(t = s) = ν(t)∩ν(s); ν(t ≡ s) = ν(t)∩ν(s); ν(¬Φ) = ν(Ф); ν(∨ΦΨ) = ν(Φ)∩ν(Ψ).
SSФ) Згортка суперпозицій для формул (тут позначення: u для u1,..., un ; t для t1,..., tn ; x для x1,..., xk ; r для r1,..., rk ; w для w1,..., wk ; v для v1,..., vm ; s для s1,..., sm ):
Su ,x (S x,v (Φ, r , s ), t , w) TF Su ,x,v (Φ, t , Su ,x (r1, t , w), ..., Su ,x (rk , t , w), Su ,x (s1, t , w),..., Su ,x (sm , t , w)) . CNФ) Згортка імен для формул: S x,v (Φ,'x, t ) TF S v (Φ, t ) ; зокрема, S x (Φ,'x) TF Φ . СUФ) Згортка за неістотним іменем для формул: S x,v (Φ, s, t ) TF S v (Φ, t ) , якщо x неістотне для Φ; зокрема, S x (Φ,t) TF Φ , якщо x неістотне для Φ . Властивості SS, CN, CU для функцій та властивості SD, SF, які формулюються лише для функцій, у випадку БКФЛ індукують відповідні властивості нормалізації термів у формулах, які подаємо у вигляді ї теореми: Теорема 4. Нехай формула Ψ отримана з формули Φ заміною деяких входжень термів: rpSS) Su ,x (S x,v (τ, r , s ), t , w) на Su ,x,v (τ, t , Su ,x (r1, t , w), ..., Su ,x (rk , t , w), Su ,x (s1, t , w),..., Su ,x (sm , t , w)); rpCN) S x,v (τ,'x, t ) на S v (τ, t ) , зокрема, S x (τ,'x) на τ ; rpCU) S x,v (τ,t, t ) на S v (τ, t ) , якщо x неістотне для τ; зокрема, S x (τ,t) на τ , якщо x неістотне для τ.
Тоді Φ ∼TF Ψ .
=IR ):
Основою еквівалентних перетворень формул є теорема еквівалентності:
1) Якщо Φ1 ∼TF Ψ1,..., Φ n ∼TF Ψn , то Φ ∼ Φ′ (тут ∼ – одне з відношень ∼T, ∼F, ∼TF, ∼IR).
2) Якщо Φ1 ∼IR Ψ1,..., Φ n ∼IR Ψn , то Φ ∼IR Φ′ .
Для відношень ∼T та ∼F теорема 5 невірна (див. [
RfS) =id t ≡ t ; SmS) =id t ≡ s ↔ s ≡ t ; TrS) =id t ≡ s & s ≡ r → t ≡ r .
Враховуючи, що t ≡ s та s ≡ t завжди інтерпретуються як тотожні предикати, властивості SmS та TrS можна подати так: t ≡ s ∼TF s ≡ t ; t ≡ s , s ≡ r =TF t ≡ r .
EFS) |=id t ≡ s → S v ,z (τ, r ,t) ≡ S v ,z (τ, r , s) ; це можна подати так: t ≡ s =TF S v ,z (τ, r ,t) ≡ S v ,z (τ, r , s) . Подібну властивість для формул так подати неможливо, адже формула вигляду S x (Φ, t ) ↔ S x (Φ, s ) не завжди інтерпретується як тотальний предикат. Подібним способом можна записати лише ослаблену властивість = t ≡ s → (S v ,z (Φ, r ,t) ↔ S v ,z (Φ, r , s)) , або t ≡ s =IR (S v ,z (Φ, r ,t) ↔ S v ,z (Φ, r , s)) Тому EPS формулюємо так:
EPSL) t ≡ s, S v ,z (Φ, r ,t) |=TF S v ,z (Φ, r , s) . SЕS) =id S v (s ≡ r, t ) ↔ S v (s, t ) ≡ S v (r, t ) ; це можна подати так: S v (s ≡ r, t ) TF S v (s, t ) ≡ S v (r, t ) . Тавтології. Введемо поняття тавтології для КНЛ безкванторно-функціональних рівнів.
Формула мови БКФЛ (БКФЛР, БКФЛРС) пропозиційно нерозкладна, якщо вона атомарна або має вигляд
S v Φt (вигляд S v Φt чи t = s, вигляд S v Φt чи t ≡ s). Множину таких формул позначимо Fr0
Істиннiсна оцiнка мови РНЛ – це [
Fr0 → {T, F}. Таке відображення продовжимо до τ : Fr → {T, F} так: τ(¬Φ) = {T , якщо τ(Φ) = F, τ(∨ΦΨ) = {T , якщо τ(Φ) = T або τ(Ψ) = T ,
F , якщо τ(Φ) = T ; F, якщо τ(Φ) = F та τ(Ψ) = F. Враховуючи Rf, Sm, Tr, EF, EP, у випадках БКФЛР та БКФЛРС на τ накладаємо додаткові умови: τ(t = t) = T; τ(t = s) = τ(s = t); τ(t = s) = τ(s = r) = T ⇒ τ(t = r) = T; τ(t = s) = T ⇒ τ(S z,v (ρ,t, r ) = S z,v (ρ, s, r )) = T ; τ(t = s) = T ⇒ τ(S z,v (Φ,t, r ) = τ(S z,v (Φ, s, r ) ; τ(х ≡ х) = T; τ(х ≡ y) = τ(y ≡ х); τ(х ≡ y) = τ(х ≡ y) = T ⇒ τ(х ≡ z) = T; τ(t ≡ s) = T ⇒ τ(S z,v (ρ, t, r ) ≡ τ(S z,v (ρ, s, r ) = T ; τ(t ≡ s) = T ⇒ τ(S z,v (ρ, t, r )) = τ(S z,v (ρ, s, r )) . Формула Φ – тавтологiя, якщо τ(Φ) = T для кожної істиннісної оцінки τ. Твердження 4. Кожна тавтологія є неспростовною формулою. Нормальні форми. Терм мови БКФЛ назвемо нормальним, якщо:
всі його символи суперпозиції (якщо вони є) застосовані тільки до ФНС; − − − щення;
− в усіх його символах суперпозиції (якщо вони є) згорнуті неістотні імена й виконані спрощення згідно з пп. 2–5 теореми 4.
Терм мови БКФЛР (мови БКФЛРР) назвемо нормальним, якщо: −
всі його символи суперпозиції (якщо вони є) застосовані тільки до ФНС; − в усіх його символах суперпозиції (якщо вони є) згорнуті неістотні імена й виконані спрощення згідно з CNT, CUT, SD, SF (згідно з CNTS, CUTS, SDS, SFS).
Формула Ψ мови БКФЛ (мови БКФЛР, мови БКФЛРР) знаходиться в нормальній формі, або Ψ є нормальною формулою, якщо: в усіх символах суперпозиції формули Ψ (якщо вони є) згорнуті неістотні імена й виконані спроусі символи суперпозиції формули Ψ (якщо вони є) застосовані тільки до ФНС чи ПС.
Нормальність формули Ф мови БКФЛ (мови БКФЛР, мови БКФЛРР) означає, що вона набуває класичноподібного вигляду: усі її символи суперпозиції застосовані тільки до ФНС чи ПС, усі її терми нормальні та в усіх її символах суперпозиції згорнуті неістотні імена й виконані належні спрощення. Теорема 7. Для кожної формули Φ мови БКФЛ можна збудувати нормальну формулу Ψ таку: ∨L) Φ∨Ψ, Γ = Δ ⇔ Φ, Γ = Δ та Ψ, Γ = Δ. ∨R) Γ = Δ, Φ∨Ψ ⇔ Γ = Δ, Φ, Ψ. ¬∨L) ¬(Φ∨Ψ), Γ = Δ ⇔ ¬Φ, ¬Ψ, Γ = Δ. ¬∨R) Γ = Δ, ¬(Φ∨Ψ) ⇔ Γ = Δ, ¬Φ та Γ = Δ, ¬Ψ.
Для відношення =IR можна знімати заперечення, переносячи формулу з лівої частини відношення у праву і навпаки (проте це невірно для =TF , =T , =F ): ¬L) ¬Φ, Γ =IR Δ ⇔ Γ =IR Δ, Φ. ¬R) Γ =IR Δ, ¬Φ ⇔ Φ, Γ =IR Δ. Наявність кожного з відношень =TF , =T , =F , =IR . гарантує властивість: С) Φ, Γ = Δ, Φ. Додатково гарантують наявність відношень логічного наслідку такі властивості: СL) Φ, ¬Φ, Γ = Δ ( = – це =T чи =IR ); СR) Γ = Δ, Φ, ¬Φ ( = – це =F чи =IR ); СLR) Φ, ¬Φ, Γ =TF Δ, Ψ, ¬Ψ. Для =IR в силу ¬L та ¬R властивості СLR, СL, СR зайві, бо зводяться до властивості С Для відношення =t справджуються усі наведені вище властивості пропозиційного рівня. Властивості С, СL, СR, СLR назвемо умовами наявності логічного наслідку. Властивості декомпозиції формул ¬¬L, ¬¬R, ∨L, ∨R, ¬∨L, ¬∨R, ¬L, ¬R назвемо властивостями переходу. Наведемо властивості, пов’язані з суперпозицією. Такі властивості віднесемо до властивостей переходу, вони безпосередньо відтворюють відповідні семантичні властивості, пов’язані з еквівалентністю формул.
Рівень БКФЛ. Для БКФЛ це властивості спрощення, базовані на CNФ і СUФ, та властивості нормалізації SSФ, S¬, S∨ та теоремі 4. Для відношення =IR кожна така властивість розщеплюється на дві відповідні влаCNФR) Γ |= S x,v (Φ,'x, t ), Δ ⇔ Γ |= S v (Φ, t ), Δ ; ¬CNФL) ¬S x,v (Φ,'x, t ), Γ |= Δ ⇔ ¬S v (Φ, t ), Γ |= Δ ; ¬CNФR) Γ |= ¬S x,v (Φ,'x, t ), Δ ⇔ Γ |= ¬S v (Φ, t ), Δ ; CUФL) S x,v (Φ, s, t ), Γ |= Δ ⇔ S v (Φ, t ), Γ |= Δ , де x неістотне для Φ; CUФR) Γ |= S x,v (Φ, s, t ), Δ ⇔ Γ |= S v (Φ, t ), Δ , де x неістотне для Φ; ¬CUФL) ¬S x,v (Φ, s, t ), Γ |= Δ ⇔ ¬S v (Φ, t ), Γ |= Δ , де x неістотне для Φ; ¬CUФR) Γ |= ¬S x,v (Φ, s, t ), Δ ⇔ Γ |= ¬S v (Φ, t ), Δ , де x неістотне для Φ. В наступних властивостях SSФL, SSФR, ¬SSФL, ¬SSФR позначено як Ξ формулу S u ,x,v (Φ, t , S u ,x (r1, t , w),..., S u ,x (rk , t , w), S u ,x (s1, t , w),..., S u ,x (sm , t , w)) : SSФL) S u ,x (S x,v (Φ, r , s ), t , w), Γ |= Δ ⇔ Ξ, Γ |= Δ ; SSФR) Γ |= S u ,x (S x,v (Φ, r , s ), t , w), Δ ⇔ Γ |= Ξ, Δ ; ¬SSФL) ¬S u ,x (S x,v (Φ, r , s ), t , w), Γ |= Δ ⇔ ¬Ξ, Γ |= Δ ; ¬SSФR) Γ |= ¬S u ,x (S x,v (Φ, r , s ), t , w), Δ ⇔ Γ |= ¬Ξ, Δ ; S¬L) S v (¬Φ, t ), Γ |= Δ ⇔ ¬S v (Φ, t ), Γ |= Δ ; S¬R) Γ |= S v (¬Φ, t ), Δ ⇔ Γ |= ¬S v (Φ, t ), Δ ; ¬S¬L) ¬S v (¬Φ, t ), Γ |= Δ ⇔ ¬¬S v (Φ, t ), Γ |= Δ ; ¬S¬R) Γ |= ¬S v (¬Φ, t ), Δ ⇔ Γ |= ¬¬S v (Φ, t ), Δ ; S∨L) S v (Φ ∨ Ψ, t ), Γ |= Δ ⇔ S v (Φ, t ) ∨ S v (Ψ, t ), Γ |= Δ ; S∨R) Γ |= S v (Φ ∨ Ψ, t ), Δ ⇔ Γ |= S v (Φ, t ) ∨ S v (Ψ, t ), Δ ; ¬S∨L) ¬S v (Φ ∨ Ψ, t ), Γ |= Δ ⇔ ¬(S v (Φ, t ) ∨ S v (Ψ, t )), Γ |= Δ ; ¬S∨R) Γ |= ¬S v (Φ ∨ Ψ, t ), Δ ⇔ Γ |= ¬(S v (Φ, t ) ∨ S v (Ψ, t )), Δ .
NrTrL) Φ, Γ = Δ ⇔ Ψ, Γ = Δ.
NrTrR) Γ = Δ, Φ ⇔ Γ = Δ,Ψ. ¬NrTrL) ¬Φ, Γ = Δ ⇔ ¬Ψ, Γ = Δ. ¬NrTrR) Γ = Δ, ¬Φ ⇔ Γ = Δ,¬Ψ. До цих властивостей додаємо базовані на теоремі 4 властивості нормалізації термів.
Нехай формула Ψ отримана з формули Φ нормалізацією термів на основі еквівалентних перетворень згідно з теоремою 4. Тоді маємо: Рівень БКФЛP. Розглянемо властивості, пов’язані з композицією слабкої рівності. Із SmW отримуємо: SmW) t = s, Γ = Δ ⇔ t = s, s = t, Γ = Δ; зокрема, t = s, Γ =IR Δ ⇔ t = s, s = t, Γ =IR Δ; Із TrW отримуємо транзитивність слабкої рівності для =IR : TrW) t = s, s = r, Γ =IR Δ ⇔ t = s, s = r, t = r, Γ =IR Δ.
Водночас у випадку БКФЛР для відношень =T , =F , =TF транзитивність слабкої рівності порушується. Це випливає з того, що властивість TrW можна посилити лише так:
TrL) x = y, y = z, Γ = Δ ⇔ x = y, y = z, x = z, Γ = Δ (тут = – це =IR чи =T ); TrR) Γ = Δ, ¬ x = y, ¬ y = z ⇔ Γ = Δ, ¬ x = y, ¬ y = z, ¬ x = z (тут = – це =IR чи =F ). Справді, маємо T(t = s) ∩ T(s = r) = T(t = s) ∩ T(s = r) ∩ T(t = r), звідси TrL вірне для =T та TrR вірне для =F . Згідно =T ⊂ =IR та в силу =F ⊂ =IR властивості TrL та TrR вірні для =IR .
Маємо ′x = ′y, ′y = ′z |≠F ′x = ′y & ′y = ′z & ′x = ′z та ¬ ′x = ′y ∨ ¬ ′y = ′z ∨ ¬ ′x = ′z |≠T ¬ ′x = ′y, ¬ ′y = ′z. Справді, при a ≠ b для d = [xaa, zab] маємо d∉F(′x = ′y) ∪ F(′y = ′z), проте d∈F(′x = ′z) ⇒ d∈F(′x = ′z) ∪ F(′x = ′y) ∪ F(′y = ′z). Водночас ′x = ′y, ′y = ′z, ′x = ′z |=F ′x = ′y & ′y = ′z & ′x = ′z та ¬ ′x = ′y ∨ ¬ ′y = ′z ∨ ¬ ′x = ′z |=T ¬ ′x = ′y, ¬ ′y = ′z, ¬ ′x = ′z. Таким чином, TrL невірна для =F , а TrR невірна для =T . тому для =TF невірні обидві властивості TrL та TrR. Отже, для БКФЛР адекватним залишається лише відношення |=IR . Властивість RfW індукує достатню умову наявності відношення |=IR : СRfW) Γ |=IR t = t, Δ. Властивість SЕ індукує властивості дистрибутивності суперпозиції відносно рівності для відношення |=IR : SЕL) S v (s = r, t ), Γ |=IR Δ ⇔ S v (s, t ) = S v (r, t ), Γ |=IR Δ ; SЕR) Γ |=IR S v (s = r, t ), Δ ⇔ Γ |=IR S v (s, t ) = S v (r, t ), Δ . Властивість EP індукує властивості заміни рівних для відношення |=IR : EPL) t = s, S v ,z (Φ, r , t), Γ |=IR Δ ⇔ t = s, S v ,z (Φ, r ,t), S v ,z (Φ, r , s), Γ |=IR Δ ; EPR) t = s, Γ |=IR S v ,z (Φ, r , t), Δ ⇔ t = s, Γ |=IR S v ,z (Φ, r ,t), S v ,z (Φ, r , s), Δ . Властивості кроку нормалізації термів, індуковані ST, CNT, CUT, SDT, SFT, мають вигляд: Nr*L) Φ, Γ |=IR Δ ⇔ Ψ, Γ |=IR Δ; Nr*R) Γ |=IR Δ, Φ ⇔ Γ |=IR Δ,Ψ.
Тут Ψ утворена із Φ заміною деяких входжень термів, що є лівими частинами рівностей, які фігурують в цих властивостях, на терми, що є правими частинами відповідних рівностей, так, як описано в теоремі 4. Рівень БКФЛPС. Розглянемо властивості, пов’язані з композицією строгої рівності. Властивість RfS індукує достатню умову наявності кожного з відношень |=IR , |=T, |=F, |=TF : СRfS) Γ = t ≡ t, Δ. На основі SmS та TrS отримуємо: SmS) t ≡ s, Γ = Δ ⇔ t ≡ s, s ≡ t, Γ = Δ; TrS) t ≡ s, s ≡ r, Γ = Δ ⇔ t ≡ s, s ≡ r, t ≡ r, Γ = Δ. Властивість SЕS індукує властивості дистрибутивності суперпозиції відносно рівності: SЕSL) S v (s ≡ r, t ), Γ |= Δ ⇔ S v (s, t ) ≡ S v (r, t ), Γ |= Δ ; SЕSR) Γ |= S v (s ≡ r, t ), Δ ⇔ Γ |= S v (s, t ) ≡ S v (r, t ), Δ . Властивість EPS індукує властивості заміни рівних: EPSL) t ≡ s, S v ,z (Φ, r ,t), Γ |= Δ ⇔ t ≡ s, S v ,z (Φ, r , t), S v ,z (Φ, r , s), Γ |= Δ ; EPSR) t ≡ s, Γ |= S v ,z (Φ, r , t), Δ ⇔ t ≡ s, Γ |= S v ,z (Φ, r , t), S v ,z (Φ, r , s), Δ . ¬EPSL) t ≡ s, ¬S v ,z (Φ, r ,t), Γ |= Δ ⇔ t ≡ s, ¬S v ,z (Φ, r , t), ¬S v ,z (Φ, r , s), Γ |= Δ ; ¬EPSR) t ≡ s, Γ |= ¬S v ,z (Φ, r ,t), Δ ⇔ t ≡ s, Γ |= ¬S v ,z (Φ, r ,t), ¬S v ,z (Φ, r , s), Δ . Для відношення |=IR достатньо властивостей EPSLта EPSR.
Властивості кроку нормалізації термів, індуковані STS, CNTS, CUTS, SDS, SFS, мають вигляд:
NrS*L) Φ, Γ = Δ ⇔ Ψ, Γ = Δ; NrS*R) Γ = Δ, Φ ⇔ Γ = Δ,Ψ. Тут Ψ утворена із Φ заміною деяких входжень термів, що є лівими частинами рівностей, які фігурують в цих властивостях, на терми, що є правими частинами відповідних рівностей, так, як описано в теоремі 4. Підсумовуючи, отримуємо наступне.
Для відношення |=IR множин формул БКФЛ маємо базові властивості переходу NrTrL, NrTrR, CNФL,
Для відношень =TF , =T , =F множин формул БКФЛ маємо базові властивості переходу NrTrL, NrTrR, ¬NrTrL, ¬NrTrR, CNФL, CNФR, ¬CNФL, ¬CNФR, СUФL, CUФR, ¬СUФL, ¬CUФR, SSФL, SSФR, ¬SSФL, ¬SSФR, С та СLR для =TF ; С та СL для =T ; С та СR для =F .
Для відношення =IR множин формул БКФЛР маємо базові властивості переходу Nr*L, Nr*R, SmW, TrW,
Для відношень =TF , =T , =F множин формул БКФЛРС маємо базові властивості переходу NrS*L, NrS*R, SmW, TrW, SЕSL, SЕSR, EPSL, EPSR, ¬EPSL, ¬EPSR, ¬NrTrL, ¬NrTrR, CNФL, CNФR, ¬CNФL, ¬CNФR, СUФL, CUФR, ¬СUФL, ¬CUФR, SSФL, SSФR, ¬SSФL, ¬SSФR, S¬L, S¬R, ¬S¬L, ¬S¬R, S∨L, S∨R, ¬S∨L, ¬S∨R; ¬¬L, ¬¬R, ∨L, ∨R, ¬∨L, ¬∨R .
Властивості наявності логічного наслідку: С, СRfS, СLR для =TF ; С, СRfS, СL для =T ; С, СRfS, СR для =F .
Описані властивості відношень логічного наслідку для множин формул є семантичною основою побудови для цих відношень в БКФЛ, БКФЛР та БКФЛРС низки числень секвенційного типу. Властивості наявності логічного наслідку індукують умови замкненості секвенції, властивості переходу індукують відповідні секвенційні форми. Висновки
Досліджено безкванторні композиційно-номінативні логіки часткових квазіарних предикатів. Виділено наступні рівні цих логік: реномінативний, реномінативний з предикатами слабкої рівності, реномінативний з предикатами строгої рівності, безкванторно-функціональний, безкванторно-функціональний з композицією слабкої рівності, безкванторно-функціональний з композицією строгої рівності. Основна увага приділена логікам безкванторно-функціональних рівнів з рівністю. Описано мови та семантичні моделі безкванторних логік, досліджено їх семантичні властивості. Наведено властивості композицій суперпозиції, слабкої рівності та строгої рівності, розглянуто нормальні форми термів та формул. Досліджено властивості відношень логічного наслідку для множин формул. Такі властивості є семантичною основою побудови для різних класів безкванторних логік низки числень секвенційного типу, що планується зробити в наступних роботах.