CЕКВЕНЦІНІ ЧИСЛЕННЯ КОМПОЗИЦІИНО-НОМІНАТИВНИХ ЛОГІК ЧАСТКОВИХ

Умови замкненості секвенції в різних численнях
Нехай Ξ – множина специфікованих формул.
Введемо для Ξ множини означених та неозначених квазівільних предметних імен, або множини val-змінних та unv-змінних:
val(Ξ)= {x∈V | –|εx∈Ξ};
unv(Ξ) = {x∈V | |–εx∈Ξ}.
Множину нерозподілених для Ξ імен введемо так:
ud(Ξ) = free(Ξ) \ (val(Ξ) ∪ unv(Ξ)).
Базова умови замкненості секвенції |–Γ–|Δ (індукована властивістю С):
С) існує формула Φ: Φ∈Γ та Φ∈Δ.
Властивості СL, СR, СLR, які істотні для відношень |=T, |=F, |=TF, індукують додаткові умови СL, СR, СLR замкненості секвенції |–Γ–|Δ:
СL) існує формула Φ: Φ∈Γ та ¬Φ∈Γ;
СR) існує формула Ψ: Ψ∈Δ та ¬Ψ∈Δ;
СLR) існують формули Φ та Ψ такі: Φ∈Γ, ¬Φ∈Γ, Ψ∈Δ, ¬Ψ∈Δ.
Зрозуміло, що СLR ⇔ СL та СR.

Додаткова умова замкненості секвенції – unv-замкненість(unvalued).
Множиною unv-змінних секвенції |–Γ–|Δ назвемо Un = {u∈V | εu∈Γ}.
При інтерпретатаціях змінні множини Un трактуються як неозначені.
Вводимо Un-unv-форми (unv-форми відносно заданої множини unv-змінних Un)
Нехай R-формула така:
{r1,…, rk, s,…, sk, y1,…, yn} ⊆ Un, {x1,…, xn}∩Un = ∅, {v1,…, vm}∩Un = ∅.
Un-unv-форма формули – це вираз вигляду
де ε позначає невизначене значення.
R-формули Φ та Ψ Un- unv-еквівалентні: Φ та Ψ мають однакові Un-unv-форми.
Якщо R-формули Φ та Ψ Un-unv-еквівалентні, то ΦA(d) = ΨA(d) для кожних моделі мови A та d∈VA, для яких εu(d) = T для всіх u∈Un.
Секвенція |–Γ–|Δ із множиною unv-змінних Un unv-замкнена:
UnС) існує пара Un-unv-еквівалентних R-формул Φ та Ψ таких, що Φ∈Γ та Ψ∈Δ.
Теорема. Якщо секвенція |–Γ–|Δ unv-замкнена, то Γ |= Δ.

Числення QG
Формалізує відношення |=TF (загальна семантика)
Замкненість секвенції визначається умовою C ∨ UnС.
Вводимо такі базові секвенційні форми:

Ми вводимо дві різновидності форм для елімінації кванторів:
– елімінації квантора під реномінацією (∃R-форми)
– елімінації зовнішнього квантора (∃-форми).
Форми |–∃Rε, –|¬∃Rε, |–∃ε, –|¬∃ε назвемо ∃T-формами.

Форми –|∃v, |–¬∃v, –|∃Rv, |–¬∃Rv назвемо ∃F-формами.
Для ∃F-форм умова: |–εy не входить до Σ.

Формули вигляду – ∃T-формули
Формули вигляду – ∃F-формули
При елімінації кванторів додатково застосовуються форми ε-розподілу.
εd за умови: εx не входить до Σ.
εv за умови: z∈VT та z∉nm(Σ).
Маємо три різновидності базових секвенційних форм.
– допоміжні – форми типів RT, ¬RT, ΦU, ¬ΦU, R∃R, ¬R∃R, R∃p ¬R∃p;
– форми ε-розподілу – це εd та εv;
– основнi – всі інші базові секвенційні форми

