Classical theorems in the Implicational Propositional Calculus
P. L. Robinson
TL;DR
This paper demonstrates that classical propositional calculus theorems can be directly translated into implicational propositional calculus proofs, establishing a link between the two systems and ensuring completeness transfer.
Contribution
It shows that proofs in classical propositional calculus can be converted into implicational calculus proofs, confirming the completeness of IPC based on PC.
Findings
PC proofs can be transformed into IPC proofs
Completeness of PC implies completeness of IPC
Theorems of PC are provable in IPC
Abstract
For formulas of the Implicational Propositional Calculus (IPC) that are theorems of the classical Propositional Calculus (PC) we show that PC proofs yield IPC proofs. As a consequence, completeness of PC yields completeness of IPC.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge