This paper is an appendix to Keisler's papers [3], [4]. We assume that the reader is fully acquainted with these papers and use their terminology without further explanation. One of the main tools in a number of proofs in [4] is the following result which is all but stated explicitly in [4].

In his paper [3] Henkin proved for a first order language with identity symbol but without operation symbols the following version of the Craig-Lyndon interpolation theorem:

Theorem 1. If Γ╞Δ then there is a formula θ such that Γ ├Δand

(i) any relation symbol with a positive (negative) occurrence in θ has a positive (negative) occurrence in some formula of Γ.

In [1], the principle of semisubstitutivity of implication (SSI) was introduced for ordinary PC and quantification theory. This metatheorem generalizes the notions of “antecedent” and “consequent” to cover all wf subformulas of a given formula; each such subformula will be classified as being either in “antecedental position” (A-pos) or “consequential position” (C-pos). It is simplest to check these positions in a conjunction-negation primitive system: reduce a formula φ to primitive notation (K—N) ; choose a subformula ψ of φ; count the negation signs in φ within whose scope ψ falls.

We shall take “strong negation” to be a unary operator with some of the properties usually associated with negation, and such that the strong negation of a statement implies the “ordinary” negation ofthat statement, but not vice-versa. This paper will consider two varieties of strong negation: first, strong negation set in the context of the propositional calculus, specifically, the intuitionist PC, and secondly, strong negation in modal systems, that is, strong negation as impossibility. In the latter part of the paper, we shall present axiomatizations of several classical Lewis-modal systems having only material implication and impossibility primitive.

The present paper is a sequel to [1]. It is our purpose to formulate a general theory derived from the methods used to obtain three results for the field of real algebraic numbers in [1]. As there, we shall concern ourselves almost exclusively with fields of characteristic zero; thus we assume a convenient formulation of first order logic with extralogical constants E(x, y), S(x, y, z), F(x, y, z), F(x, y), N(x) and 0, whose intended interpretations are equality, sum, product, y is the successor of x, x ∈ (where is a substructure satisfying all first order truths of the natural numbers) and zero, respectively. In addition, we shall use Q(x, y) for x ≤ y in those cases where our field is ordered, e.g. the field of real algebraic numbers.

The well-developed theory of recursion has been applied to certain algebraic structures with countable universes to obtain interesting and natural results on the question of effective procedures in such structures ([2], [9], [10], [13]). It has also been applied to structures related to the real numbers, via approximations; we cite [3] as but one example. We are interested, however, in the problem of what operations in an arbitrary algebraic structure, possibly quite large and unnatural, can reasonably be considered “effective” in terms of the underlying operations and relations of the structure.

The semantical account that Meyer and Lambert give in [7] of their quantificational calculus FQ can be considerably simplified, and—supposing as the authors do at the close of their paper that ‘ = ’ counts as a primitive sign—so can their axiom system for FQ.

(1) As the authors remark, axiom schema 102 can be simplified to read : A ⊃ (∀Χ)A, where Χ does not occur free in A. Following Tarski's [9], it can be further simplified: A ⊃ (∀Χ)A, where Χ does not occur in A.

It is extremely difficult to make general statements about functional completeness. (For the main reference on the subject see Post [2].) In this paper we restrict ourselves to the case of unary functions in a finite valued logic, and prove a result concerning minimal functionally complete sets, along with a necessary and sufficient condition for completeness. A basic familiarity with group theory would be helpful.

Given a class U which is the result of closing a finite class of expressions with respect to a binary mode of combination, there exists, according to RFBL,1 a recursively enumerable subclass K* of U, and concepts of representation (5.3) and complete representation (6.2) such that:

(a) A relation among members of U is recursively enumerable if and only if it is represented in K*. (6.7.)

(b) A relation among members of U is recursive if and only if it is completely represented in K*. (6.10.)

In [1], William H. Jobe has shown that a certain three-valued proper logic is canonically complete, i.e., each first order J is expressible by a formula that is in M-normal form. The first order operator Jk(p)1 represents the truth table of a possible formula which has the truth value k in the ith row and the truth value 1 in all other rows. “The M-normal form of a given formula is another formula which has the same truth table as the given formula but which contains no operation symbols other than those of conjunction, disjunction, and undefined unary operations, with no nonunary operation, i.e., conjunction or alternation, included in the scope of an operation which is unary, and no alternation included in the scope of a conjunction.” Here it is shown that it is possible to construct a canonically complete proper logic for each choice of M which contains, in addition to alternation and conjunction, exactly two unary operations. Moreover, it is further shown that at least two unary operations are necessary in order for such a logic to be canonically complete.