This note shows that the inconsistency proof of the system of illative combinatory logic given in [1] can be simplified as well as extended to the absolute inconsistency of a more general system.

One extension of the result in [1] lies in the fact that the following weakened form of the deduction theorem for implication will lead to the inconsistency:

Also the inconsistency follows almost as easily for

as it does for ⊢ H2X for arbitrary X, so we will consider the more general case.

The only properties we require other than (DT), (1) and Rule Eq for equality are modus ponens,

and

Let G = [x] Hn−1x⊃: . … H2x⊃ :Hx⊃ . x ⊃ A, where A is arbitrary. Then if Y is the paradoxical combinator and X = YG, X = GX.

Now X ⊂ X, i.e.,

In this paper we will do some model theory with respect to the models, defined in [7] and, as in [7], we will work again in intuitionistic metamathematics.

In this paper we will only consider models M = ‹S, TM›, where S is one fixed spreadlaw for all models M, namely the universal spreadlaw. That we can restrict ourselves to this class of models is a consequence of the completeness proof, which is sketched in [7, §3].

The main tools in this paper will be two model-constructions:

(i) In §1 we will consider, under a certain condition C(M0, M, s), the construction of a model R(M0, M, s) from two models M0 and M with respect to the finite sequence s.

(ii) In §2 we will construct from an infinite sequence M0, M1, M2, … of models a new model Σi∈INMi.

Syntactic proofs of the disjunction property and the explicit definability theorem are well known.

C. Smorynski [8] gave semantic proofs of these theorems with respect to Kripke models, however using classical metamathematics. In §1 we will give intuitionistically correct, semantic proofs with respect to the models, defined in [7] using Brouwer's continuity principle.

Let W be the fan of all models (see [7, Theorem 2.7]) and let Γ be a countably infinite sequence of sentences.

Early work combining recursion theory and algebra had (at least) two different sets of motivations. First the precise setting of recursion theory offered a chance to make formal classical concerns as to the effective or algorithmic nature of algebraic constructions. As an added benefit the formalization gives one the opportunity of proving that certain constructions cannot be done effectively even when the original data is presented in a recursive way. One important example of this sort of approach is the work of Frohlich and Shepardson [1955] in field theory. Another motivation for the introduction of recursion theory to algebra is given by Rabin [1960]. One hopes to mathematically enrich algebra by the additional structure provided by the notion of computability much as topological structure enriches group theory. Another example of this sort is provided in Dekker [1969] and [1971] where the added structure is that of recursive equivalence types. (This particular structural view culminates in the monograph of Crossley and Nerode [1974].)

More recently there is the work of Metakides and Nerode [1975], [1977] which combines both approaches. Thus, for example, working with vector spaces they show in a very strong way that one cannot always effectively extend a given (even recursive) independent set to a basis for a (recursive) vector space.

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 λ-theory T is a consistent set of equations between λ-terms closed under derivability. The degree of T is the degree of the set of Gödel numbers of its elements. is the λ-theory axiomatized by the set {M = N∣ M, N unsolvable}. A λ-theory is sensible iff T ⊃ ; for a motivation see [6] and [4].

In §1 it is proved that the theory is Σ20-complete. We present Wadsworth's proof that its unique maximal consistent extension * (= Th(D∞)) is Π20-complete. In §2 it is proved that η (= λη-calculus + ) is not closed under the ω-rule (see [1]). In §3 arguments are given to conjecture that is Π11-complete. This is done by representing recursive sets of sequence numbers as λ-terms and by connecting wellfoundedness of trees with provability in ω. In §4 an infinite set of equations independent over η will be constructed. From this it follows that there are 2ℵ0 sensible theories T such that and 2ℵ0 sensible hard models of arbitrarily high degrees. In §5 some nonprovability results needed in §§1 and 2 are established. For this purpose one uses the theory η extended with a reduction relation for which the Church–Rosser theorem holds. The concept of Gross reduction is used in order to show that certain terms have no common reduct.

In [1] there were given postulates for an abstract “projective algebra” which, in the words of the authors, represented a “modest beginning for a study of logic with quantifiers from a boolean point of view”. In [5], D. Monk observed that the study initiated in [1] was an initial step in the development of algebraic versions of logic from which have evolved the cylindric and polyadic algebras.

Several years prior to the publication of [1], J. C. C. McKinsey [3] presented a set of postulates for the calculus of relations. Following the publication of [1], McKinsey [4] showed that every projective algebra is isomorphic to a subalgebra of a complete atomic projective algebra and thus, in view of the representation given in [1], every projective algebra is isomorphic to a projective algebra of subsets of a direct product, that is, to an algebra of relations.

Of course there has since followed an extensive development of projective algebra resulting in the multidimensional cylindric algebras [2]. However, what appears to have been overlooked is the correspondence between the Everett–Ulam axiomatization and that of McKinsey.

