Admissibility of structural rules for contraction-free systems of intuitionistic logic (Q2710593)

The contraction-free sequent calculus for intuitionistic propositional logic, called G4ip in \textit{A. S. Troelstra} and \textit{H. Schwichtenberg}'s book [Basic proof theory, Cambridge Univ. Press, Cambridge (1996; Zbl 0868.03024); 2nd ed. (2000; Zbl 0957.03053)], has a useful feature that root-first proof search terminates without any loop-detection, and the admissibility of its structural rules has been already shown by several authors. However, all the known proofs are carried out depending on the corresponding admissibility in another system G3ip and on sequent weight, which brings about some problem in applying the method for extensions of G4ip such as its first-order version G4i. In this paper the authors give a direct proof of admissibility of cut and contraction for G4ip and its multi-succedent version along Dragalin's approach making use of inversion lemmas, which is immediately applied to the first-order case G4i as well.