In this paper we set out the basic model theory of differential fields of characteristic 0, which have finitely many commuting derivations. We give axioms for the theory of differentially closed differential fields with m derivations and show that this theory is ω-stable, model complete, and quantifier-eliminable, and that it admits elimination of imaginaries. We give a characterization of forking and compute the rank of this theory to be ωm + 1.

In this paper I give a characterization of the closed fragment of the provability logic of I Δ0 + EXP with a propositional constant for EXP. In three appendices many details on arithmetization are provided.

We shall apply some of the results of Jensen [4] to deduce new combinatorial consequences of the axiom of constructibility, V = L. We shall show, among other things, that if V = L then for each cardinal λ there is a set A ⊆ λ such that neither A nor λ – A contain a closed set of type ω1. This is an extension of a result of Silver who proved it for λ = ω2, providing a partial answer to Problem 68 of Friedman [2].

The main results of this paper were obtained independently by both authors.

If λ is an ordinal, E is said to be Mahlo (or stationary) in λ, if λ – E does not contain a closed cofinal subset of λ.

Consider the statements:

(J1) There is a class E of limit ordinals and a sequence Cλ defined on singular limit ordinals λ such that

(i) E ⋂ μ is Mahlo in μ for all regular > ω;

(ii) Cλ is closed and unbounded in λ;

(iii) if γ < is a limit point of Cλ, then γ is singular, γ ∉ E and Cγ = γ ⋂ Cλ.

For each infinite cardinal κ:

(J2,κ) There is a set E ⊂ κ+ and a sequence Cλ(Lim(λ), λ < κ+) such that

(i) E is Mahlo in κ+;

(ii) Cλ is closed and unbounded in λ;

(iii) if cf(λ) < κ, then card Cλ < κ;

(iv) if γ < λ is a limit point of Cλ then γ ∉ E and Cγ = ϣ ⋂ Cλ.

In this paper we introduce a new notion of realizability for intuitionistic arithmetic in all finite types. The notion seems to us to capture some of the intuition underlying both the recursive realizability of Kjeene [5] and the semantics of Kripke [7]. After some preliminaries of a syntactic and recursion-theoretic character in §1, we motivate and define our notion of realizability in §2. In §3 we prove a soundness theorem, and in §4 we apply that theorem to obtain new information about provability in some extensions of intuitionistic arithmetic in all finite types. In §5 we consider a special case of our general notion and prove a kind of reflection theorem for it. Finally, in §6, we consider a formalized version of our realizability notion and use it to give a new proof of the conservative extension theorem discussed in Goodman and Myhill [4] and proved in our [3]. (Apparently, a form of this result is also proved in Mine [13]. We have not seen this paper, but are relying on [12].) As a corollary, we obtain the following somewhat strengthened result: Let Σ be any extension of first-order intuitionistic arithmetic (HA) formalized in the language of HA. Let Σω be the theory obtained from Σ by adding functionals of finite type with intuitionistic logic, intensional identity, and axioms of choice and dependent choice at all types. Then Σω is a conservative extension of Σ. An interesting example of this theorem is obtained by taking Σ to be classical first-order arithmetic.

The principal aim of this paper is to establish a theorem stating, roughly, that the addition of the fan theorem and the. continuity schema to an intuitionistic system of elementary analysis results in a conservative extension with respect to arithmetical statements.

The result implies that the consistency of first order arithmetic cannot be proved by use of the fan theorem, in addition to standard elementary methods—although it was the opposite assumption which led Gentzen to withdraw the first version of his consistency proof for arithmetic (see [B]).

We must presuppose acquaintance with notation and principal results of [K, T], and with §1.6, Chapter II, and Chapter III, §4-6 of [T1]. In one respect we shall deviate from the notation in [K, T]: We shall use (n)x (instead of g(n, x)) to indicate the xth component of the sequence coded by n, if x < lth(n), 0 otherwise.

We also introduce abbreviations n ≤* m, a ≤ b which will be used frequently below:

