Geometric theories for real number algebra
without sign test or dependent choice axiom

Henri Lombardi and Assia Mahboubi

last version is available in
http://hlombardi.free.fr/Real-Geom.pdf

First proposal, 27th August 2024

Abstract

In this memoir, we seek to construct a dynamical theory that is as complete as
possible to describe the algebraic properties of the real number field in constructive
mathematics without a dependent choice axiom.

In the first part, we give a few general points about geometric theories and their
dynamical version, dynamical theories.

The second part is devoted to the study of a finitary geometric theory whose am-
bition is to describe exhaustively the algebraic properties of the real number field, and
more generally of a *non* discrete real closed field, at least those that can be expressed
in a restricted language close to the language of ordered rings. The result is a theory
which, in classical mathematics, turns out to be the theory of local real closed rings.
The theory of real closed rings is presented here in a constructive form as a purely
natural equational theory, based on the virtual root maps introduced in earlier work.
All this constitutes a development, with some minor terminological modifications, of
the ideas given in the article [40]. Finally, we ask whether an infinitary axiom of
archimedianity would provide a better understanding of the proposed finitary theory.

In the third part, we introduce a more ambitious theory in which continuous semial-
gebraic maps are given their own place: new sorts are created for them. This makes it
possible to talk inside the theory about the uniform continuity modulus of a continuous
semialgebraic map on a bounded closed subset of Rn. This new theory is resolutely
infinitary. We then obtain a better description of the algebraic properties of R, but
also a first outline for a constructive theory of certain o-minimal structures.
<figure><img src="image_1.png" /></figure>
# Contents

Foreword 3

I Geometric theories 5

Introduction 7

A Finitary geometric theories 11

A.1 Coherent and finitary dynamical theories 12

A.2 Dynamic algebraic structures 18

A.3 Conservative extensions of a dynamical theory 27

A.4 Distributive lattices associated with a dynamic algebraic structure 30

A.5 Model theory 33

B Infinitary geometric theories 35

B.1 General 35

B.2 Barr's Theorem 37

II Finitary geometric theories for real algebra 39

Introduction 41

C Ordered fields 43

Introduction 43

C.1 About discrete ordered fields 44

C.2 Formal Positivstellensätze 48

C.3 Non discrete ordered fields 51

C.4 A non-archimedean non discrete ordered field 54

C.5 Non discrete real closed fields: position of the problem 57

C.6 General properties of continuous semialgebraic maps 61

C.7 Some questions 62

D f-rings 65

Introduction 66

D.1 Distributive lattices 66

D.2 l-groups 68

D.3 f-rings 72

D.4 Beyond purely equational theories 77

D.5 Back to ordered fields 80

D.6 The real lattice and spectrum of a commutative ring 83
<table><tr><td>E Non discrete real closed fields</td><td>85</td></tr><tr><td>Introduction</td><td>86</td></tr><tr><td>E.1 2-closed ordered field (or euclidean field)</td><td>86</td></tr><tr><td>E.2 Virtual roots</td><td>87</td></tr><tr><td>E.3 Real closed rings</td><td>93</td></tr><tr><td>E.4 Non discrete real closed fields</td><td>99</td></tr><tr><td>E.5 A non-archimedean non discrete real closed field</td><td>100</td></tr><tr><td>E.6 Use of virtual roots in constructive real algebra</td><td>104</td></tr><tr><td>E.7 Some questions</td><td>107</td></tr><tr><td>F The axiom of archimedianity</td><td>111</td></tr><tr><td>F.1 Archimedean non discrete real closed fields</td><td>111</td></tr><tr><td>F.2 Some questions</td><td>111</td></tr><tr><td>Conclusion</td><td>113</td></tr></table>

### III Improved version of the theory of non discrete real closed fields 115

<table><tr><td>Introduction</td><td>117</td></tr><tr><td>G O-minimal structures</td><td>119</td></tr><tr><td>H Rings of bounded real maps</td><td>121</td></tr><tr><td>H.1 Some reminders of the second part</td><td>121</td></tr><tr><td>H.2 Dynamical theory of rings of bounded real maps</td><td>121</td></tr><tr><td>H.3 Dynamical theory of compact real intervals</td><td>122</td></tr><tr><td>J A reinforced language and the first corresponding axioms</td><td>123</td></tr><tr><td>Introduction</td><td>123</td></tr><tr><td>J.1 The sorts of reinforced language</td><td>123</td></tr><tr><td>J.2 An abstraction principle</td><td>124</td></tr><tr><td>J.3 First structures on sorts Df<sub>m,n</sub></td><td>124</td></tr><tr><td>K Decisive axioms</td><td>127</td></tr><tr><td>K.1 Upper bound axioms</td><td>127</td></tr><tr><td>K.2 Axioms for smooth maps</td><td>129</td></tr><tr><td>K.3 Axioms of real closure or o-minimal closure</td><td>130</td></tr><tr><td>K.4 O-minimal structures</td><td>132</td></tr><tr><td>K.5 Some questions</td><td>133</td></tr><tr><td>General conclusion</td><td>135</td></tr></table>

<table><tr><td>References and index</td><td>139</td></tr><tr><td>References. Books</td><td>139</td></tr><tr><td>References. Articles</td><td>140</td></tr><tr><td>Notations index</td><td>147</td></tr><tr><td>Terms index</td><td>150</td></tr></table>
# Foreword

The memoir we present here is an unfinished development of the article [40]. Compared to that paper, however, we have modified the definition of continuous semialgebraic maps (Definition C.5.5), in the same spirit in which Bishop defines a continuous real map as a uniformly continuous map on any bounded interval.

Despite its unfinished nature and the many questions that we do not currently know how to answer, we hope that this paper will arouse interest for its original approach to the subject.

The paper is written in the style of constructive mathematics à la Bishop, i.e. mathematics with intuitionistic logic (see [Bishop, Bishop & Bridges, Bridges & Richman, CACM, MRR, CCAPM]).

Let us define real algebra as the study of the algebraic properties of real numbers, i.e., the properties of $\mathbb{R}$ formulable in a first-order formal theory on the language of strictly ordered rings defined by the signature

$$ \text{Signature: } \Sigma_{\text{Aso}} = (\cdot = 0, \cdot > 0, \cdot \ge 0; \cdot + \cdot, \cdot \times \cdot, \cdot - \cdot, 0, 1) $$

with possibly all or some of the constructive reals as constants. We can also envisage introducing new function symbols for well-defined (from a constructive point of view) maps $\mathbb{R}^n \to \mathbb{R}$ whose description is purely algebraic, such as the sup, inf maps and many continuous semialgebraic maps defined on $\mathbb{Q}$.

Real constructive algebra is not well understood! Constructive analysis (≈ certified methods in numerical analysis) is much better studied.

From a constructive point of view, real algebra is far removed from the usual classical theory of real closed fields à la Artin-Schreyer-Tarski, in which we assume that we have a sign test for the reals.

Most algorithms in classical real algebra fail with real numbers, because they require a sign test.

Even in constructive analysis, there could be interesting spin-offs from further study of real algebra. For example, it would help us to understand how to avoid using the axiom of dependent choice (which is common in Bishop's work).

The understanding of constructive real algebra can also be a first step towards a constructive (and therefore algorithmic) theory of o-minimal structures (cf. [Coste], [van den Dries]). The real line and the $\mathbb{R}^n$ spaces studied from a purely algebraic point of view can be seen as constituting the simplest of o-minimal structures. The classical (non-algorithmic) theory of o-minimal structures yields pseudo-algorithms which, in order to work correctly, require at least one sign test on the reals (sorts must also be introduced for the definable parts of $\mathbb{R}^n$). And the theory of o-minimal structures has, a priori, a very important area of applications in analysis.

Thus we are looking for as complete a dynamical theory as possible to describe the algebraic properties of the real number field in constructive mathematics without an axiom of dependent choice.

In the study we present here, we also avoid the use of negation. Fred Richman [59] shows that constructive mathematics is more elegant when the axiom of dependent choice is dispensed with. We believe that they are also more elegant if negation is dispensed with.
In the first part, consisting of Chapters A and B we give some general information on geometric theories and their dynamical version, dynamical theories. For the most part, we refer to sections 1 to 3 of the article [41].

The second part is devoted to the study of a geometric theory whose ambition is to describe exhaustively the algebraic properties of the real number field, and more generally of a *non* discrete real closed field, at least those expressible in a restricted language, close to the language of ordered rings. This constitutes a development, with some minor terminological modifications, of the ideas given in the article [40].

Chapter C proposes a definition of the ordered field structure in the absence of a sign test.

Chapter D deals with *f*-rings and some derived structures.

Chapter E tries to define the structure of a real closed ordered field in the absence of a sign test.

Chapter F discusses an infinitary geometric theory when we add the axiom that the real number field is *archimedean*.

So, at the end of this second part, we propose for the coveted dynamical theory that of the archimedean local real closed ring structure. The theory of real closed rings is presented here in an elementary, purely equational form, in the style of [69].

In the third part, we add the sorts corresponding to continuous semialgebraic maps on bounded closed semialgebraic subsets. In this way, we hope to obtain a more precise description of real algebra and to be able to sketch a first constructively satisfactory theory for o-minimal structures.

Throughout the text, theorems or lemmas in classical mathematics that have no known constructive proof, and often cannot have one, are indicated with a star.

Finally, the article [38] contains reflections, in a more philosophical framework, similar to those proposed here.

**Acknowledgements** We would like to thank Michel Coste and Marcus Tressl for their patient answers to our many questions.

Henri Lombardi, Assia Mahboubbi, 27th August 2024
# Part I

## Geometric theories
<figure><img src="image_2.png" /></figure>
# Introduction

This first part is the subject of a more detailed memoir in preparation [39], which can be found at:
http://hlombardi.free.fr/Theories-geometriques.pdf

We give the main definitions and refer for the main part to sections 1 to 3 of the article [41].

A dynamical theory can be understood as a formalisation of a well-defined piece of intuitive mathematics. This intuitive mathematics, practised by the mathematical community, is studied in a completely computational form independent of any philosophical point of view. But where the classical point of view makes free use of LEM<fnref n="1" /> and the axiom of choice, dynamical theories replace these non-computational tools with the dynamical point of view of incompletely specified structures, which is the point of view of lazy evaluation in Computer Algebra.

Chapter A deals with finitary dynamical theories.

A finitary geometric theory corresponds to what is known in classical mathematics as a coherent formal theory. But the geometric theory we are considering is governed by intuitionistic logic, whereas the coherent theory is generally governed by classical logic.

What's more, the corresponding dynamical theory is a minimalist version of the geometric theory: it's pure computational machinery without logic, rather similar to Goodstein's recursive arithmetic.

A dynamical theory can also be seen as a partial version of natural deduction, in which the formulas examined are all of a very simple type, without the implication connector (hence without negation) and with very limited use of quantifiers.

The surprise is that dynamical theories are nevertheless very expressive (in classical mathematics any first-order formal theory can be seen as a coherent theory) and that they erase the distinction between classical logic and intuitionistic logic.

In the frequent case where the signature is a countable set and the axioms form a decidable part of the language, the mathematical world outside the theory, which is where we situate ourselves in order to study a given structure, see how the formal system that describes it works, and establish theorems about it, has no interference with the dynamical theory itself. This is confirmed in a general way by the fundamental theorem A.3.6: if we force a finitary geometric theory to behave in a classical way, the dynamical rules written in the initial language that are valid afterwards were already valid before.

This corresponds to the fact that Grothendieck's coherent topos, which are another form of coherent theories, have an intuitionistic internal logic, but that they can nevertheless be understood in different ways depending on whether or not we are in a constructive external mathematical world.<fnref n="2" />

In constructive mathematics, only certain structures come under finite dynamical theories. For example, the discrete field structure, but not the Heyting field structure.<fnref n="3" /> In this respect, the restricted viewpoint of dynamical theories opens the way to a relevant classification, invisible in classical mathematics, concerning the degrees of complexity of mathematical beings invented by humans.

<footnote n="1">¹Law of Excluded Middle.</footnote>

<footnote n="2">²That is, essentially, whether or not we accept LEM in this external world.</footnote>

<footnote n="3">³A discrete field is a non-trivial ring in which every element is zero or invertible, and a Heyting field is a local ring in which every non-invertible element is zero. Classical mathematics does not know the relevant distinction between the notion of a discrete field and that of a Heyting field.</footnote>
Chapter B deals with infinitary dynamical theories, in which infinite disjunctions are allowed in the conclusion of a dynamical rule.

An essential restriction must be noted: the free variables present in such a disjunction must be specified in advance and in finite number.

Intuitively, such rules are used in the proof system of dynamical theories by “opening the branches of computation corresponding to the infinite disjunction”. What does this mean precisely? It means that a conclusion will be declared valid if it is valid in each of the branches.

These theories are more expressive than finitary theories and make it possible to axiomatise a very large number of common mathematical structures.

Unlike finitary dynamical theories, the external mathematical world inevitably intervenes to certify the validity of a dynamical rule.

Let's take a simple example and show what happens if the axioms contain an infinitary rule of the following type

$$ \vdash_{x_1, \dots, x_k} \mathbf{OP}_{i \in I} \Gamma_i $$

with an infinite set $I$ and the $\Gamma_i$ are lists of atomic formulas with no free variables other than those mentioned (i.e. $x_1, \dots, x_k$). If for each $i \in I$ we have a valid rule $\Gamma_i \vdash B(\underline{x})$, then we declare the rule $\vdash_{x_1, \dots, x_k} B(\underline{x})$ to be valid.

There is therefore necessarily an intuitive proof external to the dynamical theory to certify that the desired conclusion is valid in each of the branches. In fact, the computation system at work in the dynamical theory cannot handle such an infinite number of proofs. A purely mechanical computation cannot open up an infinite number of branches! For example, with $I = \mathbb{N}$ the external intuitive proof could be a proof by induction.

Note, on the other hand, that the internal proof must show the validity of the desired conclusion according to the rules of proof “without logic” of the dynamical theory.

**Terminology.** Since we are dealing with constructive mathematics, terminological problems inevitably arise, simply because, for example, the same classical concept generally gives rise to several interesting constructive concepts which are not equivalent, but which are equivalent in classical mathematics.

Below are small tables comparing our terminology (in constructive mathematics) and the most common English terminology (in classical mathematics) for geometric theories. The one found in [Johnstone, Sketches 2, Chapter D1], [Caramello] and in [4].

The comparison is somewhat biased by the fact that dynamical theories do not use logic as such. They are pure computational machines. Thus, although a finitary dynamical theory “generate” a (first-order formal) consistent theory and although every consistent theory admits a version “finitary dynamical theory”, they are not the same formal objects. Witness the fact that a coherent theory does not work in the same way with classical logic and with intuitionistic logic, whereas a dynamical theory is insensitive to this distinction because, structurally, dynamic proofs are always constructive.
Finitary geometric theories

<table><tr><td>Our terminology</td><td>Elephant</td></tr><tr><td>geometric theory</td><td>geometric theory</td></tr><tr><td>dynamical theory</td><td></td></tr><tr><td>purely equational</td><td>algebraic</td></tr><tr><td>direct</td><td></td></tr><tr><td>Horn</td><td>Horn</td></tr><tr><td>disjunctive</td><td></td></tr><tr><td>propositional</td><td>propositional</td></tr><tr><td>existential, or regular</td><td>regular</td></tr><tr><td>existentially rigid</td><td></td></tr><tr><td>existential existential rigid, or cartesian</td><td>cartesian</td></tr><tr><td>rigid</td><td>disjunctive, [29]</td></tr><tr><td>finitary dynamical</td><td></td></tr><tr><td>intuitionist coherent</td><td></td></tr><tr><td>classical coherent</td><td>coherent</td></tr></table>

General (infinitary) geometric theories

<table><tr><td>Theory</td><td>Theory</td></tr><tr><td>dynamical</td><td></td></tr><tr><td>geometric</td><td>geometric intuitionist</td></tr><tr><td>geometric classical</td><td>geometric</td></tr></table>

<table><tr><td>Dynamical theories</td><td>Geometric theories</td></tr><tr><td>identical (same signature)</td><td>equivalent</td></tr><tr><td>essentially identical (same sorts)</td><td></td></tr><tr><td>classically essentially identical (same sorts)</td><td>definitionally equivalent</td></tr><tr><td>essentially equivalent</td><td></td></tr><tr><td>classically essentially equivalent?</td><td>Morita equivalent</td></tr></table>
<figure><img src="image_3.png" /></figure>
# A. Finitary geometric theories

## Sommaire

<table><tbody><tr><td><strong>A.1 Coherent and finitary dynamical theories</strong></td><td><strong>12</strong></td></tr><tr><td>Coherent theories</td><td>12</td></tr><tr><td>Finitary dynamical theories</td><td>12</td></tr><tr><td>Logic replaced by computation</td><td>13</td></tr><tr><td>Equality predicate</td><td>14</td></tr><tr><td>Simple extension of a dynamical theory</td><td>14</td></tr><tr><td>Structural rules</td><td>14</td></tr><tr><td>Collapsus</td><td>16</td></tr><tr><td>Classification of dynamical theories</td><td>17</td></tr><tr><td>Horn theories</td><td>17</td></tr><tr><td>Disjunctive theories</td><td>17</td></tr><tr><td>Existential theories</td><td>17</td></tr><tr><td>Existentially rigid, cartesian theories</td><td>17</td></tr><tr><td>Rigid theories</td><td>17</td></tr><tr><td>Propositional theories</td><td>17</td></tr><tr><td><strong>A.2 Dynamic algebraic structures</strong></td><td><strong>18</strong></td></tr><tr><td>Definitions, examples</td><td>18</td></tr><tr><td>Positive diagram of an algebraic structure</td><td>21</td></tr><tr><td>Constructive versus classical models</td><td>21</td></tr><tr><td>Morphisms between dynamic algebraic structures of the same type</td><td>21</td></tr><tr><td>Examples</td><td>22</td></tr><tr><td>Primitive recursive arithmetic</td><td>23</td></tr><tr><td>Goodstein's formal system</td><td>23</td></tr><tr><td>A finitary geometric theory for primitive recursive arithmetic</td><td>24</td></tr><tr><td><strong>A.3 Conservative extensions of a dynamical theory</strong></td><td><strong>27</strong></td></tr><tr><td>Essentially equivalent extensions</td><td>27</td></tr><tr><td>Comparison with intuitionistic logic</td><td>28</td></tr><tr><td>Fundamental theorem of dynamical theories</td><td>28</td></tr><tr><td>Skolemisation</td><td>29</td></tr><tr><td><strong>A.4 Distributive lattices associated with a dynamic algebraic structure</strong></td><td><strong>30</strong></td></tr><tr><td>Distributive lattices and entailment relations</td><td>30</td></tr><tr><td>The spectrum of a distributive lattice</td><td>30</td></tr><tr><td>Stone's antiequivalence</td><td>31</td></tr><tr><td>The Zariski lattice and spectrum of a commutative ring</td><td>31</td></tr><tr><td>Other examples</td><td>32</td></tr><tr><td>First example.</td><td>32</td></tr><tr><td>More generally</td><td>33</td></tr><tr><td>Case of an extension T<sub>1</sub> which reflects valid disjunctive rules.</td><td>33</td></tr></tbody></table>
<table><tr><td>Zariski lattices, however, give a lesser image</td><td>33</td></tr><tr><td><b>A.5 Model theory</b></td><td><b>33</b></td></tr><tr><td>Completeness theorem, simultaneous collapse</td><td>33</td></tr><tr><td>Representation theorem, theories proving the same Horn rules</td><td>34</td></tr></table>

# A.1. Coherent and finitary dynamical theories

## Coherent theories

A coherent theory $\mathcal{T} = (\mathcal{L}, \mathcal{A})$ is a first-order formal theory based on the language $\mathcal{L}$ in which the axioms (the elements of $\mathcal{A}$) are all “geometric”, i.e. of the following form:

$$ \forall \underline{x} \ (C \implies \exists \underline{y}^1 D_1 \lor \dots \lor \exists \underline{y}^m D_m) \qquad (A.1) $$

where $C$ and the $D_j$ are conjunctions of atomic formulas of the language $\mathcal{L}$ of the formal theory, the $\underline{y}^j$ are lists of variables, and $\underline{x}$ is the list of other occuring variables (these lists may be empty). The variables in $C$ are only in the $\underline{x}$ list. The variables in $D_j$ are only in the disjoint lists $\underline{x}$ and $\underline{y}^j$. An empty disjunction in the second member can be replaced by the symbol $\perp$ representing **False**.

We also say finite geometric theory instead of coherent theory when we use intuitionist logic.

In the remainder of Chapter A, we almost always omit the qualifier “finitary” before “geometric theory” or “dynamical theory”

## Finitary dynamical theories

Main reference [17]. This article introduces the notions of “dynamical theory” and “dynamical proof”. See also: the article [6, Bezem & Coquand, 2005] which describes a number of advantages provided by this approach, and the precursor articles [55, Prawitz 1971, sections 1.5 and 4.2], [53, Matijasevič 1975] and [33, Lifschitz, 1980].

If $\mathcal{T}$ is a (finitary) geometric theory, the corresponding (finitary) dynamical theory differs from it only by an extremely limited use of proof methods:

* Firstly, no formulas other than atomic formulas are ever used: no new predicates using logical connectors or quantifiers are ever introduced. Only lists of atomic formulas from the $\mathcal{L}$ language are manipulated.

* Secondly, and in accordance with the previous point, axioms are not seen as true formulas, but as deduction rules: an axiom such as (A.1) is used as a rule (A.2)

$$ \Gamma \vdash \text{Introduce } \underline{y}^1 \text{ such that } \Delta_1 \text{ op } \dots \text{ op Introduce } \underline{y}^m \text{ such that } \Delta_m \qquad (A.2) $$

Here the conjunctions of atomic formulas $C, D_1, \dots, D_m$ of (A.1) have been replaced by the corresponding lists $\Gamma, \Delta_1, \dots, \Delta_m$.

* Thirdly, we only prove dynamical rules, i.e. theorems which are in the form of the deduction rules above.

* Fourth, the only way to prove a dynamical rule is by a tree computation “without logic”. At the root of the tree are all the hypotheses of the theorem we want to prove. The tree develops by applying the axioms according to pure algebraic computation machinery in the structure. See Examples A.1.1. The precise formal definitions are given in [17], we extend them to the case where there are several types of objects as in the theory of modules on a commutative ring with objects of type “elements of the ring” and objects of type “elements of the module”.
When we apply an axiom such as (A.2), we substitute arbitrary terms ($t_i$) from the language for the free variables ($x_i$) present in the rule. If the hypotheses, rewritten with these terms, are already proven, then branches of computation are opened in each of which fresh variables corresponding to the dummy variables $y^k$ are introduced (their names may have to be changed to avoid conflict with the free variables present in the $t_i$ terms) and each conclusion $B_k$ is valid in its branch.<fnref n="1" />

The very elementary examples A.1.1 show how to validate a dynamic rule in a given dynamical theory. We develop a computation tree using the axioms of the dynamical theory as indicated above and we have won when, at each leaf of the tree, the conclusion is validated.

**Examples A.1.1.** The dynamical theory *Cd* of discrete bodies is based on the language of commutative rings and its axioms are those of non-trivial commutative rings (theory *Ac* in the example A.2.1) and the dynamic rule for discrete fields:

CD $\vdash$ $x = 0$ op Introduce y such that $xy = 1$

1) To demonstrate the dynamic rule

ASDZ $xy = 0 \vdash x = 0$ op y = 0$

we open two branches in accordance with the axiom **CD**. In the first we have $x = 0$ and the conclusion is proved. In the second, we introduce a "parameter" (a fresh variable) $z$ with the relation $xz = 1$. The axioms of commutative rings can then be used to prove the equalities $y = 1$ times $y = (xz)y = (xy)z = 0$ times $z = 0$. The conclusion is therefore validated for each of the two leaves of the tree.

2) Then, for example, we deduce from the previous dynamic rule the rule

Anz $z^2 = 0 \vdash z = 0$

because this time both leaves of the tree have the same conclusion $z = 0$.

3) The theory *Al* of local rings is based on the language of commutative rings and its axioms are those of commutative rings (theory *Ac0* in Example A.2.1) and the dynamic rule for local rings

AL $(x+y)z = 1 \vdash$ Introduce u such that $xu = 1$ op Introduce u such that $yu = 1$

To prove that a discrete field satisfies the rule **AL**, we open two branches in accordance with the axiom **CD**. In the first, we have $x = 0$ and the conclusion is proved because $(x+y)z = 1$ gives $yz = 1$. In the second we introduce a "parameter" (a fresh variable) $v$ with the relation $xv = 1$. The conclusion in the rule **AL** is therefore proven at both leaves of the calculation tree. ■

Note also that the validity of the following rule, which could be called "Concrete existence implies formal existence", is purely tautological.

Let us consider a list $\Gamma(\underline{x}, \underline{y})$ of atomic formulas in a dynamical theory $\mathcal{T}$. Let us denote $\Gamma(\underline{x}, \underline{t})$ the list of these formulas in which we have substituted for each variable $y_j$ a term $t_j$ constructed on the $x_i$ and on the constants of the theory. Then the following existential rule is valid.

$$ \Gamma(\underline{x}, \underline{t}) \vdash \exists y_1, \dots, y_m \Gamma(\underline{x}, \underline{y}). $$

### Logic replaced by computation

In practice, proving a dynamical rule within the framework of a dynamical theory always follows an intuitive natural reasoning, and this gymnastics can be seen as a simplified version of Gentzen's natural deduction. The symbol **op** should be understood as an abbreviation for "open (branches in the calculation)".

The symbols **op** and **Introduce** · **such that** have been preferred to $\mathbf{V}$ and $\exists$, to make it clear that their use in deduction rules is not the use of new formulas constructed from atomic formulas.

<footnote n="1">¹$B_k$ is the list $\Delta_k$ in which the $x_i$ variables have been replaced by the $t_i$ terms.</footnote>
The symbol $\vdash$ has been preferred to $\vdash$ to avoid confusion with the symbol used for entailment relations in distributional lattices. Note also that it does not have the same interpretation as the analogous symbol used in Gentzen-style sequence calculations.

