Semantica Kripke pentru logica intuiționistă urmează aceleași principii ca și semantica logicii modale, dar folosește o altă definiție a satisfacției.
Un model Kripke intuitionist este un triple ⟨W, ≤, ⊩⟩, unde ⟨W, ≤⟩ este un cadru Kripke parțial ordonat și ⊩ satisface următoarele condiții:
dacă p este o variabilă propozițională, w ≤ u și w ⊩ p, atunci u ⊩ p (condiție de persistență),
w ⊩ A ∧ B dacă și numai dacă w ⊩ A și w ⊩ B,
w ⊩ A ∨ B dacă și numai dacă w ⊩ A sau w ⊩ B,
w ⊩ A → B dacă și numai dacă pentru toate u ≥ w, u ⊩ A implică u ⊩ B,
nu w ⊩ ⊥.
Logica intuiționistă este solidă și completă cu privire la semantica ei Kripke și are Proprietatea modelului finit.
Logica intuiționistă de ordinul întâi
Fie L un limbaj de prim ordin. Un model Kripke de L este un triple ⟨W, ≤, {M w} w ∈ W⟩, unde ⟨W, ≤⟩ este un cadru Kripke intuitionist, Mw este o structură (clasică) L pentru fiecare nod w ∈ W, iar următoarele condiții de compatibilitate sunt valabile ori de câte ori u ≤ v:
domeniul lui Mu este inclus în domeniul Mv,
realizările simbolurilor funcțiilor în Mu și Mv sunt de acord asupra elementelor lui Mu,
pentru fiecare predicat n și a elementelor a1, …, an ∈ Mu: dacă P (a1, …, an) deține în Mu, atunci el deține în Mv.
Având în vedere o evaluare a variabilelor de către elemente ale lui Mw, definim relația de satisfacție w ⊩ A [e]:
w ⊩ P (t 1, …, t n) [e] dacă și numai dacă P (t 1 [e], …, t n [
w ⊩ (A ∧ B) [e] dacă și numai dacă w ⊩ A [e] și w ⊩ B [e],
w ⊩ (A ∨ B) [e] dacă și numai dacă w ⊩ A [e] sau w ⊩ B [e],
w ⊩ (A → B) [e] dacă și numai dacă pentru toate u ≥ w, u ⊩ A [e] implică u ⊩ B [e],
nu w ⊩ ⊥ [e],
w ⊩ (∃ x A) [e] dacă și numai dacă există un a ∈ M w astfel încât w ⊩ A [e (x → a)],
w ⊩ (∀ x A) [e] dacă și numai dacă pentru fiecare u ≥ w și fiecare a ∈ M u, u ⊩ A [e (x → a)].
Aici e (x → a) este evaluarea care dă x valoarea a, și este de acord cu e.
Lasă un răspuns