Davis, Matijasevic, and Robinson, in their admirable survey article [D-M-R], interpret the negative solution of Hilbert's Tenth Problem as a resounding positive statement about the versatility of Diophantine equations (that any listable set can be coded as the set of parameter values for which a suitable polynomial possesses integral solutions).

One can also view the Matijasevic result as implying that there are families of Diophantine equations parametrized by a variable t, which have integral solutions for some integral values t = a > 0, and yet there is no computable function of t which provides an upper bound for the smallest integral solution for these values a. The smallest integral solutions of the Diophantine equation for these values are, at least sporadically, too large to be bounded by any computable function. This is somewhat difficult to visualize, since there is quite an array of computable functions. But let us take an explicit example. Consider the function

Matijasevic's result guarantees the existence of parametrized families of Diophantine equations such that even this function fails to yield an upper bound for its smallest integral solutions (for all values of the parameter t for which there are integral solutions).

Families of Diophantine equations in a parameter t, whose integral solutions for t = 1, 2, 3,… exhibit a certain arythmia in terms of their size, have fascinated mathematicians for centuries, and this phenomenon (the size of smallest integral solution varying wildly with the parameter-value) is surprising, even when the equations are perfectly “decidable”.

A new axiom is proposed, the Ground Axiom, asserting that the universe is not a nontrivial set forcing extension of any inner model. The Ground Axiom is first-order expressible, and any model of ZFC has a class forcing extension which satisfies it. The Ground Axiom is independent of many well-known set-theoretic assertions including the Generalized Continuum Hypothesis, the assertion V=HOD that every set is ordinal definable, and the existence of measurable and supercompact cardinals. The related Bedrock Axiom, asserting that the universe is a set forcing extension of a model satisfying the Ground Axiom, is also first-order expressible, and its negation is consistent.

If dominating functions in ωω are adjoined repeatedly over a model of GCH via a finite-support c.c.c. iteration, then in the resulting generic extension there are no long towers, every well-ordered unbounded family of increasing functions is a scale, and the splitting number (and hence the distributivity number ) remains at ω1.

According to Gödel's completeness theorem, every consistent theory1 has a model whose domain is a set of natural numbers. The objects of the model corresponding to the predicate symbols of the theory are then predicates of natural numbers. Kleene [5] p. 398 showed that, if the theory is axiomatizable,2 then the model can be chosen so that these predicates are in both two-quantifier forms, i.e., they can be expressed in both the forms (x)(Ey)R and (Ex)(y)S with R and S recursive. An alternative proof has been given by Hasen jaeger [3].

A completeness theorem is established for logics with congruence endowed with general semantics (in the style of general frames). As a corollary, completeness is shown to be preserved by fibring logics with congruence provided that congruence is retained in the resulting logic. The class of logics with equivalence is shown to be closed under fibring and to be included in the class of logics with congruence. Thus, completeness is shown to be preserved by fibring logics with equivalence and general semantics. An example is provided showing that completeness is not always preserved by fibring ligics endowed with standard (non general) semantics. A categorial characterization of fibring is provided using coproducts and cocartesian liftings.

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).

The λμ-calculus is an extension of the λ-calculus that has been introduced by M Parigot to give an algorithmic content to classical proofs. We show that Böhm's theorem fails in this calculus.

A previously unexplored method, combining logical and mathematical elements, is shown to yield substantial numerical improvements in the area of Diophantine approximations. Kreisel illustrated the method abstractly by noting that effective bounds on the number of elements are ensured if Herbrand terms from ineffective proofs of Σ2-finiteness theorems satisfy certain simple growth conditions. Here several efficient growth conditions for the same purpose are presented that are actually satisfied in practice, in particular, by the proofs of Roth's theorem due to Roth himself and to Esnault and Viehweg. The analysis of the former yields an exponential bound of order exp(70ε−2d2) in place of exp(285ε−2d2) given by Davenport and Roth in 1955, where α is (real) algebraic of degree d ≥ 2 and ∣α − pq−1∣ < q−2−ε. (Thus the new bound is less than the fourth root of the old one.) The new bounds extracted from the other proof are polynomial of low degree (in ε−1 and log d). Corollaries: Apart from a new bound for the number of solutions of the corresponding Diophantine equations and inequalities (among them Thue's inequality), log log qν, < Cα, εν5/6+ε, where qν are the denominators of the convergents to the continued fraction of α.

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.

