Tam, kad apibrėžtume nekintamo domeno predikatų modalinės logikos semantiką, mums reikės poros papildomų terminų. Nekintamo domeno papildytas Kripkės rėmas G – tai trejetas (W, R, D), kai W – tai aibė galimų pasaulių, R – prieinamumo ryšys tarp galimų pasaulių, R ⊆ W2, o D – tai netuščia aibė, vadinama rėmo domenu. Intuityviai, D – tai aibė individų. Sakome, kad rėmas yra papildytas, nes modalinės teiginių logikos rėmą papildėme nauju elementu D. Anksčiau aptartoje modalinėje teiginių logikoje interpretacinė funkcija specifikavo, kurie sakiniai yra teisingi kuriuose galimuose pasauliuose. Atitinkamai predikatų logikoje interpretacinė funkcija specifikuos kiekvieno predikato ekstensiją kiekviename galimame pasaulyje ir kiekvienos individinės konstantos denotaciją. Nekintamo domeno modelis M, paremtas nekintamo domeno papildytu Kripkės rėmu G – tai ketvertas (W, R, D, V), kur (W, R, D) = G, o V – tai interpretacinė funkcija, kuri (i) kiekvienam w∊W ir n-viečiam predikatui P priskiria n-vietį domeno D sąryšį, t. y. V(P, w) ⊆ Dn; ir (ii) visoms individinėms konstantoms a priskiria objektą iš D, t. y. V(a)∊D. Pabrėžiame, kad šiame modelyje individinės konstantos visuose galimuose pasauliuose turi tą pačią denotaciją. Įprastai po Kripkės paskaitų ciklo Vardai ir būtinumas (1980) priimama, kad vardai visuose galimuose pasauliuose nurodo į tą patį objektą, t. y. priimama, kad vardai yra rigidiniai dezignatoriai (plačiau žr. Rigidiniai dezignatoriai). Sakykime, kad KINT – tai aibė visų mūsų formalioje kalboje esančių kintamųjų aibė, o TERM – tai aibė visų termų. Kintamųjų priskyrimo funkcija a modelyje M – tai funkcija iš kintamųjų aibės KINT į modelio domeną D, kuri kiekvienam kintamajam priskiria domeno narį, t. y. kiekvienam kintamajam x, a(x)∊D. Žymėkime a[d / x] tokią pat kintamųjų priskyrimo funkcija, kaip ir a, išskyrus tai, kad a[d / x] x-ui priskiria objektą d iš domeno D. Atžvilgiu modelio M ir kintamųjų priskyrimo funkcijos a, termų denotacinė funckija dena – tai funkcija iš TERM į modelio domeną D, kuri kiekvienam termui priskiria domeno narį. Funkcijos reikšmę nustatome tokiu būdu: jei t yra konstanta, tai dena(t)=V(t), o jei t yra kintamasis, tai dena(t)= a(t). [Tiesa modelyje] Taisyklinga modalinės predikatų logikos formulė φ yra teisinga nekintamo domeno modelyje M=(W, R, D, V), modelio galimame pasaulyje w∊W, remiantis kintamųjų priskyrimo funkciją a (žymime M, w, a ⊨ φ), kai: M, w, a ⊨ P(t1, …, tn), jei ir tik jei (dena(t1), …, dena(tn)) ∊ V(P, w); M, w, a ⊨ t1 = t2, jei ir tik jei dena(t1)= dena(t2); M, w, a ⊨ ~φ, jei ir tik jei M, w, a ⊭ φ; M, w, a ⊨ φ & ψ, jei ir tik jei M, w, a ⊨ φ ir M, w ⊨ ψ; M, w, a ⊨ □φ, jei ir tik jei M, w′, a ⊨ φ visiems w′∊W, kurie wRw′; M, w, a ⊨ ◇φ, jei ir tik jei M, w′, a ⊨ φ bent viename w′∊W, kuris wRw′; M, w, a ⊨ ∃xφ, jei ir tik jei M, w, a[d / x] ⊨ φ bent vienam d ∊ D; M, w, a ⊨ ∀xφ, jei ir tik jei M, w, a[d / x] ⊨ φ visiems d ∊ D. Intuityviai kalbant, objektai, kurie yra termų t1, …, tn semantinės reikšmės, yra sąryšyje P, galimame pasaulyje w, jei ir tik jei jie patenka į to predikato ekstensiją galimame pasaulyje w. Predikato ekstensija gali kisti skirtinguose galimuose pasauliuose. Pavyzdžiui, jei dvivietis predikatas P reiškia būti gimus tais pačiai metais, tai nors Valdas Adamkus ir Michelis Foucault faktiniame pasaulyje yra susieti šiuo sąryšiu (t. y. abu gimę 1926 metais), tačiau jei Adamkus būtų gimęs dviem mėnesiais vėliau, tai jie nebūtų susieti šiuo sąryšiu (Adamkus gimė lapkričio 3-ią dieną). Sakome, kad visi x yra tokie, kad φ yra teisinga formulė, jei ir tik jei, kad ir kokį individą priskirtume x’ui, vis tiek gausime teisingą formulę. Mutatis mutandis dalinio kvantoriaus atveju. Formulė φ yra tapačiai teisinga nekintamo domeno modelyje M, žymime M ⊨NL φ, jei ir tik jei M, w, a ⊨NL φ, kiekvienam a ir kiekvienam modelio galimam pasauliui. Tokias formules kaip: tapačiai teisinga nekintamo domeno papildytam rėme, rėmų rinkinyje ir t. t. apibrėžiame, mutatis mutandis, kaip ir modalinės teiginių logikos atveju. Skirtingos nekintamo domeno semantikos predikatų modalinės logikos semantiškai nusakomos pagal L-tapačiai teisingų formulių aibes, t. y. iš esmės nurodant skirtingas L-nekintamo domeno papildytų rėmų klases. Atitinkamai, žymime: ⊨NK, ⊨NT, ⊨NK4 ir t. t. NL žymės bet kurią iš šių logikų. Parodome, kad Barcan schema yra tapačiai teisinga silpniausioje nekintamo domeno logikoje K, t. y. (Barcan schema) ⊨NK ◊∃xφ(x) → ∃x◊φ(x). Tarkime, kad M, w, a ⊨NK ~(◊∃xφ(x) → ∃x◊φ(x)), kažkokiems M, w, ir a. Taigi, M, w, a ⊨NK ◊∃x φ(x) ir M, w, a ⊨NK ~∃x◊φ(x). Jei M, w, a ⊨NK ◊∃xφ(x), tai kažkokiam w1, wRw1 ir M, w1, a ⊨NK ∃xφ(x). Tad, M, w1, a[d / x] ⊨NK φ(x), kažkokiam d ∊ D. Bet, jei M, w, a ⊨NK ~∃x◊φ(x), tai M, w, a ⊨NK ∀x~◊φ(x). Pagal ~◇φ≡□~φ, gauname M, w, a ⊨NK ∀x□~φ(x). Taigi, M, w, a[d / x] ⊨NK □~φ(x), nes D yra apibrėžtas visam modeliui, o ne lokaliai kiekvienam pasauliui, taigi žinome, kad objektas d egzistuoja visuose pasauliuose. Kadangi wRw1, tai M, w1, a[d / x] ⊨NK ~φ(x). Priėmę prielaidą, kad M, w, a ⊨NK ~(◊∃xφ(x) → ∃x◊φ(x)), gavome prieštaravimą, t. y. M, w1, a[d / x] ⊨NK φ(x) ir M, w1, a[d / x] ⊨NK ~φ(x). Kadangi, tiek nekintamo domeno modelis, tiek galimas pasaulis, tiek kintamųjų priskyrimo funkcija buvo pasirinkti arbitraliai, galime daryti išvadą, kad ⊨NK ◊∃xφ(x) → ∃x◊φ(x). ▮ Įrodymas, kad Barcan schemos konversija, t. y. ∃x◊φ(x) → ◊∃xφ(x), yra tapačiai teisinga, beveik identiškas ką tik pateiktajam. Paliekame jį skaitytojui.
