Symboles de fonction mal définis

La façon d'encoder les maths dans des fondations comme ZF n'est presque jamais documentée nulle part, même si presque tout le monde dit "qu'il est possible d'écrire quasiment toutes les maths dans la théorie des ensembles". Quelques remarques.

Soit $\Phi(x_1,...,x_n,y)$ un énoncé à $n+1$ variables libres en logique du premier ordre sur une signature donnée. Si on travaille dans une théorie ambiante $T$ qui démontre l'énoncé $\forall x_1,...\forall x_n, \exists ! y, \Phi(x_1,...,x_n,y)$ alors on obtient une extension conservative de $T$ en ajoutant à la signature un symbole de fonction $f$ à $n$ arguments et en ajoutant l'axiome $\forall x_1 \forall x_2...\forall x_n, \Phi(x_1,...,x_n, f(x_1,...,x_n))$. De plus ce symbole est éliminable (chaque formule est équivalente à une formule où $f$ n'apparaît pas; c'est important quand on travaille avec des théories ayant des schémas d'axiomes comme ZF/ZFC: ça veut dire qu'on a le droit d'ajouter "des symboles de fonctions à la volée" comme on fait en maths tous les jours).

La preuve de ce théorème est syntaxique (trouvable dans le livre de @Martial par exemple) et plus simple que sa version plus générale avec des fonctions de Skolem (dont je n'ai jamais vu de preuve convaincante hors théorie des modèles ; de plus pour ce cas général il n'y a plus d'éliminabilité du symbole introduit).

Le fait que la relation fonctionnelle est définie partout sert dans la preuve (je n'ai pas de contre-exemple sous la main sinon mais ça doit se trouver).

Par exemple, étant donné un énoncé à 3 variables libres $D(x,y,z)$ qui dit intuitivement que $x=y*z$ et $y$ est non nul, on peut introduire l'axiome $\forall x\forall y \left [\left ((x\in \R) \wedge (y \in \R) \wedge y \neq 0 \wedge  D(x,y,(f(x,y))) \right) \vee \left ( (x\notin \R \vee y \notin \R \vee y=0)\right ) \wedge  f(x,y) = \emptyset \right ] $.

$f$ va être la "division" entre réels, $\emptyset$ est traité en terme d'erreur quand l'opération est mal définie. On note encore $x/y$ au lieu de $f(x,y)$ et bien sûr $0/0$ (qui est $\emptyset$) est un terme légitime du langage (!!!) il n'y a jamais de problème puisque dans un calcul vous faites toujours la vérification $y\neq 0$ afin de garantir que vous êtes dans le bon cas (à gauche dans la formule) d'application de l'axiome ci-dessus.

Une autre solution différente (mais qui va toujours définir des symboles de fonction partout) est d'encoder les formules dans ZF comme le font Takeuti et Zaring dans leur livre "introduction to axiomatic theory" https://www.amazon.com/Introduction-Axiomatic-Theory-Graduate-Mathematics/dp/0387906835 (assez aride, on trouve une autre version du même propos dans "Basic set theory" d'Azriel Levy, ainsi qu'un encodage, différent cette fois, dans "Axiomatic set theory" de Patrick Suppes).