Complexity of deciding the first-order theory of real closed fields

1991 ◽  
Vol 55 (2) ◽  
pp. 1553-1587
Author(s):  
D. Yu. Grigor'ev
1977 ◽  
Vol 42 (2) ◽  
pp. 297-305 ◽  
Author(s):  
Jan Mycielski

We consider first-order logic only. A theory S will be called locally interpretable in a theory T if every theorem of S is interpretable in T. If S is locally interpretable in T and T is consistent then S is consistent. Most known relative consistency proofs can be viewed as local interpretations. The classic examples are the cartesian interpretation of the elementary theorems of Euclidean n-dimensional geometry into the first-order theory of real closed fields, the interpretation of the arithmetic of integers (rational numbers) into the arithmetic of positive integers, the interpretation of ZF + (V = L) into ZF, the interpretation of analysis into ZFC, relative consistency proofs by forcing, etc. Those interpretations are global. Under fairly general conditions local interpretability implies global interpretability; see Remarks (7), (8), and (9) below.We define the type (interpretability type) of a theory S to be the class of all theories T such that S is locally interpretable in T and vice versa. There happen to be such types and they are partially ordered by the relation of local interpretability. This partial ordering is of lattice type and has the following form:The lattice is distributive and complete and satisfies the infinite distributivity law of Brouwerian lattices:We do not know if the dual lawis true. We will show that the lattice is algebraic and that its compact elements form a sublattice and are precisely the types of finitely axiomatizable theories, and several other facts.


1972 ◽  
Vol 37 (3) ◽  
pp. 546-556 ◽  
Author(s):  
G. L. Cherlin

If Σ is the class of all fields and Σ* is the class of all algebraically closed fields, then it is well known that Σ* is characterized by the following properties:(i) Σ* is the class of models of some first order theory K*.(ii) If m1m2 are in Σ* and m1 ⊆ m2 then m1 ≺ m2 (m1 is an elementary substructure of m2, i.e. any first order sentence true in m1 is true in m2).(iii) If m1 is in Σ then there is a structure m2 in Σ* such that m1 ⊆ m2.If Σ is some other class of models of a first order theory K and a subclass Σ* of Σ exists satisfying (i)–(iii) then Σ* is uniquely determined and K* (which is unique up to logical equivalence) is called the model-companion of K. This notion is a generalization of the fundamental notion of model-completion introduced and extensively studied by A. Robinson [6], When the model-companion exists it provides the basis for a satisfactory treatment of the notion of an algebraically closed model of K.Recently A. Robinson has developed a more general formulation of the notion of “algebraically closed” structures in Σ, which is applicable to any inductive elementary class Σ of structures (by elementary we always mean ECΔ). Condition (i) must be weakened to(i′) Σ* is closed under elementary substructure (i.e. if m1 is in Σ* and m2 ≺ m1 then m2 is in Σ*).


2002 ◽  
Vol 67 (3) ◽  
pp. 957-996 ◽  
Author(s):  
Zoé Chatzidakis

The study of pseudo-algebraically closed fields (henceforth called PAC) started with the work of J. Ax on finite and pseudo-finite fields [1]. He showed that the infinite models of the theory of finite fields are exactly the perfect PAC fields with absolute Galois group isomorphic to , and gave elementary invariants for their first order theory, thereby proving the decidability of the theory of finite fields. Ax's results were then extended to a larger class of PAC fields by M. Jarden and U. Kiehne [21], and Jarden [19]. The final word on theories of PAC fields was given by G. Cherlin, L. van den Dries and A. Macintyre [10], see also results by Ju. Ershov [13], [14]. Let K be a PAC field. Then the elementary theory of K is entirely determined by the following data:• The isomorphism type of the field of absolute numbers of K (the subfield of K of elements algebraic over the prime field).• The degree of imperfection of K.• The first-order theory, in a suitable ω-sorted language, of the inverse system of Galois groups al(L/K) where L runs over all finite Galois extensions of K.They also showed that the theory of PAC fields is undecidable, by showing that any graph can be encoded in the absolute Galois group of some PAC field. It turns out that the absolute Galois group controls much of the behaviour of the PAC fields. I will give below some examples illustrating this phenomenon.


2003 ◽  
Vol 03 (02) ◽  
pp. 217-238 ◽  
Author(s):  
B. ZILBER

We study structures on the fields of characteristic zero obtained by introducing (multi-valued) operations of raising to power. Using Hrushovski–Fraisse construction we single out among the structures exponentially-algebraically closed once and prove, under certain Diophantine conjecture, that the first order theory of such structures is model complete and every its completion is superstable.


1979 ◽  
Vol 44 (4) ◽  
pp. 643-652
Author(s):  
Werner Stegbauer

The notion of a model companion for a first-order theory T was introduced and discussed in [1] and [2] as a generalization of the concept of a model completion of a theory. Both concepts reflect, on a general model theoretic level, properties of the theory of algebraically closed fields. The literature provides many examples of first-order theories with and without model companions—see [3] for a survey of these results. In this paper, we give a further generalization of the notion of a model companion.Roughly speaking, we allow instead of embeddings more general classes of maps (e.g. homomorphisms) and we allow any set of formulas which is preserved by these maps instead of existential formulas. This plan is worked out in detail in [5], where we discuss also several examples. One of these examples is given in this paper.In order to clarify the model theoretic background, we now introduce the relevant concepts and theorems from [5].


Computability ◽  
2019 ◽  
Vol 8 (3-4) ◽  
pp. 347-358
Author(s):  
Matthew Harrison-Trainor

Sign in / Sign up

Export Citation Format

Share Document