Thus the language of a dynamical theory contains no logical symbols (connectors or quantifiers) that can be used to construct complicated formulas from atomic formulas. The “logic” is replaced by the symbols $\vdash$, `op` and **Introduce** · **such that** and by the separator “, ”, but these symbols are used to describe a machinery of arborescent calculations and not to form formulas. The non-logical part of a dynamical theory consists of symbols for variables, and the *signature*, which contains symbols for sorts, predicates and functions.

> In the following, we replace “**Introduce** · **such that** ... ” with the less cumbersome “∃ ... ”, which is closer to and yet different from the traditional “∃ ... ”.

• **Equality predicate**

In a dynamical theory each sort must be provided with an equality predicate $\cdot = \cdot$ and we give the axioms which authorise the substitution of a term $t$ by a term $t'$ when $\vdash t = t'$ is valid in the theory<fnref n="2" /> in any occurrence of an atomic formula present in a valid dynamical rule.

We could just as well not give any axioms relating to this substitution and consider that it is simply a legitimate calculation procedure.

• **Simple extension of a dynamical theory**

**Definition A.1.2.** It is said that the dynamical theory $\mathcal{T}' = (\mathcal{L}', \mathcal{A}')$ is a simple extension of the dynamical theory $\mathcal{T} = (\mathcal{L}, \mathcal{A})$ if $\mathcal{L} \subseteq \mathcal{L}'$ and $\mathcal{A} \subseteq \mathcal{A}'$. In this case the dynamical rules formulated in $\mathcal{L}$ and valid (i.e. demonstrable) in $\mathcal{T}$ are valid in $\mathcal{T}'$.

**Remark A.1.3.** In the previous definition, the expression “simple extension” can be questioned. If $\mathcal{L}, \mathcal{A}, \mathcal{L}', \mathcal{A}'$ are finite sets, or if they are discrete countable sets, we can consider that everything is intuitively clear. However, it may happen that we wish to use more complicated sets, for example to introduce all the reals as constants in a theory of which one sort is intended to describe the real numbers. In such a case, the word “simple extension” is questionable because there is no canonical monomorphism in Bishop’s category **Set**: in Bishop’s conception, a part of a set corresponds to the categorical notion of a subobject. In this framework, therefore, “simplicity” is not an objective notion, or if you prefer, it has no precise mathematical definition. ■

Structural rules

Here we give *admissible structural rules* for a dynamical theory. These are *external deduction rules* (different from dynamical rules, which are internal to the theory). They say that if certain dynamical rules are valid, then other dynamical rules are automatically valid.

Here are the admissible structural rules that we feel are the most important.

Admissible structural rules A.1.4.

0. *Free variables, dummy variables*

(a) *Substitution*. In a dynamical rule, you can replace all occurrences of a free variable with a term, provided that you never create a conflict between free and dummy variables.

(b) *Renaming*. In a dynamical rule, you can rename free variables or dummy variables (those present in the $∃$) as long as you never create a conflict between free and dummy variables.

<footnote n="2">²This excludes the case where $t$ contains a variable $x$ under the dependence of an $∃x$.</footnote>
1. Benefit from work already done

(a) *Shortcuts*. Once the validity of a dynamical rule has been demonstrated, it can be added to the axioms of the theory.

(b) *Simultaneous reinforcement of hypothesis and conclusions*. In a dynamical theory, we consider a valid rule

$$ \Gamma \vdash \exists y^1 \Delta_1 \mathbf{op} \dots \mathbf{op} \exists y^m \Delta_m $$

Let A be an atomic formula which does not involve any of the existential variables of the second member. Let $\Gamma'$ be the list $\Gamma$ followed by A and $\Delta'_i$ the list $\Delta_i$ followed by A. Then the following rule is also valid:

$$ \Gamma' \vdash \exists y^1 \Delta'_1 \mathbf{op} \dots \mathbf{op} \exists y^m \Delta'_m $$

2. Lists as finite sets

(a) *Permutation of atomic formulas appearing in a list.*

(b) *Contraction* If two identical atomic formulas appear in a list, one of the two can be deleted.
Conversely, you can duplicate an atomic formula in an arbitrary list.

(c) *Monotony*. Atomic formulas can be added as required to the list to the left of $\vdash$.

(d) *Permutation, contraction and monotony for the op to the right of the $\vdash$.*

3. Lists of atomic formulas as conjunctions

(a) *To prove a list of atomic formulas is to prove each of them.* In a theory, consider a dynamical rule $\Gamma \vdash (A_1, \dots, A_n)$. This dynamical rule is valid if, and only if, the rules $\Gamma \vdash A_k (k \in [1..n])$ are valid.

(b) *Distributivity of op on the implicit “and” in the lists.* In a theory, we consider a dynamical rule

$$ \Gamma \vdash (A_1, \dots, A_n) \mathbf{op} \exists y^1 \Delta_1 \mathbf{op} \dots \mathbf{op} \exists y^m \Delta_m. $$

This dynamical rule is valid if, and only if, the following dynamical rules are valid

$$ \Gamma \vdash A_k \mathbf{op} \exists y^1 \Delta_1 \mathbf{op} \dots \mathbf{op} \exists y^m \Delta_m \quad (k \in [1..n]). $$

4. Transitivity and variants

(a) *Transitivity*. We give an example, leaving it to the reader to give the general formulation.
Let us suppose that we have valid dynamical rules in a dynamical theory

$$ \Gamma(\underline{x}) \vdash \exists y, z \Delta_1(\underline{x}, y, z) \mathbf{op} \exists u \Delta_2(\underline{x}, u), $$

$$ \Gamma(\underline{x}), \Delta_1(\underline{x}, y, z) \vdash \exists r, s, t \Delta_3(\underline{x}, y, z, r, s, t), $$

$$ \Gamma(\underline{x}), \Delta_2(\underline{x}, u) \vdash \exists v \Delta_4(\underline{x}, u, v) \mathbf{op} \exists w \Delta_5(\underline{x}, u, w). $$

Then the rule

$$ \Gamma(\underline{x}) \vdash \exists y, z, r, s, t \Delta_3(\underline{x}, y, z, r, s, t) \mathbf{op} \exists u, v \Delta_4(\underline{x}, u, v) \mathbf{op} \exists u, w \Delta_5(\underline{x}, u, w). $$

is also valid.

(b) *Cut*. Consider lists of atomic formulas $\Gamma(\underline{x}), \Delta_0(\underline{x}), \Delta_1(\underline{x}), \dots, \Delta_m(\underline{x})$ ($m \ge 1$) in a dynamical theory $\mathcal{T}$. If the two dynamical rules

$$ \Gamma \vdash \Delta_0 \mathbf{op} \Delta_1 \mathbf{op} \dots \mathbf{op} \Delta_m \quad \text{and} \quad \Gamma, \Delta_0 \mathbf{op} \Delta_1 \mathbf{op} \dots \mathbf{op} \Delta_m $$

are valid in $\mathcal{T}$, then the rule $\Gamma \vdash \Delta_1 \mathbf{op} \dots \mathbf{op} \Delta_m$ is also valid.
(c) *Cut with existence.* A more general version is as follows. Consider lists of atomic formulas $\Gamma(x), \Delta_0(x, y^0), \Delta_1(x, y^1), \dots, \Delta_m(x, y^m)$ ($m \ge 1$) dans une dynamical theory $\mathcal{T}$ ($m \ge 1$) in a dynamical theory $\mathcal{T}$. If the two dynamical rules

$\Gamma \vdash \exists y^0 \Delta_0 \ op \ \exists y^1 \Delta_1 \ op \ \dots \ op \ \exists y^m \Delta_m$ and $\Gamma, \Delta_0 \vdash \exists y^1 \Delta_1 \ op \ \dots \ op \ \exists y^m \Delta_m$ are valid in $\mathcal{T}$, then the rule $\Gamma \vdash \exists y^1 \Delta_1 \ op \ \dots \ op \ \exists y^m \Delta_m$ is also valid.

## Collapsus

A dynamical rule is called a *collapse rule* when the second member is “False”, which we note $\bot$. We can also see $\bot$ as designating the empty disjunction. Once $\bot$ has been proved, the universe of discourse collapses, and every atomic formula is then deemed to be “true”, or at least “valid”. This is the application of the rule “ex falso quod libet”, which is the relevant intuitive meaning of False in constructive mathematics. Thus in dynamical theories the rules

False$_P$ $\bot \vdash P$ (ex falso quod libet)

are valid for all atomic formulas.

In the language, we also give the logical constant $T$ for “True”, with the following Horn rule as its axiom.

True $\vdash T$

We can also see $T$ as designating the empty conjunction.<fnref n="3" /> The constants $\bot$ and $T$ are the only logical symbols in dynamical theories.

When a dynamical theory has no collapse rule, it always admits the model reduced to a point<fnref n="4" /> where all atomic formulas are evaluated true. This is the final object in the category of models of the theory.

We can say that a dynamical theory without a collapse rule collapses if all the atomic formulas are valid, with the exception of $\bot$.

A dynamical theory with a collapse rule is said to collapse when $\bot$ is provable, and consequently so are all the dynamical rules. In this case the theory admits no model.

To consider collapse in the sense of a single model reduced to a point, rather than in the sense of pure nothingness, is merely a matter of taste which changes nothing in the essence of things.<fnref n="5" />

Instead of saying that a collapsing dynamic algebraic structure has no model, we say (without negation) that any model of this dynamic algebraic structure is trivial, reduced to a point, and that “everything in it is true”.

To formally reconcile these two points of view, the best solution seems to be the following: each sort $S$ introduced is accompanied by at least two constants in this sort, say $0_S$ and $1_S$ to fix ideas, with the axiom $0_S = S 1_S \vdash \bot$. In what follows, this is what would normally happen for the theory of non-trivial distributive lattices and the theory of non-zero commutative rings, as well as in all their extensions. But we prefer to use the following convention.

> Throughout this memoir, in the case of a ring or a distributive lattice, we consider that the collapse is always given in the form $0 = 1$ or a formula of the same style, for example $0 > 0$ for an ordered field. One disadvantage of using the symbol $\bot$ is that it takes us out of the realm of Horn theories when we could be staying there. Readers who so wish can add an axiom of the type $0 = 1 \vdash \bot$.

<footnote n="3">³When there's nothing to prove, let's prove nothing and everything will be OK. Moreover, in a dynamical theory with at least one sort $S$, $T$ is equivalent to $x =_S x$.</footnote>

<footnote n="4">⁴If there are several sorts, each sort is reduced to a point.</footnote>

<footnote n="5">⁵In fact, one of the authors must have a horror of the void :), the silence of this infinite space frightens him :(. Moreover, if total disappearance into nothingness is the true meaning of False, the fact remains that, even before forbidding the existence of models, False begins by reducing them to a single point, which satisfies all the predicates. As Boris Vian's song says: "on est descendu chez Satan et en bas c'était épatant!".</footnote>
# Classification of dynamical theories

## Horn theories

A dynamical rule which does not contain to the right of the symbol $\vdash$ either **op**, or $\exists$ or $\bot$ is called a *Horn rule*. A dynamical theory is said to be *Horn* when it contains only Horn rules as axioms. In the french version of this paper and in the paper [17], Horn theories are called *théories algébriques*. A special case is provided by purely equational theories, which are Horn theories with a single sort and the only predicate being the equality predicate.

*Note.* We use the following terminology from [17]. A Horn rule is said to be *direct* when, to the left of the symbol $\vdash$, there are only atomic formulas relating to variables different from each other or to constants. The other Horn rules are called *simplification rules*. For example, in the two examples below, the first is direct, the second is not.

$$ \bullet x = 0, y = 0 \vdash x + y = 0 $$

$$ \bullet x + y = 0, x = 0 \vdash y = 0 $$

## Disjunctive theories

A dynamical theory is said to be *disjunctive* if in the axioms there are no $\exists$ to the right of the $\vdash$.

## Existential theories

A dynamical rule is said to be *simple existential* if the second member (the conclusion) is of the form $\exists y \Delta$ where $\Delta$ is a finite list of atomic formulas.

A dynamical theory is said to be *existential* if its axioms are all simple algebraic or existential rules (a Horn rule can also be considered as a special case of a simple existential rule). A typical existential theory is the theory of *Bézout rings* (any finitely generated ideal is principal). In the English literature on categorical logic (studied in the context of classical mathematics), an existential theory is called a *regular theory*. In the french version of this paper an existential theory is called a *théorie existentielle*

## Existentially rigid, cartesian theories

Existentially rigid theories are dynamical theories in which the existential axioms are simple and correspond to unique existences. This generalises (very slightly) the disjunctive theories.

An existentially rigid theory is said to be cartesian. This generalises (very slightly) Horn theories.

## Rigid theories

A dynamical theory is said to be *rigid* if it is existentially rigid and if the disjuncts of the second member in the disjunctive axioms are two by two incompatible. For example, the theory of discrete fields is rigid, but the theory of local rings is not. The theory of real closed discrete fields can be stated rigidly, but the theory of algebraically closed discrete fields cannot. See [29], who uses the terminology “disjunctive theory” where we use “rigid theory”.

## Propositional theories

The (classical or intuitionistic) logic of propositions has a very abstract character, which may seem useless from a dynamic point of view, since it is already present in the form of some of the admissible structural rules A.1.4. However, it is useful for the definition of distributive lattices associated with dynamic algebraic structures (Section A.4.)

The logic of propositions can be presented in a minimal dynamic form as follows, without any sort, which implies that the constants must be interpreted as pure abstract truth values (in classical logic they only hesitate between True and False).

The constants are therefore $\bot$, $T$, and *propositional constants* or *propositions*. To define such a theory ($\mathcal{L}, \mathcal{A}$), we give a set $G$ of propositional constants.<fnref n="6" /> and a set $\mathcal{A}$ of axioms which are disjunctive rules on the language $\mathcal{L}$)

<footnote n="6">⁶This fixes the language $\mathcal{L}$ via the signature $\{G, T, \bot\}$</footnote>
First we have the axioms $\perp \vdash p$ and $p \vdash \top$, and the axioms which handle equality in $G$: $p \vdash q$ each time $p =_G q$. If $G$ is not a discrete set, these axioms reflect the structure of the set $G$ in the informal category *Set*.

The additional axioms given in $\mathcal{A}$ are of the type $p_1, p_n \vdash q_1 \ op \ \dots \ op \ q_m$ where $p_i$ and $q_j$ are constants in $G$ (with possibly $m = 0$ or $n = 0$).

Two constants $p$ and $q$ are said to be *opposite* or *complementary* if they satisfy the axioms of negation

$$ \bullet \vdash p \ op \ q $$

$$ \bullet p, q \vdash \perp $$

While classical propositional logic can be interpreted as given by dynamical theories without any sort of the type described above, the same cannot be said for intuitionistic logic. Indeed, the $\Rightarrow$ connector cannot be described by restricting ourselves to dynamical theories. Obviously, this connector can be introduced into the language, but the external structural rule used to introduce implication in natural deduction cannot be formulated as a dynamical rule.

## A.2. Dynamic algebraic structures

References: [17], [37], [41].

The dynamic algebraic structures are explicitly named in [37]. In [17], they are implicit, but explicit in the form of their presentation. They are also implicit in [36], and, last but not least, in [18, D5, 1985], which has been an essential source of inspiration: one can compute safely in the algebraic closure of a discrete field, even when it is not possible to construct this algebraic closure. It is therefore sufficient to consider the algebraic closure as a dynamic algebraic structure “à la D5” rather than as a usual algebraic structure: *lazy evaluation in D5 provides a constructive semantics for the algebraic closure of a discrete field*.

### Definitions, examples

**Example A.2.1.** Our first example is the purely equational theory of commutative rings (with only one sort, called $Ac$) in which most of the calculations are entrusted to machines outside the formal theory. This possibility is based on the fact that the elements of the ring $\mathbb{Z}[x_1, \dots, x_n]$ can be reduced to a predefined normal form. This implies that the equality of two terms is equivalent to the identity of their normal forms. Consequently, the binary equality predicate can be replaced by the equality to 0 predicate.

The theory $Ac$ of commutative rings is written on the following signature. There is only one sort, called $Ac$.

$$ \text{Signature: } \Sigma_{Ac} = (\cdot =_{Ac} 0 ; \cdot + , \cdot \times , \cdot, - , 0_{Ac}, 1_{Ac}) $$

The only axioms are the following (these are direct rules):$^7$

$$ \mathbf{ac0} \vdash 0_{Ac} =_{Ac} 0 $$

$$ \mathbf{ac1} \quad x =_{Ac} 0 \vdash_{x,y:Ac} x \times y =_{Ac} 0 $$

$$ \mathbf{ac2} \quad x =_{Ac} 0, y =_{Ac} 0 \vdash_{x,y:Ac} x + y =_{Ac} 0 $$

The term “$x - y$” is an abbreviation for “$x + (-y)$” and the binary predicate “$\cdot =$” is defined by convention: “$x = y$” is an abbreviation for “$x - y = 0$”.

We often consider the theory $Ac$ of *non-trivial commutative rings*, which is obtained from $Ac$ by adding the collapse axiom

$$ \mathbf{CL}_{=,Ac} \quad 1 =_{Ac} 0 \vdash \perp $$

<footnote>$^7$The names of the rules are written as follows: for the direct rules, all lower case, for the other Horn rules (the simplification rules), the first letter in upper case, and finally the other dynamical rules, all upper case.</footnote>
### Explanations.

1. The rules that define the $Ac0$ theory of commutative rings must be understood precisely as follows. Any term of the theory can be seen as a polynomial with integer coefficients in the present variables. We then use the computational machinery of commutative polynomials with integer coefficients ("external" to the theory), which rewrites any term (formed over constants and variables) as a polynomial with integer coefficients in a predefined normal form.

The distributivity rule $x(y + z) =_{Ac} xy + xz$, for example, is then entrusted to an automatic calculation which reduces to 0 the term $x(y + z) - (xy + xz)$.

Similarly, the transitivity of binary equality is handled by the rule **ac2** and by the automatic calculation which reduces the term $(x - y) + (y - z)$ to $(x - z)$.

2. In the three rules **ac0**, **ac2** and **ac1** we recognise the axioms of ideals, which make it possible to create a quotient ring structure, and which signify the compatibility of equality with addition and multiplication. In the $Ac0$ theory, any atomic formula is of the form "$t(x_1, \dots, x_n) =_{Ac} 0$" where $x_i$'s are variables and $t$ a term of the language. Any atomic formula is therefore immediately equivalent to an atomic formula in which $t$ is an element of the ring $\mathbb{Z}[x_1, \dots, x_n]$, written in the agreed normal form. The $Ac0$ theory is therefore the "the theory of algebraic identities", in the old sense of the expression. Precisely, it is easy to check that the validity of a simple Horn rule such as

$$ \bullet \quad p_1 =_{Ac} 0, \dots, p_m =_{Ac} 0 \vdash_{x_1, \dots, x_r : Ac} q =_{Ac} 0 $$

means exactly that the polynomial $q \in \mathbb{Z}[x_1, \dots, x_r]$ is in the ideal generated by the polynomials $p_1, \dots, p_m$ of $\mathbb{Z}[x_1, \dots, x_r]$. This property is rather difficult to decide.<fnref n="8" />

The dynamical theory of a purely equational theory does not provide any additional tool to the purely equational theory itself. There is therefore nothing really "dynamic" about purely equational dynamical theories. The really interesting dynamical theories are obtained by adding dynamical axioms to Horn theories.

For the theory $Ac0$ the validity of more complicated rules than those considered above is handled by the structural rule 3a page 15.

3. The theory $Ac0$ as it is presented does not seem "purely equational" at first sight because the axioms are not simple equalities between terms. This is due to our decision to replace equality with the unary predicate "$\cdot = 0$" accompanied by the external computational machinery of polynomials with integer coefficients. This approach has the advantage, in our opinion, of showing the true logical structure of the theory by reducing it to three very simple axioms and by entrusting to an automatic calculation what can be entrusted to it, which has little to do with logic proper. The same remark will subsequently apply to many theories that we will describe as purely equational.

**Definition A.2.2.** If $\mathcal{T} = (\mathcal{L}, \mathcal{A})$ is a dynamical theory, a *dynamic algebraic structure of type* $\mathcal{T}$ is given by a set $G$ of *generators* and a set $R$ of *relations*. A "relation" is by definition an atomic formula $P(\underline{t})$ constructed on the language $\mathcal{L} \cup G$ with closed terms $t_i$ in this language. Such a relation is associated with the axiom "$\vdash P(\underline{t})$" of the dynamic algebraic structure. So, this dynamic algebraic structure is the dynamical theory $(\mathcal{L} \cup G, \mathcal{A} \cup R)$, also denoted by $((G, R), \mathcal{T})$.

**Example A.2.3.** For example, we obtain a dynamic algebraic structure for a discrete field

$$ K = ((G, R), Cd) $$

by taking $G = \{a, b\}$ and $R = \{105 = 0, a^2 + b^2 - 1 = 0\}$. This dynamic discrete field corresponds to any discrete field of characteristic 3 or 5 or 7 generated by two elements $\alpha$ and $\beta$ satisfying $\alpha^2 + \beta^2 = 1$.

In addition to the dynamical rules valid in all discrete fields, there are now those obtained by extending the language with the constants taken from $G$ and by adding to the axioms the relations taken from $R$. For example the disjunctive rule

<footnote n="8">⁸This follows for example from Theorem VIII-1.5 in [MRR].</footnote>
$$ \bullet 3 = 0 \ \mathbf{op} \ 5 = 0 \ \mathbf{op} \ 7 = 0 $$

is valid, and so is the dynamical rule

$$ \bullet \exists z 15z = 1 \ \mathbf{op} \ \exists z 21z = 1 \ \mathbf{op} \ \exists z 35z = 1 $$

■

**Definitions and notations A.2.4.**

Let $\mathbf{S} = ((G, R), \mathcal{T})$ be a dynamic algebraic structure of type $\mathcal{T} = (\mathcal{L}, \mathcal{A})$.

* We will indicate that the rule “$\Gamma \vdash \dots$” is valid in the dynamic algebraic structure $\mathbf{S}$ in the following abbreviated form: “$\Gamma \vdash_{\mathbf{S}} \dots$”. We could also use the notation “$R, \Gamma \vdash_{\mathcal{T}} \dots$”, which means that the proof can use a finite list of axioms extracted from $R$.

* The set of closed terms of $\mathbf{S}$, i.e. the terms built on $\mathcal{L} \cup G$, is denoted by $\mathrm{Tcl}(\mathbf{S})$. The set of closed atomic formulas is denoted by $\mathrm{Atcl}(\mathbf{S})$.

* An Horn rule $\vdash P$ for $P \in \mathrm{Atcl}(\mathbf{S})$ is called a *fact in S*. The set of valid facts in $\mathbf{S}$ is called $\mathrm{Atclv}(\mathbf{S})$. A fact only concerns syntactically definable objects in the structure. It is clear that $\mathbf{S}$ proves exactly the same dynamical rules as the dynamic algebraic structure $\tilde{\mathbf{S}} = ((\mathrm{Tcl}(\mathbf{S}), \mathrm{Atclv}(\mathbf{S})), \mathcal{T})$.

Concrete algebra very often consists of proving facts or dynamic rules in particular dynamic algebraic structures. It is a little more general than the (inexhaustible) theory of algebraic identities, i.e. the universal algebra behind a large proportion of the great theorems of abstract algebra.

In the case of a Horn theory $\mathcal{T}$, a dynamic algebraic structure of type $\mathcal{T}$ gives a usual algebraic structure, defined by generators and relations, satisfying the required Horn rules.

The dynamic method is often a practical way of constructing algebraic identities ("Positivstel- lensätze" for example), following as closely as possible the paths indicated in the proofs given in classical mathematics.

In a dynamic algebraic structure a fact $P(t)$ is absolutely true if it is provable (i.e. if the rule “$\vdash P(t)$” is valid). It is absolutely false, or more precisely catastrophic if “$P(t) \vdash \bot$” is valid. There are many possibilities in between these two cases: a dynamic algebraic structure does not have a single fixed model, but represents all the possible ideal realisations of the structure in the potential state (this notion remains deliberately vague). Adding a catastrophic fact as an axiom amounts to eliminating all models.<fnref n="9" />

**Example A.2.5.** We consider a presentation $(G, R)$ in the language of $\mathcal{A}_c$. Let $\mathcal{T}$ be a dynamical theory which extends the theory $\mathcal{A}_c$ without extending the language, for example the theory $\mathcal{C}d$ of discrete fields. Any closed term of the dynamic algebraic structure $((G, R), \mathcal{T})$ is rewritten as a polynomial $f(x) \in \mathbb{Z}[G]$ with integer coefficients in the “constants” $x_i \in G$ of the dynamic algebraic structure. The elements of $R$ are relations $f(x) = 0$, so that by a slight abuse of language, we can consider $R$ as a set of elements of $\mathbb{Z}[G]$.

We are therefore studying the ring $\mathbf{A} = \mathbb{Z}[G]/\langle R \rangle$, or more precisely what happens to this ring when we ask it to satisfy certain new axioms. We will note $\mathcal{T}(\mathbf{A})$ the dynamic algebraic structure $((G, R), \mathcal{T})$.

In many examples, the theory collapses if, and only if, $\mathbf{A}$ is trivial. For example, the dynamic algebraic structure $\mathcal{C}d(\mathbf{A})$ collapses if, and only if, $1 =_{\mathbf{A}} 0$. In classical mathematics we say: indeed a non-trivial ring has a prime ideal $\mathfrak{p}$, and the field of fractions of the integral ring $\mathbf{A}/\mathfrak{p}$ is a non-trivial model of $\mathcal{C}d(\mathbf{A})$. More simply, without using model theory or the axiom of the prime ideal, we transform a proof of $1 = 0$ in $\mathcal{C}d(\mathbf{A})$ into a proof of $1 = 0$ in $\mathcal{A}_c(\mathbf{A})$ (proof analogous to that of [17, Theorem 2.4]).

<footnote n="9">⁹In the variant where the collapse reduces all models to a singleton: ... amounts to allowing only the trivial model.</footnote>
Concerning the facts $\theta = 0^{10}$ valid in the theory $\mathcal{T}(\mathbf{A})$, the situation is a little more complicated.
The theory of local rings $\mathcal{Al}$ proves $\theta = 0$ exactly when $\theta = {}_{\mathbf{A}}0$, hence the great importance of
local rings in commutative algebra.

