We revisit the foundations of positive model theory, introducing h-inductive sentences. These allow a considerably simplified presentation of positive model theory, as well as a characterisation of Hausdorffcats by an amalgamation property of their h-inductive theory.

By induction for a formula φ we mean the schema

(where the terms in brackets are implicitly substituted for some fixed variable, with the usual restrictions). Let be the schema IAφ for φ in Πn (i.e. ); similarly for . Each instance of is Δn+2, and each instance of is Σn+1 Thus the universal closure of an instance α is Πn+2 in either case. Charles Parsons [72] proved that and are equivalent over Z0, where Z0 is essentially Primitive Recursive Arithmetic augmented by classical First Order Logic [Parsons 70].

Theorem. For each n > 0 there is a Πn formula π for whichis not derivable in Z0from

(i) true Πn+1sentences; nor even

(ii) Πn+1sentences consistent withZ0.

A structure is recursive if the set of quantifier-free sentences in the complete diagram ⊿() of is recursive. It has been known for some time that every decidable theory has a recursive model. In fact, every decidable theory has a decidable model (that is a model such that ⊿() is recursive). In this paper we find other conditions which imply that a theory have a recursive model.

In §1 we study the relation between an ℵ0-categorical theory T having a recursive model and the complexity of the quantificational hierarchy of that theory. We let ∃0 denote the set of quantifier-free sentences, and let ∃n÷1 denote the set of sentences beginning with an existential quantifier and having n alternations of quantifiers. (∀n is defined analogously.) Then we show that if T is an arithmetical ℵ0-categorical theory such that T ⋂ ∃n÷2 is Σn÷10 for each n < ω, then T has a recursive model. We show that this is a best possible result by giving an example of a ⊿n÷20 ℵ0-categorical theory T such that T ⋂ ∃n÷1 is recursive yet T has no recursive model.

In §2 we consider the theory of trees. Ershov [1] had proved that every Σ10 theory of trees has a recursive model. We show this to be best possible by giving an example of a ⊿20 theory of trees which has no recursive model.

A set S of natural numbers is called recursively enumerable if there is a general recursive function F(x, y) such that

In other words, S is the projection of a two-dimensional general recursive set. Actually, it is no restriction on S to assume that F(x, y) is primitive recursive. If S is not empty, it is the range of the primitive recursive function

where a is a fixed element of S. Using pairing functions, we see that any non-empty recursively enumerable set is also the range of a primitive recursive function of one variable.

We use throughout the logical symbols ⋀ (and), ⋁ (or), → (if…then…), ↔ (if and only if), ∧ (for every), and ∨(there exists); negation does not occur explicitly. The variables range over the natural numbers, except as otherwise noted.

Martin Davis has shown that every recursively enumerable set S of natural numbers can be represented in the form

where P(y, b, w, x1 …, xλ) is a polynomial with integer coefficients. (Notice that this would not be correct if we replaced ≤ by <, since the right side of the equivalence would always be satisfied by b = 0.) Conversely, every set S represented by a formula of the above form is recursively enumerable. A basic unsolved problem is whether S can be defined using only existential quantifiers.

In this paper I shall show that no one of the four primitive symbols of Heyting's calculus of propositions is definable in terms of the other three. So as to make the paper self-contained, I begin by stating the rules and primitive sentences given by Heyting.

The primitive symbols of the calculus are “⅂”, “∨”, “∧”, and “⊃”, which may be read, respectively, as “not,” “either…or,” “and,” and “if…then.” The symbol “⊃⊂”, which may be read “if and only if,” is defined in terms of these as follows:

The rule of substitution is assumed, and the rule that S2 follows from S1 and S1⊃S2; in addition it is assumed that S1∧S2 follows from S1 and S2. The primitive sentences are as follows:

We study the strictness of the modal μ-calculus hierarchy over some restricted classes of transition systems. First, we prove that over transitive systems the hierarchy collapses to the alternation-free fragment. In order to do this the finite model theorem for transitive transition systems is proved. Further, we verify that if symmetry is added to transitivity the hierarchy collapses to the purely modal fragment. Finally, we show that the hierarchy is strict over reflexive frames. By proving the finite model theorem for reflexive systems the same results holds for finite models.