Числення QL формалізує:
– відношення |=T для неокласичної семантики ЧКНЛ;
– відношення |=F для пересиченої семантики ЧКНЛ.
Умова замкненості секвенції: C ∨ CL ∨ UnС.
Базові секвенційні форми такі ж, як форми числення QG.
Числення QR формалізує:
– відношення |=F для неокласичної семантики ЧКНЛ;
– відношення |=T для пересиченої семантики ЧКНЛ.
Умова замкненості секвенції: C ∨ CR ∨ UnС.
Базові секвенційні форми такі ж, як форми числення QG.
Числення QLR формалізує відношення |=TF для випадку неокласичної семантики та для випадку пересиченої семантики.
Умова замкненості секвенції: C ∨ CLR ∨ UnС.
Базові секвенційні форми такі ж, як форми числення QG.

Числення QC
Формалізує |=Cl (неокласична семантика) та |=Cm (пересичена семантика)
Замкненість секвенції визначається умовою C ∨ UnС.
Базові секвенційні форми числення QC:
|–RT, –|RT, |–ΦU, |–ΦU, |–R∃R, –|R∃R, |–R∃p, –|R∃p,
|− ¬, −| ¬, |−∨, −|∨, |–RR, –|RR, |–R¬, –|R¬, |–R∨, –|R∨,
|–∃ε, |–∃Rε, –|∃v, –|∃Rv, а також форми ε-розподілу εd та εv
Для |=Cl та |=Cm можна знімати заперечення, переносячи формулу з лівої частини наслідку в праву і навпаки, тому в численні QC форми для зовнішнього заперечення не потрібні. Форми |− ¬ та −| ¬ традиційні:

Спектр секвенційних числень чистих першопорядкових КНЛ
|=Cl |=Cm |=T |=F |=TF
_______________________________________________________________
Неокласична QC – QL QR QLR
Пересичена – QC QR QL QLR
Загальна – – QG QG QG
На основі властивостей відношень |= отримуємо основну властивість секвенційних форм:
Теорема 1. Нехай – базові секвенційні форми
Тоді: 1) Λ |= Κ ⇒ Γ |= Δ; Λ |= Κ та Χ |= Ζ ⇒ Γ |= Δ;
2) Γ |≠ Δ ⇒ Λ |≠ Κ; Γ |≠ Δ ⇒ Λ |≠ Κ або Χ |≠ Ζ

Процедура побудова секвенційного дерева
Процедура побудови дерева розбита на етапи. Вона починається з кореня дерева. Кожне застосування секвенційної форми проводиться до скінченної множини доступних на даний момент формул.
Перед побудовою дерева для секвенції Σ зафіксуємо нескінченний список TN "нових" тотально неістотних імен такий, що nm(Σ)∩TN = ∅.
Це означає, що імена із TN не зустрічаються у формулах секвенції Σ.
Виділимо деяке f∈TN (використовується формою εv).
Специфіковані формули вигляду |–εx та –|εx індукуються формами елімінації кванторів, вони не можуть бути в складі секвенції Σ.
На початку кожного етапу – крок доступу: до списку доступних додаємо по одній формулі зі списків T-формул та F-формул.
На початку побудови доступна лише пара перших формул списків (єдина T-формула чи F-формула, якщо один зі списків порожній).
Після додавання до секвенції пари нових доступних формул перевіряємо умову ud(Ξ) = ∅,
де Ξ – множина доступних формул секвенцій на шляху від Σ до цієї η.

