Théories géométriques et calcul formel. Que faire avec les réels (à la Cauchy)?

Les théories géométriques du premier ordre (théories cohérentes)
peuvent être interprétées
comme de pures machineries calculatoires (sans logique) qui réconcilient
logique classique et logique
constructive, et peuvent être utilisées de manière immédiate en calcul
formel. Cependant, pour un bon nombre de types de structures algébriques
usuelles, les théories géométriques infinitaires
sont nécessaires pour les appréhender de manière correcte. En calcul
formel, cela correspond au formalisme des machines à oracle.
L’exemple des nombres réels, tout d’abord vus comme fournissant une
structure algébrique de corps ordonné,
mais ensuite comme structure o-minimale en ajoutant certaines classes de
fonctions dans la structure, est fondamental pour les mathématiques
couramment utilisées.
La divergence avec les mathématiques classiques doit être ici soulignée:
le tiers exclu ne s’applique
pas pour l’égalité des nombres réels (ceux de l'analyse). Nous parlerons
ici de tentatives de description de ces structures.
Un autre titre de l’exposé aurait pu être: qu’est-ce qu’un corps réel
clos sans test de signe?