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.

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.

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:

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.

For a fixed countably infinite structure Γ with finite relational signature τ, we study the following computational problem: input are quantifier-free τ-formulas ϕ0, ϕ1, …, ϕn that define relations R0, R1, …, Rn over Γ. The question is whether the relation R0 is primitive positive definable from R1, …, Rn, i.e., definable by a first-order formula that uses only relation symbols for R1, …, Rn, equality, conjunctions, and existential quantification (disjunction, negation, and universal quantification are forbidden).

We show decidability of this problem for all structures Γ that have a first-order definition in an ordered homogeneous structure Δ with a finite relational signature whose age is a Ramsey class and determined by finitely many forbidden substructures. Examples of structures Γ with this property are the order of the rationals, the random graph, the homogeneous universal poset, the random tournament, all homogeneous universal C-relations, and many more. We also obtain decidability of the problem when we replace primitive positive definability by existential positive, or existential definability. Our proof makes use of universal algebraic and model theoretic concepts, Ramsey theory, and a recent characterization of Ramsey classes in topological dynamics.

We use some simple facts about the wtt-degrees of r.e. sets together with a construction to answer some questions concerning the join and meet operators in the r.e. degrees. The construction is that of an r.e. Turing degree a with just one wtt-degree in a such that a is the join of a minimal pair of r.e. degrees. We hope to illustrate the usefulness of studying the stronger reducibility orderings of r.e. sets for providing information about Turing reducibility.

In this paper we consider certain formal properties of deductive systems which, in special cases, reduce to the property of ω-consistency; and we then seek to understand the significance of these properties by relating them to the use of models in providing interpretations of the deductive systems.

The notion of ω-consistency arises in connection with deductive systems of arithmetic. For definiteness, let us suppose that the system is a functional calculus whose domain of individuals is construed as the set of natural numbers, and that the system possesses individual constants ν0, ν1, ν2, … such that νi functions as a name for the number i. Such a system is called ω-consistent, if there is no well-formed formula A(x) (in which x is the only free variable) such that A(ν0), A(ν1), A(ν2), … and ∼(x)A(x) are all formal theorems of the system, where A(νi) is the formula resulting from A(x) by substituting the constant νi for each free occurrence of the individual variable x.

Now consider an arbitrary applied functional calculus F, and let Γ be any non-empty set of its individual constants. In imitation of the definition of ω-consistency, we may say that the system F is Γ-consistent, if it contains no formula A(x) (in which x is the only free variable) such that ⊦ A (α) for every constant α in Γ, and also ⊦ ∼(x)A(x) (where an occurrence of “⊦” indicates that the formula which it precedes is a formal theorem). We easily see that the condition of Γ-consistency is equivalent to the condition that the system F contain no formula B(x) such that ⊦ ∼ B(α) for each α in Γ, and also ⊦ (∃x)B(x).

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.

We prove that the additive group of the rationals does not have an automatic presentation. The proof also applies to certain other abelian groups, for example, torsion-free groups that are p-divisible for infinitely many primes p, or groups of the form ⊕pϵIZ(p∞), where I is an infinite set of primes.

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.

We solve a major open problem concerning algorithmic properties of products of ‘transitive’ modal logics by showing that products and commutators of such standard logics as K4, S4, S4.1, K4.3, GL, or Grz are undecidable and do not have the finite model property. More generally, we prove that no Kripke complete extension of the commutator [K4, K4] with product frames of arbitrary finite or infinite depth (with respect to both accessibility relations) can be decidable. In particular, if l1 and l2 are classes of transitive frames such that their depth cannot be bounded by any fixed n < ω, then the logic of the class {5ℑ1 × ℑ2 ∣ ℑ1 ∈ l1, ℑ2, ∈ l2} is undecidable. (On the contrary, the product of, say, K4 and the logic of all transitive Kripke frames of depth ≤ n, for some fixed n < ω, is decidable.) The complexity of these undecidable logics ranges from r.e. to co-r.e. and Π11-complete. As a consequence, we give the first known examples of Kripke incomplete commutators of Kripke complete logics.

The present work may perhaps be seen as a point of convergence of two historically distinct sequences of results. One sequence of results started with the work of Tennenbaum [59] who showed that there could be no nonstandard recursive model of the system PA of first order Peano arithmetic. Shepherdson [65] on the other hand showed that the system of arithmetic with open induction was sufficiently weak to allow the construction of nonstandard recursive models. Between these two results there remained for many years a large gap occasioned by a general lack of interest in weak systems of arithmetic. However Dana Scott observed that the addition alone of a nonstandard model of PA could not be recursive, while more recently McAloon [82] improved these results by showing that even for the weaker system of arithmetic with only bounded induction, neither the addition nor the multiplication of a nonstandard model could be recursive.

Another sequence of results starts with the work of Lessan [78], and independently Jensen and Ehrenfeucht [76], who showed that the structures which may be obtained as the reducts to addition of countable nonstandard models of PA are exactly the countable recursively saturated models of Presburger arithmetic. More recently, Cegielski, McAloon and the author [81] showed that the above result holds true if PA is replaced by the much weaker system of bounded induction.

However in both the case of the Tennenbaum phenomenon and in that of the recursive saturation of addition the problem remained open as to how strong a system was really necessary to generate the required phenomenon. All that was clear a priori was that open induction was too weak to produce either result.

The notion of a D-ring, generalizing that of a differential or a differenee ring, is introduced, Quantifier elimination and a version of the Ax—Kochen—Eršov principle is proven for a theory of valued D-fields of residual characteristic zero.

Let κ < λ be regular uncountable cardinals. Using a finite support iteration (in fact a matrix iteration) of ccc posets we obtain the consistency of . If μ is a measurable cardinal and μ < κ < λ, then using similar techniques we obtain the consistency of .

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.

We show that the modal propositional logic G, originally introduced to describe the modality “it is provable that”, is also sound for various interpretations using filters on ordinal numbers, for example the end-segment filters, the club filters, or the ineffable filters. We also prove that G is complete for the interpretation using end-segment filters. In the case of club filters, we show that G is complete if Jensen's principle □κ holds for all κ < ℵω; on the other hand, it is consistent relative to a Mahlo cardinal that G be incomplete for the club filter interpretation.