ud(Ξ) = free(Ξ) \ val(Ξ) ≠ ∅ та η має ∃F-формули ⇒ виконуємо крок розподілу:
за допомогою εd-форм розподілюємо усі імена ud(Ξ) на означені та неозначені.
Це веде до побудови піддерева висоти m = |ud(Ξ)| з вершиною η:
маємо k = 2m наступників секвенції η: η1,…, ηk.
Якщо було val(Ξ) = ∅, то для одного наступника (нехай η1) маємо val(η1) = ∅; для такої секвенції η1 застосовуємо εv-форму для виділеного f∈TN.
Після цього val(ξ) ≠ ∅ для кожного із наступників ξ секвенцій η1,…, ηk.
Отже, εv-форма застосовується ≤1 разу на шляху
Перед кожним етапом перевіряємо, чи усі листи дерева – замкнені секвенції.
– так ⇒ отримано замкнене секвенційне дерево, процедура виведення завершена позитивно.
– ні ⇒ у випадку виведення скінченної секвенції додатково перевіряємо, чи буде хоч один із листів фінальною секвенцією.
Незамкнена вершина Ω виведення секвенції Σ – фінальна, якщо до неї вже незастосовна жодна секвенційна форма, або якщо кожне застосування форми до Ω не вводить нових формул, відмінних від формул на шляху від Σ до Ω.
Поява фінальної секвенції ⇒ повторення незамкненої секвенції на даному шляху ⇒ є незамкнений шлях ⇒ процедура виведення завершена негативно

Якщо процедура не завершена, то для кожного незамкненого листа ξ робимо наступний крок доступу, далі добудовуємо скінченне піддерево з вершиною ξ:
– активізуємо всі доступні (окрім примітивних) формули ξ.
– до кожної активної формули застосовуємо відповідну секвенційну форму.
Після застосування основної форми утворені нею формули на даному етапі пасивні, до таких формул на цьому етапі основні форми не застосовуються.
При виконані основних форм за можливості робимо спрощення, застосовучи допоміжні форми типів RT, ¬RT, ΦN, ¬ΦN, R∃R, ¬R∃R, R∃p, ¬R∃p.
Застосування на етапі основних форм проводимо так.
– спочатку виконуємо всі ∃T-форми. При кожному її застосуванні беремо зі списку TN нове z як перше незадіяне на даному шляху від кореня.
– виконуємо форми типу RR, ¬RR, R¬, ¬R¬, R∨, ¬R∨, ¬¬, ∨, ¬∨;
– виконуємо ∃F-форми; кожну ∃F-форму – ∀ у∈val(Θ); Θ – множина доступних формул на шляху від Σ до секвенції, в якій починаємо виконання цих ∃F-форм.
Після виконання кожної форми в секвенції перевіряємо її на замкненість.
Повтори формул у секвенціях усуваємо

Таким чином, при побудові секвенційного дерева можливі такі випадки:
1) Процедуру завершено позитивно, маємо скінченне замкнене дерево.
2) Процедуру завершено негативно, в дереві є скінченний незамкнений шлях.
3) Процедура не завершується, маємо нескінченне дерево. Нескінченне дерево зі скінченним розгалуженням має хоч один нескінченний шлях (лема Кеніга)
У випадках 2) і 3) у дереві існує незамкнений шлях ℘, всі його вершини – незамкнені секвенції. Кожна з формул секвенції Σ зустрінеться на ℘ і стане доступною.
Теорема 2 (коректності). Нехай секвенція |–Γ–|Δ вивідна в численні β. Тоді Γ |=* Δ в семантиці α.
Назву β числення читаємо на перетині стовпця |=* та рядка α (див. табл.).
Якщо секвенція |–Γ–|Δ вивідна, то для неї побудоване замкнене секвенційне дерево. Із процедури побудови дерева випливає:
Λ |=* Κ для кожної його вершини |–Λ–|Κ.
Для листів дерева це випливає з визначень замкненої та unv-замкненої секвенцій. Збереження секвенційними формами відношення |=* (від засновків до висновку) випливає з теореми 1. Тому для кореня дерева |–Γ–|Δ – теж Γ |=* Δ.

