Kripkes Completeness Theorem (K&L)

Saul Kripke – Definitionen, Axiome, Regeln, etc.

Symbole:
^ ............und
~ ........... nicht
□........... notwendig
(x) ......... Allquantor
= ........... ist ident mit

Definitionen:
AvB...........~(~A^~B)
A-> B ........~(A^~B)
◊A............ ~□ ~A
(∃x)A(x)..... ~(x)~A(x)

Axiome und Regeln:
A1: □A->A
A2: ~ □A->□~ □A
A3: □ (A->B)-> (□A->□B)

R1: wenn ├A und ├A->B, ├B
R2: wenn ├A, ├□A

Regeln für semantische Baumstrukturen nach Beth (wenn [fett], dann [nicht fett]) :

Regel wahr falsch

Nl ~A A
Nr A ~A

Λl A^B
A
B
Λr1 A^B Baum teilt sich!
A
Λr2 A^B
B

Πl (x)A(x)
A (a)
Πr (x)A(x)
A(a)

Il a=b
A(a,b) ersetzen
durch A(b,b)
Ir ---

Yl □A
A Yr □A
Neuer Hilfstableau: wahr falsch
A