1. This paper grew out of an attempt to answer a question raised in [4]. Let a logic L containing “numerals” z1, z2, … and a certain statement N(x) (intended to express the proposition that x is a natural number) be called ω-inconsistent if there is a statement such that ⊦ F(zk) for k = 1, 2, …, and ⊦ ∼(x)·N(x) ⊃ F(x); then it is evident that L cannot have a model in which N(x) is satisfied by the images of the numerals and nothing else if L is ω-inconsistent.

Question: If L is ω-consistent, i.e. not ω-inconsistent, must there be such a model? Calling a model of the kind just described a special model, we ask for necessary and sufficient conditions on L to insure the existence of a special model. We give several sets of such conditions, applicable to a certain very inclusive class of logics, in Theorem 1 and Theorems 3 and 4. Theorem 2 shows that a logic may be ω-consistent but still not have a special model.

This paper was close to completion when [3] appeared. For systems with only denumerably many symbols our results include Henkin's, for, by adjoining a new predicate N(x) to each of the systems considered in [3] which have only a denumerable number of constant symbols and then adding as an axiom (x)N(x), these systems become special cases of the systems we consider. It is easily seen that Henkin's Theorem 7 essentially proves the equivalence of conditions (2) and (3) in our Theorem 1, and Theorem 3 of [3] corresponds to our Theorem 2. Incidentally, our argument of Theorem 2 could also serve to prove Henkin's Theorem 6.

It has been proved by S. C. Kleene and David Nelson that the formula

is intuitionistically non-deducible, i.e., non-deducible within the intuitionistic functional calculus.

The aim of this note is to outline a general method which permits us to establish the intuitionistic non-deducibility of many formulas and in particular of the formula (1).

Various equivalents and weakenings of the combinatorial principle ◊ are considered. The paper contains both absolute results and consistency results. Also included is a new characterisation of the notion of a stationary subset of ω1.

The paper establishes the general structure of the inconsistent models of arithmetic of [7]. It is shown that such models are constituted by a sequence of nuclei. The nuclei fall into three segments: the first contains improper nuclei: the second contains proper nuclei with linear chromosomes: the third contains proper nuclei with cyclical chromosomes. The nuclei have periods which are inherited up the ordering. It is also shown that the improper nuclei can have the order type of any ordinal, of the rationals, or of any other order type that can be embedded in the rationals in a certain way.

We discuss a ‘negative’ way of defining frame classes in (multi)modal logic, and address the question of whether these classes can be axiomatized by derivation rules, the ‘non-ξ rules’, styled after Gabbay's Irreflexivity Rule. The main result of this paper is a metatheorem on completeness, of the following kind: If ⋀ is a derivation system having a set of axioms that are special Sahlqvist formulas and ⋀+ is the extension of ⋀ with a set of non-ξ rules, then ⋀+ is strongly sound and complete with respect to the class of frames determined by the axioms and the rules.

In Kripke [8] the first-order intuitionjstic predicate calculus (without identity) is proved semantically complete with respect to a certain model theory, in the sense that every formula of this calculus is shown to be provable if and only if it is valid. Metatheorems of this sort are frequently called weak completeness theorems—the object of the present paper is to extend Kripke's result to obtain a strong completeness theorem for the intuitionistic predicate calculus of first order; i.e., we will show that a formula A of this calculus can be deduced from a set Γ of formulas if and only if Γ implies A. In notes 3 and 5, below, we will indicate how to account for identity, as well. Our proof of the completeness theorem employs techniques adapted from Henkin [6], and makes no use of semantic tableaux; this proof will also yield a Löwenheim-Skolem theorem for the modeling.

The modal logic GL has been found by Solovay [13] to formalize the provable propositional properties of the provability-predicate for Peano's Arithmetic PA (cf. §1 below). We give several sequential calculi for GL, compare their merits, and use one calculus to syntactically derive several metamathematical results about GL.

