Predikaat logica: Een eenvoudige theorie

♟
Predikaatlogica: Een Eenvoudige
Theorie
Type HOC

Class Logica en formele systemen

Les 11



Substitutie

Bewering
Substitutie
Voor termen t, t’ en variabele x geldt:

VM ,b ([t/x]t’) = VM ,b[x↦VM ,b (t)] (t’)


Prenexvormen
Prenexvorm:
Een formule van de vorm Q1 x1 ...Qn xn ψ waarbij
Qi kwantoren (∃ of ∀) zijn,
i = 1, ..., n

ψ een formule is waarin geen kwantoren meer voorkomen
heet een prenexvorm met Q1 x1 ...Qn xn als prefix en ψ als matrix.


Prenexstelling:
Voor elke formule φ bestaat er een prenexformule ψ zodat φ en ψ logisch equivalent zijn, i.e (V (φ) =
V (ψ)).


Fragmenten van Predikaatlogica
→ beperken


Adequaatheidsstelling
Als Σ een formuleverzameling is en φ een formule, dan geldt:
Σ ⊨ φ desda er bestaat een gesloten semantisch tableau voor Σ o φ



Predikaatlogica: Een Eenvoudige Theorie 1