Modele canonice
Pentru orice logică modală normală L, poate fi construit un model Kripke (numit model canonic), care validează exact teoremele L, printr-o adaptare a tehnicii standard de a folosi seturi consistente maximale ca modele. Modelele Canonice Kripke joacă un rol similar construcției algebrei Lindenbaum-Tarski în semantica algebrică.
Un set de formule este L-consistent, dacă nu se poate deduce nici o contradicție de la ei folosind axiomele L și modus ponens. Un set maximal L-consecvent (un L-MCS pentru scurt) este un set L-consistent, care nu are supraset corespunzător L-consistent.
Modelul canonic al L este un model Kripke ⟨W, R, ⊩⟩, unde W este setul tuturor L-MCS, iar relațiile R și ⊩ sunt după cum urmează:
X R Y dacă și numai dacă pentru fiecare formula A, dacă ◻ A ∈ X atunci A ∈ Y,
X ⊩ A dacă și numai dacă A ∈ X.
Modelul canonic este un model de L, deoarece fiecare L-MCS conține toate teoremele lui L. Prin lemma lui Zorn, fiecare set L-consistent este conținut într-un L-MCS, în special fiecare formula care nu poate fi dovedită în L are un exemplu în canonul model.
Principala aplicație a modelelor canonice este dovada integrității. Proprietățile modelului canonic al lui K implică imediat completitudinea K în raport cu clasa tuturor cadrelor Kripke. Acest argument nu funcționează pentru L arbitrar, deoarece nu există nicio garanție că cadrul de bază al modelului canonic satisface condițiile cadru ale L.
Spunem că o formulă sau un set X de formule este canonic cu privire la proprietatea P a cadrelor Kripke, dacă
X este valabil în fiecare cadru care satisface P,
pentru orice logică modală normală L care conține X, cadrul de bază al modelului canonic al lui L satisface P.
O uniune de seturi canonice de formule este ea însăși canonică. Din discuția precedentă rezultă că orice logică axiomatică de un set canonic de formule este Kripke completă și compactă.
Axiomele T, 4, D, B, 5, H, G (și astfel orice combinație a acestora) sunt canonice. GL și Grz nu sunt canonice, deoarece nu sunt compacte. Axiomul M în sine nu este canonic (Goldblatt, 1991), dar logica combinată S4.1 (de fapt chiar K4.1) este canonică.
În general, este indiscutabil dacă o anumită axiomă este canonică. Știm o condiție suficient de bună: H. Sahlqvist a identificat o clasă largă de formule (numite acum formule Sahlqvist) astfel încât:
o formulă Sahlqvist este canonică,
clasa de cadre care corespunde unei formule Sahlqvist este definită de primul ordin,
există un algoritm care calculează condiția corespunzătoare a cadrului la o formulă Sahlqvist dată.
Acesta este un criteriu puternic: de exemplu, toate axiomele enumerate mai sus ca fiind canonice sunt (echivalente cu) formulele Sahlqvist. O logică are proprietatea modelului finit (FMP) dacă este completă în raport cu o clasă de cadre finite. O aplicație a acestei noțiuni este chestiunea decidabilității: rezultă din teorema lui Post că o logică modializată recursiv axiomatică L care are FMP este decisabilă, cu condiția să se decidă dacă un anumit cadru finit este un model al lui L. În special, fiecare logică finit axiomatizabilă cu FMP este decisabil.
Există diferite metode pentru stabilirea FMP pentru o logică dată. Rafinările și extensiile construirii modelului canonic funcționează adesea, utilizând instrumente cum ar fi filtrarea sau dezintegrarea. Ca o altă posibilitate, dovezile de completitudine bazate pe calculul secvențial tăiat gratuit produc de obicei modele finite direct.
Cele mai multe dintre sistemele modale utilizate în practică (inclusiv toate cele enumerate mai sus) au FMP.
În unele cazuri, putem folosi FMP pentru a dovedi completitudinea Kripke a unei logici: fiecare logică modală normală este completă cu o clasă de algebre modale, iar o algebră modalitară finită poate fi transformată într-un cadru Kripke. De exemplu, Robert Bull a demonstrat folosind această metodă că orice extensie normală a lui S4.3 are FMP, iar Kripke este completă.
Semantica Kripke are o generalizare directă a logicii cu mai mult de o modalitate. Un cadru Kripke pentru un limbaj cu {◻ i | i ∈ I} ca set de operatori necesari constă dintr-un set non-gol W echipat cu relații binare Ri pentru fiecare i ∈ I. Definirea unei relații de satisfacție este modificată ca urmează:
w ⊩ ◻ i A dacă și numai dacă ∀ u (w R i u ⇒ u ⊩ A).
Modele Carlson
O semantică simplificată, descoperită de Tim Carlson, este adesea folosită pentru logica probulenței polimodale. Un model Carlson este o structură ⟨W, R, {D i} i ∈ I, ⊩⟩ cu o singură relație de accesibilitate R și submulțim Di ⊆ W pentru fiecare modalitate. Satisfacția este definită ca:
w ⊩ ◻ i A dacă și numai dacă ∀ u ∈ D i (w R u ⇒ u ⊩ A).
Modelele Carlson sunt mai ușor de vizualizat și de utilizat decât modelele Kripke polimodale uzuale; există, cu toate acestea, logica Kripke polimodală completă, care este incompletă de Carlson.
În considerentele semantice privind logica modală, publicat în 1963, Kripke a răspuns la o dificultate cu teoria cuantificării clasice. Motivația abordării relative a lumii a fost aceea de a reprezenta posibilitatea ca obiectele dintr-o singură lume să nu reușească să existe în altul. Cu toate acestea, dacă se utilizează reguli standard de cuantificare, fiecare termen trebuie să se refere la ceva care există în toate lumile posibile. Acest lucru pare incompatibil cu practica obișnuită de a folosi termeni pentru a se referi la lucruri care există în mod contingent.
Răspunsul lui Kripke la această dificultate a fost eliminarea termenilor. El a dat un exemplu de sistem care folosește interpretarea relativă a lumii și păstrează regulile clasice. Cu toate acestea, costurile sunt grave. În primul rând, limba sa este în mod artificial sărăcită, iar în al doilea rând, regulile logicii modale propice trebuie să fie slăbite.
Teoria lumii posibile a lui Kripke a fost folosită de naratologi (începând cu Pavel și Dolezel) pentru a înțelege “manipularea cititorului a dezvoltărilor alternative de complot sau a seriei de acțiuni alternative planificate sau fantastice”. Această aplicație a devenit deosebit de utilă în analiza hiperfecției .
Lasă un răspuns