When a logician approaches the world of mathematics, he may have in mind one or more of several purposes. He may try to find in mathematics a framework for formalizing commonly accepted laws of thought or perhaps laws of thought that are not commonly accepted. He may want to assist the mathematician by providing him with firm foundations for his theories. But it may also be the case that the logician wishes to use his own characteristic tools—formalized languages, explicit relations between symbols and objects, rigidly expressed and controlled rules of deduction—in order to gain a better understanding of the various and variegated kinds of structures, methods, theories and theorems that are to be found in mathematics. We may then expect him to adopt the attitude of the physicist or psychologist who (whatever his professed philosophy) feels that he deals with phenomena of the external world, whose rules cannot be imposed by him arbitrarily. He, or those that come after him, may indeed use the understanding thus gained in order to modify these phenomena, but as a scientist he would not regard this possibility as his only justification.

For many years now, I have concentrated on the third of the lines of approach sketched above, and it seemed natural that I should discuss it again on the present occasion. However, today I do not wish to emphasize past developments but, using some of them as a background, I propose to enumerate a number of open problems. These problems seemed to me of some interest not only for their own sake but also because their solution might well require weapons whose introduction would close definite gaps in our armory.

By means of models in toposes of C-sets (where C is a small category), necessary conditions are found for the minimum quantified extension of a propositional (intermediate, modal) logic to be complete with respect to Kripke semantics; in particular, many well-known systems turn out to be incomplete.

A fundamental problem in the theory of abelian groups is to determine the structure of Ext(A, Z) for arbitrary abelian groups A. This problem was raised by L. Fuchs in 1958, and since then has been the center of considerable activity and progress.

We briefly summarize the present state of this problem. It is a well-known fact that

where tA denotes the torsion subgroup of A. Thus the structure problem for Ext(A, Z) breakdown to the two distinct cases, torsion and torsion free groups. For a torsion group T,

which is compact and reduced, and its structure is known explicitly [12].

For torsion free A, Ext(A, Z) is divisible; hence it has a unique representation

Thus Ext(A, Z) is characterized by countably many cardinal numbers, which we denote as follows: ν0(A) is the rank of the torsion free part of Ext(A, Z), and νp(A) are the ranks of the p-primary parts of Ext(A, Z), Extp(A, Z).

If A is free it is an elementary fact that Ext(A, Z) = 0. The second named author has shown [16] that in the presence of V = L the converse is also true. For countable torsion free, nonfree A, C. Jensen [13] has shown that νp(A) is either finite or and νp(A) ≤ ν0(A). Therefore, the case for uncountable, nonfree, torsion free groups A remains to be studied.

Let us call an integer part of an ordered field any subring such that every element of the field lies at distance less than I from a unique element of the ring. We show that every real closed field has an integer part.

It is well known that iteration of any number-theoretic function f, which grows at least exponentially, produces a new function f′ such that f is elementary-recursive in f′ (in the Csillag-Kalmar sense), but not conversely (since f′ majorizes every function elementary-recursive in f). This device was first used by Grzegorczyk [3] in the construction of a properly expanding hierarchy {ℰn: n = 0, 1, 2, …} which provided a classification of the primitive recursive functions. More recently it was shown in [7] how, by iterating at successor stages and diagonalizing over fundamental sequences at limit stages, the Grzegorczyk hierarchy can be extended through Cantor's second number-class. A problem which immediately arises is that of classifying all recursive functions, and an answer to this problem is to be found in the general results of Feferman [1]. These results show that although hierarchies of various types (including the above extensions of Grzegorczyk's hierarchy) can be produced, which range over initial segments of the constructive ordinals and which do provide complete classifications of the recursive functions, these cannot be regarded as classifications “from below”, since the method of assigning fundamental sequences at limit stages must be highly noneffective. We therefore adopt the more modest aim here (as in [7], [12], [14]) of characterising certain well-known (effectively generated) subclasses of the recursive functions, by means of hierarchies generated in a natural manner, “from below”.

In [1] and [2] I investigated logics intermediate between intuitionistic and classical propositional logic. In the present paper I shall study inclusion and non-inclusion between certain intermediate predicate logics. All the logics considered result from intuitionistic predicate logic by addition of classically valid axiom schemes.