We show that for every computable limit ordinal α, there is a computable structure that is categorical, but not relatively categorical (equivalently, it does not have a formally Scott family). We also show that for every computable limit ordinal α, there is a computable structure with an additional relation R that is intrinsically on , but not relatively intrinsically on (equivalently, it is not definable by a computable Σα formula with finitely many parameters). Earlier results in [7], [10], and [8] establish the same facts for computable successor ordinals α.

The Rainbow Ramsey Theorem is essentially an “anti-Ramsey” theorem which states that certain types of colorings must be injective on a large subset (rather than constant on a large subset). Surprisingly, this version follows easily from Ramsey's Theorem, even in the weak system RCA0 of reverse mathematics. We answer the question of the converse implication for pairs, showing that the Rainbow Ramsey Theorem for pairs is in fact strictly weaker than Ramsey's Theorem for pairs over RCA0. The separation involves techniques from the theory of randomness by showing that every 2-random bounds an ω-model of the Rainbow Ramsey Theorem for pairs. These results also provide as a corollary a new proof of Martin's theorem that the hyperimmune degrees have measure one.

Contents: Introduction. §1: Computable rings and modules. §2: Ideal membership relation. §3: Effective structured domains. §4: Completion of a local ring as a domain. §5: The recursive completion. Epilogue. References.

Introduction. Completion is an important general mathematical device. Often, but not always, a completion takes the following form. Let A be a topological algebraic structure whose topology is derived from a metric. For A, a topological algebra  and an embedding i: A →  are constructed such that  is a complete metric space in which A is densely embedded by i. The long list of structures for which such completions exist begins with Cantor's construction of the real number field and includes objects like the p-adic integers, Baire space, and Boolean algebras. In Bourbaki [6] a careful and thorough account of completions for arbitrary topological groups and fields is given, for which it is important to note that the topological structures need not be metrizable, but must possess a uniformity.

The effectiveness of the completion process of a computable structure A cannot be readily studied using the tools of computable algebra, simply because the resulting structure  is almost invariably uncountable. However, in particular cases, it has been possible to define and study the substructure Ak of computable elements of Â; this has been done for the structures mentioned above, starting with the field of recursive real numbers.

In this paper we analyse the effectivity of the completion of a local ring R. We do this using structured Scott-Ershov domains. Our study may be considered as a prototype containing methods applicable to a broad class of completions, including all the examples mentioned above, except for the real number field, which needs a generalisation of the domain concept.

A Scott-Ershov domain D formalises how a set Dt of possibly “infinite” elements, called total elements, is constructed from a set Dc of “finite” elements, called compact elements. This is achieved by means of an approximation ordering which determines a topology on D and, in particular, on Dt . Our methodology is to associate to a given topological algebra A a structured domain D(A) such that the total elements D(A)t form a topological algebra topologically isomorphic to A. In such circumstances A is said to be domain definable by D(A). The theory of computability for domains is now applied to study the effectivity of the topological algebra A.

In this paper a theorem about numerical relations will be established and shown to have certain consequences concerning decidability in quantification theory, as well as concerning the foundation of number theory. The theorem is that relations of natural numbers are reducible in elementary fashion to symmetric ones; i.e.:

Theorem I. For every dyadic relation R of natural numbers there is a symmetric dyadic relation H of natural numbers such that R is definable in terms of H plus just truth-functions and quantification over natural numbers.

To state the matter more fully, there is a (well-formed) formula ϕ of pure quantification theory, or first-order functional calculus, which meets these conditions:

(a) ϕ has ‘x’ and ‘y’ as sole free individual variables;

(b) ϕ contains just one predicate letter, and it is dyadic;

(c) for every dyadic relation R of natural numbers there is a symmetric dyadic relation H of natural numbers such that, when the predicate letter in ϕ is interpreted as expressing H, ϕ comes to agree in truth-value with ‘x bears R to y’ for all values of ‘x’ and ‘y’.

