This is a mathematical logic problem on the Sequent Calculus
Γ ⊢ φ
Γ ⊢ ¬¬φ
(Prove Γ ⊢ ¬¬φ is formally provable from Γ ⊢ φ )
Since "¬¬" is not generated by any of the rules, I have tried to use the Assumption Rule (Asm) and the Contradiction Rule 2 (Ctr2) to generate the ¬¬φ term. I am stuck here though.
1) Γ ⊢ φ (Premise)
2)...
3)...
......
n-1) Γ ⊢ ¬φ
n) Γ ⊢ ¬¬φ (Conclusion) --> Apply (Ctr2) on 1) & n-1)
Any idea is appreciated. ;)
Unfortunately, there are several versions of the sequent calculus. The following works in the version I'm accustomed to; I hope it or something similar works in the version you want. From $\Gamma\vdash\phi$, and the logical axiom $\neg\phi\vdash\neg\phi$, we get both $\Gamma\cup\{\neg\phi\}\vdash\phi$ and $\Gamma\cup\{\neg\phi\}\vdash\neg\phi$ by weakening. These last two give $\Gamma\cup\{\neg\phi\}\vdash\bot$, and this in turn gives $\Gamma\vdash\neg\neg\phi$.
For the system on Wikipedia, you can do it in two steps. From $\Gamma \vdash \phi$ you obtain $\Gamma, \lnot \phi \vdash $ from rule $\lnot L$. Then you get $\Gamma \vdash \lnot \lnot \phi$ from $\lnot R$.
