Classical theorems in the Implicational Propositional Calculus

2016/02/06 by P. L. Robinson, Robinson, P. L.
Computer Science · Mathematics · #03B05 #03B20 #FOS: Mathematics #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #math.LO #msc:03B05 #msc:03B20

paper · pdf · doi:10.48550/arxiv.1602.02301

arxiv created 2016/02/06 · openalex publication_date 2016/02/06 · arxiv updated 2016/02/09 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Related

• Implicational Completeness
• Implicational Propositional Calculus: Tableaux and Completeness
• Q-tableaux for Implicational Propositional Calculus
• Every super-polynomial proof in purely implicational minimal logic has a polynomially sized proof in classical implicational propositional logic
• Kalmár-style constructive completeness proofs for classical positive propositional calculi