Silver and subsequently Galvin and Hajnal, got bounds on , for ℵα strong limit cardinal of cofinality > ℵ0. We somewhat improve those results.

In two papers appearing in successive issues of this Journal, Quine and Goodman, impelled by a philosophical standpoint which forswears all traffic in abstract entities, have explored the possibility of reinterpreting the language of classical mathematics so as to give it meaning (consistent with the observed overt pattern of standard usage) in terms of the narrow domain of entities which they recognize. The present paper offers several comments on this program.

A realizability notion that employs only primitive recursive functions is defined, and, relative to it, the soundness of the fragment of Heyting Arithmetic (HA) in which induction is restricted to formulae is proved. A dual concept of falsifiability is proposed and an analogous soundness result is established for a further restricted fragment of HA.

Suppose T is a first order intuitionistic theory (more precisely, a theory of Heyting's predicate calculus, e.g., abelian groups, one unary function, dense linear order, etc.) presented to us by a set of axioms (denoted also by) T.

Question. Is T decidable?

One knows that if the classical counterpart of T (i.e., take the same axioms but with the classical predicate calculus as the underlying logic) is not decidable, then T cannot be decidable. The problem remains for theories whose classical counterpart is decidable. In [8], sufficient conditions for undecidability were given, and several intuitionistic theories such as abelian groups and unary functions (both with decidable equality) were shown to be undecidable. In this note we show decidability results (see Theorems 1 and 2 below), and compare these results with the undecidability results previously obtained. The method we use is the reduction-method, described fully in [12] and widely applied in [3], which is applied here roughly as follows:

Let T be a given theory of Heyting's predicate calculus. We know that Heyting's predicate calculus is complete for the Kripke-model type of semantics. We choose a class M of Kripke models for which T is complete, i.e., all axioms of T are valid in any model of the class and whenever φ is not a theorem of T, φ is false in some model of M.

We study reals with infinitely many incompressible prefixes. Call A ∈ 2ωKolmogorov random if . where C denotes plain Kolmogorov complexity. This property was suggested by Loveland and studied by Martin-Löf. Schnorr and Solovay. We prove that 2-random reals are Kolmogorov random. Together with the converse—proved by Nies. Stephan and Terwijn [11]—this provides a natural characterization of 2-randomness in terms of plain complexity. We finish with a related characterization of 2-randomness.

I first heard the name of Kurt Gödel when, as a graduate student at Princeton in the fall of 1931, I attended a colloquium at which John von Neumann was the speaker, von Neumann could have spoken on work of his own; but instead he gave an exposition of Gödel's results of formally undecidable propositions [1931].

Today I shall begin with Gödel's paper [1930] on The completeness of the axioms of the functional calculus of logic, or of what we now often call “the first-order predicate calculus”, using “predicate” as synonymous with “propositional function”.

Alonzo Church wrote ([1944, p. 62] and [1956, pp. 288–289]), “the first explicit formulation of the functional calculus of first order as an independent logistic system is perhaps in the first edition of Hilbert and Ackermann's Grundzüge der theoretischen Logik (1928).” Clearly, this formalism is not complete in the sense that each closed formula or its negation is provable. (A closed formula, or sentence, is a formula without free occurrences of variables.) But Hilbert and Ackermann observe, “Whether the system of axioms is complete at least in the sense that all the logical formulas which are correct for each domain of individuals can actually be derived from them is still an unsolved question.” [1928, p. 68].

This question Gödel answered in the affirmative in his Ph.D. thesis (Vienna, 1930), of which the paper under discussion is a rewritten version.

I shall not describe Gödel's proof. Perhaps no theorem in modern logic has been proved more often than Gödel's completeness theorem for the first-order predicate calculus. It stands at the focus of a complex of fundamental theorems, which different scholars have approached from various directions (e.g. Kleene [1967, Chapter VI]).

The primary purpose of this work is to analyze the constructive interpretations of classical theorems concerning the continuity of effective operations. These theorems are the “recursivizations” of the statements that all functions (on various spaces) are continuous. To discuss the question whether these statements are constructively valid, it would be necessary to analyze the notion of “constructively valid,” which is beyond the scope of this paper. We now proceed to describe our results. We deal with two kinds of effective operations: (i) partial operations on indices of partial functions, and (ii) total operations on indices of total functions. The two principal theorems of the subject assert that each such operation is continuous; for (i) this is due to Myhill-Shepherdson [7] and called MS here; for (ii) it is due to Kreisel, Lacombe, and Shoenfield [5] and called KLS. (Explicit formulations of these and other principles mentioned in the introduction will be given in §1 below.)

Several interpretations (of, e.g., Heyting's arithmetic HA) in the literature satisfy Markov's principle MP, and for these MS and KLS are valid, since a close inspection of the classical proofs of MS and KLS shows that they are derivable in HA + MP. But we also find an interpretation in the literature under which MS and KLS are valid while MP is not (hence MS and KLS do not imply MP in systems for which this interpretation is sound). This work is in §2.

We use κ-free but not Whitehead Abelian groups to construct Abstract Elementary Classes (AEC) which satisfy the amalgamation property but fail various conditions on the locality of Galois-types. We introduce the notion that an AEC admits intersections. We conclude that for AEC which admit intersections, the amalgamation property can have no positive effect on locality: there is a transformation of AEC's which preserves non-locality but takes any AEC which admits intersections to one with amalgamation. More specifically we have: Theorem 5.3. There is an AEC with amalgamation which is not (ℵ0, ℵ1)-tame but is (, ∞)-tame; Theorem 3.3. It is consistent with ZFC that there is an AEC with amalgamation which is not (≤ ℵ2, ≤ ℵ2)-compact.

Sanchis [Sa] and Diller [Di] have introduced an interesting relation between terms for primitive recursive functionals of finite type in order to obtain a computability proof. The method is as follows. First the relation is shown to be well-founded. Then computability of each term is obtained by transfinite induction over the relation.

Their relation is given by various clauses which define the (immediate) successors of a term. Hence, starting with a term H and repeatedly applying the successor relation one generates the tree of H (say). The problem is to prove that the trees are well-founded. In their proofs Sanchis and Diller use the axiom of bar induction. Diller also gives a proof using transfinite induction: each tree is shown to have a length b < φω(0) (the first ω-critical number) and the induction is over ordinals less than or equal to b.

For proof-theoretic purposes it would be desirable to employ a method of proof which is more elementary than the axiom of bar induction and also to obtain a smaller ordinal bound. The purpose of the following is to provide such a method. We show that for a primitive recursive term H of finite type the tree generated by the relation of Sanchis and Diller has length less than ε0. Our method is similar to that used by Tait [Ta] in his theory of infinite terms. The immediately natural metamathematics is elementary intuitionistic analysis with the axiom of choice and transfinite induction over the relevant ordinal notations. We give several versions of the basic list of successor clauses, and for one version we show how to carry out the treatment in Skolem arithmetic (with primitive recursion of lowest type).

This note presents a practical algorithm for carrying out abstraction on combinatory terms. The well-known abstraction algorithms [1, pp. 188ff.] defining abstracts in terms of the combinator sets { S, K }, { B, C, K, W }, etc. operate on one variable at a time, and result in rather long abstracts when several variables are involved. These algorithms are not practical for the applications of the combinatory logic to the theory of computing which make much use of multi-variable abstraction (e.g., [2], [3]). The present algorithm performs the abstraction with respect to all specified variables in a single step, and yields abstracts in a concise form (with sizes proportional to those of given combinatory terms).

Let Q be the class of closed quantificational formulas ∀x∃u∀yM without identity such that M is a quantifier-free matrix containing only monadic and dyadic predicate letters and containing no atomic subformula of the form Pyx or Puy for any predicate letter P. In [DKW] Dreben, Kahr, and Wang conjectured that Q is a solvable class for satisfiability and indeed contains no formula having only infinite models. As evidence for this conjecture they noted the solvability of the subclass of Q consisting of those formulas whose atomic subformulas are of only the two forms Pxy, Pyu and the fact that each such formula that has a model has a finite model. Furthermore, it seemed likely that the techniques used to show this subclass solvable could be extended to show the solvability of the full class Q, while the syntax of Q is so restricted that it seemed impossible to express in formulas of Q any unsolvable problem known at that time.

In 1966 Aanderaa refuted this conjecture. He first constructed a very complex formula in Q having an infinite model but no finite model, and then, by an extremely intricate argument, showed that Q (in fact, the subclass Q2 defined below) is unsolvable ([Aa1], [Aa2]). In this paper we develop stronger tools in order to simplify and extend the results of [Aa2]. Specifically, we show the unsolvability of an apparently new combinatorial problem, which we shall call the linear sampling problem (defined in §1.2 and §2.3). From the unsolvability of this problem there follows the unsolvability of two proper subclasses of Q, which we now define. For each i ≥ 0, let Pi be a dyadic predicate letter and let Ri be a monadic predicate letter.

Using an idea developed in joint work with Shelah, we show how to redefine Laver's notion of forcing making a supercompact cardinal κ indestructible under κ-directed closed forcing to give a new proof of the Kimchi-Magidor Theorem in which every compact cardinal in the universe (supercompact or strongly compact) satisfies certain indestructibility properties. Specifically, we show that if K is the class of supercompact cardinals in the ground model, then it is possible to force and construct a generic extension in which the only strongly compact cardinals are the elements of K or their measurable limit points, every κ ∈ K is a supercompact cardinal indestructible under ∈-directed closed forcing, and every κ a measurable limit point of K is a strongly compact cardinal indestructible under κ-directed closed forcing not changing ℘(κ). We then derive as a corollary a model for the existence of a strongly compact cardinal κ which is not κ+ supercompact but which is indestructible under κ-directed closed forcing not changing ℘(κ) and remains non-κ+ supercompact after such a forcing has been done.

In this paper we shall consider some decision problems for ordinary differential equations. All differential equations will be algebraic differential equations, i.e. equations of the form P(x, y, y′, …, y(n)) = 0 (or P(x, y1, …, ym, y′1 …, y′m, …) = 0 in the case of several dependent variables), where P is a polynomial in all its variables with rational coefficients. (We call P a differential polynomial.)

Jáskowski [6] showed that there is no algorithm to determine if a system of algebraic differential equations (in several dependent variables) has a solution on [0, 1]. An easier proof of this using results on Hilbert's tenth problem is given in [2]. It is natural to restrict the problem in the hope of finding something which is decidable. Two ways to do this are the following: (a) One can ask only for the existence of solutions locally, say around x = 0. Here solution may mean (i) analytic functions, (ii) germs of C∞ functions, or (iii) formal power series, (b) One can consider only one equation in one dependent variable, but ask for the existence of a solution on an interval. In [4] we gave an algorithm for deciding (a)(ii) and (a)(iii) and showed that (a)(i) is undecidable. In §4 (Theorem 4.1) we shall show that (b) (for real analytic solutions) is undecidable. This partially answers Problem 9 of Rubel [13], which stimulated this investigation. We shall also prove (Theorem 4.2) that, given an analytic function f(x) which is the solution of an algebraic differential equation, determined by some initial conditions at x = 0, one cannot in general determine if the radius of convergence of f is < 1 or ≥ 1.

Ackermann introduced in [1] a system of axiomatic set theory. The quantifiers of this set theory range over a universe of objects which we call classes. Among the classes we distinguish the sets. Here we shall show that, in some sense, all the theorems of Ackermann's set theory can be proved in Zermelo-Fraenkel's set theory. We shall also show that, on the other hand, it is possible to prove in Ackermann's set theory very strong theorems of the Zermelo-Fraenkel set theory.

Using a combinatorial theorem of Herwig on extending partial isomorphisms of relational structures, we give a simple proof that certain classes of algebras, including Crs, polyadic Crs, and WA, have the ‘finite base property’ and have decidable universal theories, and that any finite algebra in each class is representable on a finite set.

We present a survey of proof theory in the USSR beginning with the paper by Kolmogorov [1925] and ending (mostly) in 1969; the last two sections deal with work done by A. A. Markov and N. A. Shanin in the early seventies, providing a kind of effective interpretation of negative arithmetic formulas. The material is arranged in chronological order and subdivided according to topics of investigation. The exposition is more detailed when the work is little known in the West or the original presentation can be improved using notions or results which appeared later. This includes such topics as Novikov's cut-elimination method (regular formulas) and Maslov's inverse method for the predicate logic.

We continue the study of simple theories begun in [3] and [5]. We first find the right analogue of definability of types. We then develop the theory of generic types and stabilizers for groups definable in simple theories. The general ideology is that the role of formulas (or definability) in stable theories is replaced by partial types (or ∞-definability) in simple theories.

The existence and uniqueness of a maximum point for a continuous real–valued function on a metric space are investigated constructively. In particular, it is shown, in the spirit of reverse mathematics, that a natural unique existence theorem is equivalent to the fan theorem.

Let M be a term of the type free λ-calculus and let be a set of occurrences of redexes in M. A reduction sequence from M which first contracts a member of and afterwards only residuals of is called a development (of M with respect to ). The finite developments theorem says that developments are always finite.

There are several proofs of this theorem in the literature. A plausible strategy is to define some kind of measure for pairs (M, ), which—if M′ results from M by contracting a redex occurrence in and ′ is the set of residuals of in M′— decreases in passing from (M, ) to (M′, ′). This procedure is followed as a matter of fact in the proofs in Hyland [4] and in Barendregt [1] (both are covered in Klop [5]). If, as in the latter proof, the natural numbers are used as measures, then the measure of (M, ) will actually denote an upper bound of the number of reduction steps in a development of M with respect to .

In the present proof we straightforwardly define for each pair (M, ) a natural number, which can easily be seen to indicate the exact number of reduction steps in a development of maximal length of M with respect to .