A completeness proof for $C$-calculus.
H. HiÅ ⁄ · Notre Dame Journal of Formal Logic · 1973
To Alfred Tarskί who first axiomatίzed C-calculusIntroduction, Every true formula of the classical implicational logic, the C-calculus, is provable, by means of substitution and detachment, from the following three axioms:In effect 1, 2 and 3 jointly assert the inferential equivalence of a formula of the form CCaβγ with the set of two formulas of the forms Cβγ and CCaγγ. 2 The completeness proof which follows is of elementary nature. 3First, the deduction of useful theorems is given.Then, it is shown that a formula in the implicational normal form is true if and only if it satisfies the chain condition, and that every formula in the implicational normal form which satisfies the chain condition is deducible from 1, 2 and 3. Finally, it is shown that every formula of the C-calculus is inferentially equivalent to a finite set of formulas in the implicational normal form.1.This axiomatization was discovered in 1961.2. Equivalence asserting axiomatizations, besides being pedagogically transparent, may be of interest in connection with systematization of metalogic by means of inferential equivalence; see [1].3. The first completeness proof of an axiomatization of C-calculus was given by Tarski, but never published.See footnote to p. 145 of [3].Formula 2 was used by Tarski in his first axiomatization of C-calculus.Another completeness proof of C-calculus was given by Kurt SchUtte, cf.[5] and [4], pp.214-217.Schϋtte's proof presupposes completeness of the logic of implication and negation (the C-Nc alculus).