Fried and Kollár constructed a fully faithful functor from the category of graphs to the category of fields. We give a new construction of such a functor and use it to resolve a longstanding open problem in computable model theory, by showing that for every nontrivial countable structure ${\cal S}$, there exists a countable field ${\cal F}$ of arbitrary characteristic with the same essential computable-model-theoretic properties as ${\cal S}$. Along the way, we develop a new “computable category theory”, and prove that our functor and its partially defined inverse (restricted to the categories of countable graphs and countable fields) are computable functors.

In this paper I am going to set forth a formal system based on five inter-class relations. These relations exist respectively between a class of a's and a class of b's.

(i) if and only if every a is a b and every b is an a,

(ii) if and only if every a is a b and not every b is an a,

(iii) if and only if it is not the case that either every a is a b or every b is an a or no a is a b,

(iv) if and only if every b is an a and not every a is a b,

(v) if and only if no a is a b.

These relations between classes, which correspond, as will be seen, to the five relations between two circles a and b shown in the well-known Eulerian diagrams,

are of course connected in an intimate way with the four forms of proposition, A, E, I, O, of the traditional syllogistic logic. The French mathematician, J. D. Gergonne, seems to have been the first to recognize these relations explicitly and to understand their importance in syllogistic theory. It is therefore appropriate that they should be called by his name.

Gergonne first of all showed with reference to these relations what are the sufficient and necessary conditions of the truth of propositions of each of the four traditional forms: for example, an A proposition, ‘All a is b’ is true if and only if either the first or the second relation exists between the class of a's and the class of b's.

We give examples of calculi that extend Gentzen’s sequent calculus LK by unsound quantifier inferences in such a way that (i) derivations lead only to true sequents, and (ii) proofs therein are nonelementarily shorter than LK-proofs.

In part I of this paper it is shown that if the simple theory of types (with an axiom of infinity) is consistent, then so is the system obtained by adjoining axioms of extensionality; in part II a similar metatheorem for Gödel-Bernays set theory will be proved. The first of these results is of particular interest because type theory without the axioms of extensionality is fundamentally rather a simple system, and it should, I believe, be possible to prove that it is consistent.

Let us consider — in some unspecified formal system — a typical expression of the axiom of extensionality; for example:

where A(h) is a formula, and A(f), A(g) are the results of substituting in it the predicate variagles f, g for the free variable h. Evidently, if the system considered contains the predicate calculus, and if h occurs in A(h) only in parts of the form h(t) where t is a term which lies within the range of the quantifier (x), then 1.1 will be provable. But this will not be so in general; indeed, by introducing into the system an intensional predicate of predicates we can make 1.1 false. For example, Myhill introduces a constant S, where ‘Sϕψχω’ means that (the expression) ϕ is the result of substituting ψ for χ in ω.

The current paper proves the results announced in [5].

We isolate a new large cardinal concept, “remarkability.” Consistencywise, remarkable cardinals are between ineffable and ω-Erdös cardinals. They are characterized by the existence of “0#-like” embeddings; however, they relativize down to L. It turns out that the existence of a remarkable cardinal is equiconsistent with L(ℝ) absoluteness for proper forcings. In particular, said absoluteness does not imply determinacy.

The material presented here belongs to the model theory of the Lκ, λ languages. Our results are either infinitary analogs of important theorems in finitary model theory, or else show that such analogs do not exist.

For example, it is well known that whenever i, and , have the same true Lω, ω sentences (i.e., are elementarily equivalent) for i = 1, 2, then the cardinal sums 1 + 2 and + have the same true Lω, ω sentences, and the direct products 1 · 2 and · have the same true Lω, ω sentences [3]. We show that this is true when ‘Lω, ω’ is replaced by ‘Lκ, λ’ if and only if κ is strongly inaccessible. For Lω1, ω this settles a question, posed by Lopez-Escobar [7].

In §3 we give a complete description of the expressive power of those sentences of Lκ, λ in which the identity symbol is the only relation symbol which occurs. This extends a result by Hanf [4].

We present a variety of (ω, ∞)-distributive forcings which when applied to models of Martin's Maximum separate certain well known reflection principles. In particular, we do this for the reflection principles SR, SRα (α ≤ ω1), and SRP.

