The dependence of an axiom of Łukasiewicz

Abstract

In this note we prove that axiom scheme A5 (cf. 10 of the preceding paper by Rose and Rosser, [l]) is derivable from the axiom schemes A1-A4. We use the notation of [l], and the formulas of [l] are referred to by their numbers. We shall use formulas only from the first three sections, which depend only on axion schemes A1-A4. Indeed, except for the result (3.51), we use formulas only from the first two sections, which depend only on axiom schemes A1-A3. Thus we actually show that axiom scheme A5 can be derived from (3.51) and axiom schemes A1-A3. This gives added point to the question raised by Rose and Rosser in [l] whether (3.51) can be proved from A1-A3 alone.