РЕНОМІНАТИВНА ЛОГІК А Семантичні моделі РНЛ

При запису використовуємо традиційні скорочення формул.
nm(Φ) – множина всіх предметних імен, які фігурують в символах реномінації формули Φ.
Таку nm(Φ) назвемо множиною імен формули Φ.
Розширимо пт на множини формул
Для логік ЕП КС набувають вигляду (VА, ЕPrA, C).
Такі об’єкти – КС еквітонних предикатів реномінативного рівня.
Інтерпретуємо мову РНЛ на КС реномінативного рівня (VА, PrA, C)
Задамо тотальне однозначне I : Ps→PrA, яке визначає значення ПС як базові предикати відповідної АС даних (А, PrA)
Для інтерпретації формул продовжимо I до відображення Fr→PrA:
1. I(¬Φ) = ¬(I(Φ)).
2. I(∨ΦΨ) = ∨(I(Φ), I(Ψ)).
3.

Відображення I прив'язує АС даних (А, PrA) до мови.
Отримуємо об'єкти вигляду ((A, PrA), I) – АС з доданою сигнатурою.
Така АС фактично визначає KC (VA, PrA, C)
АС з доданою сигнатурою ((A, PrA), I) скорочено позначаємо (A, I).
АС з доданою сигнатурою є інтегрованими семантичними моделями, які пов'язують мову КНЛ із АС даних. Називаємо їх моделями мови.
Предикат I(Φ) – значення формули Φ при інтерпретації на A=(A, I) – позначаємо ΦA
Формула Φ істинна при інтерпретації на A, або A-істинна, якщо
ΦA – істинний предикат.
Цей факт позначимо A |= Φ.
Формула Φ виконувана при інтерпретації A, або A-виконувана, якщо
ΦA – виконуваний предикат.
Φ всюди iстинна, якщо Φ iстинна при кожнiй iнтерпретацiї.
Цей факт позначимо |= Φ.
Φ виконувана, якщо Φ виконувана при деякiй iнтерпретацiї.

Для встановлення істинності формули при повнототальних еквітонних інтерпретаціях досить перевірити значення відповідного ΦA тільки на V-повних даних.
Теорема 1. A |= Φ ⇔ для кожного d∈AV маємо ΦA(d)=T.
Наслідок. A |= Φ ⇔ для кожних A=(A, I), d∈AV маємо ΦA(d)=T.
Для повнототальних еквітонних інтерпретацій справджується
Теорема 2. Для кожної A , якщо A |= Φ та A |= Φ→Ψ, то A |= Ψ.
Наслідок. Якщо |= Φ та |= Φ→Ψ, то |= Ψ.
Ім'я x∈V (строго) неiстотне для формули Φ, якщо
для кожної моделі мови A ім'я x (строго) неiстотне для ΦA .
У випадку логіки ЕП критерій неістотності предметних імен для формул встановлює
Теорема 3. Ім'я x∈V неістотне для Φ ⇔ для всіх v∈V маємо

Успадкування властивостей ПЛ для РНЛ відбувається перенесенням на рівень РНЛ понять тавтології, тавтологічних наслідку і еквiвалентностi.
Тавтологiї – формули, якi мають структуру тавтологiй мови ПЛ.
Формула пропозиційно нерозкладна, якщо вона атомарна або вигляду
Fr0 – множина всiх пропозиційно нерозкладних формул мови L.
Iстиннiсна оцiнка мови L – довiльне відображення τ : Fr0 →{T, F}.
Продовжимо його до вiдображення τ : Fr→{T, F}:
– τ(¬Φ)=T ⇔ τ(Φ)=F;
– τ(∨ΦΨ)=T ⇔ τ(Φ)=T або τ(Ψ)=T.
Φ тавтологiя, якщо τ(Φ)=T при кожнiй iстиннiснiй оцiнцi τ.
Кожна тавтологія є всюди істинною формулою.
Приклад 4. Формула всюди iстинна, але не тавтологiя

