Cut theorem for tableau?

47 Views Asked by At

Cut theorem is

Suppose Γ |- ϕ and Γ ∪{ϕ} |- ψ.Then Γ |- ψ.

For natural deduction, it's simply a corollary of deduction theorem.

PROOF.Suppose we have Γ |- ϕ and Γ ∪ {ϕ} |- ψ.Then by the deduc-tion theorem we have Γ |- ϕ → ψ.Thus we may combine the derivations of ϕ and ϕ → ψ from Γ to get a derivation of ψ from Γ using →-E.

However, when we want to prove it for tableau in the same way, we go wrong.

However, given that we have deduction theorem for tableau, it's strange given Γ |- ϕ and Γ ∪{ϕ} |- ψ, i. e. Γ |- ϕ and Γ |- ϕ → ψ, we don't have Γ |-ψ.

What goes wrong here?

1

There are 1 best solutions below

0
On

There is a result in R.Smullyan, First-order Logic (1968):

if $\Gamma_1 \cup \{ \phi \}$ closes and $\Gamma_2 \cup \{ \lnot \phi \}$ closes, then $\Gamma_1 \cup \Gamma_2$ closes.

Apply it to $\Gamma_1=\Gamma$ and $\Gamma_2= \Gamma \cup \{ \lnot \psi \}$.