Побудова виведення для скінченної секвенції
Опишемо модифіковану процедуру побудови виведення для скінченної Σ.
Процедура побудови дерева розбита на етапи. Вона починається з кореня Σ.
На кожному етапі – 1-кратне застосування сек. форми до формул секвенції.
Перед побудовою дерева зафіксуємо нескінченний список TN "нових" тотально строго неістотних імен такий, що nm(Σ)∩TN = ∅.
Виділимо деяке f∈TN (використовується формою εv).
Початок побудови дерева. Перевіряємо умову ud(Σ) = ∅.
Якщо ud(Σ) = free(Σ) = ∅, то застосовуємо εv-форму для виділеного f∈TN.
Якщо ud(Σ) = free(Σ) ≠ ∅, то виконуємо крок розподілу: за допомогою εd-форм робимо розподіл усіх імен із ud(Σ) на означені та неозначені.
Це веде до побудови піддерева висоти m = |ud(Σ)| з вершиною η: отримуємо k = 2m наступників секвенції η: η1,…, ηk.
Для одного наступника, нехай це η1, маємо val(η1) = ∅;
Для такої η1 застосовуємо εv-форму для виділеного f∈TN.
Після цього val(ξ) ≠ ∅ для кожного із наступників ξ секвенцій η1,…, ηk.
При побудові дерева εv-форма застосовується не більше 1 разу.

Зауваження. Якщо формули початкової секвенції не містять символів квантифікації, то крок розподілу не виконуємо. Зрозуміло, що тоді форми, де фігурують символи квантифікації, також незастосовні.
Перед кожним етапом перевіряємо, чи усі листи дерева – замкнені секвенції.
– так ⇒ отримано замкнене секвенційне дерево, процедура виведення завершена позитивно.
– ні ⇒ у випадку виведення скінченної секвенції додатково перевіряємо, чи буде хоч один із листів фінальною секвенцією.
Поява фінальної секвенції ⇒ поява незамкненого шляху ⇒ процедура виведення завершена негативно.
Кроки етапу. Процедура не завершена ⇒ добудовуємо скінченне піддерево з вершиною ξ.
– активізуємо всі доступні (окрім примітивних) формули ξ.
– до кожної активної формули застосовуємо відповідну форму.
Після застосування основної форми утворені нею формули на даному етапі пасивні, до них на цьому етапі основні форми не застосовуються.
При виконані основних форм за можливості робимо спрощення, застосовучи допоміжні форми типів RT, ¬RT, ΦN, ¬ΦN, R∃R, ¬R∃R, R∃p, ¬R∃p

Застосування на етапі основних форм до формул секвенції проводимо так. – виконуємо всі ∃T-форми та форми типу RR, ¬RR, R¬, ¬R¬, R∨, ¬R∨, ¬¬, ∨, ¬∨. При застосуванні ∃T-форми беремо зі списку TN нове z як перше незадіяне на даному шляху від кореня до даної вершини.
– виконуємо ∃F-форми; кожну з них – ∀ у∈val(Θ), де Θ – множина доступних формул на шляху від Σ до секвенції, в якій починаємо виконання цих ∃F-форм.
Після виконання кожної форми в секвенції перевіряємо її на замкненість.
Повтори формул у секвенціях усуваємо.
Таким чином, при побудові секвенційного дерева можливі такі випадки:
1) Процедуру завершено позитивно, маємо скінченне замкнене дерево.
2) Процедуру завершено негативно, в дереві є скінченний незамкнений шлях.
3) Процедура не завершується, маємо нескінченне дерево. За лемою Кеніга в дереві існує хоча б один нескінченний шлях.
У випадках 2) і 3) у дереві існує незамкнений шлях ℘, всі його вершини – незамкнені секвенції. Кожна з формул секвенції Σ зустрінеться на ℘ і стане доступною

Теореми про контрмоделі
Теореми повноти секвенційних числень ЧКНЛ опираються на теореми про існування контрмоделі для множини формул незамкненого шляху.
Для доведення теореми про контрмоделі використовується метод модельних (хінтікківських) множин.
Теорема 3. Нехай ℘ – незамкнений шлях у секвенційному дереві, збудованому для секвенції |–Γ–|Δ, нехай Н – множина всіх специфікованих формул секвенцій цього шляху. Тоді існують моделі мови A = (A, I1), B = (A, I2) та δ, η∈VA такі:
1) |–Φ∈Н ⇒ δ∈T(ΦA) та –|Φ∈Н ⇒ δ∉T(ΦA);
2) |–Φ∈Н ⇒ η∉F(ΦB) та –|Φ∈Н ⇒ η∈F(ΦB).
Пари (A, δ) та (B, η) із такими властивостями назвемо T-контрмоделлю та F-контрмоделлю для секвенції |–Γ–|Δ.
Доведення. Для Н задамо множини означених імен та неозначених імен
W = { y∈V | –|εy∈Н} та Un = {y∈V | |–εy∈Н}

