 Later we show how the system can be extended to include additional logical connectives, such as formula_14 and formula_15, without enlarging the class of deducible formulas.The first four logical axiom schemes allow (together with modus ponens) for the manipulation of logical connectives.The axiom P1 is redundant, as it follows from P3, P2 and modus ponens.