It is the purpose of this paper to demonstrate the above, that is, we show that given a calculus of relations as defined by McKinsey it is possible to introduce projections and a partial product so that this algebra is a projective algebra and conversely, for a certain class of projective algebras it is possible to define a multiplication so that the resulting algebra is McKinsey's calculus of relations.

In this paper, we give consistency proofs for the existence of a κ-saturated ideal on an inaccessible κ, and for the existence of an ω2-saturated ideal on ω1. We also include an historical survey outlining other known results on saturated ideals.

§1. Forcing. We assume that the reader is familiar with the usual techniques in forcing and Boolean-valued models (see Jech [3] or Rosser [11]), so we shall just specify here some of the less standard notation.

“cBa” abbreviates “complete Boolean algebra”.

If P (= ‹P, <›) is a notion of forcing, is the associated cBa. We write VP for .

Notions like κ-closed, κ-complete, etc. always mean < κ. Thus, P is κ-closed iff every decreasing chain of length less than κ has a lower bound, and a Boolean algebra is κ-complete iff sups of subsets of of cardinality less than κ always exist.

If is a cBa, x̌ is the object in representing x in V. In many cases, especially with ordinals, the ̌ is dropped. V̌ is the Boolean-valued class representing V — i.e.,

Let Γ be a class of subsets of Baire space (ωω) closed under inverse images by continuous functions. We say such a Γ is continuously closed. Let , the class dual to Γ, consist of the complements relative to ωω of members of Γ. If Γ is not selfdual, i.e., , then let . A continuously closed nonselfdual class Γ of subsets of ωΓ is said to have the first separation property [2] if

The set C is said to separate A and B. The class Γ is said to have the second separation property [3] if

We shall assume the axiom of determinateness and show that if Γ is a continuously closed class of subsets of ωω and then

(1) Γ has the first separation property iff does not have the second separation property, and

(2) either Γ or has the second separation property.

Of course, (1) and (2) taken together imply that Γ and cannot both have the first separation property.

In this paper, we show that the theory of ordered differential fields has a model completion. We also show that any real differential field, finitely generated over the rational numbers, is isomorphic to some field of real meromorphic functions. In the last section of this paper, we combine these two results and discuss the problem of deciding if a system of differential equations has real analytic solutions. The author wishes to thank G. Stengle for some stimulating and helpful conversations and for drawing our attention to fields of real meromorphic functions.

§ 1. Real and ordered fields. A real field is a field in which −1 is not a sum of squares. An ordered field is a field F together with a binary relation < which totally orders F and satisfies the two properties: (1) If 0 < x and 0 < y then 0 < xy. (2) If x < y then, for all z in F, x + z < y + z. An element x of an ordered field is positive if x > 0. One can see that the square of any element is positive and that the sum of positive elements is positive. Since −1 is not positive, an ordered field is a real field. Conversely, given a real field F, it is known that one can define an ordering (not necessarily uniquely) on F [2, p. 274]. An ordered field F is a real closed field if: (1) every positive element is a square, and (2) every polynomial of odd degree with coefficients in F has a root in F. For example, the real numbers form a real closed field. Every ordered field can be embedded in a real closed field. It is also known that, in a real closed field K, polynomials satisfy the intermediate value property, i.e. if f(x) ∈ K[x] and a, b ∈ K, a < b, and f(a)f(b) < 0 then there is a c in K such that f(c) = 0.

We say that a ring admits elimination of quantifiers, if in the language of rings, {0, 1, +, ·}, the complete theory of R admits elimination of quantifiers.

Theorem 1. Let D be a division ring. Then D admits elimination of quantifiers if and only if D is an algebraically closed or finite field.

A ring is prime if it satisfies the sentence: ∀x∀y∃z (x =0 ∨ y = 0∨ xzy ≠ 0).

Theorem 2. If R is a prime ring with an infinite center and R admits elimination of quantifiers, then R is an algebraically closed field.

Let be the class of finite fields. Let be the class of 2 × 2 matrix rings over a field with a prime number of elements. Let be the class of rings of the form GF(pn)⊕GF(pk) such that either n = k or g.c.d. (n, k) = 1. Let be the set of ordered pairs (f, Q) where Q is a finite set of primes and such that the characteristic of the ring f(q) is q. Finally, let be the class of rings of the form ⊕q ∈ Qf(q), for some (f, Q) in .

Theorem 3. Let R be a finite ring without nonzero trivial ideals. Then R admits elimination of quantifiers if and only if R belongs to.

Theorem 4. Let R be a ring with the descending chain condition of left ideals and without nonzero trivial ideals. Then R admits elimination of quantifiers if and only if R is an algebraically closed field or R belongs to.

In contrast to Theorems 2 and 4, we have

Theorem 5. If R is an atomless p-ring, then R is finite, commutative, has no nonzero trivial ideals and admits elimination of quantifiers, but is not prime and does not have the descending chain condition.

We also generalize Theorems 1, 2 and 4 to alternative rings.

