PA is Peano arithmetic. The formula $\operatorname{Interp}_\mathrm{PA}(\alpha, \beta)$ is a formalization of the assertion that the theory PA + α interprets the theory PA + β (the variables α and β are intended to range over codes of sentences of PA). We extend Solovay's modal analysis of the formalized provability predicate of PA, Pr PA (x), to the case of the formalized interpretability relation $\operatorname{Interp}_\mathrm{PA}(x, y)$ . The relevant modal logic, in addition to the usual provability operator `□', has a (...) binary operator ` $\triangleright$ ' to be interpreted as the formalized interpretability relation. We give an axiomatization and a decision procedure for the class of those modal formulas that express valid interpretability principles (for every assignment of the atomic modal formulas to sentences of PA). Our results continue to hold if we replace the base theory PA with Zermelo-Fraenkel set theory, but not with Gödel-Bernays set theory. This sensitivity to the base theory shows that the language is quite expressive. Our proof uses in an essential way earlier work done by A. Visser, D. de Jongh, and F. Veltman on this problem. (shrink)

We prove that the theory IΔ0, extended by a weak version of the Δ0-Pigeonhole Principle, proves that every integer is the sum of four squares (Lagrange's theorem). Since the required weak version is derivable from the theory IΔ0 + ∀x (xlog(x) exists), our results give a positive answer to a question of Macintyre (1986). In the rest of the paper we consider the number-theoretical consequences of a new combinatorial principle, the ‘Δ0-Equipartition Principle’ (Δ0EQ). In particular we give a new proof, (...) which can be formalized in IΔ0 + Δ0EQ, of the fact that every prime of the form 4n + 1 is the sum of two squares. (shrink)

We prove that if G is a group definable in a saturated o-minimal structure, then G has no infinite descending chain of type-definable subgroups of bounded index. Equivalently, G has a smallest type-definable subgroup G00 of bounded index and G/G00 equipped with the “logic topology” is a compact Lie group. These results give partial answers to some conjectures of the fourth author.

Let PLω be the provability logic of IΔ0 + ω1. We prove some containments of the form L ⊆ PLω < Th(C) where L is the provability logic of PA and Th(C) is a suitable class of Kripke frames.

We develop an intersection theory for definable Cp-manifolds in an o-minimal expansion of a real closed field and we prove the invariance of the intersection numbers under definable Cp-homotopies . In particular we define the intersection number of two definable submanifolds of complementary dimensions, the Brouwer degree and the winding numbers. We illustrate the theory by deriving in the o-minimal context the Brouwer fixed point theorem, the Jordan-Brouwer separation theorem and the invariance of the Lefschetz numbers under definable Cp-homotopies. A. (...) Pillay has shown that any definable group admits an abstract manifold structure. We apply the intersection theory to definable groups after proving an embedding theorem for abstract definably compact Cp-manifolds. In particular using the Lefschetz fixed point theorem we show that the Lefschetz number of the identity map on a definably compact group, which in the classical case coincides with the Euler characteristic, is zero. (shrink)

Models of normal open induction are those normal discretely ordered rings whose nonnegative part satisfy Peano's axioms for open formulas in the language of ordered semirings. (Where normal means integrally closed in its fraction field.) In 1964 Shepherdson gave a recursive nonstandard model of open induction. His model is not normal and does not have any infinite prime elements. In this paper we present a recursive nonstandard model of normal open induction with an unbounded set of infinite prime elements.

Let M be an o-minimal expansion of an ordered field. Let φ be a formula in the language of ordered domains. In this note we establish some topological properties which are transferred from $\varphi^M$ to $\varphi^R$ and vice versa. Then, we apply these transfer results to give a new proof of a result of M. Edmundo-based on the work of A. Strzebonski-showing the existence of torsion points in any definably compact group defined in an o-minimal expansion of an ordered field.

By recent work on some conjectures of Pillay, each definably compact group G in a saturated o-minimal expansion of an ordered field has a normal "infinitesimal subgroup" G00 such that the quotient G/G00, equipped with the "logic topology", is a compact (real) Lie group. Our first result is that the functor G → G/G00 sends exact sequences of definably compact groups into exact sequences of Lie groups. We then study the connections between the Lie group G/G00 and the o-minimal spectrum (...) G̃ of G. We prove that G/G00 is a topological quotient of G̃. We thus obtain a natural homomorphism ψ* from the cohomology of G/G00 to the (Čech-)cohomology of G̃. We show that if G00 satisfies a suitable contractibility conjecture then $\widetilde{G^{00}}$ is acyclic in Čech cohomology and ψ* is an isomorphism. Finally we prove the conjecture in some special cases. (shrink)

Wilkie 5 397) proved a “theorem of the complement” which implies that in order to establish the o-minimality of an expansion of with C∞ functions it suffices to obtain uniform bounds on the number of connected components of quantifier free definable sets. He deduced that any expansion of with a family of Pfaffian functions is o-minimal. We prove an effective version of Wilkie's theorem of the complement, so in particular given an expansion of the ordered field with finitely many C∞ (...) functions, if there are uniform and computable upper bounds on the number of connected components of quantifier free definable sets, then there are uniform and computable bounds for all definable sets. In such a case the theory of the structure is effectively o-minimal: there is a recursively axiomatized subtheory such that each of its models is o-minimal. This implies the effective o-minimality of any expansion of with Pfaffian functions. We apply our results to the open problem of the decidability of the theory of the real field with the exponential function. We show that the decidability is implied by a positive answer to the following problem ): given a language L expanding the language of ordered rings, if an L-sentence is true in every L-structure expanding the ordered field of real numbers, then it is true in every o-minimal L-structure expanding any real closed field. (shrink)

We prove that if G is a Δ 0 -definable function on the natural numbers and F = Π i = 0 n G , then F is also Δ 0 -definable. Moreover, the inductive properties of F can be proved inside the theory IΔ 0.

By recent work on some conjectures of Pillay, each definably compact group in a saturated o-minimal structure is an extension of a compact Lie group by a torsion free normal divisible subgroup, called its infinitesimal subgroup. We show that the infinitesimal subgroup is cohomologically acyclic. This implies that the functorial correspondence between definably compact groups and Lie groups preserves the cohomology.

Skolem studied the germs at infinity of the smallest class of real valued functions on the positive real line containing the constant $1$, the identity function ${\mathbf {x}}$, and such that whenever f and g are in the set, $f+g,fg$ and $f^g$ are in the set. This set of germs is well ordered and Skolem conjectured that its order type is epsilon-zero. Van den Dries and Levitz computed the order type of the fragment below $2^{2^{\mathbf {x}}}$. Here we prove that (...) the set of asymptotic classes within any Archimedean class of Skolem functions has order type $\omega $. As a consequence we obtain, for each positive integer n, an upper bound for the fragment below $2^{n^{\mathbf {x}}}$. We deduce an epsilon-zero upper bound for the fragment below $2^{{\mathbf {x}}^{\mathbf {x}}}$, improving the previous epsilon-omega bound by Levitz. A novel feature of our approach is the use of Conway’s surreal number for asymptotic calculations. (shrink)

Skolem studied the germs at infinity of the smallest class of real valued functions on the positive real line containing the constant $1$, the identity function ${\mathbf {x}}$, and such that whenever f and g are in the set, $f+g,fg$ and $f^g$ are in the set. This set of germs is well ordered and Skolem conjectured that its order type is epsilon-zero. Van den Dries and Levitz computed the order type of the fragment below $2^{2^{\mathbf {x}}}$. Here we prove that (...) the set of asymptotic classes within any Archimedean class of Skolem functions has order type $\omega $. As a consequence we obtain, for each positive integer n, an upper bound for the fragment below $2^{n^{\mathbf {x}}}$. We deduce an epsilon-zero upper bound for the fragment below $2^{{\mathbf {x}}^{\mathbf {x}}}$, improving the previous epsilon-omega bound by Levitz. A novel feature of our approach is the use of Conway’s surreal number for asymptotic calculations. (shrink)

The topology of definable sets in an o-minimal expansion of a group is not fully understood due to the lack of a triangulation theorem. Despite the general validity of the cell decomposition theorem, we do not know whether any definably compact set is a definable CW-complex. Moreover the closure of an o-minimal cell can have arbitrarily high Betti numbers. Nevertheless we prove that the cohomology groups of a definably compact set over an o-minimal expansion of a group are finitely generated (...) and invariant under elementary extensions and expansions of the language. (shrink)