Gentzen-style Axiomatizations for Conservative Extensions of Basic Propositional Logic

Mojtaba Aghaei

This is a joint work with Mohammad Ardeshir. Basic Propositional Logic, BPL, is first introduced by A. Visser in [4]. He axiomatized it in natural deduction style. His motivation comes from Modal (Provablity) Logic. The relation of BPL to K4 is like Intuitionistic Propositional Calculus, IPC, to the Modal logic S4. We introduce two Gentzenstyle sequent calculus axiomatizations for conservative extensions of Basic propositional logic. Our first axiomatization is an improvement of [2], in the sense that it has a kind of the subformula property and is a slight modification of [3]. In this system the cut rule is eliminated. The second axiomatization is a classical conservative extension of Basic propositional logic. Using these axiomatizations, we prove two interpolation theorems for Basic propositional logic.

[1] M. Aghaei and M. Ardeshir. Gentzen style axiomatizations for some conservative extensions of basic propositional calculus, submitted.

[2] M. Ardeshir. Aspects of Basic Logic, PhD thesis, Marquette University, Wisconsin, U. S. A., 1995.

[3] K. Sasaki. A Gentzen-style axiomatization of Visser’s propositional logic, Nanzan Management Review 12 (1998), 343-451.

[4] A. Visser. A propositional logic with explicit fixed points, Studia Logica 40 (1981), 155-175.

Address: Institute for Studies in Theoretical Physics and Mathematics, P.O. Box 19395-5746, Tehran, Iran

E-mail: aghaei@karun.ipm.ac.ir