Let θ(ν) be a formula in the first-order language of arithmetic and let

In this note we study the relationship between the schemas I′ and I+.

Our interest in I+ lies in the fact that it is ostensibly a more reasonable schema than I′. For, if we believe the hypothesis of I+(θ) then to verify θ(n) only requires at most 2log2(n) steps, whereas assuming the hypothesis of I′(θ) we require n steps to verify θ(n). In the physical world naturally occurring numbers n rarely exceed 10100. For such n applying 2log2(n) steps is quite feasible whereas applying n steps may well not be.

Of course this is very much an anthropomorphic argument so we would expect that it would be most likely to be valid when we restrict our attention to relatively simple formulas θ. We shall show that when restricted to open formulas I+ does not imply I′ but that this fails for the classes Σn, Πn, n ≥ 0.

We shall work in PA−, where PA− consists of Peano's Axioms less induction together with

∀u, w(u + w = w + u ∧ u · w = w · u),

∀u, w, t ((u + w) + t = u + (w + t) ∧ (u · w) · t = u · (w · t)),

∀u, w, t(u · (w + t) = u · w + u · t),

∀u, w(u ≤ w ↔ ∃t(u + t = w)),

∀u, w(u ≤ w ∨ w ≤ u),

∀u, w, t(u + w = u + t → w = t).

The reasons for working with PA− rather than Peano's Axioms less induction is that our additional axioms, whilst intuitively reasonable, will not necessarily follow from some of the weaker forms of I+ which we shall be considering. Of course PA− still contains those Peano Axioms which define + and

Notice that, trivially, PA− ⊦ I′(θ) → I+(θ) for any formula θ.

By [12] we know that transfinite induction up to ΘεΩN+10 is not provable in IDN, the theory of N-times iterated inductive definitions. In this paper we will show that conversely transfinite induction up to any ordinal less than ΘεΩN+10 is provable in IDNi, the intuitionistic version of IDN, and extend this result to theories for transfinitely iterated inductive definitions.

In [14] Schütte proves the wellordering of his notational systems using predicates is wellordered) with Mκ ≔ {x ∈ and 0 ≤ κ ≤ N. Obviously the predicates are definable in IDNi with the defining axioms:

where Prog [Mκ, X] means that X is progressive with respect to Mκ, i.e.

The crucial point in Schütte's wellordering proof is Lemma 19 [14, p. 130] which can be modified to

where TI[Mκ + 1, a] is the scheme of transfinite induction over Mκ + 1 up to a.

This paper continues the study of existentially complete nilpotent groups initiated in [6]. Following [6], we let Kn denote the theory of groups nilpotent of class ≤ n and let Kn+ denote the theory of torsion-free groups nilpotent of class ≤ n. The principal results of [6] were that for n ≥ 2, neither Kn nor Kn+ has a model companion, and the classes E, F, and G of existentially complete, finitely generic and infinitely generic models of Kn are all distinct. The question of the relationships between these classes in the context of Kn was left open, however, and the proof of their distinctness for Kn+ obviously did not carry over to Kn+, because it made strong use of torsion elements.

In this paper we establish the relationships between E, F, and G for K2+. We show that all three classes are distinct. We also show that there is only one countable finitely generic model, and only one countable infinitely generic model, and that all the countable existentially complete models can be arranged in a sequence N1 ⊆ N2 ⊆ N3 ⊆ … ⊆ Nω, where Z(Nn) is the direct sum of n copies of Q. Another result is that the finite and infinite forcing companions of K2+ differ by an ∀∃∀ sentence. Finally, we show that there exist finitely generic models of K2+ in all infinite cardinalities.

Let A be a subset of ω, the set of natural numbers. The degree of A is its degree of recursive unsolvability. We say that A is rich if every degree above that of A is represented by a subset of A. We say that A is poor if no degree strictly above that of A is represented by a subset of A. The existence of infinite poor (and hence nonrich) sets was proved by Soare [9].

Theorem 1. Suppose that A is infinite and not rich. Then every hyperarith-metical subset H of ω is recursive in A.

In the special case when H is arithmetical, Theorem 1 was proved by Jockusch [4] who employed a degree-theoretic analysis of Ramsey's theorem [3]. In our proof of Theorem 1 we employ a similar, degree-theoretic analysis of a certain generalization of Ramsey's theorem. The generalization of Ramsey's theorem is due to Nash-Williams [6]. If A ⊆ ω we write [A]ω for the set of all infinite subsets of A. If P ⊆ [ω]ω we let H(P) be the set of all infinite sets A such that either [A]ω ⊆ P = ∅. Nash-Williams' theorem is essentially the statement that if P ⊆ [ω]ω is clopen (in the usual, Baire topology on [ω]ω) then H(P) is nonempty. Subsequent, further generalizations of Ramsey's theorem were proved by Galvin and Prikry [1], Silver [8], Mathias [5], and analyzed degree-theoretically by Solovay [10]; those results are not needed for this paper.