SINGLE GENERATORS FOR HENKINIAN FRAGMENTS
OF THE 2-VALUED PROPOSITIONAL CALCULUS by ALAN ROSE in Nottingham (England) HENKIN has shown,) that if the truth-tables of the primitive functors of a 2-valued propositional calculus are such that material implication is definable2) in this propositional calculus then the calculus can be formalised completely by means of a finite number of axiom schemes and the rule of modus ponem. If there are exactly b primitive functors other than implication, or exactly b primitive functors if implication is not a primitive, and these b functors F,, . . . , Fb are functors of n,, . . ., nb arguments respectively, the number of axiom schemes given by
We shall now establish that in each such propositional calculus there is a definable functor G such that, if the primitives so far considered are replaced by the single primitive G , the functors C , F,, . . ., Fb are definable. Thus a functor is definable i n t h e C -F , --. . --Fb-prOpOSitiOnal calculus if and only if it is definable in the G-propositional calculus. If the G-propositional calculus is formalised by the method of HEN KIN^) and no modifications are made, the number of axiom schemes will, of course, be 3 + 2") where 01 is the number of arguments of G . It will, however, be fairly simple, in this case, to reduce the number of axiom schemes to 3 + 2"-' . We shall conclude with a few results concerning many-valued propositional calculi and a result concerning the impossibility of solving a related problem for the m-valued (2 5 m < N,,) propositional calculus.
We shall consider first the relatively simple case where, for some integer i (1 =( i b ) , the formula F , P , . . . P,, takes the truth-value P when P, , . . . , P,, all take the truth-value T. I n this case the C -Fl -. . -Fbpropositional calculus will be functionally complete, since we may make the definition N P =df CPFiP . . . P and the C -N-propositional calculus is, of course, functionally complete. We may therefore, of course, replace our primitive functors by the incompatability functor. I ) L. HENHIN, Fragments of the propositional calculus, J. Symb. Logic 14 (1949), 42-48.
z, We regard as included here the case where implication is a primitive functor. 3, See, however, M. L'ABB~, On the independence of Henkin's axioms for fragments of the propositional calculus, J. Symb. Logic 16 (1951), 43-45. 4) o p . cit.