The concepts of ω-consistency and ω-completeness are closely related. The former concept has been generalized to notions of Γ-consistency and strong Γ-consistency, which are applicable not only to formal systems of number theory, but to all functional calculi containing individual constants; and in this general setting the semantical significance of these concepts has been studied. In the present work we carry out an analogous generalization for the concept of ω-completeness.

Suppose, then, that F is an applied functional calculus, and that Γ is a non-empty set of individual constants of F. We say that F is Γ-complete if, whenever B(x) is a formula (containing the single free individual variable x) such that ⊦ B(α) for every α in Γ, then also ⊦ (x)B(x). In the paper “Γ-con” a sequence of increasingly strong concepts, Γ-consistency, n = 1,2, 3,…, was introduced; and it is possible in a formal way to define corresponding concepts of Γn-completeness, as follows. We say that F is Γn-complete if, whenever B(x1,…, xn) is a formula (containing exactly n distinct free variables, namely x1…, xn) such that ⊦ B(α1,…,αn) for all α1,…,αn in Γ, then also ⊦ (X1)…(xn)B(x1,…,xn). However, unlike the situation encountered in the paper “Γ-con”, these definitions are not of interest – for the simple reason that F is Γn-complete if and only if it is Γ-complete, as one easily sees.

Faris [1] presents a system for non-void classes employing four primitive functors with another defined, and based on ten asserted and eleven rejected axioms, with a special rule of rejection analogous to Słupecki's for the syllogistic. Primitive functors are here reduced to three, axioms are simplified, and it is shown that the system is decidable by the easier syllogistic means, e.g. the tabular method of Thomas [3].

From the theses (original numbering to the right with axioms starred)

we can deduce

La théorie de la quaternalité, telle que Piaget et Gottschalk l'ont appliquée aux connectifs binaires du calcul bivalent, appelle quelques précisions et compléments.

Les seize connectifs ne comportent que deux quaternes complets: celui des jonctions et celui des implications. Leurs similitudes formelles ne doivent pas dissimuler une différence dans leur mode de construction. Elle apparaît sur leurs diagrammes (inspirés du “carré logique” traditionnel) par la place de la cellule initiale et par celles des signes barrés du trait vertical de la négation:

En effet, la dualité qui se combine avec celle de la négation contradictoire (DN, flèche diagonale) est, pour les jonctions, la dualité “morganienne” (DM, flèche verticale) et pour les implications, la dualité des réciproques (DR, flèche horizontale). Car dans les jonctions, liaisons symétriques, il n'y a point de vraies réciproques; inversement, les implications ne comportent pas (pourvu, bien sûr, qu'on ne les traduise pas en termes de jonctions) de dualité morganienne. Le quatrième terme, obtenu par la combinaison des deux relations génératrices, sera donc, pour les jonctions, une contreduale (DM × DN) et, pour les implications, une contreréciproque (DR × DN).

The notion of a variable restricted in range to some set of values, or to values having some property, is widespread in logic and mathematics. To avoid continual explicit mention of such a restriction the common device is to resort to a typographically different set of letters for such variables. But a notation of this kind is clearly inadequate when a general discussion, including more than one kind of restriction, is under consideration. For example, two restrictions may have some inner connection, as in the case of mutually exclusive restrictions, and this the usual symbolism doesn't depict; or, one may wish to study the dependence of such restrictions upon one or more parameters as in the case of bounded quantifiers of recursive function theory; or, one can even conceive of restrictions which may in turn depend upon restricted variables. In each of these cases the currently used notation is deficient.

If x is an individual-variable and Q a formula of the predicate calculus, then for the idea ‘x such that Q’ the notation ‘vxQ’ is proposed as one having the requisite degree of notational multiplicity – the ‘vx’ acting as a binding operator for free occurrences of x in Q. The expression ‘vxQ’ is referred to as a restricted-variable and it may occupy positions in formulas appropriate to individual-variables, in argument places as well as in quantifiers. In § 2 a first-level predicate calculus, called ‘‘, is presented in which the restricted-variable is an integral part.

This paper contains examples T1 and T2 of theories which answer the following questions:

(1) Does there exist an essentially undecidable theory with a finite number of non-logical constants which contains a decidable, finitely axiomatizable subtheory?

(2) Does there exist an undecidable theory categorical in an infinite power which has a recursive set of axioms? (Cf. [2] and [3].)

The theory T1 represents a modification of a theory described by Myhill [7]. The common feature of theories T1 and T2 is that in both of them pleonasms are essential in the construction of the axioms.

Let T1 be a theory with identity = which contains one binary predicate R(x, y) and is based on the axioms A1, A2, A3, B1, B2, B3, B4, Cnm which follow.

A1: x = x. A2: x = y ⊃ y = x. A3: x = y ∧ y = z ⊃ x = z.

(Axioms of identity.)

B1: R(x, x). B2: R(x, y) ⊃ R(y, x). B3: R (x, y) ∧ R(y, z) ⊃ R(x, z).

(Axioms of equivalence.)

B4: x = y ⊃ [R(z, x) ≡ R(z,y)].

Let φn be the formula

which express that there is an abstraction class of the relation R which has exactly n elements.

Let f(n) and g(n) be two recursive functions which enumerate two recursively inseparable sets [5], and call these sets X1 and X2.

We now specify the axioms Cmm.

It is obvious that the set composed of the formulas A1−A3, B1−B4, Cnm (n,m = 1,2, …) is recursive.

The theory T1 is essentially undecidable; for if there were a complete and decidable extension T′1 (of it, then the recursive sets Z = {n: φn is provable in T′1} and Z′ = {n: ∼φn is provable in T′1} would separate the sets X1 and X2.

There are a number of open problems involving the concepts of decidability and essential undecidability. This paper will present solutions to some of these problems. Specifically:

(1) Can a decidable theory have an essentially undecidable, axiomatizable extension (with the same constants)?

(2) Are all the complete extensions of an undecidable theory ever decidable?

We shall show that the answer to both questions is in the affirmative. In answering question (1), the decidable theory for which an essentially undecidable axiomatizable extension will be constructed is the theory of the successor function and a single one-place predicate. It will also be shown that the decidability of this theory is a “best possible” result in the following direction: the theory of either of the common diadic arithmetic functions and a one-place predicate; i.e., of addition and a one-place predicate, or of multiplication and a one-place predicate, is undecidable.

Before establishing the main result, it is convenient to give a simple proof that a decidable theory can have an axiomatizable (simply) undecidable extension. This is, of course, an immediate consequence of the main result; but the proof is simple and illustrates the methods that we are going to use in this paper.

This paper treats of semantical systems S of sufficient strength so that for any set W definable in S (in a sense which will be made precise), there must exist a sentence X which is true in S if and only if it is an element of W. We call such an X a Tarski sentence for W. It is the sentence which (in a purely extensional sense) says of itself that it is in W. If W is the set of all expressions not provable in some syntactical system C, then X is the Gödel sentence which is true (in S) if and only if it is not provable (in C). We provide a novel method for the construction of these sentences, which yields sentences particularly simple in structure. The method is applicable to a variety of systems, including a form of elementary arithmetic, and some systems of protosyntax self applied. In application to the former, we obtain an extremely simple and direct proof of a theorem, which is essentially Tarski's theorem that the truth set of elementary arithmetic is not arithmetically definable.

The crux of our method is in the use of a certain function, the ‘norm’ function, which replaces the classical use of the diagonal function. To give a heuristic idea of the norm function, let us define the norm of an expression E (of informal English) as E followed by its own quotation.