Nusakėme modalinės teiginių logikos simbolius bei taisyklingas formules. Dabar specifikuojame, kada taisyklingos formulės yra teisingos modeliuose. Šiam tikslui mums reikės poros papildomų apibrėžimų.
Kripkės rėmas F – tai dvejetas (W, R), kur formaliai W – tai netuščia aibė, o R apibrėžiame kaip R ⊆ W2. Intuityviai W suprasime kaip galimų pasaulių aibę, o R – kaip prieinamumo sąryšį tarp galimų pasaulių. Toliau Kripkės rėmus vadinsime tiesiog rėmais.
Pabrėžiame, kad nors modalinėje logikoje W intuityviai suprantame kaip aibę galimų pasaulių, tačiau siekiant matematiškai įrodyti, jog ši logika pasižymi tam tikromis savybėmis, ar parodyti tam tikrų samprotavimų pagrįstumą, to galima ir nedaryti. Matematine prasme W yra indeksų, kurių atžvilgiu priskiriame sakiniams logines teisingumo reikšmes, aibė. Indeksų aibės funkciją gali vienodai gerai atlikti ir natūralieji skaičiai, ir bet kurių kitų objektų aibė. Tas pats pasakytina ir apie prieinamumo ryšį R.
Prie Kripkės rėmo prijungiame funkciją, kuri specifikuoja sakinių interpretaciją – nusako, kokie sakiniai yra teisingi kiekviename pasaulyje.
Kripkės modelis (Kripke model) M, paremtas rėmu F – tai trejetas (W, R, V), kur (W, R) = F, o V – tai funkcija iš sakinių kintamųjų aibės PS į aibę galimų pasaulių aibės W poaibių, t. y. V: PS → P(W). Toliau Kripkės modelius vadinsime tiesiog modeliais.
[Tiesa modelyje] Taisyklinga modalinės teiginių logikos formulė φ yra teisinga modelyje M = (W, R, V) galimame pasaulyje w ∊ W (žymime M, w ⊨ φ):
M, w ⊨ p, jei ir tik jei w ∊ V(p);
M, w ⊭⊥;
M, w ⊨ ~φ, jei ir tik jei M, w ⊭ φ;
M, w ⊨ φ & ψ, jei ir tik jei M, w ⊨ φ ir M, w ⊨ ψ;
M, w ⊨ □φ, jei ir tik jei M, w′ ⊨ φ visiems w′ ∊ W, kurie wRw′.
Disjunkcija, implikacija ir ekvivalencija gali būti apibrėžiamos per konjunkciją ir neigimą įprastu būdu. Pažymime, kad pagal anksčiau pateiktą galimybės ◇ apibrėžimą per būtinumą □, t. y. ◇φ := ~□~φ, ir ką tik pateiktą formulės □φ semantiką galime išvesti, jog:
M, w ⊨ ◇φ, jei ir tik jei M, w′ ⊨ φ bent viename w′∊W, kuris wRw′.
Taip pat iš duotų apibrėžimų galime išvesti, jog ~◇φ ≡ □~φ ir ◇~φ ≡ ~□φ: nėra taip, kad galimai φ yra ekvivalentu tam, kad būtina, jog ne-φ, o galimai ne-φ yra ekvivalentu tam, kad nėra taip, kad būtinai φ.
Pateikiame kelis modalinėje logikoje ypač svarbius apibrėžimus:
formulė φ yra tapačiai teisinga modelyje M (žymima M ⊨ φ), jei ir tik jei φ yra teisinga formulė visuose modelio M pasauliuose;
formulė φ yra tapačiai teisinga rėme F (žymima F ⊨ φ), jei ir tik jei φ yra tapačiai teisinga kiekviename modelyje M, kuris yra paremtas rėmu F;
jei L yra rėmų rinkinys, tai sakoma, kad formulė φ yra L-tapačiai teisinga, (žymima ⊨L φ), jei ir tik jei φ yra tapačiai teisinga kiekviename rėme, esančiame L;
formulė yra K-tapačiai teisinga (žymima ⊨K φ), jei ir tik jei φ yra tapačiai teisinga visuose rėmuose;
formulė φ yra išpildoma (modelyje, rėme ar rėmų rinkinyje L), jei ir tik jei ~φ nėra tapačiai teisinga formulė (atitinkamai modelyje, rėme ar rėmų rinkinyje L);
visi modeliai, paremti bet kuriuo rėmu iš L-rėmų, yra L-modeliai.
Skirtingos modalinės teiginių logikos semantiškai nusakomos pagal L-tapačiai teisingų formulių aibes, t. y. iš esmės nurodant skirtingas L-rėmų klases. Pavyzdžiui, jei kalbėsime tik apie visus Kripkės rėmus, kuriuose kiekvienas galimas pasaulis yra prieinamas pats sau, tai turėsime modalinę logiką, kurioje formulė □φ → φ yra tapačiai teisinga. Intuityviai kalbant, tokiuose modeliuose tai, kas būtinai teisinga, yra ir faktiškai teisinga. Jei kalbėsime apie visus Kripkės rėmus nenurodę jokių sąlygų, tai □φ → φ nebus tapačiai teisinga formulė. Dėl šios priežasties modalinėse logikose ypač svarbus tampa prieinamumo sąryšis ir jam keliamos sąlygos. Logika, kurioje rėmams nenurodomos jokios sąlygos, vadinama K.
Kalbėdami apie rėmus pabrėžėme, jog siekiant įrodyti matematines modalinės logikos savybes W nereikia interpretuoti kaip aibės galimų pasaulių. Kaip iliustraciją pateikiame įrodymą, kad □(φ→ ψ) → (□φ →□ψ) yra tapačiai teisinga visuose modeliuose.
Įrodome, kad ⊨K □(φ→ ψ) → (□φ →□ψ).
Tarkime, kad M – tai bet koks modelis, o w – tai bet koks w ∊ W. Taip pat sakykime, kad M, w ⊨K ~(□(φ → ψ) → (□φ → □ψ)), t. y. pagal neigimo ir implikacijos teisingumo sąlygas, M, w ⊨K □(φ → ψ), bet M, w ⊭K (□φ → □ψ). Tai, kad pastaroji implikacija nėra teisinga w, reiškia, kad M, w ⊨K □φ ir M, w ⊨ ~□ψ. Iš fakto, kad ~□ψ yra teisinga formulė w, galime išvesti, kad M, w ⊨◇~ψ (pagal ◇~φ ≡ ~□φ). Tarkime, kad w1 – tai bet koks W narys, kuris wRw1 ir M, w1 ⊨ ~ψ. Kadangi wRw1 ir žinome, kad M, w ⊨K □(φ → ψ) ir M, w ⊨K □φ, tai M, w1 ⊨K (φ → ψ) ir M, w1 ⊨K φ. Kadangi M, w1 ⊨K (φ → ψ), tai M, w1 ⊭K φ arba M, w1 ⊨K ψ. Bet jau žinome, kad M, w1 ⊨K φ, taigi, M, w1 ⊨K ψ. Bet jau anksčiau įrodėme, kad M, w1 ⊨ ~ψ, taigi, gaunamas prieštaravimas. Taigi, priėmę prielaidą, kad M, w ⊨K ~(□(φ→ ψ) → (□φ →□ψ)), gavome prieštaravimą, t. y. M, w1 ⊨K ~ψ ir M, w1 ⊨ ψ. Kadangi ir modelis M, ir w buvo pasirinkti arbitraliai, galime daryti išvadą, kad ⊨K □(φ→ ψ) → (□φ →□ψ). ▮
Dabar nurodome pagrindines formalias sąlygas rėmams. Tarkime, kad (W, R) – tai rėmas F. Sakome, kad F yra:
1. serialus – jei kiekvienam w ∊ W yra toks w′ ∊ W, kuris wRw′;
2. refleksyvus – jei kiekvienam w ∊ W galioja, kad wRw;
3. simetriškas – jei visiems w, w′ ∊ W galioja, kad wRw′ implikuoja w′Rw;
4. tranzityvus – jei visiems w, w′, w′′ ∊ W galioja, kad jei wRw′ ir w′Rw′′, tai wRw′′.
Atitinkamai sakome, kad modelis yra serialus (refleksyvus, simetriškas, tranzityvus), jei rėmas, kuriuo paremtas modelis, yra serialus (refleksyvus, simetriškas, tranzityvus).