Syntactic proof: If Γ, ϕ ⊢ Θ and Γ, ¬ϕ ⊢ Θ then Γ ⊢ Θ

55 Views Asked by At

How can I prove this syntactically: If Γ, ϕ ⊢ Θ and Γ, ¬ϕ ⊢ Θ, then Γ ⊢ Θ?

If I weren't constrained by a particular formal system (see below), I think I could use the deduction theorem to first derive Γ ⊢ ϕ -> Θ and Γ ⊢ ¬ϕ -> Θ, and then use the law of the excluded middle to argue that ϕ v ¬ϕ, followed by an argument by cases to conclude Θ. But I don't know how to do that in this particular system.

I know how to derive '¬¬ϕ → ϕ', which is equivalent to the law of the excluded middle, but I'm not sure how to use it in this context.

The system I'm supposed to prove this in is defined as follows:

Definition of the formal system S

Maybe I could use proof by contradiction twice: Assume ¬Θ and ¬ϕ to derive Θ and therefore ϕ and use the latter to derive Θ again and therefore ¬¬Θ?