Let M⟦…⟧(…) be the “meaning” function from Propositions ×State to {tt,ff} and let σ0 be a state then
M⟦true⟧(σ0) |
≜ |
tt |
M⟦P⟧(σ0) | ≜ | σ0(P) |
M⟦¬f⟧(σ0) | ≜ | not (M⟦f⟧(σ
0)) |
M⟦f1 ∧ f2⟧(σ0) |
≜ |
(M⟦f1⟧(σ0) and M⟦f2⟧(σ0)) |
Let σ0(P) = tt and σ0(Q) = ff.
M⟦P ∨ Q⟧(σ0) |
|
= |
M⟦¬(¬P ∧¬Q)⟧(σ0) |
= |
not (M⟦¬P ∧¬Q⟧(σ0)) |
= |
not (M⟦¬P⟧(σ0) and M⟦¬Q⟧(σ0)) |
= | not (not (M⟦P⟧(σ0)) and not (M⟦Q⟧(σ0))) |
= | not (not (σ
0(P)) and not (σ0(Q))) |
= |
not (not (tt) and not (ff)) |
= |
not (ff and tt) |
= |
not (ff) |
= |
tt |