We deal in the following with certain theories S, by which we mean sets of sentences closed under logical deduction. The basic logic is understood to be the classical one, but we place no restriction on the orders of the variables to be used. However, we do assume that we can at least express certain notions from classical first-order number theory within these theories. In particular, there should correspond to each primitive recursive function ξ a formula φ(χ), where ‘x’ is a variable ranging over natural numbers, such that for each numeral ñ, φ(ñ) expresses in the language of S that ξ(η) = 0. Such formulas, when obtained say by the Gödel method of eliminating primitive recursive definitions in favor of arithmetical definitions in +. ·. are called PR-formulas (cf. [1] §2 (C)).

A standard set of axioms for the intuitionist propositional calculus is the following (we associate to the right, and use the convention that ⊃ binds less strongly than the other connectives).

In [1] McKinsey gives a method of defining possibility in terms of “substitutions”, or transformations of one sentence into another. Roughly, the motivation is that a sentence be possible if a sentence of “like form”, i.e. a transformation of it, is true.

The purpose of this paper is to show that the two systems given in [1], shown by McKinsey to be at least as strong as Lewis' systems S4 and S5, do exactly characterize S4 and S5, and that the system given by omitting rule A4 from the first system exactly characterizes von Wright's system M.1

It is shown in Sobociński [1] that the number of irreducible modalities in T is infinite. The infinity of modalities in T collapses if the axiom CLpL2p is added to T, since T plus CLpL2p is equivalent to S4 and the number of irreducible modalities in S4 is finite as proved in Parry [2]. But the addition of the axiom CL2pL3p does not collapse the infinity of modalities in T. The aim of the present paper is to prove this theorem and its corollaries.

This paper examines the questions of functional completeness and canonical completeness in many-valued logics, offering proofs for several theorems on these topics.

A skeletal description of the domain for these theorems is as follows. We are concerned with a proper logic L, containing a denumerably infinite class of propositional symbols, P, Q, R, …, a finite set of unary operations, U1, U2,…, Ub, and a finite set of binary operations, B1, B2, …, Bc. Well-formed formulas in L are recursively defined by the conventional set of rules. With L there is associated an integer, M ≧ 2, and the integers m, where (1 ≦m≦M), are the truth values of L.

The object of this note is to extend to Post's m-valued propositional calculus1 the axiomatization by Anderson and Belnap2 of the 2-valued propositional calculus.

Notation and definitions. We shall use the symbols ∼ and v for the primitives of Post and shall otherwise, except as stated below, use the same notation and definitions as in the previous paper.

In a paper in this Journal [1], McKinsey used as a criterion for the independence (non-definability) of a connective F in a propositional calculus L, the existence of a matrix for L in which the functions corresponding to all the connectives other than F are class-closing over some subset S of the elements, while the function corresponding to F is not class-closing over S (i.e., for a certain choice of arguments in S its value is not in S).

If numbers be used to designate classes, there can be derived from a conjunct of classes numbers corresponding to the expanded product classes.

For example, let the product classes ābc and āb be designated by numbers I and 5 as in the following matrix:

By using 1 (20) instead of a, 2 (21) instead of b, 4 (22) instead of c, etc., the following relationship emerges between the designation of the conjunct of classes (take 12) and the product classes (I and 5): the product class(es) of any conjunct of classes is (are) (1) the sum of any negated class numbers and (2) seven less the sum of any unnegated class numbers.

There is a distinction within the natural language between those singular terms which designate and those which do not. On the basis of this distinction there arise irregularities both in the assignment to expressions of semantical properties and relations and in the presumed attribution of existence to individuals. Although such irregularities are characteristic of the employment of singular terms, they are not reproduced either for or within the usual formalized languages. Accordingly, we construct a formalized language for which the mentioned irregularities are reproduced — hence, a language which in this respect mirrors more faithfully than is customary the structure of the natural language.