Theorem 1.4.20
(Completeness of the Kripke semantics)
.
Assuming that:
φ
a proposition
Then
Γ
⊢
IPC
φ
if and only if
for all
Kripke models
(
S
,
≤
,
⊩
)
, the condition
S
⊩
Γ
implies
S
⊩
φ
.