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.

In Herbrand's Theorem [2] or Gentzen's Extended Hauptsatz [1], a certain relationship is asserted to hold between the structures of A and A′, whenever A implies A′ (i.e., A ⊃ A′ is valid) and moreover A is a conjunction and A′ an alternation of first-order formulas in prenex normal form. Unfortunately, the relationship is described in a roundabout way, by relating A and A′ to a quantifier-free tautology. One purpose of this paper is to provide a description which in certain respects is more direct. Roughly speaking, ascent to A ⊃ A′ from a quantifier-free level will be replaced by movement from A to A′ on the quantificational level. Each movement will be closely related to the ascent it replaces.

The new description makes use of a set L of rules of inference, the L-rules. L is complete in the sense that, if A is a conjunction and A′ an alternation of first-order formulas in prenex normal form, and if A ⊃ A′ is valid, then A′ can be obtained from A by an L-deduction, i.e., by applications of L-rules only. The distinctive feature of L is that each L-rule possesses two characteristics which, especially in combination, are desirable. First, each L-rule yields only conclusions implied by the premisses.

In his well-known paper [11], Post founded a general theory of recursively enumerable sets, which had its metamathematical source in questions about the decision problem for deducibility in formal systems. However, in centering attention on the notion of degree of unsolvability, Post set a course for his theory which has rarely returned to this source. Among exceptions to this tendency we may mention, as being closest to the problems considered here, the work of Kleene in [8] pp. 298–316, of Myhill in [10], and of Uspenskij in [15]. It is the purpose of this paper to make some further contributions towards bridging this gap.

From a certain point of view, it may be argued that there is no real separation between metamathematics and the theory of recursively enumerable sets. For, if the notion of formal system is construed in a sufficiently wide sense, by taking as ‘axioms’ certain effectively found members of a set of ‘formal objects’ and as ‘proofs’ certain effectively found sequences of these objects, then the set of ‘provable statements’ of such a system may be identified, via Gödel's numbering technique, with a recursively enumerable set; and conversely, each recursively enumerable set is identified in this manner with some formal system (cf. [8] pp. 299–300 and 306). However, the pertinence of Post's theory is no longer clear when we turn to systems formalized within the more conventional framework of the first-order predicate calculus. It is just this restriction which serves to clarify the difference in spirit of the two disciplines.

One task of metamathematics is to relate suggestive but nonelementary modeltheoretic concepts to more elementary proof-theoretic concepts, thereby opening up modeltheoretic problems to proof-theoretic methods of attack. Herbrand's Theorem (see [8] or also [9], vol. 2) or Gentzen's Extended Hauptsatz (see [5] or also [10]) was first used along these lines by Beth [1]. Using a modified version he showed that for all first-order systems a certain modeltheoretic notion of definability coincides with a certain proof theoretic notion. In the present paper the Herbrand-Gentzen Theorem will be applied to generalize Beth's results from primitive predicate symbols to arbitrary formulas and terms.

This may be interpreted as showing that (apart from some relatively minor exceptions which will be made apparent below) the expressive power of each first-order system is rounded out, or the system is functionally complete, in the following sense: Any functional relationship which obtains between concepts that are expressible in the system is itself expressible and provable in the system.

A second application is concerned with the hierarchy of second-order formulas. A certain relationship is shown to hold between first-order formulas and those second-order formulas which are of the form (∃T1)…(∃Tk)A or (T1)…(Tk)A with A being a first-order formula. Modeltheoretically this can be regarded as a relationship between the class AC and the class PC⊿ of sets of models, investigated by Tarski in [12] and [13].

The main aims of this paper are firstly to present new and simpler postulate sets for certain well-known systems of modal logic, and secondly, in the light of these results, to suggest some new or newly formulated calculi, capable of interpretation as systems of epistemic or deontic modalities. The symbolism throughout is that of [9] (see especially Part III, Chapter I). In what follows, by a Lewis modal system is meant a system which (i) contains the full classical propositional calculus, (ii) is contained in the Lewis system S5, (iii) admits of the substitutability of tautologous equivalents, (iv) possesses as theses the four formulae:

We shall also say that a system Σ1 is stricter than a system Σ2, if both are Lewis modal systems and Σ1 is contained in Σ2 but Σ2 is not contained in Σ1; and we shall call Σ1absolutely strict, if it possesses an infinity of irreducible modalities. Thus, the five systems of Lewis in [5], S1, S2, S3, S4, and S5, are all Lewis modal systems by this definition; they are in an order of decreasing strictness from S1 to S5; and S1 and S2 alone are absolutely strict.

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.

1. Let X be a statement which is formulated in the lower predicate calculus in terms of the relations of addition, multiplication, and equality, and — possibly — of the elements of a given commutative field M. Suppose moreover that X is in prenex normal form, e.g.

where Z does not include any further quantifiers. In order that X be satisfied by the algebraic closure M* of M, it is necessary and sufficient that there exist Herbrand functions (or choice functions) φ1(x1, x2), φ2(x1, x2), φ3(x1, x2, x3, x4) with arguments ranging over M* and taking values in M* such that

holds for all x1, x2, x3, x4 in M*. In general the definition of these functions is far from being unique, and a priori they bear no relation to the functions which are defined ‘naturally’ in M* i.e. the rational, and more generally the algebraic, functions with coefficients in M or M*. However, we shall show in the present paper that the entire domain of variation of the arguments x1, x2, x3, x4 — regarded as the affine space S4 over M* — can be divided up into a finite number of regions Di such that in each Di the functions ϕk can be chosen as algebraic functions of their arguments. Indeed, our complete result (§ 3) proves rather more than that. In particular, it turns out that the regions Di may be taken as differences of algebraic varieties in M*.