A FORMALlSATlON OF THE TYI -VALUED LUKASIEWICZ Ii\lPLICATIONAL YItOPOSlTIONAL CALCULUS WITH VARIABLE FUNCTORS by ALAN ROSE in Not,tingham (England)
It has been shown1) that the m-valued LUKASIEWICZ implicational proposit,ioiial calculus with one designated truth-value may be fomialised by means of five axioms and the rules of subst,itution and modus ponens (with respect to the primitjive implication funct,or C). The object of the present paper is to show that from this2) formalisation we may obtain a plausible and complete formalisation of t,he corresponding proposit(iona1 calculus with variable functors by modifying the substitution rule in the usual3) way and adjoining one additional4) axiom.
Let, us denote t)he generalised subst,itution rule and the rule of modus poneibs (with respect to C) by R l , R 2 respectively. We shall make the definition IPQ (CP)m-lQ.
Thus the implication functor 1 satisfies the "st,andard conditions" 6, of ROSSER and TURQUETTE. Clearly, tzhe rule of modus ponens with respect t'o I is derivable by means of n~ -1 applications of R2. We shall denot'e t'his new rule of modus ponem by R3. The additional axiom, which we shall denotes) by A6, is ICpqICqpISpGq .
Clearly, this formula takes the trut,h-value 1 always. It, then follows, in the usual may, that, 7, the formalisation is plausible. We shall consider now the complet,eness of the formalisation. To bhis. end we shall make c,ert$ain definitions. The disjunction functor A and the suniniation operators*) l ) A. ROSE, Formalisation du calcul propositionnel implicatif B .m valeurs de Lukasiewicz, Comptcs rendus 213 (1956), 1263-1264.
2, The result does, of course, apply to any complete formalisation of the corresponding propositional calculufi without variable functors provided that R. 1 and R 2 are (primitive or derived) rules of procedure of the new formalisation.