Содержание
- 2. Умови замкненості секвенції в різних численнях Нехай Ξ – множина специфікованих формул. Введемо для Ξ множини
- 3. Додаткова умова замкненості секвенції – unv-замкненість(unvalued). Множиною unv-змінних секвенції |–Γ–|Δ назвемо Un = {u∈V | εu∈Γ}.
- 4. Числення QG Формалізує відношення |=TF (загальна семантика) Замкненість секвенції визначається умовою C ∨ UnС. Вводимо такі
- 8. Ми вводимо дві різновидності форм для елімінації кванторів: – елімінації квантора під реномінацією (∃R-форми) – елімінації
- 9. Форми –|∃v, |–¬∃v, –|∃Rv, |–¬∃Rv назвемо ∃F-формами. Для ∃F-форм умова: |–εy не входить до Σ.
- 10. Формули вигляду – ∃T-формули Формули вигляду – ∃F-формули При елімінації кванторів додатково застосовуються форми ε-розподілу. εd
- 11. Числення QL формалізує: – відношення |=T для неокласичної семантики ЧКНЛ; – відношення |=F для пересиченої семантики
- 12. Числення QC Формалізує |=Cl (неокласична семантика) та |=Cm (пересичена семантика) Замкненість секвенції визначається умовою C ∨
- 13. Спектр секвенційних числень чистих першопорядкових КНЛ |=Cl |=Cm |=T |=F |=TF _______________________________________________________________ Неокласична QC – QL
- 14. Процедура побудова секвенційного дерева Процедура побудови дерева розбита на етапи. Вона починається з кореня дерева. Кожне
- 15. ud(Ξ) = free(Ξ) \ val(Ξ) ≠ ∅ та η має ∃F-формули ⇒ виконуємо крок розподілу: за
- 16. Якщо процедура не завершена, то для кожного незамкненого листа ξ робимо наступний крок доступу, далі добудовуємо
- 17. Таким чином, при побудові секвенційного дерева можливі такі випадки: 1) Процедуру завершено позитивно, маємо скінченне замкнене
- 18. Побудова виведення для скінченної секвенції Опишемо модифіковану процедуру побудови виведення для скінченної Σ. Процедура побудови дерева
- 19. Зауваження. Якщо формули початкової секвенції не містять символів квантифікації, то крок розподілу не виконуємо. Зрозуміло, що
- 20. Застосування на етапі основних форм до формул секвенції проводимо так. – виконуємо всі ∃T-форми та форми
- 21. Теореми про контрмоделі Теореми повноти секвенційних числень ЧКНЛ опираються на теореми про існування контрмоделі для множини
- 22. Застосування секвенційних форм до секвенцій шляху ℘ відбувається до тих пір, поки це можливо, тому кожна
- 25. Н¬¬) |–¬¬Φ∈Н ⇒ |–Φ∈Н –|¬¬Φ∈Н ⇒ –|Φ∈Н Н∨) |–Φ∨Ψ∈Н ⇒ |–Φ∈Н або |–Ψ∈Н –|Φ∨Ψ∈Н ⇒ –|Φ∈Н
- 26. Mножинy специфікованих формул Н, для якої виконуються ці умови, назвемо G-модельною. Побудуємо контрмодель за G-модельною множиною
- 27. Для числень QL, QR, QLR теорема про контрмоделі формулюється аналогічно. Відмінність – у різних умовах коректності
- 28. Сформулюємо теорему про контрмоделі для числення QС. Теорема 4. Нехай ℘ – незамкнений шлях у секвенційному
- 29. Тут умова Н¬: Н¬) |–¬Φ∈Н ⇒ –|Φ∈Н; –|¬Φ∈Н ⇒ |–Φ∈Н. Множину Н із такими властивостями назвемо
- 30. Теореми повноти На основі теорем про контрмоделі маємо теореми повноти для числень ЧКНЛ. Теорема 5. Нехай
- 31. 2. Доведення для |=TF в неокласичній чи пересиченій семантиці та QLR. Аналогічно п.1 отримуємо, що існують
- 32. 3. Доведення для |=T в неокласичній семантиці та QL. Нехай супротивне: Γ |=T Δ та секвенція
- 33. 5. Доведення для |=F в неокласичній семантиці та QR. Нехай супротивне: Γ |=F Δ та секвенція
- 34. 7. Доведення для |=Cl в неокласичній семантиці та QС. Нехай супротивне: Γ |=CT Δ та секвенція
- 36. Скачать презентацию
Слайд 2Умови замкненості секвенції в різних численнях
Нехай Ξ – множина специфікованих формул.
Умови замкненості секвенції в різних численнях
Нехай Ξ – множина специфікованих формул.
![Умови замкненості секвенції в різних численнях Нехай Ξ – множина специфікованих формул.](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-1.jpg)
Введемо для Ξ множини означених та неозначених квазівільних предметних імен, або множини 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.
Слайд 3Додаткова умова замкненості секвенції – unv-замкненість(unvalued).
Множиною unv-змінних секвенції |–Γ–|Δ назвемо Un = {u∈V | εu∈Γ}.
Додаткова умова замкненості секвенції – unv-замкненість(unvalued).
Множиною unv-змінних секвенції |–Γ–|Δ назвемо Un = {u∈V | εu∈Γ}.
![Додаткова умова замкненості секвенції – unv-замкненість(unvalued). Множиною unv-змінних секвенції |–Γ–|Δ назвемо Un](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-2.jpg)
При інтерпретатаціях змінні множини 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-замкнена, то Γ |= Δ.
Слайд 4 Числення QG
Формалізує відношення |=TF (загальна семантика)
Замкненість секвенції визначається умовою
Числення QG
Формалізує відношення |=TF (загальна семантика)
Замкненість секвенції визначається умовою
![Числення QG Формалізує відношення |=TF (загальна семантика) Замкненість секвенції визначається умовою C](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-3.jpg)
Вводимо такі базові секвенційні форми:
Слайд 8 Ми вводимо дві різновидності форм для елімінації кванторів:
– елімінації
Ми вводимо дві різновидності форм для елімінації кванторів:
– елімінації
![Ми вводимо дві різновидності форм для елімінації кванторів: – елімінації квантора під](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-7.jpg)
– елімінації зовнішнього квантора (∃-форми).
Форми |–∃Rε, –|¬∃Rε, |–∃ε, –|¬∃ε назвемо ∃T-формами.
Слайд 9
Форми –|∃v, |–¬∃v, –|∃Rv, |–¬∃Rv назвемо ∃F-формами.
Для ∃F-форм умова: |–εy
Форми –|∃v, |–¬∃v, –|∃Rv, |–¬∃Rv назвемо ∃F-формами.
Для ∃F-форм умова: |–εy
![Форми –|∃v, |–¬∃v, –|∃Rv, |–¬∃Rv назвемо ∃F-формами. Для ∃F-форм умова: |–εy не входить до Σ.](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-8.jpg)
Слайд 10Формули вигляду – ∃T-формули
Формули вигляду – ∃F-формули
При елімінації кванторів додатково
Формули вигляду – ∃T-формули
Формули вигляду – ∃F-формули
При елімінації кванторів додатково
![Формули вигляду – ∃T-формули Формули вигляду – ∃F-формули При елімінації кванторів додатково](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-9.jpg)
εd за умови: εx не входить до Σ.
εv за умови: z∈VT та z∉nm(Σ).
Маємо три різновидності базових секвенційних форм.
– допоміжні – форми типів RT, ¬RT, ΦU, ¬ΦU, R∃R, ¬R∃R, R∃p ¬R∃p;
– форми ε-розподілу – це εd та εv;
– основнi – всі інші базові секвенційні форми
Слайд 11Числення QL формалізує:
– відношення |=T для неокласичної семантики ЧКНЛ;
– відношення |=F для
Числення QL формалізує:
– відношення |=T для неокласичної семантики ЧКНЛ;
– відношення |=F для
![Числення QL формалізує: – відношення |=T для неокласичної семантики ЧКНЛ; – відношення](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-10.jpg)
Умова замкненості секвенції: C ∨ CL ∨ UnС.
Базові секвенційні форми такі ж, як форми числення QG.
Числення QR формалізує:
– відношення |=F для неокласичної семантики ЧКНЛ;
– відношення |=T для пересиченої семантики ЧКНЛ.
Умова замкненості секвенції: C ∨ CR ∨ UnС.
Базові секвенційні форми такі ж, як форми числення QG.
Числення QLR формалізує відношення |=TF для випадку неокласичної семантики та для випадку пересиченої семантики.
Умова замкненості секвенції: C ∨ CLR ∨ UnС.
Базові секвенційні форми такі ж, як форми числення QG.
Слайд 12 Числення QC
Формалізує |=Cl (неокласична семантика) та |=Cm (пересичена семантика)
Замкненість
Числення QC
Формалізує |=Cl (неокласична семантика) та |=Cm (пересичена семантика)
Замкненість
![Числення QC Формалізує |=Cl (неокласична семантика) та |=Cm (пересичена семантика) Замкненість секвенції](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-11.jpg)
Базові секвенційні форми числення 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 форми для зовнішнього заперечення не потрібні. Форми |− ¬ та −| ¬ традиційні:
Слайд 13 Спектр секвенційних числень чистих першопорядкових КНЛ
|=Cl |=Cm |=T |=F |=TF
_______________________________________________________________
Неокласична
Спектр секвенційних числень чистих першопорядкових КНЛ
|=Cl |=Cm |=T |=F |=TF
_______________________________________________________________
Неокласична
![Спектр секвенційних числень чистих першопорядкових КНЛ |=Cl |=Cm |=T |=F |=TF _______________________________________________________________](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-12.jpg)
Пересичена – QC QR QL QLR
Загальна – – QG QG QG
На основі властивостей відношень |= отримуємо основну властивість секвенційних форм:
Теорема 1. Нехай – базові секвенційні форми
Тоді: 1) Λ |= Κ ⇒ Γ |= Δ; Λ |= Κ та Χ |= Ζ ⇒ Γ |= Δ;
2) Γ |≠ Δ ⇒ Λ |≠ Κ; Γ |≠ Δ ⇒ Λ |≠ Κ або Χ |≠ Ζ
Слайд 14Процедура побудова секвенційного дерева
Процедура побудови дерева розбита на етапи. Вона починається
Процедура побудова секвенційного дерева
Процедура побудови дерева розбита на етапи. Вона починається
![Процедура побудова секвенційного дерева Процедура побудови дерева розбита на етапи. Вона починається](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-13.jpg)
Перед побудовою дерева для секвенції Σ зафіксуємо нескінченний список TN "нових" тотально неістотних імен такий, що nm(Σ)∩TN = ∅.
Це означає, що імена із TN не зустрічаються у формулах секвенції Σ.
Виділимо деяке f∈TN (використовується формою εv).
Специфіковані формули вигляду |–εx та –|εx індукуються формами елімінації кванторів, вони не можуть бути в складі секвенції Σ.
На початку кожного етапу – крок доступу: до списку доступних додаємо по одній формулі зі списків T-формул та F-формул.
На початку побудови доступна лише пара перших формул списків (єдина T-формула чи F-формула, якщо один зі списків порожній).
Після додавання до секвенції пари нових доступних формул перевіряємо умову ud(Ξ) = ∅,
де Ξ – множина доступних формул секвенцій на шляху від Σ до цієї η.
Слайд 15 ud(Ξ) = free(Ξ) \ val(Ξ) ≠ ∅ та η має ∃F-формули ⇒ виконуємо крок розподілу:
за допомогою
ud(Ξ) = free(Ξ) \ val(Ξ) ≠ ∅ та η має ∃F-формули ⇒ виконуємо крок розподілу:
за допомогою
![ud(Ξ) = free(Ξ) \ val(Ξ) ≠ ∅ та η має ∃F-формули ⇒](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-14.jpg)
Це веде до побудови піддерева висоти m = |ud(Ξ)| з вершиною η:
маємо k = 2m наступників секвенції η: η1,…, ηk.
Якщо було val(Ξ) = ∅, то для одного наступника (нехай η1) маємо val(η1) = ∅; для такої секвенції η1 застосовуємо εv-форму для виділеного f∈TN.
Після цього val(ξ) ≠ ∅ для кожного із наступників ξ секвенцій η1,…, ηk.
Отже, εv-форма застосовується ≤1 разу на шляху
Перед кожним етапом перевіряємо, чи усі листи дерева – замкнені секвенції.
– так ⇒ отримано замкнене секвенційне дерево, процедура виведення завершена позитивно.
– ні ⇒ у випадку виведення скінченної секвенції додатково перевіряємо, чи буде хоч один із листів фінальною секвенцією.
Незамкнена вершина Ω виведення секвенції Σ – фінальна, якщо до неї вже незастосовна жодна секвенційна форма, або якщо кожне застосування форми до Ω не вводить нових формул, відмінних від формул на шляху від Σ до Ω.
Поява фінальної секвенції ⇒ повторення незамкненої секвенції на даному шляху ⇒ є незамкнений шлях ⇒ процедура виведення завершена негативно
Слайд 16 Якщо процедура не завершена, то для кожного незамкненого листа ξ робимо
Якщо процедура не завершена, то для кожного незамкненого листа ξ робимо
![Якщо процедура не завершена, то для кожного незамкненого листа ξ робимо наступний](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-15.jpg)
– активізуємо всі доступні (окрім примітивних) формули ξ.
– до кожної активної формули застосовуємо відповідну секвенційну форму.
Після застосування основної форми утворені нею формули на даному етапі пасивні, до таких формул на цьому етапі основні форми не застосовуються.
При виконані основних форм за можливості робимо спрощення, застосовучи допоміжні форми типів 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-форм.
Після виконання кожної форми в секвенції перевіряємо її на замкненість.
Повтори формул у секвенціях усуваємо
Слайд 17 Таким чином, при побудові секвенційного дерева можливі такі випадки:
1)
Таким чином, при побудові секвенційного дерева можливі такі випадки:
1)
![Таким чином, при побудові секвенційного дерева можливі такі випадки: 1) Процедуру завершено](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-16.jpg)
2) Процедуру завершено негативно, в дереві є скінченний незамкнений шлях.
3) Процедура не завершується, маємо нескінченне дерево. Нескінченне дерево зі скінченним розгалуженням має хоч один нескінченний шлях (лема Кеніга)
У випадках 2) і 3) у дереві існує незамкнений шлях ℘, всі його вершини – незамкнені секвенції. Кожна з формул секвенції Σ зустрінеться на ℘ і стане доступною.
Теорема 2 (коректності). Нехай секвенція |–Γ–|Δ вивідна в численні β. Тоді Γ |=* Δ в семантиці α.
Назву β числення читаємо на перетині стовпця |=* та рядка α (див. табл.).
Якщо секвенція |–Γ–|Δ вивідна, то для неї побудоване замкнене секвенційне дерево. Із процедури побудови дерева випливає:
Λ |=* Κ для кожної його вершини |–Λ–|Κ.
Для листів дерева це випливає з визначень замкненої та unv-замкненої секвенцій. Збереження секвенційними формами відношення |=* (від засновків до висновку) випливає з теореми 1. Тому для кореня дерева |–Γ–|Δ – теж Γ |=* Δ.
Слайд 18Побудова виведення для скінченної секвенції
Опишемо модифіковану процедуру побудови виведення для скінченної
Побудова виведення для скінченної секвенції
Опишемо модифіковану процедуру побудови виведення для скінченної
![Побудова виведення для скінченної секвенції Опишемо модифіковану процедуру побудови виведення для скінченної](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-17.jpg)
Процедура побудови дерева розбита на етапи. Вона починається з кореня Σ.
На кожному етапі – 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 разу.
Слайд 19 Зауваження. Якщо формули початкової секвенції не містять символів квантифікації, то крок
Зауваження. Якщо формули початкової секвенції не містять символів квантифікації, то крок
![Зауваження. Якщо формули початкової секвенції не містять символів квантифікації, то крок розподілу](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-18.jpg)
Перед кожним етапом перевіряємо, чи усі листи дерева – замкнені секвенції.
– так ⇒ отримано замкнене секвенційне дерево, процедура виведення завершена позитивно.
– ні ⇒ у випадку виведення скінченної секвенції додатково перевіряємо, чи буде хоч один із листів фінальною секвенцією.
Поява фінальної секвенції ⇒ поява незамкненого шляху ⇒ процедура виведення завершена негативно.
Кроки етапу. Процедура не завершена ⇒ добудовуємо скінченне піддерево з вершиною ξ.
– активізуємо всі доступні (окрім примітивних) формули ξ.
– до кожної активної формули застосовуємо відповідну форму.
Після застосування основної форми утворені нею формули на даному етапі пасивні, до них на цьому етапі основні форми не застосовуються.
При виконані основних форм за можливості робимо спрощення, застосовучи допоміжні форми типів RT, ¬RT, ΦN, ¬ΦN, R∃R, ¬R∃R, R∃p, ¬R∃p
Слайд 20 Застосування на етапі основних форм до формул секвенції проводимо так.
Застосування на етапі основних форм до формул секвенції проводимо так.
![Застосування на етапі основних форм до формул секвенції проводимо так. – виконуємо](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-19.jpg)
– виконуємо ∃F-форми; кожну з них – ∀ у∈val(Θ), де Θ – множина доступних формул на шляху від Σ до секвенції, в якій починаємо виконання цих ∃F-форм.
Після виконання кожної форми в секвенції перевіряємо її на замкненість.
Повтори формул у секвенціях усуваємо.
Таким чином, при побудові секвенційного дерева можливі такі випадки:
1) Процедуру завершено позитивно, маємо скінченне замкнене дерево.
2) Процедуру завершено негативно, в дереві є скінченний незамкнений шлях.
3) Процедура не завершується, маємо нескінченне дерево. За лемою Кеніга в дереві існує хоча б один нескінченний шлях.
У випадках 2) і 3) у дереві існує незамкнений шлях ℘, всі його вершини – незамкнені секвенції. Кожна з формул секвенції Σ зустрінеться на ℘ і стане доступною
Слайд 21 Теореми про контрмоделі
Теореми повноти секвенційних числень ЧКНЛ опираються на теореми про
Теореми про контрмоделі
Теореми повноти секвенційних числень ЧКНЛ опираються на теореми про
![Теореми про контрмоделі Теореми повноти секвенційних числень ЧКНЛ опираються на теореми про](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-20.jpg)
Для доведення теореми про контрмоделі використовується метод модельних (хінтікківських) множин.
Теорема 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∈Н}
Слайд 22Застосування секвенційних форм до секвенцій шляху ℘ відбувається до тих пір, поки
Застосування секвенційних форм до секвенцій шляху ℘ відбувається до тих пір, поки
![Застосування секвенційних форм до секвенцій шляху ℘ відбувається до тих пір, поки](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-21.jpg)
Усі секвенції шляху ℘ незамкнені, тому для них не виконується умова замкненості C ∨ UnС. Отже, для Н виконуються такі умови коректності:
НС) не існує примітивної формули Φ такої, що |–Φ∈Н та –|Φ∈Н;
НСU) не існує примітивних Un-unv-еквівалентних формул
Переходи від нижчої вершини шляху ℘ до вищої відбуваються згідно з відповідною секвенційною формою, тому для Н вірні такі умови переходу:
Слайд 25Н¬¬) |–¬¬Φ∈Н ⇒ |–Φ∈Н
–|¬¬Φ∈Н ⇒ –|Φ∈Н
Н∨) |–Φ∨Ψ∈Н ⇒ |–Φ∈Н
Н¬¬) |–¬¬Φ∈Н ⇒ |–Φ∈Н
–|¬¬Φ∈Н ⇒ –|Φ∈Н
Н∨) |–Φ∨Ψ∈Н ⇒ |–Φ∈Н
![Н¬¬) |–¬¬Φ∈Н ⇒ |–Φ∈Н –|¬¬Φ∈Н ⇒ –|Φ∈Н Н∨) |–Φ∨Ψ∈Н ⇒ |–Φ∈Н або](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-24.jpg)
–|Φ∨Ψ∈Н ⇒ –|Φ∈Н та –|Ψ∈Н
Н¬∨) |–¬(Φ∨Ψ)∈Н ⇒ |–¬Φ∈Н та |–¬Ψ∈Н
–|¬(Φ∨Ψ)∈Н ⇒ –|¬Φ∈Н або –|¬Ψ∈Н
Слайд 26Mножинy специфікованих формул Н, для якої виконуються ці умови, назвемо G-модельною. Побудуємо
Mножинy специфікованих формул Н, для якої виконуються ці умови, назвемо G-модельною. Побудуємо
![Mножинy специфікованих формул Н, для якої виконуються ці умови, назвемо G-модельною. Побудуємо](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-25.jpg)
Візьмемо деяку множину А таку, що |А| = |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);
Для атомарних формул і формул вигляду та їх заперечень твердження теореми випливає з визначення базових предикатів. Далі доводимо традиційно: індукцією за складністю формули згідно з пунктами визначення множини Н.
Слайд 27Для числень QL, QR, QLR теорема про контрмоделі формулюється аналогічно. Відмінність –
Для числень QL, QR, QLR теорема про контрмоделі формулюється аналогічно. Відмінність –
![Для числень QL, QR, QLR теорема про контрмоделі формулюється аналогічно. Відмінність –](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-26.jpg)
НС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 .
Слайд 28Сформулюємо теорему про контрмоделі для числення QС.
Теорема 4. Нехай ℘ – незамкнений шлях
Сформулюємо теорему про контрмоделі для числення QС.
Теорема 4. Нехай ℘ – незамкнений шлях
![Сформулюємо теорему про контрмоделі для числення QС. Теорема 4. Нехай ℘ –](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-27.jpg)
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
Слайд 29Тут умова Н¬:
Н¬) |–¬Φ∈Н ⇒ –|Φ∈Н;
–|¬Φ∈Н ⇒ |–Φ∈Н.
Множину
Тут умова Н¬:
Н¬) |–¬Φ∈Н ⇒ –|Φ∈Н;
–|¬Φ∈Н ⇒ |–Φ∈Н.
Множину
![Тут умова Н¬: Н¬) |–¬Φ∈Н ⇒ –|Φ∈Н; –|¬Φ∈Н ⇒ |–Φ∈Н. Множину Н](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-28.jpg)
Візьмемо деяку множину А таку, що |А| = |W|, та деякі ін’єктивні δ, η∈VA з asn(δ) = W. Задамо значення базових предикатів та їх заперечень на δ і η та на іменних множинах вигляду
– |–εy∈Н ⇒ δ∈T(εy) та η∉F(εy);
– –|εy∈Н ⇒ δ∈F(εy) та η∉T(εy);
– |– р∈Н ⇒ δ∈T(рA) та η∉F(рB);
– –| р∈Н ⇒ δ∈F(рA) та η∉T(рB);
Для атомарних формул і формул вигляду та їх заперечень твердження теореми випливає з визначення базових предикатів.
Далі доводимо традиційно: індукцією за складністю формули згідно з пунктами визначення згідно з пунктами визначення C-модельної множини.
Слайд 30 Теореми повноти
На основі теорем про контрмоделі маємо теореми повноти для
Теореми повноти
На основі теорем про контрмоделі маємо теореми повноти для
![Теореми повноти На основі теорем про контрмоделі маємо теореми повноти для числень](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-29.jpg)
Теорема 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 Δ.
Слайд 312. Доведення для |=TF в неокласичній чи пересиченій семантиці та QLR.
Аналогічно
2. Доведення для |=TF в неокласичній чи пересиченій семантиці та QLR.
Аналогічно
![2. Доведення для |=TF в неокласичній чи пересиченій семантиці та QLR. Аналогічно](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-30.jpg)
|–Φ∈Н ⇒ δ∈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.
Слайд 323. Доведення для |=T в неокласичній семантиці та QL.
Нехай супротивне: Γ |=T Δ
3. Доведення для |=T в неокласичній семантиці та QL.
Нехай супротивне: Γ |=T Δ
![3. Доведення для |=T в неокласичній семантиці та QL. Нехай супротивне: Γ](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-31.jpg)
За теоремою про контрмодель існує 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 Δ.
Слайд 335. Доведення для |=F в неокласичній семантиці та QR.
Нехай супротивне: Γ |=F Δ
5. Доведення для |=F в неокласичній семантиці та QR.
Нехай супротивне: Γ |=F Δ
![5. Доведення для |=F в неокласичній семантиці та QR. Нехай супротивне: Γ](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-32.jpg)
За теоремою про контрмодель існує 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 Δ.
Слайд 347. Доведення для |=Cl в неокласичній семантиці та QС.
Нехай супротивне: Γ |=CT Δ
7. Доведення для |=Cl в неокласичній семантиці та QС.
Нехай супротивне: Γ |=CT Δ
![7. Доведення для |=Cl в неокласичній семантиці та QС. Нехай супротивне: Γ](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/374782/slide-33.jpg)
За теоремою 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 Δ.