Застосування секвенційних форм до секвенцій шляху ℘ відбувається до тих пір, поки це можливо, тому кожна непримітивна формула чи її заперечення, що зустрічається на шляху ℘, рано чи пізно буде розкладена чи спрощена.
Усі секвенції шляху ℘ незамкнені, тому для них не виконується умова замкненості C ∨ UnС. Отже, для Н виконуються такі умови коректності:
НС) не існує примітивної формули Φ такої, що |–Φ∈Н та –|Φ∈Н;
НСU) не існує примітивних Un-unv-еквівалентних формул
Переходи від нижчої вершини шляху ℘ до вищої відбуваються згідно з відповідною секвенційною формою, тому для Н вірні такі умови переходу:

Н¬¬) |–¬¬Φ∈Н ⇒ |–Φ∈Н
–|¬¬Φ∈Н ⇒ –|Φ∈Н
Н∨) |–Φ∨Ψ∈Н ⇒ |–Φ∈Н або |–Ψ∈Н
–|Φ∨Ψ∈Н ⇒ –|Φ∈Н та –|Ψ∈Н
Н¬∨) |–¬(Φ∨Ψ)∈Н ⇒ |–¬Φ∈Н та |–¬Ψ∈Н
–|¬(Φ∨Ψ)∈Н ⇒ –|¬Φ∈Н або –|¬Ψ∈Н

Mножинy специфікованих формул Н, для якої виконуються ці умови, назвемо G-модельною. Побудуємо контрмодель за G-модельною множиною Н.
Візьмемо деяку множину А таку, що |А| = |W|, та деякі ін’єктивні δ, η∈VA з asn(δ) = W. Така А дублює множину W. Задамо значення базових предикатів та їх заперечень на δ і η та на іменних множинах вигляду
– |–εy∈Н ⇒ δ∈T(εy) та η∉F(εy);
– –|εy∈Н ⇒ δ∉T(εy) та η∈F(εy);
– |– р∈Н ⇒ δ∈T(рA) та η∉F(рB);
– –| р∈Н ⇒ δ∉T(рA) та η∈F(рB);
– |–¬р∈Н ⇒δ∈T(¬pA) та η∉F(¬pB);
– –|¬p∈Н ⇒ δ∉T(¬pA) та η∈F(¬pB);
Для атомарних формул і формул вигляду та їх заперечень твердження теореми випливає з визначення базових предикатів. Далі доводимо традиційно: індукцією за складністю формули згідно з пунктами визначення множини Н.

Для числень QL, QR, QLR теорема про контрмоделі формулюється аналогічно. Відмінність – у різних умовах коректності модельної множини. Такі умови НСL, НСR, НСLR отримуємо із умов СL, СR, СLR замкненості секвенції:
НСL) не існує примітивної формули Φ такої, що |–Φ∈Н та |–¬Φ∈Н;
НСR) не існує примітивної формули Ψ такої, що –|Ψ∈Н та –|¬Ψ∈Н;
НСLR) не існує примітивних формул Φ та Ψ таких, що виконуються умови:
|–Φ∈Н, |–¬Φ∈Н, –|Ψ∈Н, –|¬Ψ∈Н.
Зрозуміло, що НСLR ⇔ НСL ∨ НСR.
Mножина специфікованих формул Н, для якої виконуються умови переходу G-модельної множини:
– L-модельна, якщо для Н виконуються умови коректності НС, НСL, НСU;
– R-модельна, якщо для Н виконуються умови коректності НС, НСR, НСU;
– LR-модельна, якщо для Н виконуються умови коректності НС, НСLR, НСU.
Зауваження. Для T-контрмоделі δ невиконання умови НСL, тобто наявність формули Φ такої, що |–Φ∈Н та |–¬Φ∈Н, дає δ∈T(ΦA) та δ∈T(¬ΦA) = F(ΦA), звідки маємо неоднозначність ΦA .
Для F-контрмоделі η невиконання умови НСR, тобто наявність Φ такої, що –|Φ∈Н та –|¬Φ∈Н, дає η∈F(ΦB) та η∈F(¬ΦB) = T(ΦB), звідки неоднозначність ΦB .

