where $g_i$ are of sort $Df_n$ and satisfy $\left[ \sum_i g_i^+ > 0 \right]$ (1). Functions $h_i$ of sort $Df_n$ are considered, for which a priori only the restrictions $h_i|_{V_i}$ are relevant. The fact that $h_i$ and $h_j$ coincide on $V_i \cap V_j$ results in the equality $[h_i g_i^+ g_j^+ = h_j g_j^+ g_i^+]$ (2). Under hypotheses (1) and (2) we ask for the existence and uniqueness of an f of sort $Df_n$ verifying $fg_i^+ = h_i g_i^+$ for each $i$ (which means that $f|_{V_i} = h_i|_{V_i}$). A priori we must have $f = (\sum_i h_i g_i^+)(\sum_i g_i^+)^{-1}$ (hence the uniqueness). And we get

$$fg_k^+ = \frac{\sum_i h_i g_i^+ g_k^+}{\sum_i g_i^+} = \frac{\sum_i h_k g_i^+ g_k^+}{\sum_i g_i^+} = \frac{(h_k g_k^+) \sum_i g_i^+}{\sum_i g_i^+} = h_k g_k^+.$$

## Gluing of maps defined on a closed covering

A finite covering of $\mathbf{I}^n$ by definable closed subsets is given here in the form

$$F_i = \{ \underline{x} \in \mathbf{I}^n \mid g_i(\underline{x}) \ge 0 \} \quad i \in [1..p]$$

where $g_i$ are of sort $Df_n$ and satisfy $\sup_i g_i \ge 0$. Functions $h_i$ of sort $Df_n$ are considered, for which a priori only the restrictions $h_i|_{F_i}$ are relevant. The fact that $h_i$ and $h_j$ coincide on $F_i \cap F_j$ results in the validity of the rules $(i, j \in [1..p])$

$$g_i(\underline{x}) \ge 0, g_j(\underline{x}) \ge 0 \vdash_{x_1, \dots, x_n; Icr; g_i, h_i, g_j, h_j; Df_n} h_i(\underline{x}) = h_j(\underline{x})$$

A uniform algebraic version of this validity can be stated as follows

$$\bullet \vdash_{g_i, h_i, q_{ij}, q_{ji}; Df_n} (h_i - h_j)^2 + g_i q_{ij}^+ + g_j q_{ji}^+ = 0$$

where the $q_{kl}$ are of sort $Df_n$. Let's abbreviate the second member as $E_{ij}$. Under the hypothesis of the equalities $E_{ij}$, we want to have a map $f$ (an object $f$ of sort $Df_n$) satisfying an identity which means that $f|_{F_i} = h_i|_{F_i}$. This can be expressed in the form of the following rule

$$\mathbf{RCVF} \sup_i g_i \ge 0, E_{1,2}, \dots, E_{p-1,p} \vdash_{g_i, h_i, q_{ij}, q_{ji}; Df_n} \exists f, q_1, \dots, q_p \wedge_i (f - h_i)^2 + g_i q_i^+ = 0$$

All the (free or dummy) variables in this rule are of sort $Df_n$.

In classical mathematics, this type of rule is valid for o-minimal structures. However, from a constructive point of view, we may have to restrict ourselves to coverings by *located closed subsets*.<fnref n="2" /> This will complicate the writing of the axioms.

Note that the object $f$ whose existence is postulated is provably unique by virtue of a classical calculation for Positivstellensätze: we use the identity $(a+b)^2 + (a-b)^2 = 2(a^2 + b^2)$.

## Axioms of extension by continuity

Typically, the **FRAC**<sub>n</sub> rules are special continuity extension axioms. The aim here is to state different rules that apply more generally (without the continuity extension giving 0 to the disputed values) but with a smooth denominator.

For example, a map that is definable outside the zeros of a smooth (non-zero) map and continuous on its domain of definition is uniquely extended by continuity if it is uniformly continuous.

The problem is to formulate this in the context of our dynamical theory.

It will be good enough to be able to formulate it for a quotient $f/g$ (well-defined outside the zeros of $g$) with $g$ smooth.

The fact that $f$ cancels at the zeros of $g$ can be put as an hypothesis in the following strong form: there exists an $\alpha$ of such a sort $Mc$ that $\alpha \circ |f| \le |g|$.

<footnote n="2">²A closed subset is said to be *located* when the distance to it is a well-defined map from a constructive point of view. It seems necessary to add an axiom saying that the distance map to the zero set of a continuous definable map is itself definable.</footnote>
The uniform continuity of $f/g$ outside the zeros of $g$ seems to be stated using the reciprocal bijection of an object of sort $Mc$ on the interval $[0, 1]$. In fact, we want to write something like

$$ \mu \left( \left| \frac{f(x)g(x') - f(x')g(x)}{g(x)g(x')} \right| \right) \le \|(x) - (x')\| $$

for $\|(x) - (x')\| > 0$, which could be rewritten without the assumption $\|(x) - (x')\| > 0$ in the framework of geometric theory as

$$ |f(x)g(x') - f(x')g(x)| \le |g(x)g(x')|, \nu(\|(x) - (x')\|) $$

with the reciprocal bijection $\nu$ (on $[0, \mu(1)]$) of $\mu|_{[0,1]}$.

## Conclusion: the improved real closed field structure

The theory *Crc3* will be obtained once all the axioms have been worked out. We have seen that the theory *Icr* can be considered as a variant of the theory *Co*. The theory *Crc3*, which could also be called the theory of *compact real closed intervals*, is an improved variant of *Crc2*, in which o-minimal structures (which are enriched structures of real closed fields) could have a place as particular dynamic algebraic structures.

**Theorem K.3.1.** In constructive mathematics, the real interval $\mathbb{I} = \mathbb{I}_R$ and the continuous semi-algebraic maps $\mathbb{I}^n \to \mathbb{I}$, provides a model of the dynamical theory *Crc3*.

*Proof.* It seems that the ad hoc definition of continuous semialgebraic maps adopted in E.3.4 reduces this theorem to a theorem concerning essentially $\mathbb{R}_{alg}$. But we need to check all the details and this may lead us to change the formulation of some axioms. $\square$

This theory *Crc3* should make it possible to demonstrate constructive results which escape the more elementary theory *Crc2* for the simple reason that they do not correspond to dynamical rules of *CRC2*. Moreover, the same question arises for the dynamical rules of *CRC2* themselves.

## K.4. O-minimal structures

It seems that the axioms proposed here for the structure of compact real closed intervals are almost correct for constructively describing certain o-minimal structures defined in classical mathematics: those generated by the restrictions to the compact cube $\mathbb{I}^n$ of certain smooth maps in the neighbourhood of $\mathbb{I}^n$.

The weakest point seems to be stability by projection. A priori, the current system of axioms only guarantees this stability for definable closed bounded parts.

The resulting structure depends on the smooth maps given at the outset in the $Li_n$ sorts.

We are primarily interested in the structure obtained by taking the real analytic maps in the vicinity of the cube as the starting smooth maps. In dimension 1, this probably works well with Chebyshev series.

It is a real challenge to give a constructive version of the classical theory, for example starting from the presentations given in [70] and [21]. It would at least be necessary to demonstrate constructively that real analytic maps in the neighbourhood of the cube give rise to a structure which is a model of the dynamical theory *CRC3*.

Note also that from a strictly computational point of view, we are a priori more interested in the *enumerable field $\mathbb{R}_{PR}$* of real numbers computable in primitive recursive time, or in the *enumerable field $\mathbb{R}_{Ptime}$* of real numbers computable in polynomial time (see Example C.3.4). As for the definable continuous maps corresponding to these fields (for a fixed o-minimal structure), they too can no doubt be enumerated using Chebyshev series.

Finally, it should be pointed out that, as things stand, the system of axioms envisaged does not seem sufficient to really describe o-minimal structures, since it only guarantees stability by projection for bounded closed definable parts.
# K.5. Some questions

**Question K.5.1.**

Does the theory *Crc3* prove more dynamical rules than the theory of the interval [−1, 1] for a real closed field described by *Crc1*, or by *Crc2*?

**Questions K.5.2.**

1) Does $\mathbb{R}$ (for the sort $\mathbb{R}$), with $I = I_{\mathbb{R}}$ (for the sort $\mathrm{Icr}$) and for $\mathrm{Li}_n$ the maps $I^n \to I$ which are analytic in a neighbourhood of $I^n$, support a model of the dynamical theory *Crc3*?