На множинi Fr формул введемо відношення
тавтологiчного наслiдку ╞ (позначаємо також |=т),
тавтологiчної еквiвалентностi ~т ,
логiчного наслiдку |=,
слабкого логiчного наслiдку ||=,
логiчної еквiвалентностi ~.
Ψ є тавтологiчним наслiдком Φ (позн. Φ╞ Ψ), якщо
Φ→Ψ – тавтологiя.
Φ та Ψ тавтологiчно еквiвалентнi (позн. Φ~тΨ): Φ╞ Ψ та Ψ╞ Φ
Ψ є логiчним наслiдком Φ (позн. Φ|=Ψ), якщо
для кожної A маємо: T(ΦA)∩F(ΨA) = ∅
Зрозуміло, що Φ|=Ψ ⇔ Φ→Ψ всюди iстинна.
Φ та Ψ логiчно еквiвалентнi (позн. Φ ~ Ψ): Φ|=Ψ та Ψ|=Φ.
Зрозумiло, що Φ ~ Ψ ⇔ формули Φ→Ψ та Ψ→Φ всюди iстиннi.
Ψ є слабким логiчним наслiдком формули Φ, що позн. Φ||=Ψ, якщо для кожної A маємо: A |=Φ ⇒ A |=Ψ.

Основні властивості відношень ╞, |=, ||= та ~:
1) Φ тавтологія ⇔ ╞ Φ;
2) Φ всюди істинна ⇔ |=Φ ⇔ ||=Φ;
3) Φ╞ Ψ ⇒ Φ|=Ψ; але не завжди Φ|=Ψ ⇒ Φ╞ Ψ;
4) Φ|=Ψ ⇒ Φ||=Ψ; але не завжди Φ||=Ψ ⇒ Φ|=Ψ;
5) Φ~тΨ ⇔ Φ↔Ψ тавтологія
6) Φ ~ Ψ ⇔ |=Φ↔Ψ;
7) відношення ╞ , |= та ||= рефлексивні і транзитивні;
8) відношення ~ рефлексивне, транзитивне і симетричне.

Семантичні властивості РНЛ
Для РНЛ успадковуються семантичні властивості пропозиційного рівня.
Вкажемо властивості формул РНЛ, пов'язані з реномінацією. Вони відображають відповідні властивості композиції реномінації.
RT) Згортка тотожної пари імен у реномінації:
Зокрема,
R¬) R¬-дистрибутивність:
R∨) R∨-дистрибутивність:
Аналогічно – властивості R→, R&, R↔.

RR) Згортка реномінацій:
RN) Нехай у неістотне для формули Φ. Тоді
Зокрема,
RП)
Теорема 4 (семантичної еквiвалентностi). Нехай формула Φ' отримана iз формули Φ замiною деяких входжень формул Φ1,..., Φn на Ψ1,..., Ψn вiдповiдно.
Якщо Φ1 ~Ψ1, ..., Φn ~Ψn, то Φ ~ Φ'.
Доводиться індукцією за побудовою формули

Теорема (про розширення). Нехай АС одної сигнатури A = (А, IА) і В = (А, IВ) та формула Φ такі: ∀р∈σ(Φ) ∀δ∈VA із рA(δ)↓ випливає рВ(δ)↓=рA(δ). Тоді ∀d∈VA із ΦA(d)↓ випливає ΦВ(d)↓=ΦA(d).
Доводиться індукцією за побудовою формули Φ.
Теорема 6 вірна для загального випадку логік квазіарних предикатів.
Нехай A = (А, IА) і В = (А, IВ) – АС однiєї сигнатури.
АС В – система розширень для АС A, якщо ∀р∈Ps ∀δ∈VA із рA(δ)↓ випливає рВ(δ)↓ = рA(δ).
Наслідок. Нехай В=(А, IВ) – система розширень для АС A=(А, IА). Тоді для довільних Φ та d∈VA із ΦA(d)↓ випливає ΦВ(d)↓ = ΦA(d).

