Natural Deduction
(I⊺)
Γ ⊢ ⊺
(Ax)
Γ, φ ⊢ φ
(I∧)
Γ ⊢ φ ∆ ⊢ ψ
Γ, ∆ ⊢ φ ∧ ψ
(E∧)
Γ ⊢ φ ∧ ψ
Γ ⊢ φ
Γ ⊢ φ ∧ ψ
Γ ⊢ ψ
(I∨)
Γ, ¬ψ ⊢ φ
Γ ⊢ φ ∨ ψ
Γ, ¬φ ⊢ ψ
Γ ⊢ φ ∨ ψ
(E∨)
Γ ⊢ φ ∨ ψ ∆, φ ⊢ ϑ ∆′
, ψ ⊢ ϑ
Γ, ∆, ∆′ ⊢ ϑ
(I¬)
Γ, φ ⊢
Γ ⊢ ¬φ
(E¬)
Γ, ¬φ ⊢
Γ ⊢ φ
(I )
Γ ⊢ φ Γ ⊢ ¬φ
Γ ⊢
(E )
Γ ⊢
Γ ⊢ φ
(I→)
Γ, φ ⊢ ψ
Γ ⊢ φ → ψ
(E→)
Γ ⊢ φ ∆ ⊢ φ → ψ
Γ, ∆ ⊢ ψ
(I↔)
Γ, φ ⊢ ψ ∆, ψ ⊢ φ
Γ, ∆ ⊢ φ ↔ ψ
(E↔)
Γ ⊢ φ ∆ ⊢ φ ↔ ψ
Γ, ∆ ⊢ ψ
Γ ⊢ ψ ∆ ⊢ φ ↔ ψ
Γ, ∆ ⊢ φ
(I∃)
Γ ⊢ φ[x ↦ t]
Γ ⊢ ∃xφ
(E∃)
Γ ⊢ ∃xφ ∆, φ[x ↦ c] ⊢ ψ
Γ, ∆ ⊢ ψ
(I∀)
Γ ⊢ φ[x ↦ c]
Γ ⊢ ∀xφ
(E∀)
Γ ⊢ ∀xφ
Γ ⊢ φ[x ↦ t]
(I=)
Γ ⊢ t = t
(E=)
Γ ⊢ s = t ∆ ⊢ φ[x ↦ s]
Γ, ∆ ⊢ φ[x ↦ t]
c a new constant symbol, s, t arbitrary terms
1
Tableaux for First-Order Logic
¬φ true
φ false
¬φ false
φ true
φ ∧ ψ true
φ true
ψ true
φ ∧ ψ false
φ false ψ false
φ ∨ ψ true
φ true ψ true
φ ∨ ψ false
φ false
ψ false
φ → ψ true
φ false ψ true
φ → ψ false
φ true
ψ false
φ ↔ ψ true
φ true
ψ true
φ false
ψ false
φ ↔ ψ false
φ true
ψ false
φ false
ψ true
∀xφ true
φ[x ↦ t] true
∀xφ false
φ[x ↦ c] false
∃xφ true
φ[x ↦ c] true
∃xφ false
φ[x ↦ t] false
c a new constant symbol, t an arbitrary term
2
Tableaux for Modal Logic
s ⊧ ¬φ
s ⊭ φ
s ⊭ ¬φ
s ⊧ φ
s ⊧ φ ∧ ψ
s ⊧ φ
s ⊧ ψ
s ⊭ φ ∧ ψ
s ⊭ φ s ⊭ ψ
s ⊧ φ ∨ ψ
s ⊧ φ s ⊧ ψ
s ⊭ φ ∨ ψ
s ⊭ φ
s ⊭ ψ
s ⊧ φ → ψ
s ⊭ φ s ⊧ ψ
s ⊭ φ → ψ
s ⊧ φ
s ⊭ ψ
s ⊧ φ ↔ ψ
s ⊧ φ
s ⊧ ψ
s ⊭ φ
s ⊭ ψ
s ⊭ φ ↔ ψ
s ⊧ φ
s ⊭ ψ
s ⊭ φ
s ⊧ ψ
s ⊧ ⟨a⟩φ
s →a
t
t ⊧ φ
s ⊭ ⟨a⟩φ
t′
⊭ φ
s ⊧ [a]φ
t′
⊧ φ
s ⊭ [a]φ
s →a
t
t ⊭ φ
s ⊧ ∀xφ
s ⊧ φ[x ↦ u]
s ⊭ ∀xφ
s ⊭ φ[x ↦ c]
s ⊧ ∃xφ
s ⊧ φ[x ↦ c]
s ⊭ ∃xφ
s ⊭ φ[x ↦ u]
t a new state, t′
every state with entry s →a
t′
on the branch, c a new constant symbol, u an arbitrary
term
3