2) If so, do the objects of sort $Df_n$ correspond exactly to the elements of the strongly real ring generated by the maps associated with the objects of sort $\mathrm{Li}_n$?
<figure><img src="image_21.png" /></figure>
# General conclusion

This dissertation, and the unanswered questions it contains, is a measure of our ignorance of real algebra.
Références et index
<figure><img src="image_22.png" /></figure>
References. Livres

[Balbes & Dwinger] Raymond Balbes and Philip Dwinger. *Distributive lattices*. University of Missouri Press, Columbia, Mo., 1974, pp. xiii+294 (cit. on p. 31).

[Bigard, Keimel & Wolfenstein] Alain Bigard, Klaus Keimel and Samuel Wolfenstein. *Groupes et anneaux réticulés*. Lecture Notes in Mathematics, Vol. 608. Springer-Verlag, Berlin-New York, 1977 (cit. on pp. 69, 70, 72, 73).

[Bishop] Errett Bishop. *Foundations of constructive analysis*. McGraw-Hill, New York, 1967 (cit. on p. 3).

[Bishop & Bridges] Errett Bishop and Douglas Bridges. *Constructive analysis*. Vol. 279. Grundlehren der Mathematischen Wissenschaften [Fundamental Principles of Mathematical Sciences]. Springer-Verlag, Berlin, 1985. DOI: 10.1007/978-3-642-61667-9 (cit. on p. 3).

[Bochnak, Coste & Roy] Jacek Bochnak, Michel Coste and Marie-Françoise Roy. *Real algebraic geometry*. Vol. 36. Ergebnisse der Mathematik und ihrer Grenzgebiete (3) [Results in Mathematics and Related Areas (3)]. Translated from the 1987 French original, Revised by the authors. Berlin: Springer-Verlag, 1998 (cit. on pp. 48, 50, 58–60, 98).

[Bridges & Richman] Douglas Bridges and Fred Richman. *Varieties of constructive mathematics*. Vol. 97. London Mathematical Society Lecture Note Series. Cambridge University Press, Cambridge, 1987. DOI: 10.1017/CB09780511565663 (cit. on p. 3).

[Caramello] Olivia Caramello. *Theories, Sites, Toposes*. Oxford University Press, 2017 (cit. on p. 8).

[Coste] Michel Coste. *An introduction to O-minimal Geometry*. Vol. 1. 1. Dip. Mat. Univ. Pisa, Dottorato di Ricerca in Matematica, Istituti Editoriali e Poligrafici Internazionali, Pisa, 2000, p. 1. URL: https://perso.univ-rennes1.fr/michel coste/polyens/OMIN.pdf (cit. on pp. 3, 119).

[van den Dries] Lou van den Dries. *Tame topology and o-minimal structures*. Vol. 248. London Mathematical Society Lecture Note Series. Cambridge University Press, Cambridge, 1998. DOI: 10.1017/CB09780511525919 (cit. on pp. 3, 119).

[Goodstein, 1957] R.L. Goodstein. *Recursive number theory. A development of recursive arithmetic in a logic-free equation calculus*. Studies in Logic and the Foundations of Mathematics. Amsterdam: North-Holland Publishing Company XII, 190 p. (1957), 1957 (cit. on p. 23).

[Goodstein, 1961] R.L. Goodstein. *Recursive analysis*. Studies in Logic and the Foundations of Mathematics. Amsterdam: North-Holland Publishing Company. VIII, 138 p. (1961), 1961 (cit. on p. 23).

[Goodstein, 1979] R.L. Goodstein. *Fundamental concepts of mathematics*. 2nd ed. 1979 (cit. on p. 23).

[Johnstone] Peter T. Johnstone. *Stone spaces*. Vol. 3. Cambridge studies in advanced mathematics. Reprint of the 1982 edition. Cambridge university press, Cambridge, 1986 (cit. on pp. 31, 72, 84).
[Johnstone, Sketches 2] Peter T. Johnstone. *Sketches of an elephant: a topos theory compendium*. Vol. 2. Vol. 44. Oxford Logic Guides. The Clarendon Press, Oxford University Press, Oxford, 2002 (cit. on p. 8).

[LPR] Henri Lombardi, Daniel Perrucci and Marie-Françoise Roy. *An elementary recursive bound for effective positivstellensatz and Hilbert's 17th problem*. Vol. 1277. Providence, RI: American Mathematical Society (AMS), 2020. URL: http://arxiv.org/abs/1404.2338 (cit. on p. 50).

[CACM] Henri Lombardi and Claude Quitté. *Commutative algebra: constructive methods*. Finite projective modules. Algebra and applications, 20. Translated from [ACMC] (Calvage & Mounet, Paris, 2011, revised and extended by the authors) by Tania K. Roblot. Springer, Dordrecht, 2015 (cit. on pp. 3, 30, 37, 50, 57, 68–71, 101).

