Kalmár-style constructive completeness proofs for classical positive propositional calculi

The completeness of the axiomatic systems usually presented as formal descriptions of classical positive propositional logics (propositional logics without negation) is known to be ensured through distinct proof procedures. In this paper, we settle the completeness of some classical positive propositional calculi (positive propositional calculi in which the so-called Peirce’s law holds) by resorting to a close adaptation of Kalmár’s completeness proof procedure, which was presented and applied to the classical propositional calculus with negation by Kalmár in 1934–1935. We employ this adaptation to establish the completeness of the most familiar axiomatic characterization of : (i) the classical logic of material implication and disjunction ; (ii) the so-called classical positive propositional calculus (the classical calculus of material implication, disjunction, and conjunction) ; (iii) the classical implicative calculus ; (iv) the classical calculus of material implication and conjunction. All these completeness proofs are constructive, that is to say, we can easily extract from each of them an effective method for producing formal deductions of all theses of the axiomatic system concerned.