Kann ein Satz in einer modelltheoretisch konservativen Erweiterung in die Sprache seines Reduktionswortes übersetzt werden?

Lassen$L1$Und$L2$zweisprachig mit$L1 \subset L2$Und$T1$Und$T2$bzw. eine Theorie in$L1$Und$L2$. Das sagen wir$T2$ist eine modelltheoretische konservative Erweiterung von$T2$iff jedes Modell$M1$von$T1$zu einem Modell erweiterbar$M2$von$T2$(siehe Konservative Erweiterung ).
Wenn wir haben$T1$was so etwas wie beweist$\forall x \exists !y F[x,y]$Wo$F[x,y]$ist eine Formel mit freien Variablen x und y, die wir definieren können$L2=L1 \cup \{f\}$Wo$f$ist eine Symbolkonstante mit der Stelligkeit 2, und$T2=T1 \cup \{\forall xF(x,f(x))\}$(siehe Konservativitätssatz ), der eine modelltheoretische Erweiterung von T1 ist.
Daher ist meine Frage die folgende. Gibt es eine Möglichkeit, einen Satz zu übersetzen?$L2$zu einem Satz in$L1$? Zum Beispiel, wenn$F$ist ein$L2$-Satz, gibt es a$L1$-Satz$F'$wie zum Beispiel$T2 \vdash F \Leftrightarrow F'$? Nehmen wir zum Beispiel die Theorie der Gruppen, ausgedrückt in$L1$die die Symbole für die Einheit (Konstante), Gleichheit (2er-Relation), Produkt (2er-Funktion) enthält, sieht man leicht, dass es eine natürliche modelltheoretische konservative Erweiterung gibt$L2$gleich$L1$plus ein Symbol für die Umkehrung (1-stellige Funktion). Es wäre bequem zu bedienen$L2$, und zu sagen, nicht nur für$L1$-Sätze, das$T2 \vdash F$, somit$T1 \vdash$(Platzieren Sie hier eine Formel, die sich nicht so sehr von F unterscheidet). Weil wir eine stärkere Sprache und Theorie verwenden, aber nicht so sehr.
Mein Hauptanliegen ist, dass wir in der alltäglichen Mathematik Konstanten (0, leere Menge usw.) und Funktionssymbole (für das Paar, für Sinus usw.) verwenden, die auf diese Weise eingeführt werden, und wir sagen, dass alles übersetzbar ist im ZFC. Nun wie ?