On cut elimination in the presence of peirce rule.
On normalization of proofs in set theory [Book]
On sequent calculi for intuitionistic propositional logic
The well-known Dyckoff's 1992 calculus/procedure for intuitionistic propositional logic is considered and analyzed. It is shown that the calculus is Kripke complete and the procedure in fact works in polynomial space. Then a multi-conclusion intuitionistic calculus is introduced, obtained by adding one new rule to known calculi. A simple proof of Kripke completeness and polynomial-space decidability of this calculus is given. An upper bound on the depth of a Kripke counter-model is obtained.
On two Classical Results in the First Order Logic