The theory $\mathcal{Cd}$ proves $\theta = 0$ exactly when $\theta \in \hat{\mathbb{Q}}\sqrt{0}$. This corresponds to the reduced quotient
of $\mathbf{A}$: if $\theta = 0$ in $\mathcal{Cd}(\mathbf{A})$ then $\theta$ is nilpotent in $\mathbf{A}$. This is a (relatively weak) abstract form of the
Nullstellensatz. The proof is elementary. Naturally, if two theories prove the same facts, they can
differ in terms of dynamical rules that are more general than Horn rules.
■

**Positive diagram of an algebraic structure**

**Definition and notation A.2.6.**

1. Let $\mathcal{T}_1 = (\mathcal{L}_1, \mathcal{A}_1)$ be a dynamical theory and $\mathbf{A}$ an algebraic structure over a language $\mathcal{L} \subseteq \mathcal{L}_1$. We call positive diagram of $\mathbf{A}$ for the language $\mathcal{L}$, a presentation $(G, R)$ of $\mathbf{A}$ as an algebraic structure over the language $\mathcal{L}$. Such a diagram is denoted $\text{Diag}(\mathbf{A}, \mathcal{L})$. We then denote $\mathcal{T}_1(\mathbf{A})$ the dynamic algebraic structure $(\text{Diag}(\mathbf{A}, \mathcal{L}), \mathcal{T}_1)$.

2. Let $\mathcal{T} = (\mathcal{L}, \mathcal{A})$ be a dynamical theory, $\mathbf{B}$ a model of $\mathcal{T}$, and $\mathcal{T}_1 = (\mathcal{L}_1, \mathcal{A}_1)$ a simple extension of $\mathcal{T}$. Consider a presentation $(G, R)$ of $\mathbf{B}$ as a dynamic algebraic structure of type $\mathcal{T}$. Such a diagram is called positive diagram of $\mathbf{B}$ for the dynamical theory $\mathcal{T}$ and it is denoted $\text{Diag}(\mathbf{B}, \mathcal{T})$. We then note $\mathcal{T}_1(\mathbf{B})$ the dynamic algebraic structure $(\text{Diag}(\mathbf{B}, \mathcal{T}), \mathcal{T}_1)$.

Item 1 can be seen as a special case of item 2, where $\mathcal{A} = \emptyset$.

**Remarks A.2.7.**

1) Here is a typical example for Item 1. The theory $\mathcal{T}_1$ is a simple extension of the theory $\mathcal{Ac}$ where equality is the only predicate. Let $\mathcal{L}$ be the language of $\mathcal{Ac}$ and let $\mathbf{A}$ be a commutative ring. For generators of $\text{Diag}(\mathbf{A}, \mathcal{L})$ we can take the elements of the set underlying $\mathbf{A}$, and for relations we can restrict ourselves to the equalities $0_{\mathbf{A}} = 0$, $1_{\mathbf{A}} = 1$, $-a = b$, $a + b = c$ and $ab = c$ when they are satisfied for elements of $\mathbf{A}$. This positive diagram does not contain any $a \neq b$ inequalities for the simple reason that they are not part of the language of $\mathcal{Ac}$. This is why we call it a "positive" diagram.

2) An element $a$ of $\mathbf{A}$ does not always have a canonical representative in a set à la Bishop, even if the set is discrete. In such a case, to return to the definition of the set underlying $\mathbf{A}$ according to Bishop, we can take a different constant $x_b$ for each representative $b$ of the element $a$. We then find in the positive diagram of $\mathbf{A}$ a relation $x_b = x_c$ each time $b = {}_{\mathbf{A}}c$. ■

**Constructive versus classical models**

Consider a dynamic algebraic structure $\mathbf{A} = ((G, R), \mathcal{T})$ of type $\mathcal{T}$ with one or more sorts. To simplify the notation, we assume a single sort. A model of $\mathbf{A}$ is a usual (static) algebraic structure $M$ described in the language associated with $\mathbf{A}$ and verifying the axioms of $\mathbf{A}$ (those of $\mathcal{T}$ and those given by the presentation of $\mathbf{A}$).

When $\mathbf{A}$ is defined by the empty presentation, we speak of *models of* $\mathcal{T}$.

The notion of model is therefore based on a priori on an intuitive notion of *algebraic structure* à la Bourbaki. We can describe these algebraic structures as “static” in contrast to the general dynamic algebraic structures. Note that here the set “underlying” the structure is a “naive set” (or several naive sets if there are several sorts) structured by giving predicates and functions (in the naive sense) subject to certain axioms.

From a constructive point of view, the models must satisfy the axioms by respecting the intuitive sense of “or” and “there exists”: to prove that a particular algebraic structure satisfies the axioms, we allow only intuitionistic logic. Note also that the set theory to which we refer is a priori Bishop’s informal set theory.

<footnote n="10">¹⁰With $\theta = t(\xi) \in \mathbf{A}$, where $t \in \mathbb{Z}[G]$ and the $\xi_k$ are the $x_k$ seen in the quotient $\mathbf{A}$ of $\mathbb{Z}[G]$.</footnote>
## Morphisms between dynamic algebraic structures of the same type

Consider a disjunctive theory $\mathcal{T}$. In this case, a possible natural notion of morphism from a dynamic algebraic structure $\mathbf{A} = ((G, R), \mathcal{T})$ to a dynamic algebraic structure $\mathbf{A}' = ((G', R'), \mathcal{T})$ for the disjunctive theory $\mathcal{T}$ is as follows.

An element of $\mathbf{Sad}_T(\mathbf{A}, \mathbf{A}')$ is given by a map $\varphi: G \to \mathrm{Tcl}(\mathbf{A}')$ which interprets the elements of $G$ by closed terms of $\mathbf{A}'$. This map uniquely extends into a map $\mathrm{Tcl}(\mathbf{A}) \to \mathrm{Tcl}(\mathbf{A}')$ respecting the construction of the terms by means of the function symbols present in $\mathcal{L}$. In addition, the elements of $R$ must give valid facts in $\mathbf{A}'$ according to this interpretation.

The equality between two elements $\varphi$ and $\psi$ of the set $M = \mathbf{Sad}_T(\mathbf{A}, \mathbf{A}')$ is defined as follows: one has $\varphi =_M \psi$ if, and only if, for all $x \in G$, the equality $\varphi(x) = \psi(x)$ is valid in $\mathbf{A}'$.

The composition of morphisms is defined in a natural way for three dynamic algebraic structures $\mathbf{A}, \mathbf{B}$ and $\mathbf{C}$.

This gives us a very interesting (informal) category. The objects are dynamic algebraic structures of type $\mathcal{T}$. The set of arrows from $\mathbf{A}$ to $\mathbf{A}'$ is $\mathbf{Sad}_T(\mathbf{A}, \mathbf{A}')$.

This category has arbitrary limits and colimits, constructed very naively at the level of the presentations $(G, R)$, based on the naive intuitive set theory that we consider in the ambient mathematical world.

For example, the product in the category $\mathbf{Sad}_T$ of $\mathbf{A} = ((G, R), \mathcal{T})$ and $\mathbf{A}' = ((G', R'), \mathcal{T})$ is the dynamic algebraic structure of type $\mathcal{T}$ whose presentation is given by $(G \times G', R \times R')$. When $\mathcal{T}$ is the theory of discrete fields, in the disjunctive version where a discrete field is defined as a connected reduced zero-dimensional ring (a function symbol must be introduced for the quasi-inverse). The previous product is a new dynamic algebraic structure of a discrete field, and $\mathbf{A} \times \mathbf{A}'$ is provided with a usual algebraic structure of a reduced zero-dimensional ring. This situation seems analogous to that of bundles of discrete fields (according to the semantics of Kripke-Joyal), which are discrete fields only in the fibres.

**Remark.** If we are dealing with an existentially rigid theory, we can reduce ourselves to the case of a disjunctive theory by skolemisation of the rigid existential rules. However, it seems that in the case of a dynamical theory with non-rigid existential axioms, things are not very clear. ■

Sometimes we are interested in a more restrictive notion of morphism between two dynamical algebraic structures $\mathbf{A}$ and $\mathbf{A}'$ of the same type $\mathcal{T}$, for example the notion of local morphism between commutative rings, adapted to a specific context. In such a case, we would like the new morphisms from $\mathbf{A}$ to $\mathbf{A}'$ to be treated as given by dynamic algebraic structures for a certain dynamical theory defined from $\mathcal{T}$, $\mathbf{A}$ and $\mathbf{A}'$ (as may be the case for local morphisms).

## Examples

1) The disjunctive theory $\mathcal{Asdz0}$ (resp. $\mathcal{Asdz}$) of rings without zerodivisor is obtained from the theory $\mathcal{Ac0}$ (resp. $\mathcal{Ac}$) by adding the dynamical rule

$$ \mathbf{ASDZ} \quad xy = 0 \vdash x = 0 \quad \mathbf{op} \quad y = 0 $$

2) Reference [ACMC, section VIII-3]. The existential theory $\mathcal{Alsdz0}$ (resp. $\mathcal{Alsdz}$) of the rings locally without zerodivisor is obtained by adding to the theory $\mathcal{Ac0}$ (resp. $\mathcal{Ac}$) the axiom **LSDZ**:

$$ \mathbf{LSDZ} \quad xy = 0 \vdash \exists u, v \ (ux = 0, vy = 0, u + v = 1) $$

3) With the signature

$$ \text{Signature: } \Sigma_{Ai} = (\cdot = 0, \cdot \neq 0; \cdot +, \cdot \times, \cdot, \cdot, 0, 1) $$

The theory $\mathcal{Ai}$ of integral rings is obtained from the theory $\mathcal{Ac0}$ by adding as axioms the following dynamical rules
$$ \bullet \quad x \neq 0, y = 0 \vdash x + y \neq 0 $$

$$ \bullet \quad x \neq 0, y \neq 0 \vdash xy \neq 0 $$

$$ \bullet \quad x \neq 0, xy = 0 \vdash y = 0 $$

$$ \bullet \quad \vdash x = 0 \quad \mathbf{op} \quad x \neq 0 $$

$$ \bullet \quad \vdash 1 \neq 0 $$

$$ \bullet \quad xy \neq 0 \vdash x \neq 0 $$

$$ \bullet \quad 0 \neq 0 \vdash \bot $$

Note the significant difference between the theories *Asdz* and *Ai*, which corresponds to an important distinction in constructive mathematics but invisible in classical mathematics.

## Primitive recursive arithmetic

This subsection shows the interest of using sorts for maps that can be defined constructively in an algebraic structure (for example here the semi-ring of natural numbers) when the language in which the structure is defined does not allow the introduction of function symbols corresponding to these maps in the corresponding geometric theory.

This example motivates us to introduce sorts for certain continuous semialgebraic maps and their continuity moduli in the theory of non discrete real closed fields.

Long before the machinery of dynamical theories was set up, R. L. Goodstein explained how to treat a large part of the usually practised mathematics by means of purely computational formal systems, *without logic*.

In the book [Goodstein, 1957] the author, following a suggestion by Skolem, shows how a calculus system “without logic, and without quantifiers” makes it possible to develop a very important part of “arithmetic”, understood in the sense of a formal theory of the natural integers.

The only problem, and it's a major problem that is likely to put off many a mathematician, is that the usual mathematical statements have to be encoded in the form of primitive recursive maps. This may seem to take us back to the realm of second-order arithmetic and Reverse Mathematics.

In a second book ([Goodstein, 1961]) Goodstein extends his study to recursive analysis. We also highly recommend [Goodstein, 1979].

## Goodstein's formal system

If we restrict ourselves to primitive recursive arithmetic,<fnref n="11" /> we can describe the formal system proposed by Goodstein as follows.

As in the formal theory *Peano*, the variables and constants represent natural numbers. There is a single constant, 0, and a single relation symbol, which is the equality $x = y$.

For any primitive recursive map $f: \mathbb{N}^{k+1} \to \mathbb{N}$, defined by simple recurrence using the equations

$$ f(x_1, \dots, x_k, 0) = g(x_1, \dots, x_k) $$

$$ f(x_1, \dots, x_k, y+1) = h(x_1, \dots, x_k, y, f(x_1, \dots, x_k, y))x_1, \dots, x_k, y, f(x_1, \dots, x_k, y) $$

where $g$ and $h$ are previously defined primitive recursive maps, we introduce a function symbol corresponding to this definition of $f$.

Similarly, for any primitive recursive map defined by composition of previously defined primitive recursive maps, we introduce a function symbol corresponding to this definition.

The function symbols which “initialise” the system are $S$ for the successor map, $0_1$ for the null map in one variable and $\pi_{n,k}$ for the $k$-th coordinate map $\mathbb{N}^n \to \mathbb{N}$ ($k \in [1..n]$, $n \in \mathbb{N}$).

In this way we obtain a function symbol of arity $r$ for each definition of a primitive recursive map $\mathbb{N}^r \to \mathbb{N}$.

Note that we have a formal name $\underline{n}$, an abbreviation of $S(S(...(S(0))...))$, for each integer $n$.

<footnote n="11">¹¹Goodstein's book studies broader systems of calculation that include maps defined by multiple recurrences, such as the Ackerman function.</footnote>
Calculations in primitive recursive arithmetic à la Goodstein consist of establishing “identities” between two functions defined in this way corresponding to two function symbols $f_i$ and $f_j$ of the same arity.

$$ \forall x_1, \dots, x_k \ f_i(x_1, \dots, x_k) = f_j(x_1, \dots, x_k) $$

which we can write in the form of a valid rule in the proposed system:

$$ \mathbf{Eq}_{i,j} \vdash f_i(x_1, \dots, x_k) = f_j(x_1, \dots, x_k) $$

However, this is not a dynamical theory because the valid rules do not result from a simple axiomatic system of dynamical rules.

In fact, we must obviously take as axioms all the equalities mentioned earlier, which are used to define arbitrary primitive recursive maps, but this is clearly not enough.

Indeed, if the equality $(\underline{m}+\underline{n})+\underline{p} = \underline{m}+(\underline{n}+\underline{p})$ can be established for arbitrary $m, n, p$ integers by simply using the definition of $+$ by recurrence, the corresponding rule

$$ \vdash (x+y)+z = x+(y+z) $$

does not result in a purely finitary way from the axioms of definition of $+$.

The same applies, for example, to an equality $f_i(\underline{m}, \underline{n}) = f_j(\underline{m}, \underline{n})$ which could be found for all integers $m, n$ by simply applying the axioms defining $f_i$ and $f_j$, whereas the corresponding rule $\mathbf{Eq}_{i,j}$ cannot in general be established in a purely finitary way if the definitions of $f_i$ and $f_j$ use the simple induction scheme.

The computational system allows us to validate composition of maps,<fnref n="12" /> because it is subject to the axioms of equality. But to complete primitive recursive arithmetic, we need the external rules corresponding to definitions by recurrence. Specifically, for example, from the following two valid rules

$$ \bullet \vdash u(x, 0) = v(x, 0) $$

$$ \bullet u(x, y) = v(x, y) \vdash u(x, y+1) = v(x, y+1) $$

we deduce the validity of the rule

$$ \bullet \vdash u(x, y) = v(x, y) $$

(here $u$ and $v$ are two terms containing $x$ and $y$ as free variables)

The use of these external rules avoids recourse to the corresponding axiom, which can be formulated in a first-order formal theory, but not in a finitary dynamical theory:

$$ [\forall x \ u(x, 0) = v(x, 0) \land \forall x, y \ ((u(x, y) = v(x, y) \Rightarrow u(x, y+1) = u(x, y+1))] \Rightarrow \forall x, y \ u(x, y) = v(x, y) $$

## A finitary geometric theory for primitive recursive arithmetic

In this subsection we show how to treat Goodstein-style primitive recursive arithmetic within the framework of a dynamical theory.

We now explain how the use of sorts for maps allows us to avoid recourse to these external rules and to define a simple formal system (a finitary Horn theory) for primitive recursive arithmetic.

### 1. Sorts

For each integer $k$ we introduce the sort $F_k$ of the primitive recursive maps $f: N^k \to N$. The sort $F_0$ is the sort of integers denoted $N$.

### 2. Predicates.

For each sort $F_k$, there is a corresponding equality symbol $\cdot =_k \cdot$.

<footnote n="12">¹²For example, $g = f_1 \circ (f_2 \circ f_3)$ and $h = (f_1 \circ f_2) \circ f_3$ which correspond to two different definitions, give rise to the identity $\vdash g(x) = h(x)$ because according to the definitions $\vdash g(x) = f_1(f_2(f_3(x)))$ and $\vdash h(x) = f_1(f_2(f_3(x)))$.</footnote>
### 3. Constants.

(a) The basic constants are (names for)

* 0 of sort $N$,

* $0_k$ of sort $F_k$ (for the constant null map, $k \ge 1$),

* the successor map $S$ of sort $F_1$,

* for $n \ge 1$, the $n$ coordinate maps$^{13}$ $\pi_{n,k}$ of sort $F_n$ ($1 \le k \le n$).

(b) For any primitive recursive map $f: \mathbb{N}^k \to \mathbb{N}$ ($k \ge 1$), defined by simple recurrence using the equations

$$ 
\begin{array}{l@{\qquad}l@{\qquad}l}
f(\underline{x}, 0) & = & g(\underline{x}) & g: \mathbb{N}^{k-1} \to \mathbb{N} \\
f(\underline{x}, S(y)) & = & h(\underline{x}, y, f(\underline{x}, y)) & h: \mathbb{N}^{k+1} \to \mathbb{N}
\end{array}
$$

where $g$ and $h$ are previously defined primitive recursive maps, we introduce a name for $f$ as a constant of sort $F_k$.<fnref n="14" />

(c) A name is also introduced for any primitive recursive map defined by composition of previously defined primitive recursive maps.

### 4. The other function symbols.
The function symbols given in 4b and 4c can be used, if desired, to avoid creating the constants given in 3b and 3c.

(a) *Evaluations.* For each $\ell \ge 1$ there is a function symbol for the evaluation $\mathrm{Ev}_\ell$ of the constant $f \in F_\ell$ in a $k$-uplet of integers. It is a symbol of the type $F_\ell \times N^\ell \to N$. We abbreviate $\mathrm{Ev}_\ell(f, x_1, \dots, x_\ell)$ to $f(x_1, \dots, x_\ell)$.

(b) *Simple recurrence.* For $k \ge 1$ we have a function symbol $R_k$ for the element $f \in F_k$ defined “by simple recurrence” from an element $g \in F_{k-1}$ and an element $h \in F_{k+1}$ (as in 3b, but here, $f$, $g$ and $h$ are variables). It is a function symbol of the type $F_{k-1} \times F_{k+1} \to F_k$.

(c) *Compositions.* For $k \ge 1$ and $\ell \ge 1$ we have a function symbol $C_{\ell,k}$ for the “composition” of the element $f \in F_\ell$ with $\ell$ elements $g_i \in F_k$. It is a symbol of the type $F_\ell \times F_k^\ell \to F_k$. We abbreviate $C_{\ell,k}(f, g_1, \dots, g_\ell)$ to $f \circ (g_1, \dots, g_\ell)$ or $f(g_1, \dots, g_\ell)$. We can see $\mathrm{Ev}_\ell$ as the special case $C_{\ell,0}$.

### 5. The axioms are as follows.

(a) The usual equality axioms for $=_{k}$ relations.

(b) A collapse axiom $S(0) = 0 \vdash \perp$. We note 1 rather than $\perp$ for $S(0)$.

(c) The axioms that establish equalities linking constants and other function symbols. For example:

$$ 
\begin{array}{l}
\vdash_{f:F_k} f \circ (\pi_{k,1}, \dots, \pi_{k,k}) = f \\
\vdash_{f_1, \dots, f_k; F_\ell} 0_k(f_1, \dots, f_k) = 0_\ell \\
\vdash_{f_1, \dots, f_k; F_\ell} \pi_{k,i}(f_1, \dots, f_k) = f_i \\
\mathbf{prod} \quad \vdash_{x,y:N} \mathbf{prod} = R_2(0_1, \sum \circ (\pi_{3,3}, \pi_{3,1}))
\end{array}
$$

The last rule gives the recurrence definition of the product (the constant prod in $F_2$) from the addition (the constant sum in $F_2$).

(d) The axioms for the associativity of compositions, including the cases of evaluations. For example:

$$ \mathbf{asC}_{1,1,1} \vdash_{f,g,h:F_1} f \circ (g \circ h) = (f \circ g) \circ h $$

$$ \mathbf{asC}_{1,1,0} \vdash_{f,g:F_1;x:N} (f \circ g)(x) = f(g(x)) $$

$$ \mathbf{asC}_{2,1,1} \vdash_{f:F_2;g_1,g_2,h_1,h_2:F_1} f \circ (g_1 \circ h_1, g_2 \circ h_2) = (f \circ (g_1, g_2)) \circ (h_1, h_2) $$

<footnote n="13">¹³Note that $\pi_{1,1}$ is the constant which designates the identity in $F_1$.</footnote>

<footnote n="14">¹⁴For $k=2$ for example this could be the name $R_2(G, H)$ if $G$ and $H$ are names for $g$ and $h$.</footnote>
(e) The axioms for definitions by recurrence. For example, $\mathbb{R}_2$:

$$ \mathbf{Rec}_{2,\text{ini}} \quad f = \mathbb{R}_2(g,h) \vdash_{f:F_2;g:F_1;h:F_3} f \circ (\pi_{1,1}, 0_1) = g $$

$$ \mathbf{Rec}_{2,\text{rec}} \quad f = \mathbb{R}_2(g,h) \vdash_{f:F_2;g:F_1;h:F_3} f \circ (\pi_{2,1}, S \circ \pi_{2,2}) = h \circ (\pi_{2,1}, \pi_{2,2}, f) $$

(f) The axioms for proofs by induction (one for each arity). For example, $\mathbf{REC}_2$:

$$ \left. \begin{array}{rcl} f_1 \circ (\pi_{1,1}, 0_1) & = & f_2 \circ (\pi_{1,1}, 0_1), \\ \mathbf{REC}_2 \quad f_1 \circ (\pi_{2,1}, S \circ \pi_{2,2}) & = & h \circ (\pi_{2,1}, \pi_{2,2}, f_1), \\ f_2 \circ (\pi_{2,1}, S \circ \pi_{2,2}) & = & h \circ (\pi_{2,1}, \pi_{2,2}, f_2) \end{array} \right\} \vdash_{f_1,f_2:F_2;h:F_3} f_1 = f_2 $$

Note that in (e) the axioms assert that the map $f = \mathbb{R}_2(g,h)$ verifies the properties expected of a definition by recurrence, whereas in (f) the axiom asserts the uniqueness of the map verifying these properties.

Let's now look at how a usual proof by induction translates into the “language of maps” that we have set up. For example, the distributivity of multiplication over addition. In the usual proof, we prove the equality $x \times (y + z) = (x \times y) + (x \times z)$ by induction on $z$ as follows:

* Initialisation.

$$ x \times (y + 0) \stackrel{1}{=} x \times y \stackrel{2}{=} (x \times y) + 0 \stackrel{3}{=} (x \times y) + (x \times 0) $$

with: 1 : initialisation of $a + \cdot$, 2 : initialisation of $a + \cdot$, 3 : initialisation of $a \times \cdot$.

* Induction.

$$ \begin{array}{lclcl} x \times (y + S(z)) & \stackrel{4}{\equiv} & x \times S(y + z) & \stackrel{5}{\equiv} & (x \times (y + z)) + x \stackrel{6}{\equiv} \\ ((x \times y) + (x \times z)) + x & \stackrel{7}{\equiv} & (x \times y) + ((x \times z) + x) & \stackrel{8}{\equiv} & (x \times y) + (x \times S(z)) \end{array} $$

with 4 : induction of $a + \cdot$, 5, 8 : induction of $a \times \cdot$, 6 : induction hypothesis, 7 : associativity of $+$ (demonstrated earlier),

Let's translate all this into the language of maps, for the elements of $F_3$

$$ f = \text{prod}(\pi_{3,1}, \text{sum}(\pi_{3,2}, \pi_{3,3})) \quad \text{and} \quad g = \text{sum}(\text{prod}(\pi_{3,1}, \pi_{3,2}), \text{prod}(\pi_{3,1}, \pi_{3,3})). $$

To validate $f = g$, we use the $\mathbf{REC}_3$ principle. To do this, we validate the three hypotheses. First of all the initialisation, which is $f(\pi_{2,1}, \pi_{2,2}, 0_1) = g(\pi_{2,1}, \pi_{2,2}, 0_1)$.

* We have $f(\pi_{2,1}, \pi_{2,2}, 0_1) = \text{prod}(\pi_{2,1}, \text{sum}(\pi_{2,2}, 0_1))$. Since $\text{sum}(\pi_{2,2}, 0_1) = \pi_{2,2}$ according to the initialisation in the recurrence definition of sum, we obtain

$$ f(\pi_{2,1}, \pi_{2,2}, 0_1) = \text{prod}(\pi_{2,1}, \pi_{2,2}). $$

* We have $g(\pi_{2,1}, \pi_{2,2}, 0_1) = \text{sum}(\text{prod}(\pi_{2,1}, \pi_{2,2}), \text{prod}(\pi_{2,1}, 0_1))$. Since $\text{prod}(\pi_{2,1}, 0_1) = 0_1$ from the recurrence definition of prod, we obtain

$$ g(\pi_{2,1}, \pi_{2,2}, 0_1) = \text{sum}(\text{prod}(\pi_{2,1}, \pi_{2,2}), 0_1), $$

then $g(\pi_{2,1}, \pi_{2,2}, 0_1) = \text{prod}(\pi_{2,1}, \pi_{2,2})$ from the recurrence definition of sum.

Next we need to validate the passage from $n$ to $S(n)$, i.e. find a suitable element $h \in F_4$, i.e. satisfying the equalities

$$ f(\pi_{3,1}, \pi_{3,2}, S(\pi_{3,3})) = h(\pi_{3,1}, \pi_{3,2}, \pi_{3,3}, f) $$