Some of our results have been proved model theoretically, and similar proofs are fairly straightforward for several of the remaining ones (G. Boolos and the referee have provided such proofs for 4.1, 4.3 and 5.1 below). However, our syntactic techniques often yield more concise and obviously constructive proofs, they offer additional insight into the nature of the systems considered, and are easily adaptable to systems for which semantical analysis is problematic.

I am indebted to G. Boolos and to the referee for their valuable advice. The referee has suggested the rule GL of §3 below as an axiomatization of GL; the resulting sequential calculus has allowed a definite improvement of our original presentation.

The jump a′ of a degree a is defined to be the largest degree recursively enumerable in a in the upper semilattice of degrees of unsolvability. We examine below some of the ways in which the jump operation is related to the partial ordering of the degrees. Fried berg [3] showed that the equation a = x′ is solvable if and only if a ≥ 0′. Sacks [13] showed that we can find a solution of a = x′ which is ≤ 0′ (and in fact is r.e.) if and only if a ≥ 0′ and is r.e. in 0′. Spector [16] constructed a minimal degree and Sacks [13] constructed one ≤ 0′. So far the only result concerning the relationship between minimal degrees and the jump operator is one due to Yates [17] who showed that there is a minimal predecessor for each non-recursive r.e. degree, and hence that there is a minimal degree with jump 0′. In §1, we obtain an analogue of Friedberg's theorem by constructing a minimal degree solution for a = x′ whenever a ≥ 0′. We incorporate Friedberg5s original number-theoretic device with a complicated sequence of approximations to the nest of trees necessary for the construction of a minimal degree. The proof of Theorem 1 is a revision of an earlier, shorter presentation, and incorporates many additions and modifications suggested by R. Epstein. In §2, we show that any hope for a result analogous to that of Sacks on the jumps of r.e. degrees cannot be fulfilled since 0″ is not the jump of any minimal degree below 0′. We use a characterization of the degrees below 0′ with jump 0″ similar to that found for r.e. degrees with jump 0′ by R. W. Robinson [12]. Finally, in §3, we give a proof that every degree a ≤ 0′ with a′ = 0″ has a minimal predecessor. Yates [17] has already shown that every nonzero r.e. degree has a minimal predecessor, but that there is a nonzero degree ≤ 0′ with no minimal predecessor (see [18]; or for the original unrelativized result see [10] or [4]).

We show that Shelah’s Eventual Categoricity Conjecture for successors follows from the existence of class many strongly compact cardinals. This is the first time the consistency of this conjecture has been proven. We do so by showing that every AEC with LS(K) below a strongly compact cardinal κ is < κ-tame and applying the categoricity transfer of Grossberg and VanDieren [11]. These techniques also apply to measurable and weakly compact cardinals and we prove similar tameness results under those hypotheses. We isolate a dual property to tameness, called type shortness, and show that it follows similarly from large cardinals.

During the past several decades, linguists have developed and applied widely techniques which enable them, to a considerable extent, to determine and state the structure of natural languages without semantic reference. It is of interest to inquire seriously into the formality of linguistic method and the adequacy of whatever part of it can be made purely formal, and to examine the possibilities of applying it, as has occasionally been suggested, to a wider range of problems. In order to pursue these aims it is first necessary to reconstruct carefully the set of procedures by which the linguist derives the statements of a linguistic grammar from the behaviour of language users, distinguishing clearly between formal and experimental in such a way that grammatical notions, appearing as definienda in a constructional system, will be formally derivable for any language from a fixed sample of linguistic material upon which the primitives of the system are experimentally defined. The present paper will be an attempt to formalize a certain part of the linguist's generalized syntax language.

From another point of view, this paper is an attempt to develop an adequate notion of syntactic category within an inscriptional nominalistic framework. The inscriptional approach seems natural for linguistics, particularly in view of the fact that an adequate extension of the results of this paper will have to deal with the problem of homonymity, i.e., with a statement of the conditions under which tokens of the same type must be assigned to different syntactic classes.