A Gentzen-style Axiomatization for Basic Predicate Logic

Mohammad Ardeshir

This is joint work with M. Aghaei.

W. Ruitenburg introduced [1] Basic Predicate Logic, BQC as the first order extension of Basic Propositional Logic, BPL invented by A. Visser [2]. Basic Logic is a proper subsystem of Intuitionistic Logic, IL in which Modus Ponens is weakened and is axiomatized in the same language of IL. Basic Logic is characterized as the logic of Kripke models with transitive frames.

Visser’s axiomatization of BPL is in natural deduction style and Ruitenburg’s BQC is in sequent notation (a sequent is an expression of the form A ⇒ B, where A and B are formulas in the language of BQC).

We introduce a cut free Gentzen style axiomatization for BQC and its propositional fragment BPL. Our new system has the subformula property. Among other things, we are able to give a syntactic proof for decidability of BPL.

[1] W. Ruitenburg Basic Predicate Calculus, Notre Dame Journal of Formal Logic, vol. 39(1998), pp. 18-46.

[2] A. Visser A propositional logic with explicit fixed points, Studia Logica, vol. 40(1981), pp. 155-75.

Address: Department of Mathematics, Sharif University of Technology, P.O. Box 11365-9415, and Institute for Studies in Theoretical Physics and Mathematics, P.O. Box 19395-5746, Tehran, Iran.

E-mail: ardeshir@math.sharif.ac.ir ardeshir@karun.ipm.ac.ir