$$ g(\pi_{3,1}, \pi_{3,2}, S(\pi_{3,3})) = h(\pi_{3,1}, \pi_{3,2}, \pi_{3,3}, g) $$
* We have $f(\pi_{3,1}, \pi_{3,2}, S(\pi_{3,3})) = \text{prod}(\pi_{3,1}, \text{sum}(\pi_{3,2}, S(\pi_{3,3})))$ which gives according to the induction in the definition by recurrence of sum

$$f(\pi_{3,1}, \pi_{3,2}, S(\pi_{3,3})) = \text{prod}(\pi_{3,1}, S(\text{sum}(\pi_{3,2}, \pi_{3,3}))),$$

then according to the recurrence definition of prod

$$f(\pi_{3,1}, \pi_{3,2}, S(\pi_{3,3})) = \text{sum}(\text{prod}(\pi_{3,1}, \text{sum}(\pi_{3,2}, \pi_{3,3})), \pi_{3,1}) = \text{sum}(f, \pi_{3,1}).$$

* In the same way (using the associativity of addition)

$$g(\pi_{3,1}, \pi_{3,2}, S(\pi_{3,3})) = \text{sum}(\text{sum}(\text{prod}(\pi_{3,1}, \pi_{3,2}), \text{prod}(\pi_{3,1}, \pi_{3,3})), \pi_{3,1}) = \text{sum}(g, \pi_{3,1}).$$

* We have therefore validated the hypotheses with the element $h \in F_4$ defined by

$$h = h(\pi_{4,1}, \pi_{4,2}, \pi_{4,3}, \pi_{4,4}) := \text{sum}(\pi_{4,4}, \pi_{4,1}).$$

We call *PRA* the dynamical theory of primitive recursive arithmetic that we have just defined. This dynamical theory demonstrates exactly the same statements as the system developed by Goodstein.

## A.3. Conservative extensions of a dynamical theory

### Essentially equivalent extensions

**Definition A.3.1.** A dynamical theory $\mathcal{T}'$ is said to be a conservative extension of the theory $\mathcal{T}$ if it is an extension of $\mathcal{T}$ and if the dynamical rules formulable in $\mathcal{T}$ and valid in $\mathcal{T}'$ are valid in $\mathcal{T}$.<fnref n="15" />

Two dynamical theories on the same language are said to be *identical* when they prove exactly the same dynamical rules. In other words, the axioms of one are valid dynamical rules in the other. Each is obviously a conservative extension of the other.

The simplest case of conservative extension when the language has grown is that of extensions which are essentially equivalent in the following meaning.

**Definition A.3.2.** An extension $\mathcal{T}'$ of the dynamical theory $\mathcal{T}$ is said *essentially equivalent* if it is obtained, up to renamings, by means of the following procedures, used iteratively, each time giving the appropriate axioms (see the details in [41, section 2.3]).

*Essentially identical* extensions are those which are obtained without adding new sorts.

* Add abbreviations.

* Addition of predicates expressing the conjunction or disjunction of already existing predicates. This amounts to accepting $\wedge$ and $\vee$ as logical symbols for constructing compound formulas, i.e. accepting a bit of intuitionist logic in the language.

* Add predicates translating a formula $\exists x P$ where $P$ is an existing predicate and $x$ is a variable. Same comment as for the previous point.

* Add a function symbol when a unique existence is valid under certain hypotheses.

* Add a sort that is the product of several sorts.

* Add a sort that is the disjoint union of several sorts.

* Add a subsort of an existing sort, defined as the elements satisfying an existing predicate.

<footnote n="15">¹⁵The reciprocal is clear.</footnote>
• Add a quotient sort of an already existing sort, defined by a binary predicate, which is provably an equivalence relation, and which defines the new equality in the quotient sort.

• Add a sort whose objects are (certain) morphisms of one sort into another that shares some algebraic structure with the first.

An essentially equivalent extension is intuitively equivalent in the following meaning.

**Informal definition A.3.3.** Consider a dynamical theory $\mathcal{T}$ and an extension $\mathcal{T}'$ of $\mathcal{T}$. We say that $\mathcal{T}'$ is an *intuitively equivalent* extension of $\mathcal{T}$ if the following three properties are verified.

1. $\mathcal{T}'$ is a conservative extension of $\mathcal{T}$.

2. Any dynamical rule formulated in the language of $\mathcal{T}'$ is equivalent$^{16}$ to a family of dynamical rules formulated in the language of $\mathcal{T}$.

2. For any presentation $(G, R)$ in the language of $\mathcal{T}$, the dynamic algebraic structures $\mathbf{A} = ((G, R), \mathcal{T})$ and $\mathcal{T}'(\mathbf{A}) := ((G, R), \mathcal{T}')$ have the same models (in constructive mathematics as in classical mathematics).

In the rest of this section we give two very important cases of conservative extensions (Theorems A.3.6 and A.3.8), relating to the use of classical logic, which do not fall into the previous simple case. Before that, we give Theorem A.3.4 relating to the use of constructive (intuitionistic) logic.

## Comparison with intuitionistic logic

Dynamical theories can be considered to be nothing more than truncated versions of intuitionistic natural deduction, in which neither the $\Rightarrow$ connector nor the $\forall$ quantifier is introduced.

This is precisely the strength of dynamical theories: not being encumbered with “complicated” formulas such as $(A \Rightarrow B) \Rightarrow C$, or $\forall x \exists y \forall z \dots$, makes it possible to see things more clearly and to simplify a certain number of non-trivial results, when they can be demonstrated at the basic level of natural deduction, i.e. with the “logic-free” system of dynamic proofs.

**Theorem A.3.4** (conservativity of intuitionistic logic with respect to dynamic proofs). Consider a finitary dynamical theory $\mathcal{T}$. If a consistent formula on the language of $\mathcal{T}$ is proved using the axioms of $\mathcal{T}$ and intuitionistic logic, the corresponding dynamical rule can be proved valid directly in the dynamical theory $\mathcal{T}$.

*Proof*. See [11, Coquand, 2005]. □

<figure><img src="image_4.png" /></figure>

Thierry Coquand intuitively interprets the proof as the construction of a certain type of model (a *generic model*) of the dynamic algebraic structure under consideration. The proof in [11] is more direct and more intuitive than that of the slightly stronger conservativity result given in Theorem A.3.6.

## Fundamental theorem of dynamical theories

To a dynamical theory $\mathcal{T}$ corresponds a coherent theory, or finitary geometric theory, obtained by replacing the dynamical rules by the corresponding formulas according to the scheme given on page 12 at the beginning of Section A.1. This coherent theory can be treated according to classical logic or intuitionistic logic. Let us note $\mathcal{T}^c$ and $\mathcal{T}^i$ respectively.

We have the fundamental theorem A.3.6 below (cf. for example Theorem 1 in [17]). This theorem is already given for purely equational theories in [55, Prawitz, 1971], and this kind of result is omnipresent in the contemporary literature, in more or less varied forms. We recommend the recent progress on this theme described in [23, 22] which shows that, properly treated, classical

<footnote>$^{16}$The equivalence in question is an external rule, like the structural rules described above. It may depend on the logic used in the external world.</footnote>
proofs do not provide significantly longer constructive proofs. The proof in [17] is constructive and relatively intuitive, but leads to an explosion in the size of proofs.

It is based on the following lemma which explains the harmlessness, in certain circumstances, of the rule **LEM** of excluded thirds.

**Lemma A.3.5 (elimination of classical negation).**

Let $\mathcal{T}$ be a finitary dynamical theory, and $P(\cdot, \cdot)$ be a predicate forming part of the signature (we have taken it here of arity 2 by way of example). Let us introduce "the predicate opposed to $P$", let us note it $Q(\cdot, \cdot)$, with the two dynamical rules which define it in classical mathematics:<fnref n="17" />

$\mathbf{In-non}_P \vdash P(x, y) \quad \mathbf{op} \quad Q(x, y)$

$\mathbf{El-non}_P P(x, y), Q(x, y) \vdash \bot$

Then, the new dynamical theory is a conservative extension of $\mathcal{T}$.

Note that this time some constructive models of the first theory may no longer be constructive models of the second. Nevertheless, this is not too serious, as the lemma indicates, and is generalised in the following fundamental theorem.

**Theorem A.3.6 (elimination of cuts).**

As far as finitary dynamical theories are concerned, logic, including classical logic (and in particular the **LEM**) only serves to shorten proofs. More precisely a dynamical rule is valid in a dynamical theory $\mathcal{T}$ if, and only if, it is valid in the corresponding classical coherent theory (the one with the same signature and axioms as $\mathcal{T}$): connectors, quantifiers and classical first-order logic are used in the coherent theory.

*Remark A.3.7.* The preceding theorem, and the following one concerning skolemisation, show that the use of dynamical theories allows Hilbert's programme to be partly realised, by providing a constructive semantics for certain uses of **LEM** and the axiom of choice. ■

## Skolemisation

We now look at the general process of skolemisation, which consists of getting rid of the $∃$ in some valid rules of a dynamical theory by replacing the existing $∃$ with functions symbols.

We have already indicated the case where this operation is harmless, according to the following informal remark: when the existent in a valid rule is provably unique, it doesn't hurt to replace the dummy variable which designates the existent by a function symbol.

On the other hand, replacing the dummy variable that designates the existing with a function symbol when the existing is not provably unique is more problematic. This is called skolemisation. Some constructive models before skolemisation may no longer be suitable after skolemisation, and the new theory may no longer have any known constructive model. And even in classical mathematics, if the models are "almost" the same, it is on condition that the axiom of choice is assumed.

**Theorem A.3.8 (skolemisation).** Consider a dynamical theory $\mathcal{T}$. We denote $\mathcal{T}'$ the "skolemised" theory, where we have skolemised all the existential axioms by replacing the $∃$ with the introduction of function symbols. Then $\mathcal{T}'$ is a conservative extension of $\mathcal{T}$.

*Proof.* A proof in classical mathematics using an axiom of choice consists in noting that the two theories have "the same models". A syntactic and constructive proof is given in [7, Bezem & Coquand, 2019]. □

<footnote n="17">¹⁷The definition of the predicate opposed to a predicate $P$ in constructive mathematics is not the same, and it cannot be treated in the framework of dynamical theories, except in the case where the predicate is decidable. The constructive meaning of $P$ is $P \Rightarrow \bot$ and the constructive implication cannot be treated by the dynamical method alone.</footnote>
## A.4. Distributive lattices and spectral spaces associated with a dynamic algebraic structure

For this section, we refer to [CACM, Chapters XI and XIII] [41, sections 1 and 3]

### Distributive lattices and entailment relations

A particularly important rule for distributive lattices, called cut, is the following

$$ \text{if } x \wedge a \leqslant b \text{ and } a \leqslant x \vee b \text{ then } a \leqslant b. \qquad (A.3) $$

If $A \in P_{\text{fe}}(\mathbf{T})$ (set of finitely enumerated parts of $\mathbf{T}$) we will note

$$ \bigvee A := \bigvee_{x \in A} x \quad \text{and} \quad \wedge A := \wedge_{x \in A} x. $$

We denote $A \vdash B$ or $A \vdash_{\mathbf{T}} B$ the relation defined as follows on the set $P_{\text{fe}}(\mathbf{T})$:

$$ A \vdash B \stackrel{\text{déf}}{\rightleftharpoons} \bigwedge A \leqslant \bigvee B. $$

This relationship verifies the following axioms, in which we write $x$ for $\{x\}$ and $A, B$ for $A \cup B$.

$$ x \vdash x \qquad (R) $$

$$ \text{if } A \vdash B \text{ then } A, A' \vdash B, B' \qquad (M) $$

$$ \text{if } (A, x \vdash B) \text{ and } (A \vdash B, x) \text{ then } A \vdash B \qquad (T). $$

The relationship is said to be *reflexive*, *monotonic* and *transitive*. The third rule (transitivity) can be seen as a rewriting of the rule (A.3) and is also called the *cut rule*.

**Definition A.4.1.** For an arbitrary set $S$, a binary relation on $P_{\text{fe}}(S)$ which is reflexive, monotonic and transitive is called an *entailment relation*.

The following theorem is fundamental. It states that the three properties of entailment relations are exactly what is needed for the interpretation of an entailment relation as the trace of that of a distributive lattice to be adequate.

**Theorem A.4.2 (fundamental theorem of entailment relations).** [46, Satz 7], [10], [ACMC, XI-5.3].
Let $S$ be a set with an entailment relation $\vdash_S$ on $P_{\text{fe}}(S)$. Consider the distributive lattice $\mathbf{T}$ defined by *generators and relations as follows: the generators are the elements of $S$ and the relations are the*

$$ A \vdash_{\mathbf{T}} B $$

each time $A \vdash_S B$. Then, for all $A, B$ in $P_{\text{fe}}(S)$, we have

$$ \text{if } A \vdash_{\mathbf{T}} B \text{ then } A \vdash_S B. $$

In particular, two elements $x$ and $y$ of $S$ define the same element of $\mathbf{T}$ if, and only if, we have $x \vdash_S y$ and $y \vdash_S x$.

### The spectrum of a distributive lattice

In classical mathematics a *prime ideal* $\mathfrak{p}$ of a distributive lattice $\mathbf{T} \neq \mathbf{1}$ is an ideal whose complementary $\mathfrak{v}$ is a filter (which is then a *prime filter*). We then have $\mathbf{T}/(\mathfrak{p} = 0, \mathfrak{v} = 1) \cong \mathbf{2}$. It is the same to give a prime ideal of $\mathbf{T}$ or a morphism of distributive lattices $\mathbf{T} \to \mathbf{2}$.

It is easy to check that if $S$ is a generating part of the distributive lattice $\mathbf{T}$, a prime ideal $\mathfrak{p}$ of $\mathbf{T}$ is completely characterised by its trace on $S$ (cf. [10]).

**Definition A.4.3.** The *spectrum of a distributive lattice* $\mathbf{T}$ is the set $\text{Spec} \, \mathbf{T}$ of its prime ideals, with the following topology: a basis of opens is given by the

$$ D_{\mathfrak{T}}(a) \stackrel{\text{déf}}{=} \{ \mathfrak{p} \in \text{Spec} \, \mathbf{T} | a \notin \mathfrak{p} \}, \quad a \in \mathbf{T}. $$
Classical mathematics verifies that

$$ \left. \begin{array}{l} D_{\mathbf{T}}(a \wedge b) = D_{\mathbf{T}}(a) \cap D_{\mathbf{T}}(b), \\ D_{\mathbf{T}}(a \vee b) = D_{\mathbf{T}}(a) \cup D_{\mathbf{T}}(b), \end{array} \right\} \begin{array}{l} D_{\mathbf{T}}(0) = \emptyset, \\ D_{\mathbf{T}}(1) = \text{Spec } \mathbf{T}. \end{array} \qquad (A.4) $$

The complementary of $D_{\mathbf{T}}(a)$ is a closed set which we denote $\mathfrak{W}_{\mathbf{T}}(a)$.