We show that the Turing degrees are not sufficient to measure the complexity of continuous functions on [0, 1]. Computability of continuous real functions is a standard notion from computable analysis. However, no satisfactory theory of degrees of continuous functions exists. We introduce the continuous degrees and prove that they are a proper extension of the Turing degrees and a proper substructure of the enumeration degrees. Call continuous degrees which are not Turing degrees non-total. Several fundamental results are proved: a continuous function with non-total degree has no least degree representation, settling a question asked by Pour-El and Lempp; every non-computable f ∈ [0,1] computes a non-computable subset of ℕ there is a non-total degree between Turing degrees a <Tb iff b is a PA degree relative to a; ⊆ 2ℕ is a Scott set iff it is the collection of f-computable subsets of ℕ for some f ∈ [0,1] of non-total degree; and there are computably incomparable f, g ∈ [0,1] which compute exactly the same subsets of ℕ. Proofs draw from classical analysis and constructive analysis as well as from computability theory.

Church's thesis, that all reasonable definitions of “computability” are equivalent, is not usually thought of in terms of computability by a continuous computer, of which the general-purpose analog computer (GPAC) is a prototype. Here we prove, under a hypothesis of determinism, that the analytic outputs of a C∞ GPAC are computable by a digital computer.

In [POE, Theorems 5, 6, 7, and 8], Pour-El obtained some related results. (The proof there of Theorem 7 depends on her Theorem 2, for which the proof in [POE] is incorrect, but for which a correct proof is given in [LIR]. Also, the proof in [POE] of Theorem 8 depends on the unproved assertion that a solution of an algebraic differential equation must be analytic on an open subset of its domain. However, this assertion was later proved in [BRR].) As in [POE], we reduce the problem to a problem about solutions of certain systems of algebraic differential equations (ADE's). If such a system is nonsingular (i.e. if the “separant” does not vanish along the given solution), then the argument is very easy (see [VSD] for an even simpler situation), so that the essential difficulties arise from singular systems. Our main tools in handling these difficulties are drawn from the excellent (and difficult) paper [DEL] by Denef and Lipshitz. The author especially wants to thank Leonard Lipshitz for his kind help in the preparation of the present paper.

We emphasize here that our proof of the simulation result applies only to the GPAC as described below. The GPAC's form a natural subclass of the class of all analog computers, and are based on certain idealized components (“black boxes”), mostly associated with the technology of past decades. One can easily envisage other kinds of black boxes of an input-output character that would lead to different kinds of analog computers. (For example, one could incorporate delays, or spatial integrators in addition to the present temporal integrators, etc.) Whether digital simulation is possible for these “extended” analog computers poses a rich and challenging set of research questions.

Following a suggestion of Feys, we use “rigorous implication” as a translation of Ackermann's strenge Implikation ([1]). Interest in Ackermann's system stems in part from the fact that it formalizes the properties of a strong, natural sort of implication which provably avoids standard implicational paradoxes, and which is consequently a good candidate for a formalization of entailment (considered as a narrower relation than that of strict implication). Our present purpose will not be to defend this suggestion, but rather to present some information about rigorous implication. In particular, we show first that the structure of modalities (in the sense of Parry [4]) in Ackermann's system is identical with the structure of modalities in Lewis's S4, and secondly that (Ackermann's apparent conjecture to the contrary notwithstanding) it is possible to define modalities with the help of rigorous implication.

The central result of this paper was proved in order to settle a problem arising from B. H. Neumann's paper [10].

In [10] Neumann proved that if a finitely generated group H is recursively absolutely presentable then H is embeddable in all nontrivial algebraically-closed groups. Harry Simmons [14] clarified this by showing that a finitely generated group H is recursively absolutely presentable if and only if H can be recursively presented with solvable word-problem. Therefore, if a finitely generated group H can be recursively presented with solvable word-problem then H is embeddable in all nontrivial algebraically-closed groups.

The problem arises of characterizing those finitely generated groups which are embeddable in all nontrivial algebraically-closed groups. In this paper we prove, by a forcing argument, that if a finitely generated group H is embeddable in all non-trivial algebraically-closed groups then H can be recursively presented with solvable word-problem. Thus Neumann's result is sharp.

Our results are obtained by the method of forcing in model-theory, as developed in [1], [12]. Our method of proof has nothing to do with group-theory. We prove general results, Theorems 1 and 2 below, about constructing generic structures without certain isomorphism-types of finitely generated substructures. The formulation of these results requires the notion of Turing degree. As an application of the central result we prove Theorem 3 which gives information about the number of countable K-generic structures.

We gratefully acknowledge many helpful conversations with Harry Simmons.

We use the word “number” for “nonnegative integer” and “set” for collection of numbers. The set of all numbers is denoted by ε and the empty set by ο. We write ⊂ for the relation of inclusion and ⊆ for that of proper inclusion. If ƒ is a function from a subset of ε into ε, its domain and range are denoted by δƒ and ρƒ respectively. For any collection Γ of entities, card Γ or card (Γ) stands for the cardinality of Γ. The cardinality of the continuum is denoted by c.

Im Folgenden wird eine Vereinfachung der Beweisanordnung für Henkin's Theorem [2] p. 162 angegeben (Abschnitt I). – Die Vereinfachung zeigt sich u.a. darin, daß für den abgeänderten Beweis eine Abschätzung der “projektiven Klasse” (im Sinne der Kleene-Mostowski'schen Theorie der projektiven Mengen von natürlichen Zahlen) für das zu konstruierende Modell gelingt (Abschnitte II–IV). Die Kenntnis der Henkin'schen Arbeit wird vorausgesetzt.

Um eine maximale widerspruchsfreie Menge Γω von geschlossenen Formeln, in der zu jeder Existenzaussage (∃x)A(x) eine Beispielaussage A(uij) vorhanden ist, zu erhalten, führt Henkin einen Turm von Kalkülen S0, S1, …, Si, … und dessen Vereinigung Sω ein. Abwechselnd wird dann die gegebene Menge von Formeln in Si zu einer maximalen widerspruchsfreien Menge Γi erweitert und in Si+1 durch Hinzunahme von Beispielaussagen für alle Existenzaussagen aus Γi ergänzt, für die das nicht schon in einem früheren Schritt geschehen ist. Γω ist dann die Vereinigung aller Γi.

Die Vereinfachung besteht nun darin, daß – nach Erweiterung von S0 zu einem Kalkül S* durch Hinzunahme einer einfachen Folge u1, u2, … von “neuen” Konstanten – in S* zu jeder Existenzaussage eine bedingte Beispielaussage gebildet wird. K sei die Klasse dieser Aussagen, Λ die gegebene widerspruchsfreie Menge; dann wird Λ* = K ◡ Λ in S* einmal zu einer maximalen widerspruchsfreien Menge ergänzt.

Unter Verwendung der Standard-Anordnung aller geschlossenen Formeln von S* erhalten wir für diejenigen von der Form (∃x)A(x) eine Aufzählung (∃x)Ai(x), dazu eine Indexfolge ji (i =1, 2, …), definiert durch:

A theory T is axiomatizable by a schema if there is a formula Γ, involving symbols of T plus a new relation symbol R, such that the set of all (universal closures of) instances of Γ in T is a set of axioms for T. (It is understood that, if R has n places, an instance of Γ in T is obtained by properly substituting for R in Γ a formula of T which has n selected free variables and is allowed to have any number of other free variables as parameters.) Obviously, the notion is unchanged if finitely many Γ's, each involving several new R's, are allowed instead. All theories we consider are assumed to be theories in the first-order logic with equality (as in [8]), to have finitely many nonlogical symbols, and to be recursively axiomatizable.

In this paper, we consider certain cardinals in ZF (set theory without AC, the axiom of choice). In ZFC (set theory with AC), given any cardinals and , either ≤ or ≤ . However, in ZF this is no longer so. For a given infinite set A consider seq1-1(A), the set of all sequences of A without repetition. We compare |seq1-1(A)|, the cardinality of this set, to ||, the cardinality of the power set of A. What is provable about these two cardinals in ZF? The main result of this paper is that ZF ⊢ ∀A(| seq1-1(A)| ≠ ||), and we show that this is the best possible result. Furthermore, it is provable in ZF that if B is an infinite set, then | fin(B)| < | (B*)| even though the existence for some infinite set B* of a function ƒ from fin(B*) onto (B*) is consistent with ZF.