ABSTRACT
TB contains no definitions, since it is simply an axiomatization of the implicational fragment of Propositional Calculus. An alternative way to extend TB would be to make additions which would enable us to define negation in the extended system. Since W is an extension of TB, so that all theorems of TB are theorems of W, the theorems of both systems are denoted in a single sequence, It reflects a pattern of inference known since antiquity, which was called the consequentia mirabilis by renaissance scholars since it asserts that if a proposition is implied by its own negation it is true. Lukasiewicz names it ‘The Law of Clavius’ after a Bavarian Jesuit who drew attention to it in the sixteenth century.
