A set of axioms for the propositional calculus with implication and converse non-implication.
Anjan Shukla · Notre Dame Journal of Formal Logic · 1965
It is well-known that implication and converse non-implication constitute a complete system of independent primitive connectives for the propositional calculus,, In this article it is the author's intention to give a set of independent axioms for the propositional calculus by means of the two connectives mentioned above, the rules of inference being substitution and modus ponens 1 .In setting up the axioms the purpose of the author has been to achieve simplicity of individual axioms while preserving their independence.In §1 we give the set of axioms and prove some preliminary theorems.In §2 we solve the decision problem.Finally, in §3, we establish the independence of the axioms and rules.In the matter of notation and style of presenting proofs of theorems we shall follow Church. §1. AXIOMS AND PRELIMINARY THEOREMS.The axioms of our logistic system, say P, are the six following Axiom 1. p ^.q ^>p Axiom 2. s ^[p ^q] =>.s ^p D. s ^q Axiom 3. p ^q =>/> ^p Axiom 4. p D [p .q =>.p .p ^s In fact, as is evident from the above set, any formulation of the implicational propositional calculus and Axioms 4-6 will suffice.We note that from the present formulation the deduction theorem-to be henceforth referred to as D.T.-follows immediately.We now go on to prove some theorems.Theorem 1. p