A Gentzen-style axiomatization for basic predicate calculus (Q1407590)

Basic Predicate Calculus, BQC, was introduced by \textit{W. Ruitenburg} [Mod. Log. 1, 271-301 (1991; Zbl 0748.03037)] as a first-order extension of Basic Propositional Logic, BPL, invented by \textit{A. Visser} [Stud. Log. 40, 155-175 (1981; Zbl 0469.03012)]. Basic Logic is a proper subsystem of Intuitionistic Logic, in which Modus Ponens is weakened. The original axiomatization of W. Ruitenburg [loc. cit.] is in sequent notation. We introduce a Gentzen-style sequent calculus axiomatization for BQC. Our new axiomatization is an improvement of the previous axiomatizations given by the second author [Aspects of basic logic. PhD thesis, Marquette University, Wisconsin, USA (1995)], in the sense that it has the subformula property. In this system the cut rule is eliminated. This cut-free sequent calculus for BQC induces a cut-free sequent calculus for BPL as well.