A Henkin-style completeness proof for the pure implicational calculus.
George F. Schumm · Notre Dame Journal of Formal Logic · 1975
Pollock has shown in [l] that Henkin-style completeness proofs can be obtained for deductive theories lacking negation, provided that disjunction is available.In this note, I show how to construct such proofs for implicational calculi without recourse to the special properties of disjunction exploited by Pollock.I shall run the argument through only for PC|, the pure implicational calculus, but the proof is easily adapted for richer theories as well.For the sake of definiteness, we suppose PC\ to have Al. AD(BDA) A2. (A D (B D C)) D ((A z>B) Z)(Az> C))A3. ((AΏB)Z)A)DA