Basic propositional calculus I

We present an axiomatization for Basic Propositional Calculus BPC and give a completeness theorem for the class of transitive Kripke structures. We present several refinements, including a completeness theorem for irreflexive trees. The class of intermediate logics includes two maximal nodes, one being Classical Propositional Calculus CPC, the other being E-1, a theory axiomatized by T --> perpendicular to. The intersection CPC boolean AND E-1 is axiomatizable by the Principle of the Excluded Middle A boolean OR inverted left perpendicular A. If B is a formula such that (T --> B) --> B is not derivable, then the lattice of formulas built from one propositional variable p using only the binary connectives, is isomorphically preserved if B is substituted for p. A formula (T --> B) --> B is derivable exactly when B is provably equivalent to a formula of the form ((T --> A) --> A) --> (T --> A).