[ACMC] Henri Lombardi and Claude Quitté. *Algèbre commutative. Méthodes constructives*. Modules projectifs de type fini. Cours et exercices. French. Second edition, revised and extended, of the 2011 book. Paris: Calvage & Mounet, 2021 (cit. on pp. 22, 30, 140).

[Mason & Handscomb] J. C. Mason and D. C. Handscomb. *Chebyshev polynomials*. Chapman & Hall/CRC, Boca Raton, FL, 2003 (cit. on p. 122).

[MRR] Ray Mines, Fred Richman and Wim Ruitenburg. *A course in constructive algebra*. Universitext. Traduction française par Henri Lombardi, révisée par Stefan Neuwirth. Un cours d'algèbre constructive. Presses Universitaires de Franche-Comté. 2020. Springer-Verlag, New York, 1988. DOI: 10.1007/978-1-4419-8640-5. URL: http://dx.doi/10.1007/978-1-4419-8640-5 (cit. on pp. 3, 19, 57, 101).

[Proofs, 2013] Dieter Probst and Peter Schuster, eds. *Concepts of proof in mathematics, philosophy, and computer science. Based on the Humboldt-Kolleg, Bern, Switzerland, September 9–13, 2013*. English. Berlin: De Gruyter, 2016. DOI: 10.1515/9781501502620 (cit. on pp. 37, 144).

[CCAPM] Ihsen Yengui. *Constructive commutative algebra: projective modules over polynomial rings and dynamical Gröbner bases*. Lecture Notes in Mathematics, 2138. Springer, Cham, 2015, pp. vii+271. DOI: 10.1007/978-3-319-19494-3 (cit. on p. 3).

[Zaanen] Adriaan C. Zaanen. *Introduction to operator theory in Riesz spaces*. Springer-Verlag, Berlin, 1997. DOI: 10.1007/978-3-642-60637-3 (cit. on p. 69).
References. Articles

[1] Ernesto Acosta and Cesar Delgado. ‘Uniform calculus and the law of bounded change’. In: *Amer. Math. Monthly* 101.4 (1994), pp. 332–338 (cit. on p. 129).

[2] María Emilia Alonso Garcia and André Galligo. ‘A root isolation algorithm for sparse univariate polynomials’. In: *ISSAC 2012—Proceedings of the 37th International Symposium on Symbolic and Algebraic Computation*. ACM, New York, 2012, pp. 35–42. DOI: 10.1145/2442829.2442839 (cit. on p. 87).

[3] María Emilia Alonso Garcia, Henri Lombardi and Hervé Perdry. ‘Elementary constructive theory of Henselian local rings’. In: *MLQ Math. Log. Q.* 54.3 (2008), pp. 253–271. DOI: 10.1002/malq.200710057. URL: https://arxiv.org/abs/2202.06595 (cit. on pp. 55, 57).

[4] Thomas William Barrett and Hans Halvorson. ‘Quine’s conjecture on many-sorted logic’. In: *Synthese* 194.9 (2017), pp. 3563–3582. DOI: 10.1007/s11229-016-1107-z (cit. on p. 8).

[5] Daniel Bembé and André Galligo. ‘Virtual roots of a real polynomial and fractional derivatives’. In: *ISSAC 2011—Proceedings of the 36th International Symposium on Symbolic and Algebraic Computation*. ACM, New York, 2011, pp. 27–34. DOI: 10.1145/1993886.1993897 (cit. on p. 87).

[6] Marc Bezem and Thierry Coquand. ‘Automating coherent logic.’ In: *Logic for programming, artificial intelligence, and reasoning. 12th international conference, LPAR 2005, Montego Bay, Jamaica, December 2–6, 2005. Proceedings*. Berlin: Springer, 2005, pp. 246–260. DOI: 10.1007/11591191_18 (cit. on p. 12).

[7] Marc Bezem and Thierry Coquand. ‘Skolem’s Theorem in Coherent Logic.’ In: *Fundam. Inform.* (2019) (cit. on p. 29).

[8] Garrett Birkhoff and R. S. Pierce. ‘Lattice-ordered rings’. In: *An. Acad. Brasil. Ci.* 28 (1956), pp. 41–69 (cit. on p. 72).

[9] Mark Bridger and Gabriel Stolzenberg. ‘Uniform calculus and the law of bounded change’. In: *Amer. Math. Monthly* 106.7 (1999), pp. 628–635. DOI: 10.2307/2589492 (cit. on p. 129).

[10] Jan Cederquist and Thierry Coquand. ‘Entailment relations and distributive lattices’. In: *Logic Colloquium '98 (Prague)*. Vol. 13. Lect. Notes Log. Assoc. Symbol. Logic, Urbana, IL, 2000, pp. 127–139 (cit. on pp. 30, 66, 84).

[11] Thierry Coquand. ‘A completeness proof for geometrical logic.’ In: *Logic, methodology and philosophy of science. Proceedings of the 12th international congress, Oviedo, Spain, August 2003*. London: King’s College Publications, 2005, pp. 79–89 (cit. on p. 28).

[12] Thierry Coquand and Henri Lombardi. ‘A logical approach to abstract algebra’. In: *Math. Structures Comput. Sci.* 16.5 (2006), pp. 885–900. DOI: 10.1017/S0960129506005627 (cit. on pp. 37, 66).

[13] Thierry Coquand and Henri Lombardi. ‘A note on the axiomatisation of real numbers’. In: *Math. Log. Q.* 54.3 (2008), pp. 224–228. DOI: 10.1002/malq.200710039 (cit. on p. 51).
[14] Thierry Coquand, Henri Lombardi and Stefan Neuwirth. 'Lattice-ordered groups generated by an ordered group and regular systems of ideals.' In: *Rocky Mt. J. Math.* 49.5 (2019), pp. 1449–1489. URL: https://arxiv.org/abs/1701.05115 (cit. on p. 71).

[15] Thierry Coquand, Henri Lombardi and Claude Quitté. 'Dimension de Heitmann des treillis distributifs et des anneaux commutatifs'. In: *Publications Mathématiques de l'Université de Franche-Comté Besançon. Algèbre et théorie des nombres. Années 2003-2006*. Besançon: Laboratoire de Mathématiques de Besançon, 2006, p. 57–100, version corrigée, 2020. URL: http://arxiv.org/abs/1712.01958 (cit. on p. 66).

