The m-valued propositional calculi of POST') with one designated truth-value have been formalised2) by means of ten axioms and the rules of substitution and modus ponens. However, in view of the definition of the functor "=" as a conjunction, several axioms may be regarded as sets of m axioms. The object of the present paper is to formalise, for a l l values of s (1 ml ) , the corresponding calculi with variable functors and with s designated truth-values. The rules of procedure will be similar to those used previously and the number of axioms will be m + s + 6 , except in the case s = 1, when it will be na $. 6 , no axiom being capable of being regarded as a set of m axioms.
s
We shall use the notation3) of LUKASIEWICZ, the primitive disjunction and negation functors being denoted by A and R respectively and i consecutive functors R being denoted by Ri (i = 0 , 1 , . . .) . Since the systems are functionally complete4) we can define binary functors I which satisfy the "standard conditions" of ROSSER and TURQUETTE~) for implication. Our primitive rules of procedure will be the usuals) substitution rule and the rule of modus ponens with respect to I . We shall denote these rules by R 1, R 2 respectively. The summation operator7) ''r" is defined with respect to I. The axioms are as stated below, A9 being omitted in the case s = 1. J , is a functor defined in terms of the primitives so as t o satisfy standard conditions and the functors J,, . . . , J , are defined by Ji,.,P =dnJ,R7'L-iP (i = 1, . . ., m -1).
l ) E. L. POST, Introduction to a general theory of elementary propositions. American J. of 2, A. ROSE, A formalisation of Post's m-valued propositional calculus. Math. Zeitschr. 56 3, See, for example, J. LUKASIEWICZ, Elements of Mathematical Logic, Oxford, Pergamon Press 1963. The explanation of the notation begins on p. 23. Another exposition of this notation is given in the paper referred to in footnote 5. Math. 43 (1921Math. 43 ( ), 163-185. (1952), 94-104. ), 94-104. 4, See footnote 1.