Theorems in Classical Logic are Instances of Theorems in Condensed BCI Logic
Martin W. Bunder · 1993
Abstract Any proof in classical logic can be rewritten as a proof in intuitionistic implicational logic with the constant formula f and two additional axioms, ex also quodlibet (f1) and double negation (f2). We show here that any classical proof in this form can be transformed into a proof of a theorem of condensed BCI logic, from which the original theorem can be recovered by means of a series of simple replacements. The fact that, for a given classical theorem, only a finite number of such replacements are possible from its condensed BCI counterpart allows us to formulate decision procedures for the intermediate systems BCif1, BCif2, BCKf1, BCKf1f2, BCIWf1, BCIWf2 and BCKWf1 in terms of known decision procedures for BCI, BCK, BCIW, and BCKW implicational logics.