Let ‘ϕ’, ‘χ’, and ‘ψ’ be variables ranging over functions from the sentence letters P0, P1, … Pn, … of (propositional) modal logic to sentences of P(eano) Arithmetic), and for each sentence A of modal logic, inductively define Aϕ by

[and similarly for other nonmodal propositional connectives]; and

where Bew(x) is the standard provability predicate for PA and ⌈F⌉ is the PA numeral for the Gödel number of the formula F of PA. Then for any ϕ, (−□⊥)ϕ = −Bew(⌈⊥⌉), which is the consistency assertion for PA; a sentence S is undecidable in PA iff both and , where ϕ(p0) = S. If ψ(p0) is the undecidable sentence constructed by Gödel, then ⊬PA (−□⊥→ −□p0 & − □ − p0)ψ and ⊢PA(P0 ↔ −□⊥)ψ. However, if ψ(p0) is the undecidable sentence constructed by Rosser, then the situation is the other way around: ⊬PA(P0 ↔ −□⊥)ψ and ⊢PA (−□⊥→ −□−p0 & −□−p0)ψ. We call a sentence S of PA extremely undecidable if for all modal sentences A containing no sentence letter other than p0, if for some ψ, ⊬PAAψ, then ⊬PAAϕ, where ϕ(p0) = S. (So, roughly speaking, a sentence is extremely undecidable if it can be proved to have only those modal-logically characterizable properties that every sentence can be proved to have.) Thus extremely undecidable sentences are undecidable, but neither the Godel nor the Rosser sentence is extremely undecidable. It will follow at once from the main theorem of this paper that there are infinitely many inequivalent extremely undecidable sentences.

Let K be an algebraically closed field of any characteristic, complete with respect to the non-trivial ultrametric absolute value ∣·∣: K → ℝ+. By R denote the valuation ring of K, and by ℘ its maximal ideal. We work within the class of subanalytic sets defined in [5], but our results here also hold for the strongly subanalytic sets introduced in [11] as well as for those subanalytic sets considered in [6]. Let X ⊂ R1 be subanalytic. In [8], we showed that there is a decomposition of X as a union of a finite number of special sets U ⊂ R1 (see below). In this note, in Theorem 1.6, we obtain a version of this result which is uniform in parameters, thereby answering a question brought to our attention by Angus Macintyre. It follows immediately from Theorem 1.6 that the theory of K in the language (see [5] and [6]) is C-minimal in the sense of [3] and [9]. The analogous uniformity result in the p-adic case was recently proved in [12].

Definition 1.1. (i) A disc in R1 is a set of one of the two following forms:

A special set in R1 is a disc minus a finite union of discs.

(ii) R-domains u ⊂ Rm, and their associated rings of analytic functions, , are defined inductively as follows. Rm is an R-domain and , the ring of strictly convergent power series in X1,…, Xm over K. If u is an R-domain with associated ring , (where K 〈X, Y〉 〚ρ〛S is a ring of separated power series, see [5, §2] and [1, §1]) and f, have no common zero on u and ◸ ϵ {<, ≤}, then

is an R-domain and

where J is the ideal generated by I and f − gZ (Z is a new variable) if ◸ is ≤, and

where J is the ideal generated by I and f − gτ (τ a new variable) if ◸ is <. (See [8, Definition 2.2].) R-domains generalize the rational domains of [2, §7.2.3]. It is true, but not easy to prove, that only depends on u as a point set, and is independent of the particular representation of u.

As is well-known, the Bernays-Schönfinkel-Ramsey class of all prenex ∃*∀*-sentences which are valid in classical first-order logic is decidable. This paper paves the way to an analogous result which the authors deem to hold when the only available predicate symbols are ∈ and =, no constants or function symbols are present, and one moves inside a (rather generic) Set Theory whose axioms yield the well-foundedness of membership and the existence of infinite sets. Here semi-decidability of the satisfiability problem for the BSR class is proved by following a purely semantic approach, the remaining part of the decidability result being postponed to a forthcoming paper.