The notation $\mathfrak{W}_{\mathbf{T}}(a)$ is extended as follows: if $I \subseteq \mathbf{T}$, then $\mathfrak{W}_{\mathbf{T}}(I) \stackrel{\text{d\'ef}}{=} \bigcap_{x \in I} \mathfrak{W}_{\mathbf{T}}(x)$. If $I$ generates the ideal $\mathfrak{I}$, then $\mathfrak{W}_{\mathbf{T}}(I) = \mathfrak{W}_{\mathbf{T}}(\mathfrak{I})$. It is sometimes said that $\mathfrak{W}_{\mathbf{T}}(I)$ is the variety associated with $I$.

**Definition A.4.4.** A topological space homeomorphic to a space $\text{Spec}(\mathbf{T})$ is called a spectral space.

The spectral spaces come from the study [68, Stone, 1937].

[Johnstone] calls these spaces coherent spaces. [Balbes & Dwinger] calls them Stone spaces. This terminology is obsolete, because since [Johnstone] Stone spaces are the spectral spaces associated with distributive lattices which are Boolean algebras.

The name spectral space was given by [28, Hochster, 1969], who popularised them in the mathematical community after a prolonged hibernation since 1937.

With classical logic and the axiom of choice, the space $\text{Spec}(\mathbf{T})$ has “enough points”: we can find the lattice $\mathbf{T}$ from its spectrum.

A point $\mathfrak{p}$ in a spectral space $X$ is said to be the *generic point of the closed set* $F$ if $F = \overline{\{\mathfrak{p}\}}$. This point (when it exists) is necessarily unique because spectral spaces are Kolmogoroff spaces. In fact, the $\{\mathfrak{p}\}$ closed sets are exactly all the irreducible closed sets of $X$. The order relation $\mathfrak{q} \in \{\mathfrak{p}\}$ will be denoted $\mathfrak{p} \leq_X \mathfrak{q}$, and we have the equivalences

$$ \mathfrak{p} \leq_X \mathfrak{q} \iff \overline{\{\mathfrak{q}\}} \subseteq \overline{\{\mathfrak{p}\}}. \qquad (A.5) $$

The closed points of $\text{Spec}(\mathbf{T})$ are the maximal ideals of $\mathbf{T}$. When $X = \text{Spec}(\mathbf{T})$ the relation $\mathfrak{p} \leq_X \mathfrak{q}$ is simply the usual inclusion relation $\mathfrak{p} \subseteq \mathfrak{q}$ between prime ideals of the distributive lattice $\mathbf{T}$.

In the category of spectral spaces we define *spectral morphisms* as maps such that the reciprocal image of any quasi-compact open is a quasi-compact open (in particular they are continuous).

## Stone's antiequivalence

Stone's antiequivalence asserts (in modern language) that in classical mathematics the category of distributive lattices is antiequivalent to the category of spectral spaces.

Although spectral spaces have invaded contemporary abstract algebra, it is only in constructive mathematics that this anti-equivalence of classical mathematics is given the attention it deserves.

The aim is to correctly define the distributive lattices corresponding to the spectral spaces in the classical literature, and, if possible, to decipher the classical discourses using spectral spaces into constructive discourses concerning the corresponding distributional lattices.

## The Zariski lattice and spectrum of a commutative ring

The Zariski lattice of a commutative ring can be obtained from rules valid in different extensions of the theory $\mathcal{A}_c$ of commutative rings.

We choose the theory of local rings because of their fundamental role in Grothendieck schemes.

We consider precisely a dynamical theory of *local rings with units* $\mathcal{A}1$, based on the signature

$$ \Sigma_{\mathcal{A}1} = (\cdot = 0, U(\cdot); \cdot + , \cdot \times , \cdot, -, 0, 1). $$

This theory is an extension of the theory of commutative rings. A predicate $U(x)$ is defined as the invertibility predicate by means of the two suitable axioms. We add the collapse axiom $\mathcal{CL}_{\mathcal{A}1}$ and the actual axiom of local rings $\mathcal{AL}$.

$\mathcal{CL}_{\mathcal{A}1}$ $U(0) \vdash \bot$

$\mathbf{AL1}$ $U(x + y) \vdash U(x) \text{ op } U(y)$
Let $\mathbf{A}$ be a commutative ring. Consider the entailment relation $\vdash_{\mathbf{A},\mathbf{Zar}}$ on the set underlying $\mathbf{A}$ defined by the following equivalence

$$ a_1, \dots, a_n \vdash_{\mathbf{A}, \mathbf{Zar}} c_1, \dots, c_m \quad \overset{\text{déf}}{\iff} \quad U(a_1), \dots, U(a_n) \vdash_{\mathcal{Al}(\mathbf{A})} U(c_1) \textbf{ op } \dots \textbf{ op } U(c_m) \tag{A.6} $$

We define the Zariski lattice of $\mathbf{A}$, denoted $\mathbf{Zar A}$ or $\mathbf{Zar}(\mathbf{A})$, as the distributive lattice generated by the entailment relation $\vdash_{\mathbf{A},\mathbf{Zar}}$.

The corresponding map $D_{\mathbf{A}} : \mathbf{A} \to \mathbf{Zar A}$ is called the Zariski support of $\mathbf{A}$. When $\mathbf{A}$ is fixed by the context we simply note $D$.

The usual Zariski spectrum is the dual spectral space of this distributive lattice.

Note that since $D(a_1) \wedge \dots \wedge D(a_n) = D(a_1 \cdots a_n)$, the elements of $\mathbf{Zar A}$ are all of the form $D(c_1, \dots, c_m) := D(c_1) \vee \dots \vee D(c_m)$.

We have the following equivalences. Equivalence between (1) and (2) essentially copies the definition of $\mathbf{Zar A}$. The equivalence with (3) is the subject of a formal Nullstellensatz. The Hilbert Nullstellensatz itself is a more difficult result.

**Theorem A.4.5 (Nullstellensatz formel).**

Let $\mathbf{A}$ be a commutative ring, et $a_1, \dots, a_n, c_1, \dots, c_m \in \mathbf{A}$. T.F.A.E.

$$ (1) \quad D(a_1), \dots, D(a_n) \vdash_{\mathbf{Zar A}} D(c_1), \dots, D(c_m) $$

$$ (2) \quad U(a_1), \dots, U(a_n) \vdash_{\mathcal{Al}(\mathbf{A})} U(c_1) \textbf{ op } \dots \textbf{ op } U(c_m) $$

$$ (3) \quad \exists k > 0 \ (a_1 \cdots a_n)^k \in \langle c_1, \dots, c_m \rangle $$

We can therefore identify the element $D(c_1, \dots, c_m)$ of $\mathbf{Zar A}$ with the ideal $\sqrt{\langle c_1, \dots, c_m \rangle}$. Modulo this identification, the order relation is the inclusion relation.

**Corollary A.4.6.** The lattice $\mathbf{Zar A}$ is generated by the smallest entailment relation on (the set underlying to) $\mathbf{A}$ satisfying the following relations.

$$ \bullet \ 0 \vdash 0_{\mathbf{T}} $$

$$ \bullet \ 1 \vdash 1_{\mathbf{T}} $$

$$ \bullet \ ab \vdash a $$

$$ \bullet \ a, b \vdash ab $$

$$ \bullet \ a + b \vdash a, b $$

In other words, the map $D : \mathbf{A} \to \mathbf{Zar A}$ satisfies the relations

$$ D(0) = 0, D(1) = 1, D(ab) = D(a) \wedge D(b), D(a + b) \le D(a) \vee D(b), $$

and any other map $D' : \mathbf{A} \to T$ which satisfies these relations factorises via $\mathbf{Zar A}$ with a unique morphism of distributive lattices $\mathbf{Zar A} \to T$.

## Other examples

Remember that a disjunctive rule is a dynamical rule without the $\exists$ symbol, and that a simple disjunctive rule is a dynamical rule of the following form, with $m, n \ge 0$.

$$ C_1, \dots, C_n \vdash D_1 \textbf{ op } \dots \textbf{ op } D_m \tag{A.7} $$

where $C_i$'s and $D_j$'s are atomic formulas. (Simple) Horn rules are special cases of (simple) disjunctive rules.

• **First example.** Consider a dynamic algebraic structure $\mathbf{A} = ((G, R), \mathcal{T})$ for a dynamical theory $\mathcal{T} = (\mathcal{L}, \mathcal{A})$. If $P(x, y)$ is a binary predicate in the signature, and if $Tcl = Tcl(\mathbf{A})$ is the set of closed terms of $\mathbf{A}$, we obtain an entailment relation $\vdash_{\mathbf{A},P}$ on $Tcl \times Tcl$ by defining
$$ (a_1, b_1), \dots, (a_n, b_n) \vdash_{\mathbf{A}, P} (c_1, d_1), \dots, (c_m, d_m) \overset{\text{déf}}{\implies} (A.8) \\ P(a_1, b_1), \dots, P(a_n, b_n) \vdash_{\mathbf{A}} P(c_1, d_1) \textbf{ op } \dots \textbf{ op } P(c_m, d_m) $$

Intuitively, the distributive lattice generated by this entailment relation is the lattice of the “truth values” of the predicate P in the dynamic algebraic structure A.

* **More generally** Consider a dynamic algebraic structure $\mathbf{A} = ((G, R), \mathcal{T})$ for a dynamical theory $\mathcal{T} = (\mathcal{L}, \mathcal{A})$. Let $S$ be a set of closed atomic formulas of $\mathbf{A}$. We define the entailment relation on $S$ associated with $\mathbf{A}$ as follows:

$$ A_1, \dots, A_n \vdash_{\mathbf{A}, S} B_1, \dots, B_m \overset{\text{déf}}{\implies} (A.9) \\ A_1, \dots, A_n \vdash_{\mathbf{A}} B_1 \textbf{ op } \dots \textbf{ op } B_m $$

We can denote $\mathbf{Zar}(\mathbf{A}, S)$ the distributive lattice generated by this entailment relation.

In particular, the lattice $\mathbf{Zar}(\mathbf{A}, \text{Atcl}(\mathbf{A}))$ is called the absolute Zariski lattice of the dynamic algebraic structure $\mathbf{A}$.

* **Case of an extension $\mathcal{T}_1$ which reflects valid disjunctive rules.** Let $\mathcal{T}_1$ be an extension of a dynamical theory $\mathcal{T}$ which proves exactly the same disjunctive rules (for example a conservative extension). Let $\mathbf{A} = ((G, R), \mathcal{T})$ and $\mathbf{A}_1 = ((G, R), \mathcal{T}_1)$. Let $S$ be a set of closed atomic formulas of $\mathbf{A}$. Then the Zariski lattices $\mathbf{Zar}(\mathbf{A}, S)$ and $\mathbf{Zar}(\mathbf{A}_1, S)$ are isomorphic.

In particular, when $\mathcal{T}_1$ is an essentially equivalent extension of $\mathcal{T}$ the absolute Zariski lattices of $\mathbf{A}$ and $\mathbf{A}_1$ are isomorphic.

* **Zariski lattices, however, give a lesser image of a dynamic algebraic structure.** On the one hand, in these Zariski lattices nothing is taken into account a priori that corresponds to valid dynamical rules when they are not disjunctive. On the other hand, adding classical logic and skolemising a dynamical theory do not change the lattices corresponding to $\text{Atcl}(\mathbf{A})$, but in this case, the absolute Zariski lattice of $\mathbf{A}_1$ is the Boolean algebra generated by $\mathbf{Zar}(\mathbf{A}, \text{Atcl}(\mathbf{A}))$. To rediscover the richness of dynamical theories seen from a constructive point of view, it is necessary to call upon the theory of bundles or topos.

## A.5. Model theory

### Completeness theorem, simultaneous collapse

First of all, here is the completeness theorem in its minimal form: its intuitive interpretation in classical mathematics is that classical logic gives exhaustive rules for reasoning in accordance with “absolute truth”, based on an ideal mathematical universe in which no doubt is ever allowed, **LEM** is absolutely true and the axiom of choice just the same.

**Theorem\* A.5.1 (Gödel's completeness theorem, first form).**
A dynamic algebraic structure that does not collapse admits a non-trivial model.

*Comment.* An equivalent form of the completeness theorem is the following special case (Krull's lemma): any non-trivial commutative ring has a non-trivial integral quotient.

The constructively acceptable form of Krull's lemma is the following easy result: when we add the dynamical rule “$xy = 0 \vdash x = 0 \textbf{ op } y = 0$” to the theory of commutative rings, a dynamical algebraic structure collapses in the former theory if, and only if, it collapses in the latter.
In other words, the theories $\mathcal{A}_c$ and $\mathcal{A}_d$ collapse simultaneously. ■

**Theorem\* A.5.2 (Gödel's completeness theorem, second form).**
Consider a dynamical theory $\mathcal{T}$ and a dynamic algebraic structure $\mathbf{A}$ of type $\mathcal{T}$. A fact is valid in $\mathbf{A}$ if, and only if, it is satisfied in all models of $\mathbf{A}$.
A dynamical theory that extends another (by adding sorts and/or predicates and/or axioms) proves a priori more results. An interesting case is when it proves the same results while offering greater facilities for proofs. This was the essence of the fundamental theorems A.3.6 and A.3.8. A variant in model theory, but only in classical mathematics, is given by the following theorems.

**Theorem**\* A.5.3 (simultaneous collapses and non-trivial models). Let $\mathcal{T}$ be a dynamical theory and $\mathcal{T}'$ an extension which collapses simultaneously with $\mathcal{T}$. If a dynamic algebraic structure of type $\mathcal{T}$ admits a non-trivial model, it also admits a non-trivial model as a dynamic algebraic structure of type $\mathcal{T}'$. More precisely, if $M$ is a non-trivial model of $\mathcal{T}$, the dynamic algebraic structure $(\mathrm{Diag}(M), \mathcal{T}')$ admits a non-trivial model.

*Comment.* A good constructive version of the completeness theorem is a pure tautology: if a dynamic algebraic structure does not collapse, then ... it does not collapse. Or again: if a first-order formal theory doesn't collapse, then ... it doesn't collapse. And for Theorem A.5.3: if $\mathcal{T}$ and $\mathcal{T}'$ collapse simultaneously, then ... they collapse simultaneously. The same would apply to Theorems A.5.2 and A.5.4.

Indeed, what we call a constructive version of a “doubtful” classical theorem is a statement, correct in constructive mathematics, which, in practice, i.e. to demonstrate concrete results, provides the same services as the classical theorem. Indeed, in practice, all these “abstract” theorems are only used, to arrive at concrete results, only in reasoning by the absurd, which uses fictitious models to conclude that they cannot exist. The concrete result, on the other hand, is much closer to the hypothesis of the abstract theorem that has been invoked. A detailed analysis of the whole proof then generally shows that one has tautologised in circles without realising it (see for example [35] for Hilbert’s 17th problem). This is one of the reasons why classical mathematics is so often constructive, contrary to the appearance given by its demonstrations. ■

## Representation theorem, theories proving the same Horn rules

**Theorem**\* A.5.4 (representation theorem). Consider a dynamical theory $\mathcal{T}'$ which extends a Horn theory $\mathcal{T}$ and proves the same Horn rules. Any algebraic structure of type $\mathcal{T}$ is a subdirect product of algebraic structures of type $\mathcal{T}'$

For example $\mathcal{T}$ is the theory of $\ell$-groups and $\mathcal{T}'$ is the theory of linearly ordered abelian groups. The important and constructive result is that these two theories prove the same Horn rules. The intuitive interpretation in classical mathematics is that every lattice group is a lattice subgroup of a product of linearly ordered groups. When Paul Lorenzen proved this result, he generalised Krull's analogous result that the integral closure of an integral ring $\mathbf{A}$ is the intersection of the valuation rings of its fraction field that contain $\mathbf{A}$.

The following intuitive theorems, which will be useful to us, concern extensions which prove the same Horn rules; they are proved in [39].

**Theorem A.5.5.** Let $\mathcal{T}_2$ be a dynamical theory which is a simple extension of a $\mathcal{T}_1$ theory and which proves the same Horn rules. Consider an essentially equivalent extension $\mathcal{T}'_1$ of $\mathcal{T}_1$ obtained without the addition of existential predicates. We assume that there is no syntactic interference at the level of language extensions between $\mathcal{T}'_1$ and $\mathcal{T}_2$. We can therefore construct an essentially equivalent extension $\mathcal{T}'_2$ of $\mathcal{T}_2$ by copying for $\mathcal{T}_2$ what was done for $\mathcal{T}_1$. In these conditions, $\mathcal{T}'_2$ proves the same Horn rules as $\mathcal{T}'_1$.

**Theorem A.5.6.** Let $\mathcal{T}_2$ be a dynamical theory which is a simple extension of a $\mathcal{T}_1$ theory and which proves the same Horn rules. Consider an extension $\mathcal{T}'_1$ of $\mathcal{T}_1$ obtained by adding a family of axioms which are all Horn rules. Consider the extension $\mathcal{T}'_2$ of $\mathcal{T}_2$ obtained by adding the same axioms. Under these conditions, $\mathcal{T}'_2$ proves the same Horn rules as $\mathcal{T}'_1$.
# B. Infinitary geometric theories

## Sommaire

<table><tr><td><b>B.1 General</b></td><td><b>35</b></td></tr><tr><td>Example: nilpotent elements, Krull dimension</td><td>35</td></tr><tr><td><b>B.2 Barr's Theorem</b></td><td><b>37</b></td></tr><tr><td>An infinitary geometric theory for primitive recursive arithmetic</td><td>37</td></tr><tr><td>Conclusion</td><td>38</td></tr></table>

## B.1. General

A very useful general notion of geometric theory is defined, which is not necessarily expressed in finitary terms. This is known as *infinitary geometric theory*. In an infinitary geometric theory, we allow dynamical rules that have an infinite disjunction in the second member. There is one essential restriction: the free variables present in such a disjunction must be specified in advance and in finite number.

Intuitively, we use such rules in the proof system of dynamical theories by “opening the branches of calculation corresponding to the infinite disjunction”. What does this mean precisely? It means that a conclusion will be declared valid if it is valid in each of the branches.

Let's take a simple example, and show what happens if we have in the axioms an infinitary rule of the type

$$ \vdash_{x_1, \dots, x_k} \mathbf{OP}_{i \in I} \Gamma_i $$

with an infinite set $I$ and the $\Gamma_i$ are lists of atomic formulas with no free variables other than those mentioned (i.e. $x_1, \dots, x_k$). If for each $i \in I$ we have a valid rule $\Gamma_i \vdash B(x)$, then we declare the rule $\vdash_{x_1, \dots, x_k} B(x)$ to be valid.

There is therefore necessarily an intuitive proof *external* to the dynamical theory to certify that the desired conclusion is valid in each of the branches. Indeed, the system of calculation “without logic” at work in the dynamical theory cannot handle such an infinity of deductions. A purely mechanical calculus cannot open up an infinite number of branches! For example, with $I = \mathbb{N}$ the external intuitive proof could be a proof by induction.

Note, on the other hand, that the internal proof must show the validity of the desired conclusion according to the deduction rules “without logic” of the dynamical theory.

The above presentation is only a sketch. All this deserves a more formal definition of what is the legal functioning of an infinitary geometric theory; even if there is an unavoidable informal aspect in the recourse to “external” proofs in intuitive mathematics.

We should also say a few words about the operation of the formal intuitionist and classical theories that extend the infinite dynamical theory (by adding the $\Rightarrow$ connector and the universal quantifier in the intuitionist case, and by adding **LEM** in the classical case).

As in the case of finitary geometric theories, we will reserve the name of dynamical theory for proofs whose internal part is “without logic”.
**Example: nilpotent elements, Krull dimension**

An element $x$ of a ring is nilpotent if there exists an $n \in \mathbb{N}^+$ such that $x^n = 0$. If we introduce a predicate $Z(x)$ for “$x$ is nilpotent”, it will be subject to the natural axioms

$$ \mathbf{nil1} \quad \vdash \quad Z(0) $$

$$ \mathbf{nil3} \quad Z(x) \vdash Z(xy) $$

$$ \mathbf{nil2} \quad Z(x), Z(y) \vdash Z(x + y) $$

$$ \mathbf{Nil} \quad Z(x^2) \vdash Z(x) $$

$$ \mathbf{NIL1} \quad Z(x) \vdash \exists z \, z(1 + x) = 1 $$

In the corresponding dynamical theory, the only $t$ terms for which we will be able to demonstrate $Z(t)$ will be those for which we will be able to demonstrate $t^n = 0$ for a $n > 0$. However, there is no guarantee that in a model of the theory, the predicate $Z(x)$ corresponds to “$x$ is nilpotent”.

The only way to be sure is to introduce the infinitary dynamical rule

$$ \mathbf{NIL} \quad Z(x) \vdash \mathbf{OP}_{n \in \mathbb{N}^+} x^n = 0 $$

This concern is directly related to the Krull dimension of commutative rings. The Krull dimension of a distributive lattice can be formulated in a dynamical theory as follows.

**Definition B.1.1.**

1. Two sequences $(x_0, \dots, x_n)$ and $(b_0, \dots, b_n)$ in a distributive lattice $\mathbf{T}$ are said to be *complementary* if

$$ \left. \begin{array}{l} b_0 \wedge x_0 = 0 \\ b_1 \wedge x_1 \le b_0 \vee x_0 \\ \vdots \quad \vdots \\ b_n \wedge x_n \le b_{n-1} \vee x_{n-1} \\ 1 = b_n \vee x_n \end{array} \right\} \qquad (\text{B.1}) $$

A sequence which has a complementary sequence is said to be *singular*.

2. For $n \ge 0$ we will say that the distributive lattice $\mathbf{T}$ is of Krull dimension $\le n$ if any sequence $(x_0, \dots, x_n)$ in $\mathbf{T}$ is singular. Furthermore, the distributive lattice $\mathbf{T}$ is of Krull dimension $-1$ if it is trivial, i.e. if $1_{\mathbf{T}} = 0_{\mathbf{T}}$.

For example, for $n = 2$ the equalities and inequalities (B.1) correspond to the following drawing in $\mathbf{T}$.

<figure><img src="image_5.png" /></figure>

And the dimension $\le 2$ corresponds to the following existential axiom.

$$ \mathbf{KDIM2} \quad \vdash \quad \exists b_0, b_1, b_2 \, (x_2 \vee b_2 = 1, x_2 \wedge b_2 \le x_1 \vee b_1, x_1 \wedge b_1 \le x_0 \vee b_0, x_0 \wedge b_0 = 0) $$

For the Krull dimension of rings, we need to involve the distributive lattice formed by the radicals of finitely generated ideals and we express for example the dimension $\le 2$ as follows, noting $\mathrm{D}_{\mathbf{A}}(x, y) = \sqrt{\langle x, y \rangle} = \{ z \in \mathbf{A} \mid \exists n \in \mathbb{N}^+, z^n \in \langle x, y \rangle \}$:
For all $x_0, x_1, x_2 \in \mathbf{A}$ there exist $b_0, b_1, b_2 \in \mathbf{A}$ such that

$$ \left. \begin{array}{l} D_{\mathbf{A}}(b_0 x_0) = D_{\mathbf{A}}(0) \\ D_{\mathbf{A}}(b_1 x_1) \subseteq D_{\mathbf{A}}(b_0, x_0) \\ D_{\mathbf{A}}(b_2 x_2) \subseteq D_{\mathbf{A}}(b_1, x_1) \\ D_{\mathbf{A}}(1) = D_{\mathbf{A}}(b_2, x_2) \end{array} \right\} \qquad (B.2) $$

Note that $D_{\mathbf{A}}(b_2x_2) \subseteq D_{\mathbf{A}}(b_1, x_1)$ means that there exist $a_1, y_1 \in \mathbf{A}$ and $n \in \mathbb{N}^+$ such that

$$ (b_2x_2)^n = a_1b_1 + y_1x_1. $$

We can therefore express “$\mathrm{Kdim} \mathbf{A} \le 2$” in the context of an infinitary geometric theory. And for example the theorems of Serre or Foster-Swan ([CACM, Chapter XIV]) with the Krull dimension as an assumption can be treated entirely within the framework of geometric theories ([12]).

## B.2. Barr's Theorem

The fundamental theorem of dynamical theories A.3.6 is a solid basis for the constructive decoding of classical proofs. In classical mathematics, we show that a coherent theory proves a dynamical rule by looking at what happens in the models of the theory, which we study with powerful but dubious tools such as the excluded third, the axiom of choice and sometimes even the full power of $ZFC$. However, Theorem A.3.6 assures us that if the rule in question is provable in formal theory with classical logic, it is also provable by the elementary methods “without logic” that constitute dynamic proofs.

The essential part of decoding is therefore to check that the classical proof can be formalised in classical first-order logic. This is not always easy, because after all, $ZFC$ theory can be used to prove results that are much more “strange” than Gödel's completeness theorem, and why not results that are downright false if $ZFC$ is inconsistent. But in practice, in classical mathematics, even the overuse of ultrafilters or the continuum hypothesis always seems to hide simpler arguments.

**Barr's theorem**, established in classical mathematics (and apparently impossible to prove in constructive mathematics), states that for geometric theories, any result proved with classical logic can also be proved with constructive logic. This is a generalisation of Theorem A.3.6 which is confirmed in practice, even if it is not completely certain from the constructive point of view. A recent study of the problem is made by Rathjen in the article [57] published in the book [Proofs, 2013].

Barr's theorem gives us good reason to believe that the type of decryption provided by Theorem A.3.6 also applies for infinitary geometric theories, with the same caveats as we indicated for finitary theories. The reader can find examples of this type in [CACM, Sections XV-6 and XV-7].

At the end of this chapter we illustrate how Barr's theorem should not be understood.

### An infinitary geometric theory for primitive recursive arithmetic

We now consider the infinitary geometric theory $\mathcal{PRA}$ obtained from the finitary geometric theory $\mathcal{PRA}$ by adding the following axiom which forces the sort $N$ to contain only usual integers.

$$ \mathbf{Nat} \vdash_{x:N} \mathbf{OP}_{n \in N} x = \underline{n} $$

In the theory thus obtained, we see that to prove $\vdash f(x) = g(x)$ with $f, g$ of sort $F_1$, it is sufficient to know how to show that for each $n \in \mathbb{N}$ the rule $\vdash f(\underline{n}) = g(\underline{n})$ is valid. Indeed, we then deduce $x = \underline{n} \vdash f(x) = g(x)$ for each concrete integer $n$, and by using the rule **Nat**, we obtain $\vdash f(x) = g(x)$.

Now for maps $f$ and $g$ defined in $\mathcal{PRA}$ (i.e. two arbitrary primitive recursive maps), $f(\underline{n})$ and $g(\underline{n})$ are two explicit usual integers. Thus two primitive recursive maps are “provably everywhere equal” in the theory if they take the same values in any integer, i.e. if they are concretely equal, i.e. if we have a proof for the fact that they are equal.
But this proof is not always formalisable within the theory (it may, for example, use a double induction). In any case, it is supposed to be produced in intuitive mathematics in the intuitive mathematical world of the natural integers.

An example is provided by the primitive recursive map $C_{PRA}: \mathbb{N} \to \mathbb{N}$ which is everywhere zero if the theory $\mathcal{PRA}$ is consistent (which we are intimately convinced). According to Gödel's incompleteness theorem, the theory $\mathcal{PRA}$ cannot prove $\vdash C_{PRA}(x) = 0$. However, it does prove $\vdash C_{PRA}(\underline{n}) = 0$ for all $n$.

In the same way it seems probable that the geometric theory $\mathcal{PRA}\omega$, although it is capable of proving $\vdash C_{PRA}(x) = 0$, cannot however prove $\vdash C_{PRA} = 0_1$.

The infinitary axiom **Nat** that we add therefore authorises up to a certain point, but only up to a certain point, the use of the $\omega$-rule for the equality of primitive recursive maps.

## Conclusion

The study we have just made casts a shadow over Barr's theorem, because it would seem to assert in this case that any primitive recursive map proved null in classical mathematics would be provably null in constructive mathematics.

However, it may be that the intuitive proof of classical mathematics uses dubious principles, such as those formalised in the theory $\mathcal{ZF}$, in which case it may lead to quite questionable results.

For example, consider the primitive recursive map $\text{consisZ}$, which always takes the value 0 until such time as we eventually find a proof of $0 = 1$ in $\mathcal{Z}$, at which point the map takes the value 1. Thus $\text{consisZ}$ is a well-defined constant of sort $F_1$ in $\mathcal{PRA}$.

In classical mathematics with a sufficiently strong intuitive set theory (e.g. $\mathcal{ZF}$), it can be shown that $\text{consisZ}$ is identically zero. And this demonstrates in classical mathematics (using $\mathcal{ZF}$ in the external intuitive mathematical world) the rule $\vdash \text{consisZ}(x) = 0$ in the geometric theory $\mathcal{PRA}\omega$.

Now this result clearly escapes any constructive proof. And there can be no constructive proof of the rule $\vdash \text{consisZ}(x) = 0$ in the geometric theory $\mathcal{PRA}\omega$.

In fact we need to clarify the statement of Barr's theorem. It does not say that the framework of classical mathematics is conservative for geometric properties in a geometric theory. It only says that when we use the same mathematics outside the formal infinitary theory, adding the connectives, quantifiers and rules of classical logic inside the infinitary geometric theory, does not allow us to prove new properties formulable as geometric rules.

ajouter une conclusion de la première partie
# Part II

## Finitary geometric theories for
real algebra
<figure><img src="image_6.png" /></figure>
# Introduction

This second part is devoted to the development of a finitary dynamical theory whose ambition is to describe exhaustively the algebraic properties of the real number field, and more generally of a *non* discrete real closed field<fnref n="1" /> at least those that are expressible in a restricted language, close to the language of ordered rings. This constitutes a development, with some minor terminological modifications, of the ideas given in the article [40]. The axiom of archimedianity, introduced in the last chapter, takes us out of the realm of finitary geometric theories.

Chapter C proposes a first definition of the ordered field structure in the absence of a sign test. It also discusses the possibility of a suitable axiomatic for discrete real closed fields, such as the field of real numbers.

Section C.1 gives some reminders about the dynamical theory of discrete ordered fields and that of discrete real closed fields.

Section C.2 discusses the decisive consequences of formal Positivstellensätze, in our framework.

Section C.3 proposes an axiomatic for *non* discrete ordered fields (Definition C.3.7).

Section C.4 describes an example of a non-archimedean discrete Heyting ordered field.

Section C.5 gives a first discussion on acceptable dynamical theories for $\mathbb{R}$ as a *non* discrete real closed field.

Chapter D deals with dynamical theories which admit extensions essentially equivalent to the theory *Co* of *non* discrete ordered fields.

We start (Section D.1) with the theory of distributive lattices (*a non* discrete ordered field is a distributive lattice for its order relation).

In Section D.2 we deal with *l*-groups of lattice groups (purely equational theory, valid for addition on the reals).

Then (Section D.3) we move on to *f*-rings (*f*-rings in french litterature), a theory inspired by rings of continuous real maps.

Section D.4 describes dynamical theories in which the predicate $\cdot > 0$ is added to the signature (strict *f*-rings and variants).

Section D.5 proposes a return to the theory *Co* by confronting it with suitable extensions of the theory of strict *f*-rings.

Chapter E proposes a definition of the structure of a real closed ordered field in the absence of a sign test.

Section E.1 explains how to introduce square roots of the elements $\ge 0$ in a *non* discrete ordered field. This is done as a warm-up to the more general notion of virtual roots.

Section E.2 introduces virtual root maps and some corresponding dynamical theories: in particular *f*-rings with virtual roots and *non* discrete ordered fields with virtual roots,

Section E.3 deals with real closed rings and Section E.4 proposes a definition for *non* discrete real closed fields as local real closed rings. The theory of real closed rings is presented here in an elementary, purely equational form, in the style of [69].

Chapter F deals with an infinitary geometric theory where we add the axiom that the field of real numbers is *archimedean*.

<footnote n="1">¹In this text, a negation is italicised when the corresponding statement, true in classical mathematics, implies in constructive mathematics a well-recorded non-constructive principle, such as **LPO** or even **MP**.</footnote>
Thus, we propose for the coveted dynamical theory the structure of a local real closed ring (possibly archimedean if that proved useful).

In a concluding chapter, we summarise the situation we have arrived at, specifying the important questions, from a constructive point of view, which we do not know how to answer satisfactorily today.
# C. Ordered fields

## Sommaire

<table><tr><td>Introduction</td><td>43</td></tr><tr><td>C.1 About discrete ordered fields</td><td>44</td></tr><tr><td>A natural dynamical theory for discrete ordered fields</td><td>44</td></tr><tr><td>Some valid rules in Cod</td><td>45</td></tr><tr><td>Weaker dynamical theories</td><td>46</td></tr><tr><td>An example with nilpotents</td><td>47</td></tr><tr><td>Adding the function symbol ∨ for the lub</td><td>48</td></tr><tr><td>C.2 Formal Positivstellensätze</td><td>48</td></tr><tr><td>The demonstrative force of formal Positivstellensätze</td><td>49</td></tr><tr><td>Concrete Positivstellensatz</td><td>50</td></tr><tr><td>C.3 Non discrete ordered fields</td><td>51</td></tr><tr><td>A first dynamical theory</td><td>51</td></tr><tr><td>The convexity axiom and the theory Co</td><td>52</td></tr><tr><td>Other continuous operations</td><td>53</td></tr><tr><td>C.4 A non-archimedean non discrete ordered field</td><td>54</td></tr><tr><td>C.5 Non discrete real closed fields: position of the problem</td><td>57</td></tr><tr><td>The principle of extension by continuity</td><td>57</td></tr><tr><td>Continuous semialgebraic maps</td><td>58</td></tr><tr><td>Continuous parametrisation of continuous semialgebraic maps</td><td>58</td></tr><tr><td>A reasonable definition</td><td>59</td></tr><tr><td>Rational dynamical theories for real number algebra</td><td>60</td></tr><tr><td>C.6 General properties of continuous semialgebraic maps</td><td>61</td></tr><tr><td>Stability by composition</td><td>61</td></tr><tr><td>Stability by upper bound</td><td>61</td></tr><tr><td>Finiteness properties</td><td>62</td></tr><tr><td>C.7 Some questions</td><td>62</td></tr><tr><td>Continuous variations</td><td>62</td></tr></table>

## Introduction

This chapter offers a first constructive approach to the classical theory of real closed fields. In fact, the classical theory applies only to real closed fields for which we have a sign test on any element of the field, if it is given in accordance with the definition. In other words, the usual classical theory is a theory of discrete real closed fields. But it is well known that matrix numerical analysis, used in applications of the theory to concrete situations, never uses such a sign test. A constructive approach to a theory of algebraic properties of the real number field requires a dynamical theory of non discrete real closed fields.
Section C.1 gives some reminders on the dynamical theory of discrete ordered fields and that of discrete real closed fields.

Section C.2 explains the great utility of formal Positivstellensätze.

Section C.3 proposes an axiomatic for non discrete ordered fields (Definition C.3.7). We must abandon the axioms of total order in their usual discrete formulation and replace them with dynamical rules relevant to $\mathbb{R}$. We then find that many well-defined continuous rational maps on $\mathbb{Q}$, such as the map sup, need to be introduced into the language.

Section C.4 describes an example of a non discrete non-archimedean Heyting ordered field.

Section C.5 gives a first discussion of acceptable dynamical theories for $\mathbb{R}$ as a non discrete real closed field. We are guided by the continuity extension principle C.5.2 which can be seen as an algebraic version of the completeness of $\mathbb{R}$. In this framework Theorem C.5.4 plays a fundamental role for a relevant definition of continuous semialgebraic maps, by reducing the definition to the case of continuous semialgebraic maps in the discrete framework of $\mathbb{R}_{alg}$.

# C.1. About discrete ordered fields

## A natural dynamical theory for discrete ordered fields

We recall here the dynamical theory of discrete ordered fields Cod given in [17].

$$ \text{Signature: } (\cdot = 0, \cdot > 0, \cdot \ge 0; \cdot + \cdot, \cdot \times \cdot, -\cdot, 0, 1). $$

If we want to give a dynamic discrete ordered field, i.e. a dynamic algebraic structure of type Cod, we add to the signature a presentation by generators and relations of the dynamic algebraic structure considered. For example, this can be the empty presentation, or a countable set of generators, without any relations, or it can be based on an existing algebraic structure in which certain relations are required to be preserved, for example all the equality relations between terms constructed on the elements of the structure. Thus any ring defines a dynamic discrete ordered field.

### Abbreviations

* $x \# 0$ means $x^2 > 0$

* $x = y$ means $x - y = 0$

* $x > y$ means $x - y > 0$

* $x < y$ means $y > x$

* $x \ge y$ means $x - y \ge 0$

* $x \# y$ means $x - y \# 0$

* $x \le y$ means $y \ge x$

### Axioms

#### Direct rules

First we put the axioms of commutative rings, then the rules concerning $\cdot = 0$ and $\cdot \ge 0$, then the rules involving $\cdot > 0$.

$$ \texttt{ga0} \vdash 0 = 0 $$

$$ \texttt{ga2} \quad x = 0, y = 0 \vdash x + y = 0 $$

$$ \texttt{gao1} \quad x = 0 \vdash x \ge 0 $$

$$ \texttt{gao2} \quad x \ge 0, y \ge 0 \vdash x + y \ge 0 $$

$$ \texttt{ac1} \quad x = 0 \vdash xy = 0 $$

$$ \texttt{ao1} \quad \vdash x^2 \ge 0 $$

$$ \texttt{ao2} \quad x \ge 0, y \ge 0 \vdash xy \ge 0 $$
$$ \mathbf{aso1} \vdash 1 > 0 $$

$$ \mathbf{aso2} \quad x > 0 \vdash x \ge 0 $$

Collapse

$$ \mathbf{col}_> 0 > 0 \vdash 1 = 0 $$

Simplification rules

$$ \mathbf{Gao} \quad x \ge 0, x \le 0 \vdash x = 0 $$

$$ \mathbf{aso3} \quad x > 0, y \ge 0 \vdash x + y > 0 $$

$$ \mathbf{aso4} \quad x > 0, y > 0 \vdash xy > 0 $$

Dynamical rules

$$ \mathbf{IV} \quad x > 0 \vdash \exists y xy = 1 $$

$$ \mathbf{ED}_> \vdash x = 0 \quad \mathbf{op} \quad x^2 > 0 $$

$$ \mathbf{lv} \quad xy = 1 \vdash x^2 > 0 $$

$$ \mathbf{OT} \quad \vdash x \ge 0 \quad \mathbf{op} \quad x \le 0 $$

The dynamical theory *Crcd* of discrete real closed fields is obtained from the theory *Cod* by adding as axioms the dynamical rules $\mathbf{RCF}_n$.<fnref n="1" />

$$ \mathbf{RCF}_n \quad a < b, P(a)P(b) < 0 \vdash \exists x (P(x) = 0, a < x < b) \quad (P(x) = \sum_{k=0}^{n} a_k x^k) $$

The rules **gao1** and **gao2** express, in the context of abelian groups, the reflexivity and transitivity of the order relation (compatible with the group law). The rule **Gao** corresponds to anti-symmetry for the order relation.

The rules **ED>_** and **OT** express that the equality is discrete and the order total. They are not satisfied constructively for $\mathbb{R}$. For Bishop's reals, the rule **ED>_** is equivalent to the omniscience principle **LPO** and the rule **OT** is equivalent to the principle **LLPO**. Note also that the principle "any regular element of $\mathbb{R}$ is invertible" is equivalent to the Markov principle<fnref n="2" /> **MP**.

Given the form "without negation" adopted here for collapse, the trivial ring is a discrete ordered field, and the collapse axiom **col>_** is a consequence of **IV**.

By means of the direct rules alone we see that $1 = 0 \vdash (x = 0, x \ge 0, x > 0)$. This justifies taking $1 = 0$ as a substitute for $\mathbf{1}$. And the collapse rule looks like a simplification rule.

## Some valid rules in Cod

Four valid simplification rules

$$ \mathbf{Anz} \quad x^2 = 0 \vdash x = 0 $$

$$ \mathbf{Aonz} \quad c \ge 0, x(x^2 + c) \ge 0 \vdash x \ge 0 $$

$$ \mathbf{Aso1} \quad x > 0, xy \ge 0 \vdash y \ge 0 $$

$$ \mathbf{Aso2} \quad x \ge 0, xy > 0 \vdash y > 0 $$

Two valid dynamical rules

$$ \mathbf{OTF} \quad x + y > 0 \vdash x > 0 \quad \mathbf{op} \quad y > 0 $$

$$ \mathbf{OTF}^* \quad xy < 0 \vdash x < 0 \quad \mathbf{op} \quad y < 0 $$

Note that the rule **Aso1** implies that elements $> 0$ are regular.

<footnote n="1">¹A theorem essentially equivalent to these rules is proved by Bishop for the field $\mathbb{R}$, but using the axiom of dependent choice.</footnote>

<footnote n="2">²Equivalence suggested by Fred Richman.</footnote>
**Lemma C.1.1.** The following rule is provable with direct axioms.

$$ \mathbf{Aonz2} \quad c \ge 0, x(x^2 + c) \ge 0, x < 0 \vdash 0 > 0 $$

**Theorem C.1.2.** With the exception of the rules $\mathbf{ED}_>$ and $\mathbf{OT}$, all the above rules are constructively valid for $\mathbb{R}$, without using the axiom of dependent choice.

*Proof.* Everything is clear except perhaps the rule **Aonz**. For $x \in \mathbb{R}$, we can prove $x \ge 0$ by reducing $x < 0$ to the absurd. This is what **Aonz2** does (take $c = 0$). □

*Remark C.1.3.* The rules $\mathbf{ED}_>$ and $\mathbf{OTF}^\times$ imply the rule $\vdash x = 0 \quad \mathbf{op} \ x < 0$, $\mathbf{op} \ x > 0$, and a fortiori $\mathbf{OT}$. See also D.4.1, D.4.4 and D.5.4. ■

If $\mathbf{K}$ is a discrete ordered field, we denote $\mathbf{Cod}(\mathbf{K})$ the dynamic algebraic structure of type $\mathbf{Cod}$ having for presentation the *positive diagram of K*. A non-trivial model of $\mathbf{Cod}(\mathbf{K})$ is a non-trivial discrete ordered field $\mathbf{L}$ given with a morphism $\mathbf{K} \to \mathbf{L}$. Similarly, if $\mathbf{A}$ is a commutative ring (or an ordered ring), we denote $\mathbf{Cod}(\mathbf{A})$ the dynamic algebraic structure of type $\mathbf{Cod}$ having for presentation the *positive diagram of A*. A model of $\mathbf{Cod}(\mathbf{A})$ is a discrete ordered field $\mathbf{L}$ given with a morphism $\mathbf{A} \to \mathbf{L}$ (of commutative ring, or of ordered ring).

## Weaker dynamical theories

The rule **Aonz** implies $x^3 \ge 0 \vdash x \ge 0$, therefore also, under **Gao**, $x^3 = 0 \vdash x = 0$, and a fortiori **Anz**.

**Definition C.1.4.**

Theories based on the language of ordered rings ($\cdot = 0, \cdot \ge 0; \cdot + \cdot, \cdot \times \cdot, -\cdot, 0, 1$).

1. The direct theory *Apo* of *preordered rings*. The axioms are those of commutative rings and the direct rules **gao1**, **gao2**, **ao1**, **ao2**.

2. The Horn theory *Ao* of *ordered rings*. The axioms are those of pre-ordered rings and the simplification rule **Gao**.

3. The Horn theory *Aonz* of *strictly reduced ordered rings*<fnref n="3" /> is obtained by adding the simplification rule **Aonz** to the theory *Ao*.

4. The dynamical theory *Ato* of *linearly ordered rings*<fnref n="4" /> is obtained by adding the dynamical rule **OT** to the theory *Ao*.

5. The dynamical theory *Atonz* of *reduced linearly ordered rings* is obtained by adding the dynamical rule **Anz** to the theory *Ato*. This theory proves the rules **Aonz** and **ASDZ** (Lemma C.1.6).

Theories based on the language of strictly ordered rings: we add the predicate $\cdot > 0$.

6. The direct theory *Apro* of *proto-ordered rings* (cf. [17]). The axioms are those of commutative rings, all the direct rules stated for $\mathbf{Cod}$ (**gao1**, **gao2**, **ao1**, **ao2**, **asol** to **aso4**) and the collapsus $\mathbf{col}_>$.

7. The Horn theory *Aso* of *strictly ordered rings* is the theory *Apro* to which we add the simplification rules **Gao**, **Aso1** and **Aso2**. It can also be seen as constructed from *Ao* by adding the predicate $\cdot > 0$ in the language, the direct rules **asol** to **aso4** and the simplification rules **Aso1** and **Aso2**.

<footnote n="3">³The rule **Aonz** is stronger than the rule **Anz**, so "strictly reduced" is used rather than "reduced". However, see Item 3 of Lemma C.1.6.</footnote>

<footnote n="4">⁴An order relation is *linear* or *total* when two elements are always comparable.</footnote>
8. The Horn theory Asonz of reduced strictly ordered rings ("quasi-ordered rings" in [17]) is obtained by adding the simplification rule Aonz to Aso. It can also be seen as the theory Apro to which we add the simplification rules Gao, Aonz, Aso1 and Aso2.

9. The dynamical theory Asto of strictly linearly ordered rings is the theory Aso to which we add the dynamical rule OT. It can also be seen as constructed from Ato by adding the predicate $>0$ in the language, the direct rules aso1 to aso4 and the simplification rules Aso1 and Aso2.

10. The dynamical theory Aito of linearly ordered integral rings is obtained by adding the dynamical rule ED> to Aso. The rules Aonz, OTF and OTF × are valid in this theory.

In Items 6, 7 and 8, the meaning of $x > 0$ is not fixed a priori. This can range from "$x$ is regular and $\ge 0$" to "$x$ is invertible and $\ge 0$".

The direct theory Apro is the one in which the collapse is the clearest, directly given by an algebraic certificate, as specified in the following lemma.

Recall that in a ring, a cone is a part $C$ which contains squares and which is stable by addition and product: $C + C \subseteq C$, $C \times C \subseteq C$.

**Lemma C.1.5 (algebraic certificate of collapse).** Let $K$ be a dynamic algebraic structure of type Apro given by a presentation $(G; R_{>0}, R_{\ge 0}, R_{=0})$ with the following meaning: $G$ is the set of generators of the structure, $R_{>0}$, $R_{\ge 0}$ and $R_{=0}$ are three parts of $Z[G]$, the elements of $R_{>0}$ (resp. $R_{\ge 0}$, $R_{=0}$) are assumed $> 0$ (resp. $\ge 0$, $= 0$) in the structure. The dynamic algebraic structure $K$ collapses if, and only if, we have in $Z[G]$ an equality

$$s + p + z = 0$$

where $s$ is in the multiplicative monoid generated by $R_{>0}$, $p$ is in the cone generated by $R_{>0} \cup R_{\ge 0}$ and $z$ in the ideal generated by $R_{=0}$.

**Lemma C.1.6.** (See also Lemma D.4.1.)

1. The dynamical theory Aso proves the simplification rule **lv** and the collapsus **col**.

2. The dynamical theory Ato proves the following simplification rules.

$$\textcolor{red}{\mathbf{Afr4}} \quad y \ge 0, xy = 1 \vdash x \ge 0$$

$$\textcolor{red}{\mathbf{Afr5}} \quad c \ge 0, x(x^2 + c) \ge 0 \vdash x^3 \ge 0$$

3. The theory Atonz proves the rules Aonz and ASDZ.

*Proof.* Items 1 and 2 are easy. For Item 3, Aonz follows from Afr5. Let's look at ASDZ. Let $a, b$ be such that $ab = 0$; if $|a| \le |b|$, we have $0 \le |a|^2 \le |ab| = 0$ so $a = 0$, and in the case where $|b| \le |a|$ we get $b = 0$. $\square$

In the Aso theory, the rule Afr4 is a weakened variant of Aso1. In the Ao theory, the rule Afr5 is a weakened variant of Aonz.

In a linearly ordered ring, if we define "$x > 0$" by "$x$ is regular and $\ge 0$", all the rules that define Aso are satisfied (and $x \ne 0$ is a priori stronger than the simple negation of $x = 0$). This explains the interest of the Horn theory Aso. A lattice variant, the Asr theory of strict $f$-rings, will be defined later.

## An example with nilpotents

**Example C.1.7 (a non-reduced linearly ordered ring).** The example we now give is the one that should be kept in mind in order to fully understand the difference between linearly ordered rings and linearly ordered domains.

This is the linearly ordered ring $Q[\alpha]$ where $\alpha > 0$ and $\alpha^6 = 0$ ($\alpha$ is an infinitesimal $> 0$ nilpotent). Let $c$ be an element such that $c^2 = 0$ (for example $c = \alpha^5$). The system of constraints
$$x^2 = c^2, x \ge 0,$$

which could be suggested to characterise $|c|$ without using the sign test in the case of an ordered field, now admits an infinite number of solutions: all $r\alpha^3 + y\alpha^4$ where $r > 0$ in $\mathbb{Q}$ and $y$ arbitrary in $\mathbb{Q}[\alpha]$. ■

## Adding the function symbol $\lor$ for the lub

In a linearly ordered set, and even more so in a discrete ordered field, every pair of elements has a least upper bound (lub): the greater of the two. We therefore change nothing essential in the theory of *Cod* by adding a function symbol $\cdot \lor \cdot$ subject to the three axioms which define the sup of two elements, when it exists for a of given order relation.

**Definition C.1.8.** The dynamical theory of discrete ordered fields with sup, denoted *Codsup*, is the dynamical theory of discrete ordered fields to which we add a function symbol $\cdot \lor \cdot$ and for axioms the following Horn rules **sup1**, **sup2** and **Sup**.

$$\mathbf{sup1} \vdash x \lor y \ge x$$

$$\mathbf{sup2} \vdash x \lor y \ge y$$

$$\mathbf{Sup} \quad z \ge x, z \ge y \vdash z \ge x \lor y$$

From the theories *Ato*, *Asto*, *Aito* and *Crcd* the theories *Atosup*, *Astosup*, *Aitosup* and *Crcdsup* are defined in the same way.

In the case of discrete ordered fields and discrete real closed fields we could also have replaced the Horn rule **Sup** by the following direct rule **sup**, so as to add only direct rules to *Cod*.

$$\mathbf{sup} \vdash ((x \lor y) - x) ((x \lor y) - y) = 0$$

We can also think of the theory *Crcdsup* as the theory *Codsup* to which we add the axioms of real closure $\mathbf{RCF}_n$.

**Remark C.1.9.** The theories *Cod* and *Codsup* are essentially identical. The same applies to the other pairs of theories in Definition C.1.8. ■

## C.2. Formal Positivstellensätze

The formal Positivstellensatz of classical mathematics ([Bochnak, Coste & Roy, Theorem 4.4.2]) admits the following constructive version (see [17]).

**Formal Positivstellensatz C.2.1** (concrete formal Positivstellensatz for ordered fields, 1). Let $\mathbf{R}$ be a *dynamic algebraic structure in the language of strictly ordered rings*.

1. The dynamical theories *Apro*, *Aso*, *Cod* and *Crcd* collapse simultaneously.

2. The dynamical theories *Asonz*, *Aito*, *Cod* and *Crcd* prove the same Horn rules.

The strength of this theorem lies in the fact that the collapse of a *dynamic algebraic structure* of type *Apro* is given by an *algebraic certificate of collapse* (Lemma C.1.5), which we call a *Positivstellensatz*.

As a special case, for a commutative ring $\mathbf{R}$, the *dynamic algebraic structure* *Crcd*(R) collapses if, and only if, $-1$ is a sum of squares in $\mathbf{R}$.

In classical mathematics, thanks to Gödel's completeness theorem A.5.1, we deduce from previous Item 1 the abstract formal Positivstellensatz in the following form (see [17]).

A system of sign conditions imposed on elements of a ring $\mathbf{A}$ admits an algebraic certificate of impossibility if, and only if, the only model of *Cod*(A) is trivial, if, and only if, the only model of *Crcd*(A) is trivial.
Item 2 of C.2.1 also admits “abstract” classical versions via model theory, in application of Theorem A.5.4 (see [17]).

We now examine what happens to the previous results in the absence of the predicate “$\cdot > 0$” in the presentation of a dynamic algebraic structure.

**Formal Positivstellensatz C.2.2** (concrete formal Positivstellensatz, 1bis). Let $\mathbf{R}$ be a dynamic algebraic structure in the language of ordered rings.

1. The dynamical theories $Ao$, $Apro$, $Ato$, $Cod$ and $Crcd$ collapse simultaneously.

2. The dynamical theories $Aonz$, $Atonz$, $Cod$ and $Crcd$ prove the same Horn rules.

NB. The language used for the presentation must not mention the predicate $\cdot > 0$. There is no collapse axiom in $Ao$ and $Ato$, and a dynamic algebraic structure of type $Ao$ or $Ato$ is said to collapse when it proves $1 = 0$.

*Proof. 1.* Consider a dynamic algebraic structure $\mathbf{A}$ for $Ao$. The same presentation gives a dynamic algebraic structure $\mathbf{A}'$ for $Apro$. Suppose that $\mathbf{A}'$ proves $1 = 0$. The collapse for $\mathbf{A}'$ (of type $Apro$) has the form of a very precise algebraic certificate (a Positivstellensatz). This certificate is written $1 + p = 0$, where $p$ is $\ge 0$ by virtue of the presentation and the axioms of $Ao$. We therefore have both $1 \ge 0$ and $1 \le 0$ in $\mathbf{A}$, so $1 = 0$ by virtue of *Gao*. Conversely, if $\mathbf{A}$ proves $1 = 0$, then a fortiori the same will be true for $\mathbf{A}'$.

Finally, we apply Positivstellensatz C.2.1 and note that $Ato$ is an intermediate theory between $Ao$ and $Cod$.

2. Consider a dynamic algebraic structure $\mathbf{A}$ for $Aonz$. It suffices to prove the result for a fact of the form $x \ge 0$ (because $x = 0$ is equivalent to $x \ge 0$ and $x \le 0$). This fact is valid in $Cod$ if, and only if, the fact $x < 0$ collapses the dynamic algebraic structure $Cod(\mathbf{A})$. According to Positivstellensatz C.2.1, this corresponds to an algebraic certificate of the form $x^{2n}+p = xq$, where $p$ and $q$ are $\ge 0$ by virtue of the presentation and the axioms of $Ao$. This gives $x(x^{2n}+p) \ge 0$, then $x^k(x^{2k}+p_1) \ge 0$ for a suitable odd integer $k$. The rule **Aonz** tells us that $x^k \ge 0$ in $\mathbf{A}$. This same rule shows that $x^3 \ge 0$ implies $x \ge 0$, and consequently $x^k \ge 0$ implies $x \ge 0$ for all odd $k$. $\square$

A consequence of Item 1 in classical mathematics (via Theorem A.5.3) is that a field $\mathbf{K}$ in which $-1$ is not a sum of squares can be ordered. On the other hand, the only known computational meaning of this result of classical mathematics is that the theory $Cod(\mathbf{K})$ collapses if, and only if, $-1$ is a sum of squares in $\mathbf{K}$.

From a classical point of view, since the theory $Cod(\mathbb{R})$ does not collapse, we can provide $\mathbb{R}$ with an order relation which extends the usual order relation and which is a total order. But the only constructive meaning of this result of classical mathematics is that $-1$ is not a sum of squares in $\mathbb{R}$.

## The demonstrative force of formal Positivstellensätze

The dynamical theories we explore in the following to describe the algebraic properties of real numbers are extensions of $Asonz$ (if the predicate $\cdot > 0$ is present) or $Aonz$ (in the opposite case). Moreover, the theories explored are always weaker than $Crcd$. And any Horn rule valid in the dynamical theory $Crcd$ is valid in $Asonz$ (in $Aonz$ if the predicate $\cdot > 0$ is absent).

Now $\mathbb{R}$ constitutes a constructive model of the $Asonz$ theory for the language based on the signature $(\cdot = 0, \cdot > 0, \cdot \ge 0, \cdot + \cdot, \cdot \times \cdot, \cdot - , 0, 1)$ (Theorem C.1.2).

Thus from the point of view of Horn rules alone, the formal Positivstellensätze tell us that the theory $Crcd$ is entirely satisfactory, including for $\mathbb{R}$, which does however satisfy neither $col_>$ nor $OT$. However, to temper this optimistic statement, here is the precise result. Note also that it applies only to Horn rules, not to other dynamical rules.

**Theorem C.2.3.** Consider a Horn rule formulated in the dynamic algebraic structure $\mathbf{R} = Asonz(\mathbb{R})$. If the constants involved in the rule are in a discrete subfield $\mathbf{R}_0$ of $\mathbb{R}$, for the rule to be valid in $\mathbf{R}$, it is sufficient for it to be valid in $Crcd(\mathbf{R}_0)$.
The existential rules satisfied in $\mathbb{R}$ and introduced in the dynamical theories under consideration will as far as possible be treated in the framework of provably unique existences and can therefore be skolemised without damage, providing theories without existential axioms which are essentially equivalent to those which would have required existential axioms.

**Remark C.2.4.** We can also apply Theorem A.3.6 with the dynamical theory $\mathcal{CoO}(\mathbb{R})$ (Definition C.3.2). We will then introduce a predicate $x \succcurlyeq y$ opposed to $x < y$. The new dynamical theory will treat $\mathbb{R}$ as a discrete ordered field and any dynamical rule proved in the new theory but not using $x \succcurlyeq y$ will also be valid in $\mathbb{R}$. The disadvantage is of course that $\mathbb{R}$ is not a constructive model of the new theory. Another drawback is the mysterious status of the new predicate $x \succcurlyeq y$, which is weaker than $x \geq y$ in the new dynamical theory. In conclusion, the advantage that Theorem A.3.6 seems to provide (the use of classical logic is harmless) does not seem to go beyond the considerations we have developed on the proper use of the formal Positivstellesatz. ■

## Concrete Positivstellensatz

First, we recall Tarski's fundamental theorem. For a simple Cohen-Hormander proof, see [Bochnak, Coste & Roy, Section 1.4] or [17, Lemma 3.12]. Some instructive comments can be found in [43, Theorems 10, 11, 12].

**Theorem C.2.5 (elimination of quantifiers).** The first-order intuitionistic formal theory associated with the dynamical theory $\mathcal{Crcd}$ admits the elimination of quantifiers. It is complete and decidable. In particular, it exhaustively describes all the purely algebraic properties of $\mathbb{R}_{\text{alg}}$ (those formulated to first-order in the language of ordered rings).

This paragraph gives a theorem equivalent to Krivine-Stengle's Positivstellensatz, stated here in the language of dynamic algebraic structures.

A constructive proof of Positivstellensatz C.2.6 can be found in [17] or [34]. It is based on the formal Positivstellensatz and on Lemma 3.12 of [17], a variant of Tarski's theorem.

For a more conceptual approach and better complexity bounds see [LPR]. For the construction of the real closure of a discrete ordered field see [42, 43].

**Positivstellensatz C.2.6 (concrete Positivstellensatz).**

Let $\mathbf{K}$ be a discrete ordered field and $\mathbf{R}$ be a discrete real closed field containing $\mathbf{K}$, (for example the real closure of $\mathbf{K}$). Let $\mathbf{A} = ((G, \text{Rel}), \mathcal{Cod}(\mathbf{K}))$ be a dynamic algebraic structure where $G = (x_1, \dots, x_n)$ and where $\text{Rel}$ is finite.

1. The dynamic algebraic structure $\mathbf{A}$ collapses if, and only if, it is impossible to find a model of $\mathbf{A}$ contained in $\mathbf{R}$.

2. The collapse if it occurs is given by an algebraic certificate according to Item 1 of Theorem C.2.1 and Lemma C.1.5.

3. We have an algorithm which decides whether $\mathbf{A}$ collapses and which in the case of a negative answer gives the description of a system $(\xi_1, \dots, \xi_n)$ in $\mathbf{R}^n$ which satisfies the constraints given in the relations $\text{Rel}$.

This statement is not valid in this general form if we take $\mathbf{K} = \mathbf{R} = \mathbb{R}$ because there is no sign test in $\mathbb{R}$ and the algorithms which explicite Positivstellensatz C.2.6⁵ make crucial use of this sign test.

Here's a small example of the problems we run into. On $\mathbb{R}$, as on an arbitrary local ring<fnref n="6" /> in which $x \neq 0$ denotes the invertibility predicate, we have the equivalence

$$ \exists y x^2 y = x \iff x = 0 \text{ or } x \neq 0. \qquad (C.1) $$

<footnote n="5">⁵These algorithms are provided by the constructive proof of the theorem.</footnote>

<footnote n="6">⁶For the constructive treatment of local rings, the Jacobson radical and Heyting fields see for example [CACM, section IX-1].</footnote>
Let's assume that $x(1 - xy) = 0$. If $xy$ is invertible, then $x$ is invertible, and if $1 - xy$ is invertible, then $x = 0$. This proof translates formally into the corresponding dynamical theory by establishing the following three valid rules:

• $x^2y = x \vdash x = 0 \quad \mathbf{op} \ x \# 0$,

• $x = 0 \vdash \exists y x^2y = x$,

• $x \# 0 \vdash \exists y x^2y = x$.

This simple case of eliminating the quantifier $\exists$ shows that the calculations lead to dead ends from the point of view of decidability, since "$x = 0$ or invertible" is undecidable in $\mathbb{R}$.

Nevertheless, in the final section of the article [26], we find a fully satisfactory constructive form for the 17th Hilbert problem on $\mathbb{R}$. And other cases of constructively provable Positivstellensätze on $\mathbb{R}$ are also treated.

## C.3. Non discrete ordered fields

As a first approximation, and following a suggestion by Heyting, we could choose as a first-order formal theory for the algebraic properties of $\mathbb{R}$ the *Asonz* theory (seen as a first-order formal theory) to which we add the geometric axioms **IV** and **OTF** as well as the following axiom **HOF**, non-geometric and therefore undesirable.

**HOF** ($x > 0 \Rightarrow 1 = 0) \Rightarrow x \le 0$ (Heyting axiom for ordered field)

This amounts to replacing the axioms **col**> and **OT** by the axioms **OTF** and **HOF**. We then have a local ring structure, because the rules **IV** and **IV** imply that "$x \# 0$" means "$x$ is invertible", so **OTF** implies that for all $x$, $x$ or $1 - x$ is invertible. In this context, the axiom **HOF** means that the Jacobson radical is reduced to 0.

**Remark C.3.1.** Note that the axiom **HOF**, which can be formulated to first-order even though it is not part of dynamical theories, is satisfied indirectly in the following form: in a *dynamic algebraic structure of type Asonz*, if a *closed term* $t$ verifies $t > 0 \vdash \mathbf{1}$, then it also verifies $\vdash t \le 0$. This follows from the formal Positivstellensatz.

In fact we even have: *if a closed term $t$ verifies $t \ge 0 \vdash \mathbf{1}$, then it also verifies $\vdash t < 0$. This means that Markov's principle, which is expressed on $\mathbb{R}$ by the implication $\neg(t \ge 0) \Rightarrow t < 0$ holds as an external deduction rule*<fnref n="7" /> *admissible in the dynamical theory Asonz($\mathbb{R}$).*

The same remarks apply to dynamical theories which extend *Asonz* while simultaneously collapsing.

### A first dynamical theory

Apart from the undesirable character of **HOF**, the formal theory considered at the beginning of the section has a major drawback, which is that it cannot prove the existence of the upper bound of two elements: see on this subject [13].

It is therefore legitimate to explore the possibilities offered by the addition of a law for this upper bound, with the appropriate rules. We now propose a minimalist dynamical theory for *non discrete ordered fields* by introducing the function symbol $\lor$ into the language.

**Definition C.3.2.** A first minimal dynamical theory for *non discrete ordered fields*, denoted *Co0*, is based on the following signature. There is only one sort, named *Co0*.

$$ \text{Signature}: \quad \Sigma_{Co0} = (\cdot = 0, \cdot \ge 0, \cdot > 0; \cdot + \cdot, \cdot \times \cdot, \cdot \lor \cdot, \cdot \land 0, 1) $$

<footnote n="7">⁷We must add the word *external* here, as this is not a valid rule in the dynamic algebraic structure itself. It refers to the fact that we deduce the validity of one rule from that of another rule.</footnote>
The axioms are those of *Asonz*, the axioms **IV** and **OTF**, and the natural axioms for $\lor: \sup_1$, **sup2**, **Sup**, **grl** and **afr**. They are all listed below ($x^+$ is an abbreviation of $x \lor 0$).

$$ga0 \vdash 0 = 0$$

$$ga2 \quad x = 0, y = 0 \vdash x + y = 0$$

$$gao1 \quad x = 0 \vdash x \ge 0$$

$$gao2 \quad x \ge 0, y \ge 0 \vdash x + y \ge 0$$

$$aso1 \vdash 1 > 0$$

$$aso2 \quad x > 0 \vdash x \ge 0$$

$$sup1 \vdash x \lor y \ge x$$

$$sup2 \vdash x \lor y \ge y$$

$$Gao \quad x \ge 0, x \le 0 \vdash x = 0$$

$$Anz \quad x^2 = 0 \vdash x = 0$$

$$Aonz \quad c \ge 0, x(x^2 + c) \ge 0 \vdash x \ge 0$$

$$Sup \quad z \ge x, z \ge y \vdash z \ge x \lor y$$

$$IV \quad x > 0 \vdash \exists y xy = 1$$

$$ac1 \quad x = 0 \vdash xy = 0$$

$$ao1 \quad \vdash x^2 \ge 0$$

$$ao2 \quad x \ge 0, y \ge 0 \vdash xy \ge 0$$

$$aso3 \quad x > 0, y \ge 0 \vdash x + y > 0$$

$$aso4 \quad x > 0, y > 0 \vdash xy > 0$$

$$grl \quad \vdash x + (y \lor z) = (x + y) \lor (x + z)$$

$$afr \quad \vdash x^+ (y \lor z) = (x^+ y) \lor (x^+ z)$$

$$lv \quad xy = 1 \vdash x^2 > 0$$

$$Aso1 \quad x > 0, xy \ge 0 \vdash y \ge 0$$

$$Aso2 \quad x \ge 0, xy > 0 \vdash y > 0$$

$$OTF \quad x + y > 0 \vdash x > 0 \quad op \ y > 0$$

*Remarks C.3.3.*

1) Note that the collapse “ $0 > 0 \vdash 1 = 0$ ” is deduced from **IV**.

2) If we add the axioms **OT** and **col>** to the theory **Co0** we find a theory which is essentially identical to **Codsup** or **Cod**. In fact, we just need to add the axiom **ED>**: see Lemma D.4.1. ■

**Examples C.3.4.** Many natural subfields of $\mathbb{R}$ are non discrete, for example the enumerable field $\mathbb{R}_{\text{PR}}$ of real numbers computable in primitive recursive time, or the enumerable field $\mathbb{R}_{\text{Ptime}}$ of real numbers computable in polynomial time, or the non enumerable field $\mathbb{R}_{\text{Rec}}$ of recursive real numbers. A satisfactory dynamical theory for the algebraic properties of the real numbers will have to accept as models these natural subfields of $\mathbb{R}$. ■

The subfields $\mathbb{R}_{\text{PR}}$ and $\mathbb{R}_{\text{Ptime}}$ can be handled on a machine in a nicer way than the field $\mathbb{R}_{\text{Rec}}$. These are enumerable fields (albeit non discrete), whose elements do not need to be accompanied by “certificates” external to the dynamical theory under consideration (a general recursive map exists constructively only if it is accompanied by a “certificate”: a constructive proof of the fact that it is total).

Note that the “complete” character of $\mathbb{R}$ seems to come more from analysis than from algebra. Note also that the “field” of Puiseux series on $\mathbb{R}$ does not seem to satisfy **OTF** (for any attempt at a reasonable definition for the order relation).

## The convexity axiom and the theory Co

In addition to the lub map, other “rational” maps pose the same kind of problem.

In the theory of real closed rings, in classical mathematics, (see the articles [63, 56] and Section E.3), the following axiom “of convexity”<fnref n="8" /> is satisfied

<footnote n="8">⁸There are two very distinct uses of the term “convex” in the present text. On the one hand, an ordered ring can be declared convex, as here. On the other hand, a subgroup of an ordered group can be declared convex as page 70.</footnote>
$$ \textcolor{red}{\mathbf{CVX}} \quad 0 \le a \le b \vdash \exists z \, zb = a^2 \quad (\text{convexity}) $$

Note that if $zb = a^2$ then $(z \wedge a)b = zb \wedge ab = a^2 \wedge ab = a(a \wedge b) = a^2$. Similarly $(z \vee 0)b = a^2$. Consequently, an equivalent axiom which ensures the uniqueness of $z$ is given by the following dynamical rule:

$$ \textcolor{red}{\mathbf{FRAC}} \quad 0 \le a \le b \vdash \exists z (zb = a^2, 0 \le z \le a) $$

This rule is valid for $\mathbb{R}$ because $z$ can be defined as a continuous map of $(a, b)$ on its domain of definition.

**Lemma C.3.5.** The uniqueness of $z$ (when it exists) in the rule **FRAC** is guaranteed in the Horn theory *Atonz* and in *Co0*. The same calculation shows that uniqueness is guaranteed in the Horn theory *Afrnz* (Lemma D.4.7).

*Proof.* Suppose $yb = zb = a^2$, $0 \le z \le a$ and $0 \le y \le a$. We have $(y - z)b = 0$, $|y - z| \le a \le b$ and thus $|y - z|^2 \le |y - z|b = 0$. $\square$

**Lemma C.3.6.** The addition of the axiom **FRAC** to the theory *Co0* can be replaced by the introduction of a function symbol *Fr* with the axioms

$$ \textcolor{red}{\mathbf{fr1}} \quad \vdash \quad \mathrm{Fr}(a, b) \quad |b| = (|a| \wedge |b|)^2 $$

$$ \textcolor{red}{\mathbf{fr2}} \quad \vdash \quad 0 \le \mathrm{Fr}(a, b) \le |a| \wedge |b| $$

The same applies to the theories *Atonz* and *Afrnz*.

*Proof.* The rule **FRAC** is equivalent to the following rule

$$ \bullet \quad \vdash \quad \exists z \, (z |b| = (|a| \wedge |b|)^2, 0 \le z \le |a| \wedge |b|) $$

We have therefore simply skolemised an existential rule in the case of unique existence (Lemma C.3.5). This gives us an essentially identical extension (see page 27). Moreover, once the function symbol *Fr* and the axioms **fr1** and **fr2** are added, the rule **FRAC** clearly becomes unnecessary. $\square$

**Definition C.3.7.** The dynamical theory *Co* of non discrete ordered fields<fnref n="9" /> is the extension of the theory *Co0* obtained by adding the function symbol *Fr* and the axioms **fr1** and **fr2**.

This is a one sort dynamical theory with the signature

$$ \text{Signature:} \qquad \Sigma_{Co} = (\cdot = 0, \cdot \ge 0, \cdot > 0, \cdot +, \cdot \times, \cdot, \cdot \vee, \cdot, \cdot - , \mathrm{Fr}(\cdot, \cdot), 0, 1) $$

The non discrete subfields of $\mathbb{R}$ of Example C.3.4 are models of *Co*, and also of certain extensions of *Co* which we define later, such as *Crc1* or *Corv*.

**Remark C.3.8.** In formal Positivstellensatz C.2.1 statement, we can add the *Codsup* theory which is essentially identical to the *Cod* theory, and the *Co* theory which is intermediate between *Asonz* and *Codsup*. For more information, see formal Positivstellensatz D.5.6. ■

## Other continuous operations

Here is another paradigmatic example with a continuous function defined everywhere

$$ f(x, y) = \frac{(ax + by)xy}{x^2 + y^2} \qquad (C.2) $$

<footnote n="9">⁹In [40], a slightly different, slightly stronger definition was given, see Remark C.3.9.</footnote>
This rational map<sup>10</sup> is the prototype of a family, parametrised by $a, b$, of continuous real maps $\mathbb{R}^2 \to \mathbb{R}$ (or of a continuous real map $\mathbb{R}^4 \to \mathbb{R}$).

A dynamical rule defines this map:

$$ \vdash \exists z \quad (z(x^2 + y^2) = (ax + by)xy, |z| \le |ax + by|) \qquad (C.3) $$

and it does not seem valid in the basic theory *Co0*.

In this example, if $a = b = 1$, the fraction is of the type $z = u/v$ with $u^2 \le v^3$. It is characterised by the relationships $zv = u$ and $|z|^2 \le |v|$. The following dynamical rules are satisfied for $\mathbb{R}$, and also for discrete real closed fields:

$$ \mathbf{FRAC}_n |u|^n \le |v|^{n+1} \vdash \exists z (zv = u, |z|^n \le |v|) \quad (n \ge 1) $$

Intuitively, this rule means that the fraction $u/v$ is well-defined. In the case of a discrete ordered field we reason case by case: if $v \ne 0$ it is clear, if $v = 0$ the rule forces $z = 0$. More generally we check that existence, if assumed, is uniquely proved in the theory *Afrnz* (page 78) as follows.

If $zv = u = yv$, $|z|^n \le |v|$, $|y|^n \le |v|$, we pose $w = |z - y|$ and we obtain

$$ w|v| = 0, \le |z| + |y| \le 2|v|^{\frac{1}{n}}, w^n \le 2^n|v|, 0 \le w^{n+1} \le 2^n|v|w = 0, $$

therefore $w^{n+1} = 0$ and finally $w = 0$.

Another argument is that the Horn rule

$$ \bullet \quad zv = u, yv = u, |z|^n \le |v|, |y|^n \le |v| \vdash z = y $$

is satisfied in *Cod*, and that *Afrnz* and *Cod* prove the same Horn rules (formal Positivstel- lensatz D.5.6).

In the Horn theory *Aonz* the rule **FRAC** follows from **FRAC**<sub>1</sub> by posing $u = a^2$ and $v = b$.

Conversely, the rules **FRAC**<sub>n</sub> can be deduced from the rule **FRAC** in a fairly general framework (see Lemma D.4.8). In the following we will only use the rule **FRAC**.

**Remark C.3.9.** It would have been more logical to ask, in the definition of the theory *Co*, in addition to the validity of the rule **FRAC**, that of the rules **FRAC**<sub>n</sub> (this was the choice made in the article [40], definition 2.13). More generally, for any map $f: \mathbb{Q}^n \to \mathbb{Q}$ which extends by continuity<sup>11</sup> a fraction $h/p$, where $h$ and $p$ are semipolynomials,<sup>12</sup> the zeros of $p$ being of empty interior, we should ask that the rule analogous to **FRAC**<sub>n</sub> which says that “f exists” be valid, and more precisely introduce a corresponding function symbol with the appropriate axioms. But we did not want to complicate too much the definition of the theory *Co* of non discrete ordered fields insofar as we have essentially in view the theory of non discrete real closed fields, in which the rule **FRAC** is sufficient. ■

## C.4. A non-archimedean non discrete ordered field

In this section we describe an example of a non discrete non-archimedean Heyting ordered field.

Let $\varepsilon$ be an indeterminate. Let $Z = \mathbb{Q}[[\varepsilon]]$ be the ring of formal series with rational coefficients and $Q = \mathbb{Q}((\varepsilon)) := \mathbb{Q}[[\varepsilon]]\langle 1/\varepsilon \rangle$. In classical mathematics $Z$ is a local integral henselian ring and $Q$ is its field of fractions. Let $Z$ have the order relation for which $\varepsilon$ is an infinitesimal > 0 (i.e. $0 < \varepsilon$ and $\varepsilon < r$ for any rational $r > 0$). Let $Z$ be the linearly ordered ring thus obtained. The localised $Z\langle 1/\varepsilon \rangle$ with the order relation compatible with that of $Z$ will again be denoted $Q$. This is probably the simplest example of a non-archimedean Heyting ordered field.

<footnote n="10"><sup>10</sup>It is a priori defined for $(x, y) \ne (0, 0)$ and extends by continuity into $f(0, 0) = 0$. We can then see that it is uniformly continuous on any cube $[-a, +a]^4$.</footnote>

<footnote n="11"><sup>11</sup>More precisely: the fraction $h/p$ with coefficients in $\mathbb{Q}$, defined for $p(x) \ne 0$, must extend into a continuous map $\mathbb{Q}^n \to \mathbb{Q}$.</footnote>

<footnote n="12"><sup>12</sup>A sup-inf combination of polynomials.</footnote>
These classical statements are still valid in constructive mathematics, provided that suitable definitions are used. For example, we will see that, modulo suitable definitions, $\mathbb{Q}$ is a model of the Co theory.

From a constructive point of view, there is no sign test on $\mathbb{Z}$ or on $\mathbb{Q}$. And it is not immediate to define an order structure corresponding to the intuition given by classical mathematics.

Here's how to treat this example constructively. An element of $\mathbb{Z}$ is given by a formal series $\xi = \sum_{j=0}^{+\infty} x_j \varepsilon^j$ with $x_j \in \mathbb{Q}$. Any $c \in \mathbb{Q}$ can be considered as an element of $\mathbb{Z}$ according to the usual procedure. The coefficient $x_j$ is denoted $c_j(\xi)$. Conventionally, $c_j(\xi) = 0$ is given for $j < 0$ in $\mathbb{Z}$ and for all $\xi \in \mathbb{Z}$.

For a series $\xi = \sum_{j=0}^{+\infty} x_j \varepsilon^j$ in $\mathbb{Z}$ we define for each $k \ge 0$ a potential sign in exponent $k$, denoted $\kappa_k(\xi) \in \{-1, 0, 1\}$ as follows, by induction on $k$:

* $\kappa_0(\xi)$ is the sign of $x_0$;

* if $\kappa_k(\xi) \ne 0$ then $\kappa_{k+1}(\xi) = \kappa_k(\xi)$, otherwise $\kappa_{k+1}(\xi)$ is the sign of $x_{k+1}$;

* we conventionally pose $\kappa_j(\xi) = 0$ for $j < 0$ in $\mathbb{Z}$ and for all $\xi \in \mathbb{Z}$.

At least intuitively we have the following result: if $\kappa_k(\xi) = 1$, then $\xi > 0$; if $\kappa_k(\xi) = -1$, then $\xi < 0$; if $\kappa_k(\xi) = 0$, then the sign of $\xi$ is a priori unknown.

The set $\mathbb{Z}$ has the usual ring structure (for formal series) and the equality $\xi = \zeta$ occurs exactly when the series are identical. This is equivalent to $\forall k \ge 0 \kappa_k(\xi - \zeta) = 0$. This ring is the projective limit of the sequence of surjective morphisms $\pi_{k+1,k}: \mathbb{Q}[\xi]/\langle\varepsilon^{k+1}\rangle \to \mathbb{Q}[\xi]/\langle\varepsilon^k\rangle$ ($k \in \mathbb{N}$), via the natural morphisms $\pi_k: \mathbb{Z} \to \mathbb{Q}[\xi]/\langle\varepsilon^k\rangle$ obtained by truncation of the series to order $k$.

The foundations of the constructive theory of residually discrete henselian local rings, including the construction of the henselisation of a residually discrete local ring, are treated in the article [3].

Everything necessary for the constructive treatment of the ordered ring $\mathbb{Z}$ is now introduced in detail.

1. We define $\xi > 0$ by $\exists k \kappa_k(\xi) = 1$ and $\xi \ge 0$ by $\forall k \kappa_k(\xi) \ge 0$.

Then we have:

* $\xi = 0$ if, and only if, $\xi \ge 0$ and $\xi \le 0$;

* the rules **OTF** and **OTF**$^\times$ are valid in $\mathbb{Z}$;

* Heyting's axiom "$\neg(x > 0) \Rightarrow -x \ge 0$" is satisfied.

2. Absolute value and map sup. We define the map "absolute value" $\xi \mapsto |\xi|$ by posing $c_k(|\xi|) := \kappa_k(\xi)c_k(\xi)$ for all $k$. Finally $\xi \vee \zeta := (\xi + \zeta + |\xi - \zeta|)/2$.

3. We then check that $\mathbb{Z}$ is a strict $f$-ring (theory *Asr*, Chapter D), in other words, by adding the fact that $\mathbb{Z}$ is reduced, all the Horn rules valid in the theory *Codsup* are satisfied in $\mathbb{Z}$ (see the formal Positivstellensatz D.5.6, Item 4).

4. Valuation.

(a) We define $v(\xi) = k \iff \kappa_k(\xi) = \pm 1$, $\kappa_{k-1}(\xi) = 0$.

(b) We define $v(\xi) > k \iff \kappa_k(\xi) = 0$.

(c) Intuitively, we read $v(\xi) > k$ as "the valuation of $\xi$ is $> k$". In fact, $v(\xi)$ is not an element of $\mathbb{N}$ but of a suitable compactification of $\mathbb{N}$ containing $+\infty$.<fnref n="13" />

(d) We have precisely the following description for $\alpha < \beta$:

$$ \alpha < \beta \iff \exists k \begin{cases} (\kappa_k(\alpha) = -1, \kappa_k(\beta) \ge 0) \quad \lor \\ (\kappa_k(\alpha) \le 0, \kappa_k(\beta) = +1) \quad \lor \\ (v(\alpha) = v(\beta) = k, c_k(\alpha) < c_k(\beta)) \end{cases} \quad (C.4) $$

<footnote n="13">¹³This is the metric space obtained by taking on $\mathbb{N}$ the metric $d(k, \ell) = \sup(2^{-k}, 2^{-\ell})$ and completing (this sends $\infty$ to 0).</footnote>
(e) We have $v(\xi^2) = 2v(\xi)$ (equality defined by $v(\xi^2) > 2k - 1 \Leftrightarrow v(\xi^2) > 2k \Leftrightarrow v(\xi) > k$).

(f) We deduce that $\mathbb{Z}$ is a reduced ring (it is thus a constructive model of the *Asrnz* theory).

(g) Finally, $\mathbb{Z}$ is a valuation ring in the following sense: it is a reduced strict $f$-ring in which two strictly positive elements $\alpha$ and $\beta$ are always comparable for divisibility. In other words, the following rule **Val1** is valid.<fnref n="14" />

$$ \textbf{Val1} \quad \alpha > 0, \beta > 0 \quad \vdash \quad \exists \xi \ \alpha\xi = \beta \ \textbf{op} \ \exists\xi \ \beta\xi = \alpha $$

A neighbouring rule that is also valid in $\mathbb{Z}$ is the following.

$$ \textbf{Val2} \quad \beta \ge \alpha \ge 0, \beta > 0 \quad \vdash \quad \exists \xi \ \alpha = \beta\xi $$

Let's prove these rules. From $\beta > 0$ we deduce that there is a $k$ such that $\beta = \varepsilon^k \gamma$ with $v(\gamma) = 0$. We will see in Item 5 that $\gamma \in \mathbb{Z}^\times$. Therefore $\varepsilon^k = \gamma^{-1}\beta$. For **Val1** we also have a $\ell$ such that $\alpha = \varepsilon^\ell \delta$ with $\delta \in \mathbb{Z}^\times$. Hence the disjunction depending on whether $\ell \ge k$ or $k > \ell$. For **Val2**, from $0 \le \alpha \le \beta$ we deduce $\kappa_{k-1}(\alpha) = 0$, so $\alpha = \varepsilon^k \delta = \beta\gamma^{-1}\delta$ for a $\delta \in \mathbb{Z}$.

Note also that the following implication is satisfied.

$$ v(\alpha) = v(\beta) = k \Rightarrow \exists \xi \in \mathbb{Z}^\times \ \alpha = \beta\xi $$

(h) The valuation group is the ordered group defined as the symmetrisation of the monoid of divisibility $\mathbb{Z}^\times/\mathbb{Z}^+$ where $\mathbb{Z}^+ = \{\alpha \in \mathbb{Z} | \exists k > 0 v(\alpha) = k\}$. This valuation group is isomorphic to $(\mathbb{Z}, +, \ge)$, and is generated by (the class of) $\varepsilon$. In the usual terminology, we say that $\mathbb{Z}$ is a discrete valuation ring (DVR), but here the word “discrete” does not have the usual meaning given to it in constructive mathematics.

5. **Convergent series.** If we have an infinite sequence $(\xi_n)_{n \in \mathbb{N}}$ in $\mathbb{Z}$ and if the sequence of $v(\xi_n)$ tends to $+\infty$, then the infinite sum $\sum_{n \in \mathbb{N}} \xi_n$ is well-defined. In particular, if $v(\xi) > 0$ the sum $\zeta = 1 + \sum_{n \in \mathbb{N}} \xi^n$ is well-defined and we have $\zeta(1 - \xi) = 1$. From this we can deduce the following properties.

(a) The ring $\mathbb{Z}$ is a local ring, whose residual field is discrete, isomorphic to $\mathbb{Q}$.

(b) We have $\mathbb{Z}^\times = \{\xi \in \mathbb{Z} | \kappa_0(\xi) = \pm 1\}$ and $\text{Rad}(\mathbb{Z}) = \{\xi \in \mathbb{Z} | \kappa_0(\xi) = 0\}$.

(c) If $c(\beta) = k$, we write $\beta = \varepsilon^k \gamma$ with $\gamma = c_0(1 - \alpha)$ and $v(\alpha) > 0$, therefore: $\varepsilon^k = \beta\gamma^{-1} = \beta c_0^{-1}(1 + \text{sum}_{n \in \mathbb{N}} \alpha^n)$.

(d) The ring $\mathbb{Z}$ is henselian. Precisely, if $P \in \mathbb{Z}[X]$ satisfies the conditions $v(P(0)) > 0$ and $v(P'(0)) = 0$, there exists a (unique) $\xi \in \mathbb{Z}$ such that $P(\xi) = 0$ and $v(\xi) > 0$. To construct the series $\xi$, we use Newton's method.

(e) The ring $\mathbb{Z}$ is the henselisation of the residually discrete local ring $(\mathbb{Q}[\varepsilon])_{1+\varepsilon\mathbb{Q}[\varepsilon]}$.

6. Finally, we show that the rule **FRAC** is valid in $\mathbb{Z}$. The hypothesis is given by two elements $\xi, \zeta \in \mathbb{Z}$ which verify $0 \le \xi \le \zeta$ and we look for a $\rho$ such that $0 \le \rho \le \xi$ and $\rho\zeta = \xi^2$. According to Lemma D.4.7, the uniqueness of $\rho$ (if existence) is guaranteed in strict $f$-rings, as in the theory *Co0* (Lemma C.3.5).
We note that $0 \le \xi \le \zeta$ implies that $v(\xi) \ge v(\zeta)$. We define $c_k(\rho)$ as follows.

* If $\kappa_k(\zeta) = 0$, then $\kappa_k(\xi) = 0$, which forces $\kappa_k(\rho) = 0$, so $c_k(\rho) = 0$.

* If $v(\zeta) = k$, we have $\zeta = z_k \varepsilon^k (1 + \varepsilon\alpha)$ with $z_k > 0$ and $\alpha \in \mathbb{Z}$, and $\xi = \varepsilon^k \beta$ with $\beta \in \mathbb{Z}$. Then we must have the equality $\rho = z_k^{-1} \beta^2 \varepsilon^k (1 + \varepsilon\alpha)^{-1}$. As this equality implies $\kappa_{k-1}(\rho) = 0$, it is compatible with the coefficients of $\rho$ calculated up to exponent $k-1$. This equality makes it possible to define $c_{k+m}(\rho)$ for all $m > 0$.

<footnote n="14">¹⁴We give here a definition for the case of a strict $f$-ring. A more general definition could be given for a residually discrete local ring with a suitable $\cdot \neq 0$ predicate.</footnote>
• Finally if $\kappa_{k-1}(\zeta) = \kappa_k(\zeta) = 1$, we look for the exponent $\ell < k$ such that $\kappa_{\ell-1}(\zeta) = 0$ and $\kappa_{\ell}(\zeta) = 1$, and we are brought back to the previous case via the calculation of the series $\rho$.

So $\rho$ is well-defined.

Let's summarise the results.

**Proposition C.4.1.** The ring $Z$ is an henselian residually discrete local ring and a reduced strict $f$-ring. Moreover it satisfies the rules **OTF**, **FRAC**, **Val1** and **Val2**.

The test on $Z$ for $\forall \alpha(\alpha^2 > 0 \lor \alpha = 0)$ is equivalent to **LPO**.

Nor can we prove constructively that $Z$ is a ring without zerodivisor: the hypothesis $\xi\zeta = 0$ is equivalent to $|\xi| \wedge |\zeta| = 0$, but the implication $|\xi| \wedge |\zeta| = 0 \Rightarrow ((|\xi| = 0) \lor (|\zeta| = 0))$ is equivalent to the principle **LPPO**.

Finally, we cannot prove that every regular element $\ge 0$ is strictly positive: this is equivalent to the Markov principle **MP**. The total ring of fractions of $Z$ is therefore a somewhat mysterious object, a ring which contains $Q$ and which fortunately is of no obvious mathematical interest.

*Note.* The articles [30, 31] propose a constructive theory of valuation rings (without order relation) only in the case of integral rings with a decidable divisibility relation. It would be useful to generalise the results (obtained constructively) to valuation rings in the sense given for $Z$, and to other similar cases (we need a separation relation on the ring)<fnref n="15" /> can be used as a basis. ■

It is easy to deduce the following theorem from Proposition C.4.1.

**Theorem C.4.2.** The ring $Q = Z[1/\varepsilon]$ satisfies all the axioms of the theory *Co* as well as the ordered Heyting axiom. It is a residually discrete local ring with Rad($Q$) = 0 (thus a Heyting field in the terminology of [CACM] or [MRR]). In short, it is a non-archimedean Heyting field, and a non discrete ordered field in the sense of *Co* theory.

*Note.* An element of $Q = Z[1/\varepsilon]$ is written $\varepsilon^{j_0}\alpha$ with $\alpha \in Z$ and $j_0 \in \mathbb{Z}$, it can be encoded in the form $\gamma = (j_0, \alpha)$. The equality $(j_0, \alpha) = (j'_0, \alpha')$ is defined as follows:

• if $j_0 \le j'_0$, $\varepsilon^{j'_0 - j_0} \alpha = \alpha'$;

• si $j'_0 \le j_0$, $\varepsilon^{j_0 - j'_0} \alpha' = \alpha$.

We then define, for $\gamma = (j_0, \alpha)$:

• $\kappa_k(\gamma) = \kappa_{k-j_0}(\alpha)$ (so $\kappa_k(\gamma) = 0$ for $k < j_0$);

• $c_k(\gamma) = c_{k-j_0}(\alpha)$ (so $c_k(\gamma) = 0$ for $k < j_0$);

• $v(\gamma) = v(\alpha) - j_0$ (so $v(\gamma) \ge -j_0$).

<figure><img src="image_7.png" /></figure>

# C.5. Non discrete real closed fields: position of the problem

Our dream is to repeat the feat that Artin, Schreier and Tarski achieved for the description of the algebraic properties of $\mathbb{R}$ through the theory of discrete real closed fields, but in a constructive framework, in intuitionistic logic without **LEM**, taking into account the fact that $\mathbb{R}$ is not discrete, and avoiding the axiom of dependent choice.

*Remark C.5.1.* We can consider that our quest is the following: to fix a signature $\Sigma$ which allows us to describe as precisely as possible the structure of a non discrete real closed field, to describe on this signature a dynamical theory which is essentially equivalent to a theory weaker than *Crcd*, while being the strongest possible among the dynamical theories which admit $\mathbb{R}$ as a constructive model, without using the axiom of dependent choice. This Holy Grail seems out of reach in absolute terms, as there is no clear criterion for knowing whether a dynamical rule is constructively satisfied on $\mathbb{R}$.<fnref n="16" />

<figure><img src="image_8.png" /></figure>

<footnote n="15">¹⁵See also the article [3].</footnote>

<footnote n="16">¹⁶Moreover, the axiom of dependent choice is not allowed in proofs.</footnote>
## The principle of extension by continuity

The “completion” property of $\mathbb{R}$ is expressed naturally in the following form, without interference from the axiom of dependent choice.

**Theorem C.5.2.** If a map $f: \mathbb{Q}^n \to \mathbb{R}$ is uniformly continuous on all bounded subsets it extends uniquely into a map $\tilde{f}: \mathbb{R}^n \to \mathbb{R}$ uniformly continuous on all bounded subsets.

This theorem is a theorem of analysis and cannot be expressed directly in the context of a dynamical theory which aims at the algebraic properties of $\mathbb{R}$, because the property “to be uniformly continuous” is not geometric.

Nevertheless, it is essentially this theorem that guides us in our quest expressed in Remark C.5.1. We will replace the property “be uniformly continuous” by a formulation where uniform continuity is controlled a priori and no longer hides $\forall \exists$.

Moreover, the only maps that we can envisage inside in a purely algebraic framework are semialgebraic maps.

We must therefore rely on relevant properties of continuous semialgebraic maps, which we develop in the following paragraph.

## Continuous semialgebraic maps

First of all we recall that the uniform continuity over any bounded subset of a continuous semialgebraic map $\mathbf{R}^n \to \mathbf{R}$, where $\mathbf{R}$ is a discrete real closed field, is controlled à la Łojasiewicz precisely as follows.

**Lemma C.5.3.** Let $\mathbf{R}$ be a discrete real closed field and $K \subseteq \mathbb{R}^n$ be a bounded semialgebraic closed subset.

1. Let $g: K \to \mathbf{R}$ be a continuous semialgebraic map. Then $g$ has a uniform continuity modulus which is expressed à la Łojasiewicz as follows (with $c \in \mathbb{R}$ and $\ell$ integer $\ge 1$)

$$ \forall \xi, \xi' \in K \quad |g(\xi) - g(\xi')|^{\ell} \le |c| \|\xi - \xi'\|. \qquad (C.5) $$