[16] Michel Coste, Tomás Lajous-Loaeza, Henri Lombardi and Marie-Françoise Roy. 'Generalized Budan-Fourier theorem and virtual roots'. In: *J. Complexity* 21.4 (2005), pp. 479–486. DOI: 10.1016/j.jco.2004.11.003 (cit. on pp. 87, 89).

[17] Michel Coste, Henri Lombardi and Marie-Françoise Roy. 'Dynamical method in algebra: effective Nullstellensätze'. In: *Ann. Pure Appl. Logic* 111.3 (2001), pp. 203–256. DOI: 10.1016/S0168-0072(01)00026-4 (cit. on pp. 12, 17, 18, 20, 28, 29, 44, 46–50, 100).

[18] Jean Della Dora, Claire Dicrescenzo and Dominique Duval. 'About a new method for computing in algebraic number fields'. In: *EUROCAL '85. Lecture Notes in Computer Science no. 204*, (Ed. Caviness B.F.) Springer, Berlin, 1985, pp. 289–290 (cit. on p. 18).

[19] Charles N. Delzell. 'On the Pierce-Birkhoff conjecture over ordered fields'. In: *Rocky Mountain J. Math.* 19.3 (1989). Quadratic forms and real algebraic geometry (Corvallis, OR, 1986), pp. 651–668. DOI: 10.1216/RMJ-1989-19-3-651 (cit. on p. 76).

[20] Charles N. Delzell and James J. Madden. 'Lattice-ordered rings and semialgebraic geometry. I'. In: *Real analytic and algebraic geometry (Trento, 1992)*. de Gruyter, Berlin, 1995, pp. 103–129 (cit. on p. 72).

[21] J. Denef and Lou van den Dries. 'p-adic and real subanalytic sets.' In: *Ann. Math. (2)* 128.1 (1988), pp. 79–138. DOI: 10.2307/1971463 (cit. on pp. 119, 132).

[22] Roy Dyckhoff. 'Invited talk: coherentisation of first-order logic.' In: *Automated reasoning with analytic tableaux and related methods. 24th international conference, TABLEAUX 2015, Wroclaw, Poland, September 21-24, 2015. Proceedings*. Cham: Springer, 2015, pp. 3–5. DOI: 10.1007/978-3-319-24312-2_1 (cit. on p. 28).

[23] Roy Dyckhoff and Sara Negri. 'Geometrisation of first-order logic.' In: *Bull. Symb. Log.* 21.2 (2015), pp. 123–163. DOI: 10.1017/bsl.2015.7 (cit. on p. 28).

[24] Michael Eisermann. 'The fundamental theorem of algebra made effective: an elementary real-algebraic proof via Sturm chains'. In: *Amer. Math. Monthly* 119.9 (2012), pp. 715–752. DOI: 10.4169/amer.math.monthly.119.09.715 (cit. on pp. 107, 108).

[25] André Galligo. 'Budan tables of real univariate polynomials'. In: *J. Symbolic Comput.* 53 (2013), pp. 64–80. DOI: 10.1016/j.jsc.2012.11.004 (cit. on p. 87).

[26] Laureano González-Vega and Henri Lombardi. 'A real Nullstellensatz and Positivstellensatz for the semipolynomials over an ordered field'. In: *J. Pure Appl. Algebra* 90.2 (1993), pp. 167–188. DOI: 10.1016/0022-4049(93)90128-G. URL: http://hlombardi.free.fr/publis/PstSemiPols.pdf (cit. on pp. 51, 62, 83, 109).

[27] Laureano González-Vega, Henri Lombardi and Louis Mahé. 'Virtual roots of real polynomials'. In: *J. Pure Appl. Algebra* 124.1-3 (1998), pp. 147–166. DOI: 10.1016/S0022-4049(96)00102-8. URL: http://arxiv.org/abs/1712.01952 (cit. on pp. 86–89, 91).

[28] M. Hochster. 'Prime ideal structure in commutative rings.' In: *Trans. Am. Math. Soc.* 142 (1969), pp. 43–60. DOI: 10.2307/1995344 (cit. on p. 31).