Сформулюємо теорему про контрмоделі для числення QС.
Теорема 4. Нехай ℘ – незамкнений шлях у секвенційному дереві, збудованому для секвенції |–Γ–|Δ, нехай Н – множина всіх специфікованих формул секвенцій шляху ℘. Тоді існують моделі мови A = (A, I1), B = (A, I2) та δ, η∈VA такі:
1) |–Φ∈Н ⇒ δ∈T(ΦA) та –|Φ∈Н ⇒ δ∈F(ΦA);
2) |–Φ∈Н ⇒ η∉F(ΦB) та –|Φ∈Н ⇒ η∉T(ΦB).
Пари (A, δ) та (B, η) із такими властивостями будемо називати Cl-контрмоделлю та Cm-контрмоделлю для секвенції |–Γ–|Δ.
Доведення. Задамо W = {y∈V | –|εy∈Н} та Un = {y∈V | |–εy∈Н}.
Усі секвенції шляху ℘ незамкнені, тому для них не виконується умова замкненості C ∨ UnС. Застосування форм до секвенцій шляху ℘ відбувається до тих пір, поки це можливо, тому кожна непримітивна формула на шляху ℘ буде розкладена чи спрощена згідно з відповідною секвенційною формою числення QС.
Отже, для Н виконуються:
– умови коректності НС і НСU
– умови переходу
Н¬, Н∨, НRT, НΦN, НR∃R, НR∃p, НRR, НR¬, НR∨, Н∃, Н∃R

Тут умова Н¬:
Н¬) |–¬Φ∈Н ⇒ –|Φ∈Н;
–|¬Φ∈Н ⇒ |–Φ∈Н.
Множину Н із такими властивостями назвемо C-модельною.
Візьмемо деяку множину А таку, що |А| = |W|, та деякі ін’єктивні δ, η∈VA з asn(δ) = W. Задамо значення базових предикатів та їх заперечень на δ і η та на іменних множинах вигляду
– |–εy∈Н ⇒ δ∈T(εy) та η∉F(εy);
– –|εy∈Н ⇒ δ∈F(εy) та η∉T(εy);
– |– р∈Н ⇒ δ∈T(рA) та η∉F(рB);
– –| р∈Н ⇒ δ∈F(рA) та η∉T(рB);
Для атомарних формул і формул вигляду та їх заперечень твердження теореми випливає з визначення базових предикатів.
Далі доводимо традиційно: індукцією за складністю формули згідно з пунктами визначення згідно з пунктами визначення C-модельної множини.

Теореми повноти
На основі теорем про контрмоделі маємо теореми повноти для числень ЧКНЛ.
Теорема 5. Нехай Γ |=* Δ в семантиці α. Тоді секвенція |–Γ–|Δ вивідна в численні β.
Назву β числення читаємо на перетині стовпця |=* та рядка α (див. табл.).
1. Доведення для |=TF в загальній семантиці та числення QG.
Нехай супротивне: Γ |=TF Δ та секвенція |–Γ–|Δ невивідна. Якщо |–Γ–|Δ невивідна, то секвенційне дерево для |–Γ–|Δ незамкнене, тому в ньому існує незамкнений шлях ℘. Нехай Н – множина всіх специфікованих формул секвенцій шляху ℘. Тоді |–Γ–|Δ ⊆ Н
За теоремою 3 існують T-контрмодель (A, δ) та F-контрмодель (B, η) такі:
|–Φ∈Н ⇒ δ∈T(ΦA) та –|Φ∈Н ⇒ δ∉T(ΦA);
|–Φ∈Н ⇒ η∉F(ΦB) та –|Φ∈Н ⇒ η∈F(ΦB).
Враховуючи |–Γ–|Δ ⊆ Н, отримуємо:
T-контрмодель: для всіх Φ∈Γ маємо δ∈T(ΦA), для всіх Ψ∈Δ маємо δ∉T(ΨA). Звідси δ∈T(ΓA) та δ∉T(ΔA) ⇒ невірно T(ΓA) ⊆ T(ΔA). Останнє заперечує Γ A|=T Δ, тому й заперечує Γ |=TF Δ.
F-контрмодель: для всіх Φ∈Γ маємо η∉F(ΦB), для всіх Ψ∈Δ маємо η∈F(ΨB). Звідси η∉F(ΓB) та η∈F(ΔB) ⇒ невірно F(ΔB) ⊆ F(ΓB). Останнє заперечує Γ B|=F Δ, тому й заперечує Γ |=TF Δ.

