15 Tolkning i modeller Flashcards
modell
En modell (eng: model) M for et gitt førsteordens språk består av en ikke-tom mengde D, kalt domenet til modellen, og en funksjon som tolker alle ikke-logiske symboler på følgende måte:
- Hvis k er et konstantsymbol, er k^M ∈ D.
- Hvis f er et funksjonsymbol med aritet n, er f^M en funksjon fra D^n til D
- Hvis R er et relasjonssymbol med aritet n, er R^M en n-ær relasjon på D, det vil si en delmengde av D^n.
Vi skriver |M| for domenet D til modellen M.
lukket term
En term kalles lukket (eng: closed) hvis den ikke inneholder noen variabler
tolkning av termer
La et førsteordens språk være gitt, og la M være en modell for dette språket. Da tolker vi en lukket term f(t1, …, tn) på følgende måte:
f(t1, …, tn)^M = f^M(t1^M, …, tn^M)
tolkning av en lukket atomær formel
Anta at M er en modell for et førsteordens språk, og la R(t1, …, tn) være en lukket atomr formel. Vi sier at formelen R(t1, …, tn) er sann i M og skriver M |= R(t1, …, tn) hvis følgende holder:
⟨t1^M, …, tn^M⟩ ∈ R^M
substitusjon i termer
La s og t være termer og x en variabel. Da er s[x/t] resultatet av erstatte, eller substituere, alle forekomster av x i s med t
substitusjon i formler
Hvis φ er en formel, t en term og x en variabel, er φ[x/t] resultatet av å erstatte, eller substituere, alle frie forekomster av x i φ med t.
tolkning av lukkede formler
Anta at M er en modell for et gitt førsteordens språk. Vi definerer rekursivt hva det vil si at en lukket formel φ er sann i M. Skrivemåten M |= φ betyr at φ er sann i modellen M.
Basissteget, for atomære formler, er allerede definert. Det sier at M |= R(t1, …, tn) hvis ⟨t1^M, …, tn^M⟩ ∈ R^M. Her er rekursjonsstegene:
M |= ¬φ hvis det ikke er tilfellet at M |= φ
M |= φ ∧ Ψ hvis M |= φ og M |= Ψ
M |= φ ∨ Ψ hvis M |= φ eller M |= Ψ
M |= φ → Ψ hvis M |= φ impliserer M |= Ψ
M |= ∀xφ hvis M |= φ[x/\hat(a)] for alle a i |M]
M |= ∃xφ hvis M |= φ[x/\hat(a)] for minst én a i |M|
Når φ er sann i M, sier vi også at M er en modell for (eng: model for) φ, at M gjør φ sann og at M oppfyller (eng: satisfies) φ. Alt dette betyr det samme.
oppfyllbar, kontradiktorisk, gyldig og falsifiserbar
En lukket formel er oppfyllbar hvis det finnes en modell som gjør den sann, ellers er den kontradiktorisk. En lukket formel er gyldig hvis alle modeller gjør den sann, ellers er den falsifiserbar. En mengde lukkede formler er oppfyllbar/falsifiserbar hvis det finnes en modell som gjør alle formlene sanne/usanne.