[29] P. T. Johnstone. *A syntactic approach to Diers' localizable categories*. Applications of sheaves, Proc. Res. Symp., Durham 1977, Lect. Notes Math. 753, 466-478 (1979). 1979 (cit. on pp. 9, 17).
[30] F.-V. Kuhlmann and Henri Lombardi. ‘Construction of the Henselization of a valued field. (Construction du hensélisé d'un corps valué.)' In: *J. Algebra* 228.2 (2000), pp. 624–632. URL: http://arxiv.org/abs/2202.05503 (cit. on p. 57).

[31] Franz-Viktor Kuhlmann, Henri Lombardi and Hervé Perdry. ‘Dynamic computations inside the algebraic closure of a valued field’. In: *Valuation theory and its applications, Vol. II (Saskatoon, SK, 1999)*. Vol. 33. Fields Inst. Commun. Amer. Math. Soc., Providence, RI, 2003, pp. 133–156. URL: http://arxiv.org/abs/2202.05512 (cit. on p. 57).

[32] S. Labhalla, H. Lombardi and E. Moutai. ‘Espaces métriques rationnellement présentés et complexité: le cas de l'espace des fonctions réelles uniformément continues sur un intervalle compact’. In: *Theoret. Comput. Sci.* 250.1-2 (2001), pp. 265–332. DOI: 10.1016/S0304-3975(99)00139-5 (cit. on p. 71).

[33] Vladimir Lifschitz. ‘Semantical completeness theorems in logic and algebra’. In: *Proc. Amer. Math. Soc.* 79.1 (1980), pp. 89–96. DOI: 10.2307/2042394 (cit. on p. 12).

[34] Henri Lombardi. ‘Effective real Nullstellensatz and variants’. In: *Effective methods in algebraic geometry (Castiglioncello, 1990)*. Vol. 94. Progr. Math. Birkhäuser Boston, Boston, MA, 1991, pp. 263–288 (cit. on pp. 50, 100).

[35] Henri Lombardi. ‘Relecture constructive de la théorie d’Artin-Schreier’. In: *Ann. Pure Appl. Logic* 91.1 (1998), pp. 59–92. DOI: 10.1016/S0168-0072(97)80700-2 (cit. on p. 34).

[36] Henri Lombardi. ‘Dimension de Krull, Nullstellensätze et évaluation dynamique’. In: *Math. Z.* 242.1 (2002), pp. 23–46. DOI: 10.1007/s002090100305 (cit. on p. 18).

[37] Henri Lombardi. ‘Structures algébriques dynamiques, espaces topologiques sans points et programme de Hilbert’. In: *Ann. Pure Appl. Logic* 137.1-3 (2006), pp. 256–290. DOI: 10.1016/j.apal.2005.05.023 (cit. on p. 18).

[38] Henri Lombardi. ‘Le mystère de la structure du continu’. In: *Des Nombres et des Mondes. Actes du colloque en l’honneur de Guy Wallet (2011 à La Rochelle)*. Hermann, Paris, 2013, pp. 53–67 (cit. on p. 4).

[39] Henri Lombardi. ‘Théories géométriques pour l’algèbre constructive’. http://hlombardi.free.fr/Theories-geometriques.pdf. 2022 (cit. on pp. 7, 34).

[40] Henri Lombardi and Assia Mahboubi. ‘Théories géométriques pour l’algèbre des nombres réels’. French. In: *Ordered algebraic structures and related topics. International conference at CIRM, Luminy, France, October 12–16, 2015. Proceedings*. Vol. 697. Providence, RI: American Mathematical Society (AMS), 2017, pp. 239–264. URL: https://hal.inria.fr/hal-01426164 (cit. on pp. 1, 3, 4, 41, 53, 54, 62, 78, 81).

[41] Henri Lombardi and Assia Mahboubi. ‘Valuative lattices and spectra’. In: *Algebraic, number theoretic, and topological aspects of ring theory*. Ed. by Jean-Luc Chabert et al. Cham: Springer, 2023, pp. 275–341. DOI: 10.1007/978-3-031-28847-0_17. URL: http://arxiv.org/abs/2210.16558 (cit. on pp. 4, 7, 18, 27, 30).

[42] Henri Lombardi and Marie-Françoise Roy. ‘Elementary constructive theory of ordered fields’. In: *Effective methods in algebraic geometry (Castiglioncello, 1990)*. Vol. 94. Progr. Math. Birkhäuser Boston, Boston, MA, 1991, pp. 249–262 (cit. on pp. 50, 86–88, 100, 102).

[43] Henri Lombardi and Marie-Françoise Roy. ‘Théorie constructive élémentaire des corps ordonnés’. In: *Théorie des nombres, Années 1989/90-1990/91*. Publ. Math. Fac. Sci. Besançon. Univ. Franche-Comté, Besançon, 1991, pp. x-x+21 (cit. on pp. 50, 87, 88, 100).

[44] Paul Lorenzen. ‘Abstrakte Begründung der multiplikativen Idealtheorie’. In: *Math. Z.* 45 (1939), pp. 533–553 (cit. on p. 71).

[45] Paul Lorenzen. ‘Über halbgeordnete Gruppen’. In: *Math. Z.* 52 (1950), pp. 483–526. URL: http://eudml.org/doc/169131 (cit. on p. 71).
[46] Paul Lorenzen. ‘Algebraische und logistische Untersuchungen über freie Verbände’. In: *J. Symbolic Logic* 16 (1951). Translation by Stefan Neuwirth: *Algebraic and logistic investigations on free lattices*, http://arxiv.org/abs/1710.08138, pp. 81–106. URL: http://www.jstor.org/stable/2266681 (cit. on pp. 30, 66).

[47] Paul Lorenzen. ‘Die Erweiterung halbgeordneter Gruppen zu Verbandsgruppen’. German. In: *Math. Z.* 58 (1953), pp. 15–24. URL: http://eudml.org/doc/169331 (cit. on p. 71).

[48] F. Lucas, J. Madden, D. Schaub and M. Spivakovsky. ‘Approximate roots of a valuation and the Pierce-Birkhoff conjecture’. In: *Ann. Fac. Sci. Toulouse Math. (6)* 21.2 (2012), pp. 259–342. URL: http://afst.cedram.org/item?id=AFST_2012_6_21_2_259_0 (cit. on p. 108).

[49] James J. Madden. ‘Pierce-Birkhoff rings’. In: *Arch. Math. (Basel)* 53.6 (1989), pp. 565–570. DOI: 10.1007/BF01199816 (cit. on p. 108).

[50] James J. Madden. ‘On *f*-rings that are not formally real’. In: *Ann. Fac. Sci. Toulouse Math. (6)* 19.Fascicule Special (2010), pp. 143–157. URL: http://afst.cedram.org/item?id=AFST_2010_6_19__143_0 (cit. on p. 72).

[51] Louis Mahé. ‘On the Pierce-Birkhoff conjecture’. In: *Rocky Mountain J. Math.* 14.4 (1984). Ordered fields and real algebraic geometry (Boulder, Colo., 1983), pp. 983–985. DOI: 10.1216/RMJ-1984-14-4-983 (cit. on p. 108).

[52] Bassel Mannaa and Thierry Coquand. ‘Dynamic Newton-Puiseux theorem’. In: *J. Log. Anal.* 5 (2013), Paper 5. DOI: 10.4115/jla.2013.5.5 (cit. on p. 102).

[53] Ju. V. Matijasevič. ‘A metamathematical approach to proving theorems in discrete mathematics’. In: *Zap. Naučn. Sem. Leningrad. Otdel. Mat. Inst. Steklov. (LOMI)* 49 (1975). Theoretical applications of the methods of mathematical logic, I, pp. 31–50, 177 (cit. on p. 12).

[54] Daniel Perrucci and Marie-Françoise Roy. ‘Quantitative Fundamental Theorem of Algebra. Preprint.’ 2019. URL: http://arxiv.org/abs/1803.04358 (cit. on p. 107).

[55] Dag Prawitz. ‘Ideas and results in proof theory’. In: *Proceedings of the Second Scandinavian Logic Symposium (Univ. Oslo, Oslo, 1970)*. North-Holland, Amsterdam, 1971, 235–307. Studies in Logic and the Foundations of Mathematics, Vol. 63 (cit. on pp. 12, 28).

[56] Alexander Prestel and Niels Schwartz. ‘Model theory of real closed rings’. In: *Valuation theory and its applications, Vol. I (Saskatoon, SK, 1999)*. Vol. 32. Fields Inst. Commun. Amer. Math. Soc., Providence, RI, 2002, pp. 261–290 (cit. on pp. 52, 96, 97).

[57] Michael Rathjen. ‘Remarks on Barr’s theorem proofs in geometric theories’. In: *Concepts of proof in mathematics, philosophy, and computer science. Based on the Humboldt-Kolleg, Bern, Switzerland, September 9–13, 2013. [Proofs, 2013]*. Berlin: De Gruyter, 2016, pp. 347–374 (cit. on p. 37).

[58] Fred Richman. ‘The fundamental theorem of algebra: a constructive development without choice’. In: *Pacific J. Math.* 196.1 (2000), pp. 213–230. DOI: 10.2140/pjm.2000.196.213 (cit. on pp. 106, 107).

[59] Fred Richman. ‘Constructive mathematics without choice’. In: *Reuniting the antipodes – constructive and nonstandard views of the continuum (Venice, 1999)*. Vol. 306. Synthese Lib. Kluwer Acad. Publ., Dordrecht, 2001, pp. 199–205 (cit. on p. 3).

[60] Konrad Schmüdgen. ‘The *K*-moment problem for compact semi-algebraic sets’. In: *Math. Ann.* 289.2 (1991), pp. 203–206. DOI: 10.1007/BF01446568 (cit. on p. 112).

[61] Niels Schwartz. ‘Real closed spaces’. In: *Rocky Mountain J. Math.* 14.4 (1984). Ordered fields and real algebraic geometry (Boulder, Colo., 1983), pp. 971–972. DOI: 10.1216/RMJ-1984-14-4-971 (cit. on p. 98).

[62] Niels Schwartz. ‘Real closed spaces. Habilitationsschrift. München’. Habilitationsschrift. München, 1984 (cit. on p. 96).
[63] Niels Schwartz. 'Real closed rings'. In: *Algebra and order (Luminy-Marseille, 1984)*. Vol. 14. Res. Exp. Math. Heldermann, Berlin, 1986, pp. 175-194 (cit. on pp. 52, 96, 98).

[64] Niels Schwartz. 'The basic theory of real closed spaces'. In: *Mem. Amer. Math. Soc.* 77.397 (1989), pp. viii+122. DOI: 10.1090/memo/0397 (cit. on p. 98).

[65] Niels Schwartz. 'Rings of continuous functions as real closed rings'. In: *Ordered algebraic structures (Curaçao, 1995)*. Kluwer Acad. Publ., Dordrecht, 1997, pp. 277-313 (cit. on p. 98).

[66] Markus Schweighofer. 'An algorithmic approach to Schmüdgen's Positivstellensatz'. In: *J. Pure Appl. Algebra* 166.3 (2002), pp. 307-319. DOI: 10.1016/S0022-4049(01)00041-X (cit. on p. 112).

[67] Markus Schweighofer. 'Iterated rings of bounded elements and generalizations of Schmüdgen's Positivstellensatz'. In: *J. Reine Angew. Math.* 554 (2003), pp. 19-45. DOI: 10.1515/cr11.2003.004 (cit. on p. 112).

[68] M. H. Stone. 'Topological representations of distributive lattices and Brouwerian logics.' In: *Cas. Mat. Fys.* 67 (1937), pp. 1-25 (cit. on p. 31).

[69] Marcus Tressl. 'Super real closed rings'. In: *Fund. Math.* 194.2 (2007), pp. 121-177. DOI: 10.4064/fm194-2-2 (cit. on pp. 4, 41, 61, 86, 96, 98).

[70] Lou van den Dries. 'A generalization of the Tarski-Seidenberg theorem, and some nondefinability results.' In: *Bull. Am. Math. Soc., New Ser.* 15 (1986), pp. 189-193. DOI: 10.1090/S0273-0979-1986-15468-6 (cit. on pp. 119, 132).
<figure><img src="image_23.png" /></figure>
# Notations index

## Logic

<table><tr><td>U</td><td>deduction rule</td><td>12</td></tr><tr><td>op</td><td>open branches of computation</td><td>12</td></tr><tr><td>∃u</td><td>introduce a fresh variable u</td><td>14</td></tr><tr><td>⊥</td><td>collapse symbol</td><td>16</td></tr><tr><td>∧</td><td>logical “and”</td><td>27</td></tr><tr><td>∨</td><td>logical “or”</td><td>27</td></tr><tr><td>∃</td><td>logical “there exists”</td><td>27</td></tr></table>

## Function symbols

<table><tr><td>a ∨ b</td><td>sup(a, b)</td><td>48</td></tr><tr><td>Fr(a, b)</td><td>a/b (supposed well-defined)</td><td>53</td></tr><tr><td>fsa<sub>F</sub></td><td>continuous semialgebraic map of graph F</td><td>61</td></tr><tr><td>a ∧ b</td><td>inf(a, b)</td><td>68</td></tr><tr><td>Sqr</td><td>Sqr(x) = √x<sup>+</sup></td><td>86</td></tr><tr><td>ρ<sub>d,j</sub></td><td>virtual root</td><td>89</td></tr><tr><td>U</td><td>1/2 (x + y) on interval [-1, +1]</td><td>121</td></tr><tr><td>⊕</td><td>forced addition on [-1, +1]</td><td>121</td></tr><tr><td>Cb</td><td>barycentric coefficients</td><td>122</td></tr><tr><td>Brc</td><td>barycenters</td><td>122</td></tr><tr><td>T<sub>n</sub></td><td>Chebyshev polynomial</td><td>122</td></tr></table>

## Theories

<table><tr><td>Cd</td><td>discrete fields</td><td>13</td></tr><tr><td>Ac</td><td>commutative rings</td><td>18</td></tr><tr><td>Cod</td><td>discrete ordered fields</td><td>44</td></tr><tr><td>Apo</td><td>preordered rings</td><td>46</td></tr><tr><td>AO</td><td>ordered rings</td><td>46</td></tr><tr><td>Aonz</td><td>strictly reduced ordered rings</td><td>46</td></tr><tr><td>Ato</td><td>linearly ordered rings</td><td>46</td></tr><tr><td>Atonz</td><td>reduced linearly ordered rings</td><td>46</td></tr><tr><td>Apro</td><td>proto-ordered rings</td><td>46</td></tr><tr><td>Aso</td><td>strictly ordered rings</td><td>46</td></tr></table>
<table>
  <tbody>
    <tr>
      <td>Asto</td>
      <td>linearly, strictly ordered rings</td>
      <td>47</td>
    </tr>
    <tr>
      <td>Asonz</td>
      <td>reduced strictly ordered rings</td>
      <td>47</td>
    </tr>
    <tr>
      <td>Aito</td>
      <td>linearly ordered domains</td>
      <td>47</td>
    </tr>
    <tr>
      <td>Crcd</td>
      <td>discrete real closed fields</td>
      <td>45</td>
    </tr>
    <tr>
      <td>Codsup</td>
      <td>discrete ordered fields with sup</td>
      <td>48</td>
    </tr>
    <tr>
      <td>Atosup</td>
      <td>lineairly ordered rings with sup</td>
      <td>48</td>
    </tr>
    <tr>
      <td>Astosup</td>
      <td>strict f-rings with sup</td>
      <td>48</td>
    </tr>
    <tr>
      <td>Crcdsup</td>
      <td>real closed fields with sup</td>
      <td>48</td>
    </tr>
    <tr>
      <td>Co0</td>
      <td>minimal theory of non discrete ordered fields</td>
      <td>51</td>
    </tr>
    <tr>
      <td>Co</td>
      <td>non discrete ordered fields</td>
      <td>53</td>
    </tr>
    <tr>
      <td>Crc1</td>
      <td>non discrete real closed fields</td>
      <td>60</td>
    </tr>
    <tr>
      <td>Tr0</td>
      <td>(bounded) lattices</td>
      <td>66</td>
    </tr>
    <tr>
      <td>Tr</td>
      <td>nontrivial lattices</td>
      <td>66</td>
    </tr>
    <tr>
      <td>Trdi</td>
      <td>distributive lattices</td>
      <td>66</td>
    </tr>
    <tr>
      <td>Grl</td>
      <td>l-groups</td>
      <td>68</td>
    </tr>
    <tr>
      <td>Gtosup</td>
      <td>lineairly ordered groups with sup</td>
      <td>70</td>
    </tr>
    <tr>
      <td>Afr</td>
      <td>f-rings</td>
      <td>72</td>
    </tr>
    <tr>
      <td>Afrnz</td>
      <td>reduced f-rings</td>
      <td>78</td>
    </tr>
    <tr>
      <td>Afrsdz</td>
      <td>f-rings without zerodivisor</td>
      <td>77</td>
    </tr>
    <tr>
      <td>Asr</td>
      <td>strict f-rings</td>
      <td>78</td>
    </tr>
    <tr>
      <td>Asrnz</td>
      <td>reduced strict f-rings</td>
      <td>78</td>
    </tr>
    <tr>
      <td>Aftr</td>
      <td>strongly real f-rings</td>
      <td>80</td>
    </tr>
    <tr>
      <td>Afr2c</td>
      <td>2-closed f-rings</td>
      <td>86</td>
    </tr>
    <tr>
      <td>Asr2c</td>
      <td>2-closed strict f-rings</td>
      <td>86</td>
    </tr>
    <tr>
      <td>Co2c</td>
      <td>2-closed non discrete ordered fields</td>
      <td>86</td>
    </tr>
    <tr>
      <td>Corv</td>
      <td>non discrete ordered fields with virtual roots</td>
      <td>94</td>
    </tr>
    <tr>
      <td>Co0rv</td>
      <td></td>
      <td>94</td>
    </tr>
    <tr>
      <td>Afrrv</td>
      <td>f-rings with virtual roots</td>
      <td>92</td>
    </tr>
    <tr>
      <td>Arc</td>
      <td>real closed rings</td>
      <td>93</td>
    </tr>
    <tr>
      <td>Asrrv</td>
      <td>strict f-rings with virtual roots</td>
      <td>92</td>
    </tr>
    <tr>
      <td>Aitorv</td>
      <td>lineairly ordered domains with virtual roots</td>
      <td>92</td>
    </tr>
    <tr>
      <td>Crc2</td>
      <td>non discrete real closed fields, 2; essentially identical to Corv and to Crc1</td>
      <td>99</td>
    </tr>
    <tr>
      <td>Crca</td>
      <td>archimedean non discrete real closed fields</td>
      <td>111</td>
    </tr>
    <tr>
      <td>Icr</td>
      <td>compact real intervals</td>
      <td>122</td>
    </tr>
    <tr>
      <td>Icrc</td>
      <td>compact real closed intervals</td>
      <td>??</td>
    </tr>
  </tbody>
</table>

Some axioms and dynamical rules

<table>
  <tbody>
    <tr>
      <td>AL</td>
      <td>(x + y)z = 1 ⊢ ∃u xu = 1 op ∃v yv = 1 local rings axiom</td>
      <td>13</td>
    </tr>
    <tr>
      <td>AL1</td>
      <td>U(x + y) ⊢ U(x) op U(y)</td>
      <td>31</td>
    </tr>
    <tr>
      <td>Anz</td>
      <td>x<sup>2</sup> = 0 ⊢ x = 0</td>
      <td>13</td>
    </tr>
    <tr>
      <td>ASDZ</td>
      <td>xy = 0 ⊢ x = 0 op y = 0</td>
      <td>13</td>
    </tr>
    <tr>
      <td>CD</td>
      <td> x = 0 op ∃y xy = 1</td>
      <td>13</td>
    </tr>
    <tr>
      <td>NIL</td>
      <td>Z(x) ⊢ OP<sub>n∈N+</sub> x<sup>n</sup> = 0</td>
      <td>36</td>
    </tr>
    <tr>
      <td>Gao</td>
      <td>x ≥ 0, x ≤ 0 ⊢ x = 0</td>
      <td>45</td>
    </tr>
  </tbody>
</table>
<table>
  <tbody>
    <tr>
      <td>asol à aso4</td>
      <td>45</td>
    </tr>
    <tr>
      <td>lv</td>
      <td>xy = 1 ⊢ x² > 0..</td>
      <td>45</td>
    </tr>
    <tr>
      <td>IV</td>
      <td>x > 0 ⊢ ∃y xy = 1..</td>
      <td>45</td>
    </tr>
    <tr>
      <td>ED<sub>#</sub></td>
      <td> x = 0 op x # 0..</td>
      <td>45</td>
    </tr>
    <tr>
      <td>OT</td>
      <td>op x ≤ 0..</td>
      <td>45</td>
    </tr>
    <tr>
      <td>Aonz</td>
      <td>c ≥ 0, x(x² + c) ≥ 0 ⊢ x ≥ 0 strictly reduced ordered rings..</td>
      <td>45</td>
    </tr>
    <tr>
      <td>Aso1</td>
      <td>x > 0, xy ≥ 0 ⊢ y ≥ 0..</td>
      <td>45</td>
    </tr>
    <tr>
      <td>Aso2</td>
      <td>x ≥ 0, xy > 0 ⊢ y > 0..</td>
      <td>45</td>
    </tr>
    <tr>
      <td>OTF</td>
      <td>x + y > 0 ⊢ x > 0 op y > 0..</td>
      <td>45</td>
    </tr>
    <tr>
      <td>OTF ×</td>
      <td>xy < 0 ⊢ x < 0 op y < 0..</td>
      <td>45</td>
    </tr>
    <tr>
      <td>Afr4</td>
      <td>y ≥ 0, xy = 1 ⊢ x ≥ 0..</td>
      <td>47</td>
    </tr>
    <tr>
      <td>Afr5</td>
      <td>c ≥ 0, x(x² + c) ≥ 0 ⊢ x³ ≥ 0..</td>
      <td>47</td>
    </tr>
    <tr>
      <td>RCF<sub>n</sub></td>
      <td>a < b, P(a)P(b) < 0 ⊢ ∃x (P(x) = 0, a < x < b) (P(x) = Σ<sub>k=0</sub><sup>n</sup> a<sub>k</sub>x<sup>k</sup>) .</td>
      <td>45</td>
    </tr>
    <tr>
      <td>sup1</td>
      <td>x ∨ y ≥ x..</td>
      <td>48</td>
    </tr>
    <tr>
      <td>sup2</td>
      <td>x ∨ y ≥ y..</td>
      <td>48</td>
    </tr>
    <tr>
      <td>Sup</td>
      <td>z ≥ x, z ≥ y ⊢ z ≥ x ∨ y..</td>
      <td>48</td>
    </tr>
    <tr>
      <td>sup</td>
      <td>((x ∨ y) - x) ((x ∨ y) - y) = 0..</td>
      <td>48</td>
    </tr>
    <tr>
      <td>grl</td>
      <td>x + (y ∨ z) = (x + y) ∨ (x + z)..</td>
      <td>52</td>
    </tr>
    <tr>
      <td>afr</td>
      <td>x<sup>+</sup> (y ∨ z) = (x<sup>+</sup> y) ∨ (x<sup>+</sup> z)..</td>
      <td>52</td>
    </tr>
    <tr>
      <td>CVX</td>
      <td>0 ≤ a ≤ b ⊢ ∃z zb = a²..</td>
      <td>53</td>
    </tr>
    <tr>
      <td>FRAC</td>
      <td>0 ≤ a ≤ b ⊢ ∃z (zb = a², 0 ≤ z ≤ a)..</td>
      <td>53</td>
    </tr>
    <tr>
      <td>fr1</td>
      <td>Fr(a, b) |b| = (|a|∧|b|)²..</td>
      <td>53</td>
    </tr>
    <tr>
      <td>fr2</td>
      <td>0 ≤ Fr(a, b) ≤ |a|∧|b|..</td>
      <td>53</td>
    </tr>
    <tr>
      <td>FRAC<sub>n</sub></td>
      <td>|u|<sup>n</sup> ≤ |v|<sup>n+1</sup> ⊢ ∃z (zv = u, |z|<sup>n</sup> ≤ |v|) (n ≥ 1)..</td>
      <td>54</td>
    </tr>
    <tr>
      <td>afr1 - afr7</td>
      <td></td>
      <td>73</td>
    </tr>
    <tr>
      <td>Afr1 - Afr5</td>
      <td></td>
      <td>73</td>
    </tr>
    <tr>
      <td>Afrnz1 - Afrnz3</td>
      <td></td>
      <td>79</td>
    </tr>
    <tr>
      <td>AFRL</td>
      <td>z(x + y) = 1, x + y ≥ 0 ⊢ ∃u (ux = 1, x ≥ 0) op ∃v (vy = 1, y ≥ 0)..</td>
      <td>81</td>
    </tr>
    <tr>
      <td>sqr0</td>
      <td>op Sqr(0) = 0..</td>
      <td>86</td>
    </tr>
    <tr>
      <td>sqr1</td>
      <td>op Sqr(x) ≥ 0..</td>
      <td>86</td>
    </tr>
    <tr>
      <td>sqr2</td>
      <td>op Sqr(x) = Sqr(x<sup>+</sup>)..</td>
      <td>86</td>
    </tr>
    <tr>
      <td>sqr3</td>
      <td>op Sqr(x)<sup>2</sup> = x<sup>+</sup>..</td>
      <td>86</td>
    </tr>
    <tr>
      <td>sqr4</td>
      <td>op Sqr(x<sup>+</sup>y<sup>+</sup>) = Sqr(x)Sqr(y)..</td>
      <td>86</td>
    </tr>
    <tr>
      <td>vr<sub>i,j,k</sub></td>
      <td>axioms for virtual roots, examples..</td>
      <td>90</td>
    </tr>
  </tbody>
</table>

Algebraic structures, generic models

<table>
  <tbody>
    <tr>
      <td>R<sub>alg</sub></td>
      <td>the field of real algebraic numbers</td>
      <td>50</td>
    </tr>
    <tr>
      <td>R<sub>PR</sub></td>
      <td>the field of primitive recursive real numbers</td>
      <td>52</td>
    </tr>
    <tr>
      <td>R<sub>Ptime</sub></td>
      <td>the field of real numbers computable in polynomial time</td>
      <td>52</td>
    </tr>
    <tr>
      <td>R<sub>Rec</sub></td>
      <td>the field of recursive real numbers</td>
      <td>52</td>
    </tr>
    <tr>
      <td>F<sub>sac</sub><sub>n</sub>(R)</td>
      <td>C.5.5: semialgebraic continuous functions in n variables, see also E.3.4</td>
      <td>59</td>
    </tr>
  </tbody>
</table>

In the following **A** is a commutative ring with a suitable algebraic structure over a suitable dynamical theory in some context, **R** is an *f*-ring with virtual roots.

<table>
  <tr>
    <td>AFR(A)</td>
    <td>f-ring freely generated by A</td>
    <td>77</td>
  </tr>
</table>
<table>
  <tr>
    <td>Sipd<sub>n</sub>(A)</td>
    <td>ring of semipolynomials (or sipd maps) in n variables over A</td>
    <td>77</td>
  </tr>
  <tr>
    <td>Sipd<sub>n</sub>(A, B)</td>
    <td>ring of A-semipolynomials in n variables over B</td>
    <td>77</td>
  </tr>
  <tr>
    <td>AFR2C(A)</td>
    <td>2-closure of an f-ring</td>
    <td>87</td>
  </tr>
  <tr>
    <td>Fsace<sub>n</sub>(R)</td>
    <td>ring of integral continuous semialgebraic maps in n variables</td>
    <td>93</td>
  </tr>
  <tr>
    <td>Fsac<sub>n</sub>(R)</td>
    <td>ring of continuous semialgebraic maps in n variables</td>
    <td>94</td>
  </tr>
  <tr>
    <td>AFRNZ(A)</td>
    <td>reduced f-ring generated by A</td>
    <td>93</td>
  </tr>
  <tr>
    <td>AFRRV(A)</td>
    <td>f-ring with virtual roots generated by A</td>
    <td>93</td>
  </tr>
  <tr>
    <td>Ppm(A)</td>
    <td>ring of piecewise polynomial elements of AFRRV(A)</td>
    <td>93</td>
  </tr>
  <tr>
    <td>ARC(A)</td>
    <td>real closed ring generated by A</td>
    <td>99</td>
  </tr>
</table>