2. Доведення для |=TF в неокласичній чи пересиченій семантиці та QLR.
Аналогічно п.1 отримуємо, що існують T-контрмодель (A, δ) та F-контрмодель (B, η) такі:
|–Φ∈Н ⇒ δ∈T(ΦA) та –|Φ∈Н ⇒ δ∉T(ΦA);
|–Φ∈Н ⇒ η∉F(ΦB) та –|Φ∈Н ⇒ η∈F(ΦB).
Якщо при виконанні НСLR невірна НСL (тоді НСR), то для T-контрмоделі маємо неоднозначний предикат, а для F-контрмоделі – нетотальний предикат, тому для логіки однозначних предикатів беремо F-контрмодель, а для логіки тотальних предикатів – T-контрмодель.
Якщо при виконанні НСLR невірна НСR (тоді НСL), то для F-контрмоделі маємо неоднозначний предикат, а для T-контрмоделі – нетотальний предикат, тому для логіки однозначних предикатів беремо T-контрмодель, а для логіки тотальних предикатів – F-контрмодель.
Якщо вірні НСL i НСR, то можна брати як T-контрмодель, так і F-контрмодель.
Далі доводимо так, як в п.1.

3. Доведення для |=T в неокласичній семантиці та QL.
Нехай супротивне: Γ |=T Δ та секвенція |–Γ–|Δ невивідна. Якщо |–Γ–|Δ невивідна, то секвенційне дерево для |–Γ–|Δ незамкнене, тому в ньому існує незамкнений шлях ℘. Нехай Н – множина всіх специфікованих формул секвенцій шляху ℘. Тоді |–Γ–|Δ ⊆ Н
За теоремою про контрмодель існує T-контрмодель (A, δ) така:
|–Φ∈Н ⇒ δ∈T(ΦA) та –|Φ∈Н ⇒ δ∉T(ΦA).
Згідно з |–Γ–|Δ ⊆ Н для всіх Φ∈Γ маємо δ∈T(ΦA), для всіх Ψ∈Δ маємо δ∉T(ΨA). Звідси δ∈T(ΓA) та δ∉T(ΔA), тому невірно T(ΓA) ⊆ T(ΔA). Це заперечує Γ |=T Δ.
4. Доведення для |=F в пересиченій семантиці та QL.
Нехай супротивне: Γ |=F Δ та секвенція |–Γ–|Δ невивідна. Якщо |–Γ–|Δ невивідна, то секвенційне дерево для |–Γ–|Δ незамкнене, тому в ньому існує незамкнений шлях ℘. Нехай Н – множина всіх специфікованих формул секвенцій шляху ℘. Тоді |–Γ–|Δ ⊆ Н
За теоремою про контрмодель існує F-контрмодель (B, η) така:
|–Φ∈Н ⇒ η∉F(ΦB) та–|Φ∈Н ⇒ η∈F(ΦB).
Згідно з |–Γ–|Δ ⊆ Н для всіх Φ∈Γ маємо η∉F(ΦB), для всіх Ψ∈Δ маємо η∈F(ΨB). Звідси η∉F(ΓB) та η∈F(ΔB), тому невірно F(ΔB) ⊆ F(ΓB). Це заперечує Γ |=F Δ.