2. Let $f: \mathbb{R}^n \to \mathbf{R}$ be a continuous semialgebraic map. Then $f$ has a uniform continuity modulus over any bounded subset which is expressed à la Łojasiewicz as follows (with $c \in \mathbb{R}$ and integers $k, \ell \ge 1$)

$$ \forall \xi, \xi' \in \mathbb{R}^n \quad |f(\xi) - f(\xi')|^{\ell} \le |c| (1 + \|\xi\| + \|\xi'\|)^k \|\xi - \xi'\|. \qquad (C.6) $$

*Proof.* This is a consequence of Theorem 2.6.6 of [Bochnak, Coste & Roy] which states that on a locally closed semialgebraic set, if there are two continuous semialgebraic maps $F$ and $G$ such that $G$ vanishes at the zeros of $F$, there exists an exponent $N$ and a continuous semialgebraic map $h$ such that $G^N = hF$. In the compact case, $h$ is bounded by a constant; in the general case, $h$ is bounded by a polynomial map. We apply this with $F(x, x') = \|x - x'\|$ and $G(x, x') = |f(x) - f(x')|$. $\square$

### Continuous parametrisation of continuous semialgebraic maps

We now present a parametrisation result saying that, from the point of view of continuous semialgebraic maps, everything comes continuously from what happens on the subfield $\mathbb{R}_{\text{alg}}$ of algebraic real numbers. In other words, any continuous semialgebraic map $\mathbf{R}^n \to \mathbf{R}$ is a point with coordinates in $\mathbf{R}$ of an equicontinuous family defined on $\mathbb{R}_{\text{alg}}$.

The idea is in fact a simple generalisation of the following remark. The family of univariate polynomials $f(x) = ax^2+bx+c$ (family parametrised by $(a, b, c) \in \mathbb{R}^3$) is never just the polynomial in four variables $g(a, b, c, x) = ax^2+bx+c$ defined on $\mathbb{Q}$, where we take $(a, b, c)$ as parameters and $x$ as variable, all in $\mathbb{R}$: so we don't have to worry too much about the non discrete character of $\mathbb{R}$, since everything is defined on $\mathbb{Q}$. Each individual map $f(x)$ (depending on parameters taken from $\mathbb{R}^3$) is a real point of a family defined on $\mathbb{R}_{\text{alg}}$. This real point comes from the extension by continuity at $\mathbb{R}^4$ of a continuous map $\mathbb{R}_{\text{alg}}^4 \to \mathbb{R}_{\text{alg}}$.
**Theorem C.5.4.** Let $\mathbf{R}$ be a discrete real closed field and $f: \mathbf{R}^n \to \mathbf{R}$ be a continuous semialgebraic map. There exists an integer $r \ge 0$, a continuous semialgebraic map $g: \mathbf{R}^{r+n} \to \mathbf{R}$ defined on $\mathbb{R}_{\text{alg}}$, and an element $y \in \mathbf{R}^r$ such that

$$ \forall x_1, \dots, x_n \in \mathbf{R} \ f(x_1, \dots, x_n) = g(y_1, \dots, y_r, x_1, \dots, x_n). $$

This result seems to be part of folklore. We give here a proof inspired by the advices of Michel Coste and Marcus Tressl. However, it is not entirely constructive. This would require, for example, a constructive re-reading of Chapter 7 of [Bochnak, Coste & Roy]. See Question C.7.1.

*Proof.* The map $f$ has a closed graph $F$ which is a semialgebraic union of basic semialgebraic closed sets $F_i = \{(\underline{x}, y) \in \mathbf{R}^{n+1} | p_i(\underline{x}, y) \ge 0\}$. The coefficients of $p_i$ are in $\mathbf{R}$ but can be seen as specialisations of parameters $c_k$ ($k \in [1..m]$) so that we have polynomials $P_i(c, \underline{x}, y)$ with parameters $c_k$. The inequalities $P_i(c, \underline{x}, y) \ge 0$ define for $i$ a fixed semialgebraic closed set $G_i \subseteq \mathbf{R}^{m+n+1}$. The union of $G_i$'s, denoted $G$, is a semialgebraic which is not sufficiently relevant. We add a parameter $c_0$ and we will now restrict the domain of variation of $c_k$ to a “suitable” semialgebraic set $S$. Suitable means that the following formula is satisfied

$$ \forall \underline{\xi}, \underline{\xi}' \in \mathbf{R}^n \forall \zeta, \zeta' \in \mathbf{R} \ ((\underline{c}, \underline{\xi}, \zeta) \in G, (\underline{c}, \underline{\xi}', \zeta') \in G) \Rightarrow |\zeta - \zeta'|^{\ell} \le |c_0| (1 + \|\underline{\xi}\| + \|\underline{\xi}'\|)^k \|\underline{\xi} - \underline{\xi}'\|. $$

where $k$ and $\ell$ are integers for which the map $f$ satisfies these inequalities (for a certain specialisation of $c_0$). Note that $S \subseteq \mathbf{R}^{m+1}$. It is clear that the semialgebraic set $S$ is defined on $\mathbb{R}_{\text{alg}}$. Let $H$ be the semialgebraic subset of $\mathbf{R}^{m+n+2}$ formed by the points of $G$ whose $m+1$ first coordinates (the parameters) form a point of $S$. The semialgebraic set $H$ is the graph of a map $h: S \times \mathbf{R}^n \to \mathbf{R}$, which is seen as a family of maps $\mathbf{R}^n \to \mathbf{R}$ parametrised by $S$. For any point $s \in S$ the corresponding graph $H_s$ is that of a continuous semialgebraic map $f_s: \mathbf{R}^n \to \mathbf{R}$ whose uniform continuity modulus is controlled by $|c_0|$, $k$ and $\ell$. The initial map $f$ corresponds to a point $s_0 \in S$ with coordinates in $\mathbf{R}$. By means of a cylindrical algebraic decomposition of $\mathbf{R}^{m+1}$ adapted to $S$, we insert $s_0$ in a cell $\Gamma$ defined on $\mathbb{R}_{\text{alg}}$ semialgebraically homeomorphic to $\mathbf{R}^q$ for a $q \ge 0$ ($q = 0$ implies that $s_0$ has coordinates in $\mathbb{R}_{\text{alg}}$). Moreover the homeomorphism is defined on $\mathbb{R}_{\text{alg}}$. We then obtain a semialgebraic map $\varphi: \mathbf{R}^{q+n} \to \mathbf{R}$ defined on $\mathbb{R}_{\text{alg}}$ which has the following properties:

* There is an element $\gamma = (\gamma_1, \dots, \gamma_q) \in \mathbf{R}^q$ such that $\varphi(\gamma, \underline{\xi}) = f(\underline{\xi})$ for all $\underline{\xi} \in \mathbf{R}^n$.

* For any element $\alpha = (\alpha_1, \dots, \alpha_q) \in \mathbf{R}^q$, the map $\underline{\xi} \mapsto \varphi(\alpha, \underline{\xi})$ is continuous semialgebraic. The map $\varphi$ is locally bounded.

Under these hypotheses, Remark 7.4.9 of [Bochnak, Coste & Roy], assures us that there exists a semialgebraic partition $A_1 \cup \dots \cup A_k$ of the space of parameters $\mathbf{R}^q$, defined on $\mathbb{R}_{\text{alg}}$, such that the map $\varphi$ restricted to each of the $A_i \times \mathbf{R}^n$ is continuous. For example the point $\gamma = (\gamma_1, \dots, \gamma_q)$ belongs to $A_1$. By means of a cylindrical algebraic decomposition of $\mathbf{R}^q$ adapted to $A_1$, we insert $\gamma$ in a cell $\Delta$ defined on $\mathbb{R}_{\text{alg}}$ semialgebraically homeomorphic to $\mathbf{R}^r$ for an $r \ge 0$. Moreover the homeomorphism is defined on $\mathbb{R}_{\text{alg}}$. This provides the continuous semialgebraic map $g: \mathbf{R}^{r+n} \to \mathbf{R}$ defined on $\mathbb{R}_{\text{alg}}$ requested in the statement. $\square$

### A reasonable definition

We therefore propose the following definition in constructive mathematics, made legitimate by Theorem C.5.4.

**Definition and notation C.5.5.** Let $\mathbf{R}$ be an ordered subfield$^{17}$ of $\mathbb{R}$ containing the field of algebraic reals $\mathbb{R}_{\text{alg}}$ and a map $f: \mathbf{R}^n \to \mathbf{R}$.

1. (elementary case) The map $f$ is semialgebraic continuous if there exists a continuous semialgebraic map $g: \mathbb{R}_{\text{alg}}^n \to \mathbb{R}_{\text{alg}}$ of which $f$ is the extension by continuity. Precisely we must have the following two properties: $f$ is an extension of $g$, and $f$ has the same uniform modulus of continuity as $g$, given in Item 2 of Lemma C.5.3.

<footnote>$^{17}$Precisely $\mathbf{R}$ is a subobject of $\mathbb{R}$ for the non discrete ordered field defined by the theory $\mathcal{O}_0$. Moreover, for the simple existential rule IV, we require that an element of $\mathbf{R}$ invertible in $\mathbb{R}$ be invertible in $\mathbf{R}$.</footnote>
2. (general case) The map $f$ is semialgebraic continuous if there exist an integer $r \ge 0$, elements $y_1, \dots, y_r \in \mathbb{R}$ and a map $h: \mathbb{R}^{r+n} \to \mathbb{R}$ which belongs to the previous elementary case such that

$$ \forall x_1, \dots, x_n \in \mathbb{R} \ f(x_1, \dots, x_n) = h(y_1, \dots, y_r, x_1, \dots, x_n). $$

We denote $\mathfrak{Fsac}_n(\mathbb{R})$ the ring of these maps (it is a reduced strict $f$-ring for the natural order relation).

Some important properties of these function spaces will be established in Section C.6.

## Rational dynamical theories for real number algebra

Recall that the field $\mathbb{R}_{alg}$ of the algebraic reals is a discrete real closed field in the constructive sense.

Following on from Remark C.5.1 and Definition C.5.5, here are the properties we have in mind for a dynamical theory $\mathfrak{Crc}$ of (non discrete) real closed fields, described here in a rather informal way.

### Expected properties C.5.6.

1. The theory $\mathfrak{Crc}$ is an extension of $\mathfrak{Co}$.

2. The fields $\mathbb{R}$, $\mathbb{R}_{PR}$, $\mathbb{R}_{Ptime}$ and $\mathbb{R}_{Rec}$ (cf. Example C.3.4) are constructive models of $\mathfrak{Crc}$ (without using the axiom of dependent choice).

3. The theory $\mathfrak{Crc}$ becomes essentially equivalent to $\mathfrak{Crcd}$ when we add to it the axiom $\mathbf{ED}_>$.

4. The continuous semialgebraic maps $\mathbb{R}_{alg}^n \to \mathbb{R}_{alg}$ are nicely defined in the language of $\mathfrak{Crc}$ and the Horn rules they satisfy are valid in the theory.

5. Continuity extension principles (as broad as possible) are satisfied in a suitable form in the dynamical theory.

6. Gluing principles (the broadest possible) for maps defined on a finite covering by semialgebraic openings, or by semialgebraic closures, are satisfied in a suitable form in the dynamical theory.

The following points are open to discussion. Item 7 will be dropped if we want to describe more “structure” on $\mathbb{R}$, for example for an o-minimal structure. Item 8 will be abandoned for example if we wish to introduce all the reals as constants of the theory: in a general dynamical theory $\mathcal{T} = (\mathcal{L}, \mathcal{A})$, $\mathcal{L}$ and $\mathcal{A}$ are only supposed to be naive sets (à la Bishop).

7. All function symbols in $\mathfrak{Crc}$ define on $\mathbb{R}$ continuous semialgebraic maps of their variables (Definition C.5.5).

8. The language of $\mathfrak{Crc}$ is enumerated in a natural way and in this framework the axioms are decidable in a primitive recursive way.

A slightly crude way of getting a relatively satisfactory answer is to take seriously Item 4 above. The result is as follows.

**Definition C.5.7.** The dynamical theory $\mathfrak{Crc1}$ is obtained from the dynamical theory $\mathfrak{Co}$ by adding a function symbol and suitable axioms for each continuous semialgebraic map $f: \mathbb{R}_{alg}^n \to \mathbb{R}_{alg}$.

*Explanation.* More precisely, we proceed as follows. We know from the finiteness theorem ([Bochnak, Coste & Roy, Theorem 2.7.1]) that the graph $G_f = \{(x, y) | x \in \mathbb{R}^n, y = f(x)\}$ of $f$ (which is assumed to be semialgebraically continuous) is a semialgebraic closed set of $\mathbb{R}_{alg}^{n+1}$ which can be
described as the zero set of a semipolynomial map $F: \mathbb{R}_{\text{alg}}^{n+1} \to \mathbb{R}_{\text{alg}}$, i. e. a map written in the form

$$ \sup_i (\inf_{ij} p_{ij}) \quad \text{where } p_{ij} \in \mathbb{R}_{\text{alg}}[x_1, \dots, x_n, y] $$

We can decide whether such a semialgebraic closed set $G_f$ described in this way is that of a continuous semialgebraic map, and if so calculate a uniform continuity modulus à la Łojasiewicz. Whenever such a (description of) semipolynomial map defines a continuous semialgebraic map, we introduce a function symbol $fsa_F$ with the corresponding axiom

$$ \mathbf{Df}_F \vdash F(\underline{x}, fsa_F(\underline{x})) = 0. $$

Furthermore, for an arbitrary term $t(\underline{x})$ in the language thus defined, if this term defines a map everywhere zero on $\mathbb{R}_{\text{alg}}^n$ ($n \ge 0$), we introduce the corresponding axiom $\vdash t(\underline{x}) = 0$.

For example, for the map $fsa_F$ we will have an axiom of continuity which repeats that which is satisfied for the algebraic reals.

$$ \mathrm{Cont}_F \vdash |fsa_F(\underline{x}) - fsa_F(\underline{x}')|^\ell \le |c| (1 + \|\underline{x}\| + \|\underline{x}'\|)^k \|\underline{x} - \underline{x}'\|. $$

Indeed, an inequality between two terms, $t_1 \le t_2$, is equivalent to making the term $(t_2 - t_1)^{-}$ equal to 0. ■

Naturally, such a dynamical theory is frustrating at first sight, because it is not very natural and it is undoubtedly difficult to practise from an effective point of view.

However, we shall see that a more natural way, with the addition of few function symbols, which we propose later, leads to the theory *Corv* essentially identical to *Crc1*.

All this is closely related to the theory of real closed rings and its rewriting in concrete form in [69].

## C.6. General properties of continuous semialgebraic maps

In this section we give some remarkable properties of the rings $\mathbf{Fsac}_n(\mathbb{R})$ (continuous semialgebraic maps $\mathbb{R}^n \to \mathbb{R}$ according to Definition C.5.5) over the field $\mathbb{R} = \mathbb{R}$. More generally we can consider an ordered subfield $\mathbb{R}$ of $\mathbb{R}$ containing $\mathbb{R}_{\text{alg}}$ and in which any continuous semialgebraic map defined on $\mathbb{R}_{\text{alg}}$ takes its values in $\mathbb{R}$ at the points whose coordinates are in $\mathbb{R}$, for example $\mathbb{R}_{\text{PR}}$, $\mathbb{R}_{\text{Ptime}}$ or $\mathbb{R}_{\text{Rec}}$.

These properties known for discrete real closed fields are extended to $\mathbb{R}$ because we take the precaution of only taking properties whose formulation does not imply the discrete nature of the order.

### Stability by composition

For example we compose $f, g \in \mathbf{Fsac}_3(\mathbb{R})$ with $h \in \mathbf{Fsac}_2(\mathbb{R})$. Suppose that

* $f$ is given in the form $f(x, y, z) = \tilde{f}(a, b, x, y, z)$, for $a, b \in \mathbb{R}$ and $\tilde{f}: \mathbb{R}^5 \to \mathbb{R}$ extends by continuity $\tilde{f}: \mathbb{R}_{\text{alg}}^5 \to \mathbb{R}_{\text{alg}}$,

* $g$ is given by the form $g(x, y, z) = \tilde{g}(c, x, y, z)$, for $c \in \mathbb{R}$ and $\tilde{g}: \mathbb{R}^4 \to \mathbb{R}$ extends by continuity $\tilde{g}: \mathbb{R}_{\text{alg}}^4 \to \mathbb{R}_{\text{alg}}$,

* $h$ is given by the form $h(u, v) = \tilde{h}(d, u, v)$, for $d \in \mathbb{R}$ and $\tilde{h}: \mathbb{R}^3 \to \mathbb{R}$ is a continuous extension of $\tilde{h}: \mathbb{R}_{\text{alg}}^3 \to \mathbb{R}_{\text{alg}}$,

* then $h \circ (f, g): \mathbb{R}^3 \to \mathbb{R}$ is of the form $k(x, y, z) = \tilde{k}(a, b, c, d, x, y, z)$ for $(a, b, c, d) \in \mathbb{R}^4$ and $\tilde{k}: \mathbb{R}^7 \to \mathbb{R}$ extends by continuity the map $\bar{k}: \mathbb{R}_{\text{alg}}^7 \to \mathbb{R}_{\text{alg}}$ defined by

$$ \bar{k}(a, b, c, d, x, y, z) = h(d, f(a, b, x, y, z), g(c, x, y, z)). $$
Stability by upper bound

For example we have $f \in \text{Fsac}_4(\mathbf{R})$ and we want to show that there is a $g \in \text{Fsac}_2(\mathbf{R})$ such that
$g(x, y) = \sup_{z,t \in [0,1]} f(x, y, z, t)$. If $f$ is given in the form $f(x, y, z, t) = \tilde{f}(a, b, x, y, z, t)$, for $a, b \in \mathbf{R}$, where $\tilde{f}: \mathbf{R}^6 \to \mathbf{R}$ extends by continuity $\bar{f}: \mathbf{R}_{\text{alg}}^6 \to \mathbf{R}_{\text{alg}}$, consider the continuous semialgebraic map $\bar{g}: \mathbf{R}_{\text{alg}}^4 \to \mathbf{R}_{\text{alg}}$ defined by $\bar{g}(a, b, x, y) = \sup_{z,t \in [0,1]} \bar{f}(a, b, x, y, z, t)$.<fnref n="18" /> It extends by continuity into a map $\tilde{g}: \mathbf{R}^4 \to \mathbf{R}$ and we define $g(x, y) = \bar{g}(a, b, x, y)$. The fact that $g$ is indeed the desired lub is due to the fact that the lub on a compact is a continuous function of the parameters and that $\mathbf{R}_{\text{alg}}$ is dense in $\mathbf{R}$.

Finiteness properties

In classical mathematics, any continuous semialgebraic map $f: \mathbb{R} \to \mathbb{R}$ has a finite table of signs and variations. But this table does not depend continuously on the parameters, for example when $f(x) = g(a_1, \dots, a_n, x)$ for parameters $a_1, \dots, a_n \in \mathbb{R}^n$, where $g$ is the continuity extension of a continuous semialgebraic map $\bar{g}: \mathbb{R}_{\text{alg}}^{n+1} \to \mathbb{R}_{\text{alg}}$.

However, when $f$ is a monic polynomial, a constructive approach to the question is to use
virtual root maps. For example we can see Items 3h, 3i, 3j and 3k of Theorem E.2.6 as well as
Proposition E.6.3.

Analogous results should be established in constructive mathematics for arbitrary continuous
semialgebraic maps, at least for Proposition E.6.3, but restricted to maps on the interval $[-1, 1]$
(on $\mathbb{R}$ this would not be possible). It may be necessary to use an infinite OP.

C.7. Some questions

**Question C.7.1.** Give a complete constructive proof of Theorem C.5.4.

**Question C.7.2.** Show that the Horn rule **FRAC** is not valid in **Co0**. Similarly, show that the Horn rule (C.3) which is equivalent to the existence of the map (C.2) page 53 is not valid in **Co0**.

**Question C.7.3.** Determine which algebraic properties of $\mathbb{R}$ allow us to prove the constructively satisfying forms of Positivstellensätze proved for $\mathbb{R}$ in [26]. See in particular Question E.7.12.

Continuous variations

Continuous semialgebraic maps $\mathbb{R}^n \to \mathbb{R}$ could have been defined as follows. This was the definition
adopted in [40, Definition 3.3].

**Definition C.7.4.** Let $\mathbf{R}$ be a commutative ring. A map $f: \mathbb{R}^n \to \mathbf{R}$ is said to be *algebraic on* $\mathbf{R}[x_1, \dots, x_n] = \mathbf{R}[\underline{x}]$ if there is a polynomial $g(\underline{x}, y) = \sum_{k=0}^m g_k(\underline{x})y^k \in \mathbf{R}[\underline{x}, y]$, with at least one of the coefficients of a $g_k(\underline{x})$ invertible, such that $g(\underline{\xi}, f(\underline{\xi})) = 0$ for all $(\underline{\xi}) \in \mathbb{R}^n$.

**Definition C.7.5 (alternative definition to C.5.5).** Let $\mathbf{R}$ be a subfield of $\mathbb{R}$. A map $f: \mathbb{R}^n \to \mathbf{R}$ is said to be *semialgebraic continuous* if, on the one hand, it is algebraic on $\mathbf{R}[\underline{x}]$ and if, on the other hand, it has a uniform continuity modulus on everything bounded à la Łojasiewicz, given by an inequality C.6 as in Lemma C.5.3.

This definition is legitimate for subfields of $\mathbb{R}$ because

• it is valid in classical mathematics,

- it has a clear constructive meaning,

* semialgebraic maps which are continuous in the sense of Definition C.5.5 are also continuous
  in the sense of Definition C.7.5.

<footnote n="18">¹⁸Here, *a*, *b* are variables.</footnote>