Нормальні форми в РНЛ
Формула Φ – в слабкій нормальній формі, якщо символи реномінації в формулі Φ застосовні тільки до ПС.
Формула Φ – в нормальній формі, або нормальна, якщо Φ – в слабкій нормальній формі, причому всі із Φ не мають тотожних перейменувань.
Формула Φ примітивна: Φ атомарна або має вигляд
та відсутні тотожні перейменування
Теорема 1. ∀ Φ можна збудувати Ψ в нормальній формі: |= Φ↔Ψ
Зведення Φ до нормальної форми виконуємо так.
Використовуючи R¬ та R∨, просуваємо реномінації вглиб формули
Використовуючи RR, згортаємо сусідні символи реномінації.
При появі усуваємо тотожні перейменування згідно RТ.
За теоремою еквівалентності, після просунення всіх символів реномінації на рівень ПС та усунення тотожних перейменувань дістанемо формулу Ψ у нормальній формі таку, що |= Φ↔Ψ

Формулу Ψ у нормальній формі, утворену з Φ за допомогою перетворень на основі R¬, R∨, RR та RТ, назвемо нормалізантою формули Φ.
Наслідок 2. Нехай Ψ – нормалізанта формули Φ. Тоді |= Φ↔Ψ.
Наслідок 3. Нехай Ψ1 та Ψ2 – нормалізанти Φ. Тоді |= Ψ1↔Ψ2.
Індукцiєю за побудовою формули доводиться
Теорема 2. Нехай Ψ – нормалізанта формули Φ. Тоді нормалізанта формули є нормалізантою формули
Формула Φ – субтавтологія, якщо її нормалізанта – тавтологія.
Коректність таких визначень гарантує
Теорема 3. Якщо Ψ1 та Ψ2 – нормалізанти формули Φ, а формула Ψ1 – тавтологія, то й Ψ2 – тавтологія.
Фундаментальну роль субтавтологій встановлює
Теорема 4. Формула Φ – субтавтологія ⇔ |= Φ.

Відношення логічного наслідку для множин формул РНЛ
Γ та Δ – множини формул мови сигнатури Ps.
A=(А, I) – АС сигнатури Ps.
Δ є логічним наслідком Γ в АС A, якщо ∀d∈VA
ΦА(d)=T ∀Φ∈Γ ⇒ неможливо ΨА(d)=F ∀Ψ∈Δ.
Позначаємо Γ |=А Δ
Δ є логічним наслідком Γ, якщо
Γ |=А Δ ∀ АС A=(А, I) сигнатури Ps .
Це позначаємо Γ |= Δ
Отже, Γ |≠ Δ ⇔ існують АС A=(А, I) та d∈VA такі:
∀Φ∈Γ маємо ΦА(d)=T та ∀Ψ∈Δ маємо ΨА(d)=F
Відношення |= для множин формул рефлексивне, але не транзитивне
Теорема 1 (заміни еквівалентних). Нехай Φ ~ Ψ. Тоді
Φ, Γ |= Δ ⇔ Ψ, Γ |= Δ та Γ |= Δ, Φ ⇔ Γ |= Δ,Ψ.

Властивості відношення |=
G1, G2 та П1–П10 успадковуються на реномінативному рівні
Вкажемо властивості відношення |=, пов‘язані з композицією реномінації.
Вони безпосередньо відтворюють відповідні властивості формул.
Кожна така властивість розщеплюється на дві властивості для |=
RT|−)
RT−|)
RR|−)
RR−|)
R¬|−)
R¬−|)

R∨|−)
R∨−|)
PsN|−) при у∈μ(р), де р∈Ps
PsN−|) при у∈μ(р), де р∈Ps
ΦN|−) при умові у∈μ(Φ).
ΦN−|) при умові у∈μ(Φ).
Умову у∈μ(Φ) можна ослабити до умови у неістотне для Φ.
Базові властивості відношення |= на реномінативному рівні:
П1–П4 та RT|-, RТ-|, RR|-, RR-|, R¬|-, R¬-|, R∨|-, R∨-|, PsN|-, PsN-|