5. Доведення для |=F в неокласичній семантиці та QR.
Нехай супротивне: Γ |=F Δ та секвенція |–Γ–|Δ невивідна. Якщо |–Γ–|Δ невивідна, то секвенційне дерево для |–Γ–|Δ незамкнене, тому в ньому існує незамкнений шлях ℘. Нехай Н – множина всіх специфікованих формул секвенцій шляху ℘. Тоді |–Γ–|Δ ⊆ Н
За теоремою про контрмодель існує F-контрмодель (B, η) така:
|–Φ∈Н ⇒ η∉F(ΦB) та –|Φ∈Н ⇒ η∈F(ΦB).
Згідно з |–Γ–|Δ ⊆ Н для всіх Φ∈Γ маємо η∉F(ΦB), для всіх Ψ∈Δ маємо η∈F(ΨB). Звідси η∉F(ΓB) та η∈F(ΔB), тому невірно F(ΔB) ⊆ F(ΓB). Це заперечує Γ |=F Δ.
6. Доведення для |=T в пересиченій семантиці та QR.
Нехай супротивне: Γ |=T Δ та секвенція |–Γ–|Δ невивідна. Якщо |–Γ–|Δ невивідна, то секвенційне дерево для |–Γ–|Δ незамкнене, тому в ньому існує незамкнений шлях ℘. Нехай Н – множина всіх специфікованих формул секвенцій шляху ℘. Тоді |–Γ–|Δ ⊆ Н
За теоремою про контрмодель існує T-контрмодель (A, δ) така:
|–Φ∈Н ⇒ δ∈T(ΦA) та –|Φ∈Н ⇒ δ∉T(ΦA).
Згідно з |–Γ–|Δ ⊆ Н для всіх Φ∈Γ маємо δ∈T(ΦA), для всіх Ψ∈Δ маємо δ∉T(ΨA). Звідси δ∈T(ΓA) та δ∉T(ΔA), тому невірно T(ΓA) ⊆ T(ΔA). Це заперечує Γ |=T Δ.

7. Доведення для |=Cl в неокласичній семантиці та QС.
Нехай супротивне: Γ |=CT Δ та секвенція |–Γ–|Δ невивідна. Якщо |–Γ–|Δ невивідна, то секвенційне дерево для |–Γ–|Δ незамкнене, тому в ньому існує незамкнений шлях ℘. Нехай Н – множина всіх специфікованих формул секвенцій шляху ℘. Тоді |–Γ–|Δ ⊆ Н
За теоремою 4 існує Cl-контрмодель (А, δ) така:
|–Φ∈Н ⇒ ΦА(δ) = Т та –|Φ∈Н ⇒ ΦА(δ) = F.
Згідно з |–Γ–|Δ ⊆ Н для всіх Φ∈Γ маємо ΦА(δ) = Т, для всіх Ψ∈Δ маємо ΨА(δ) = F. Звідси δ∈T(ΓB)∩F(ΔB), тому T(ΓB)∩F(ΔB) ≠ ∅. Це суперечить Γ |=Cl Δ.
8. Доведення для |=Cm в пересиченій семантиці та QС.
Нехай супротивне: Γ |=Cm Δ та секвенція |–Γ–|Δ невивідна. Якщо |–Γ–|Δ невивідна, то дерево для |–Γ–|Δ незамкнене, тому в ньому існує незамкнений шлях ℘. Нехай Н – множина всіх специфікованих формул секвенцій шляху ℘. Тоді |–Γ–|Δ ⊆ Н
За теоремою 4 існує Cm-контрмодель (B, η) така:
|–Φ∈Н ⇒ η∉F(ΦB) та –|Φ∈Н ⇒ η∉T(ΦB).
Згідно з |–Γ–|Δ ⊆ Н для всіх Φ∈Γ маємо η∉F(ΦB), для всіх Ψ∈Δ маємо η∉T(ΨB). Звідси η∉F(ΓB)∪T(ΔB), тому F(ΓB)∪T(ΔB) ≠ VA. Це заперечує Γ |=Cm Δ.