Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models

In this paper we present LSJ, a contraction-free sequent calculus for Intuitionistic propositional logic whose proofs are linearly bounded in the length of the formula to be proved and satisfy the subformula property. We also introduce a sequent calculus RJ for intuitionistic unprovability with the same properties of LSJ. We show that from a refutation of RJ of a sequent σ we can extract a Kripke counter-model for σ . Finally, we provide a procedure that given a sequent σ returns either a proof of σ in LSJ or a refutation in RJ such that the extracted counter-model is of minimal depth.