Реномінативні числення РНЛ повнототальних ЕП
Реномінативне неокласичне числення (РНКЧ):
ФС вигляду T = (Fr, Ax, P).
Fr – множина формул мови РНЛ
Ax – множина логічних аксіом
P – множина правил виведення.
Aлог задається схемами аксіом:
АхПР) ¬Φ∨Φ – пропозиційні аксіоми
АхRT) – аксіоми елімінації тотожних перейменувань
АхR¬) – аксіоми R¬-дистрибутивності
АхR∨) – аксіоми R∨-дистрибутивності
АхRR) – аксіоми згортки реномінацій
Такі РНКЧ назвемо вільними.

Множина Р правил виведення РНКЧ:
П1) Φ |−Ψ∨Φ − правило розширення.
П2) Φ∨Φ |−Φ − правило скорочення.
П3) Φ∨(Ψ∨Ξ) |− (Φ∨Ψ)∨Ξ − правило асоціативності.
П4) Φ∨Ψ, ¬Φ∨Ξ |−Ψ∨Ξ − правило перетину.
П5) Φ |− − правило реномінації (ПР).
Теорема РНКЧ: формула, яка виводиться із аксіом за допомогою ПВ
Позначення: T |–Φ, або |–Φ, якщо T мається на увазі.
Th(T) – множина теорем РНКЧ T
Теорема. 1) Логічні аксіоми є всюди істинними формулами;
2) Висновки правил П1–П4 – логічні наслідки засновків;
3) Висновок правила П5 – слабкий логічний наслідок засновку.

Модель мови A=(A, І) – модель РНКЧ T, якщо A |=Φ для всіх Φ∈Ax
ПВ для кожної інтерпретації A зберігають істинність на A. Отже:
Теорема 2 (істинності). Кожна теорема РНКЧ T істинна на кожній моделі T.
Наслідок. ∀ теорема вільного РНКЧ − всюди істинна формула
Φ істинна в РНКЧ T, якщо Φ істинна на ∀ моделі числення T.
Те, що Φ істинна в T, позначаємо T |=Φ.
Теорема істинності. Якщо T |–Φ, то T |=Φ.
Теорема істинності засвідчує коректність РНКЧ:
із синтаксичної істинності випливає семантична істинність.
Кожне виведення засобами ПЧ є виведенням вільного РНКЧ.
Теорема 3 (тавтології). Кожна тавтологія є теоремою.
Наслiдок. Якщо {Φ1, ..., Φn}╞ Φ та |–Φ1, ..., |–Φn , то |–Φ.
Теорема 4 (еквiвалентностi). Нехай Φ' отримана iз Φ замiною деяких входжень формул Φ1, ..., Φn на Ψ1, ..., Ψn вiдповiдно. Якщо |–Φ1↔Ψ1, ..., |– Φn↔Ψn, то |–Φ↔Φ'.

Теорема 5. Нехай Ψ – нормалізанта формули Φ. Тоді |–Φ↔Ψ.
Нормалізанта Ψ формули Φ утворена із Φ за допомогою перетворень на основі RT, R¬, R∨, RR, RN. На синтаксичному рівні вони задані відповідними аксіомами.
Далі скористуємося ТТ і теоремою еквівалентності
Наслідок 1. Нехай Φ – субтавтологія, тоді |–Φ.
Нехай Ψ – нормалізанта субтавтології Φ. За теоремою 5 маємо |– Φ↔Ψ. Але Ψ –тавтологія, тому |–Ψ. Звідси |–Φ за ТТ.
Теорема 6 (повноти). ∀ РНКЧ T маємо T |=Φ ⇔ T |–Φ
За теоремою істинності із T |–Φ випливає T |=Φ.
Умова T |=Φ для стандартних РНКЧ означає μ|=Φ.
За теоремою 4 із |=Φ випливає, що Φ – субтавтологія.
За наслідком теореми 5 маємо T |–Φ
Наслідок теореми повноти – розв’язність вільних РНКЧ.

Cеквенційні числення РНЛ
Базові секвенційні форми: