Let us first distinguish between two kinds of operations that "take formulas to terms":

We might ask for *reflection* of syntax into the theory. A typical example is a quoting operator which takes a formula and returns its Gödel number.

We might ask for the ability to mix formulas and terms. A typical example is the subset-forming operation $\{x \in A \mid \phi(x)\}$.

The two are quite different because the first one is quite intensional (logically equivalent formulas produce different numbers) while the second one is extensional (logically equivalent formula produce the same subset).

Reflection of syntax into theory gets interesting once we ask for it to play nicely with respect to substitution and binding. I am not too familiar with this area, you could look at how syntax is reflected into NuPRL. You might also be interested in going in the other direction, namely how to convert internal representation of syntax to formulas. This goes under the name "meta-programming", where once again I am not too familiar with the literature. I am for instance aware of Aleks Nanevski's work on meta-programming with names and necessity.

For the second part (terms that contains formulas), that's very familiar territory in higher-order logic and type theory. If terms can appear in formulas and formulas can appear in terms, then the two-level stratification of terms and formulas familiar from first-order logic becomes meaningless. It is then better to put formulas and terms on equal footing and use sorts or types to keep track of what is what. One example of such a setup is Church's type theory where there is a special type of truth values. A more modern example is dependent type theory, especially variants of it that have a dedicated sort or universe of propositions, for instance the Calculus of constructions.

If you are interested to see how such formal systems work in practice, you can look at modern proof assistants. They all eschew the traditional first-order logic (because it is inappropriate for mathematical practice) and use one of the above mentioned formalisms instead: Isabelle/HOL uses Church-style higher-order logic, Coq uses the Inductive Calculus of Constructions, and Agda uses Martin-Löf type theory.

**Supplemental:** If you're just interested in reflecting the syntax of first-order logic into arithmetic, i.e., Gödel numberings, then you'd proceed as follows, combining standard bits about syntax and meta-programming from computer science.

First, define the abstract syntax of first-order logic, including an operator $G$ which takes formulas to terms. Find some way of encoding such trees as numbers, if you feel nostalgic about 20th century logic. Consider using de Bruijn indices to avoid nasty details about bound variables.

The syntax of $G$ is *not* $G(\phi)$, as you suggested, but rather
$$G(x_1, \ldots, x_n \mid \phi)$$
where $x_1, \ldots, x_n$ is a (possibly empty) list of variables. The variables $x_1, \ldots, x_n$ should be encoded by $G$, while any remaining free variables appearing in $\phi$ should be considered as *interpolating* variables. It might be easiest to explain this by means of an example:

$G(x, y \mid x + y = 7)$ is a closed term (it has no free variables), so it denotes a number which encodes the expression $x + y = 7$.

$G(y \mid x + y = 7)$ is a term whose only free variable is $x$.

$G( \mid x + y = 8)$ is a term whose free variables are $x$ and $y$.

We want to arrange interpolation and substitution so that they interact sensibly, i.e., we expect that
$$G(x_1, \ldots, x_n \mid \phi)[t_1/y_1, \ldots, t_m/y_m] =
G(x_1, \ldots, x_n \mid \phi[t_1/y_1, \ldots, t_m/y_m]).
$$
In words: if we first encode $\phi$ and then substitute $e_i$'s for $y_i$'s in the resulting term, that's equal to first substituting $e_i$'s for $y_i$'s in $\phi$ and then encoding. The usual provisos about free variables not getting captured apply: the free variables appearing in the terms $t_i$ must be disjoint from $x_1, \ldots, x_n$, and probably the $x_i$'s must be disjoint from $y_j$'s. (I refuse to think about this because there are non-pedestrian ways of dealing with bound variables.)

We can now sensibly answer your questions about encoding of $x = x$. The encoding of $G(x \mid x = x)$ is a particular number, say $17$. The term $G( \mid x = x)$ has one free variable and suppose it is equal to the term $3 \cdot x$. Consequently, the term $G(\mid 14= 14)$ is equal to 42. Now we see that

- $\forall x . G(x \mid x = x) = 17$ is true
- $\forall x . G(\mid x = x) = 3 \cdot x$ is true
- $\forall x . G(\mid x = x) = 17$ is false
- $G(\mid x = x) = 17$ is equivalent to $3 \cdot x = 17$