Simplified formalizations of fragments of the propositional calculus.
Alan Rose · Notre Dame Journal of Formal Logic · 1977
Henkin has given [l] a general method of formalizing 2-valued propositional calculi whose primitive functors are such that material implication is definable in terms of them.Let the primitive functors, other than implication if implication is a primitive functor, be the functors F, of m arguments (i = 1, . .., b) and let the formulae P u . .., P ni , FiPi . . .P ni take the truth-values x l9 . .., x ni ,fi( χ ι, .., χ n{ί respectively (i = 1, . .., b).The axiom schemes are Al CPCQP, A2 CCPQCCPCQRCPR, A3 CCPRCCCPQRR, Λ4 CV Xι P x Q . . .CV^.P^QVyFiP, . . .P ni Q(y=fi (#i, . .., *",-); Xί = T, F; . ..; x n l = T, F; i = 1, . .., b), S^b n A4 denoting ^-/, = i 2 ι axiom schemes and the functors F τ , Vψ being defined by the equations VjPQ =df CCPQQ, V F PQ = df CPQ.The only primitive rule of procedure is Rl If P and CPQ then Q.We shall show how to reduce 1 the number and lengths of the axiom schemes.It follows at once from a result of Lukasiewicz [3] that Al-3 may be replaced by the axiom scheme Bl CCCPQRCCRPCSP.1.The axiom schemes C are similar to those obtained by using a general method of Shoesmith [5], but his completeness proof is non-constructive.