On axiom systems of propositional calculi, XIII
Shôtarô Tanaka · Proceedings of the Japan Academy Series A Mathematical Sciences · 1965
We know some single axioms of the classical propositional calculus.In this note, we shall show that Lukasiewicz-Tarski single axiom of the propositional calculus (see [2) is equivalent to some axiom systems, for example, (L)-system.In their paper, J. Lukasiewicz and A. Tarski do not give the proof of equivalences.For notations and rules of inferences, see 3.The fundamental Lukasiewicz-Tarski axiom is the following single thesis:1CCCpCqpCCCNrCsNtCCrCsuCCtsCtuvCwv.First, we shall prove that the Lukasiewicz-Tarski axiom implies (L)-system.The proof is not so easy.Therefore, for the proofs of theses 2 and 4, we shall write the results of substitutions. 1 p/CqCrq, q/CCNrCsNtCCrCsuCCtsCtu, v/CqCrq, w/p *C1 p/q, q/r, v/CqCrq, w/CCNrCsNtCCrCsu CCtsCtu2, CCCCqCrqCCCNrCsNtCCrCsuCCtsCtuCqCrqCCCNr CsNtCCrCsuCCtsCtuCqCrqCpCqCrq 2 CpCqCrq. 2 p/CpCqCrq, q/p, r/q *C2--3, 3 CpCqp.1 v/CCpCqpCCNrCsNtCCrCsuCCtsCtu, w/CpCqp *C2 p/CpCqp, q/CCNrCsNtCCrCsuCCtsCtu, r/CpCqpC3 C34, CCCpCqpCCCNrCsNtCCrCsuCCtsCtuCCpCqpCCNr CsNtCCrCsuCCtsCtuCCpCqpCCpCqpCCNrCsNtCCr CsuCCtsCtu, 4 CCNrCsNtCCrCsuCCtsCtu.4 r/p, s/q, t/p, u/r *C3 p/Np--5, 5 CCpCqrCCpqCpr. 5 r/p, q/Cqp *C3 q/Cqp--C36, 6 Cpp. 3 p/CCpCqrCCpqCpr, q/Cqr *C5--7, 7 CCqrCCpCqrCCpqCpr 5 p/Cqr, q/CpCqr, r/CCpqCpr *C7--C3 p/Cqr, q/p--8, 8 CCqrCCpqCpr.5 p/Cqr, q/Cpq, r/Cpr *C8--9, 9 CCCqrCpqCCqrCpr.