The one variable implicational calculus (Q2560807)

The axiomatization given by \textit{H. W. Johnson} and \textit{R. Price} [Theoria 30, 1--4 (1964)], is shown to be inadequate. A correct presentation of the one variable implicational calculus based on a single (rejected) axiom and four rules of inference is given. This is akin to the computable Protothetics of Leśniewski. This presentation cannot be much improved on, for we show that the one variable implicational calculus cannot be finitely axiomatized using the rules of substitution and detachment. This proves an elementary example-of a non-axiomatizable propositional calculus.