[Elimination of the ≐ symbol from formulas] Motivation: The following procedure constructs for each FO -formula A a fulf

[answerhappygod]

[Elimination of the ≐ symbol from formulas]
Motivation: The following procedure constructs for eachFO -formula A a fulfillment equivalent formulaA^(E) without a formal equal sign ≐ , so that thefollowing holds: if A^(E) has a has a countable model M0, thenA should also have a countable model M.
Let A be in adjusted Skolem normal form.
We extend the finite(!) minimal signature S_A for A bya new 2-digit relation symbol E/2 to a signatureS´_A. We substitute this instead of ≐ in A:
A1 := A {≐ / E}
Every model M = <D, I> for A can be extended toa model for A_1: one only needs to take take the equality on D asinterpretation E^M of the new predicate symbol. Conversely,however, we do not know whether every model for A_1 is also a modelfor A or can be can be converted to one.
Idea: The goal is now to convert the formula A_1 to a formulaA^(E) after ≡ factorize (i.e., form the equivalenceclasses in the data domain) and thus obtain a newS'_A -Structure M'/E^M', in which E is interpreted asequality, and whose interpretations of the S_A -symbols are derivedfrom those of M' by applying the latter to representatives ofthe equivalence classes to be equivalence classes to be processed.Due to the congruence properties of e^M this procedure is thisprocedure is independent of the choice of these representatives andthus well-defined.
If A^(E) has a model at all, then A^(E) also has a Herbrandmodel H with respect to S'_A; this is countable. Theabove construction then yields a countable model of A^(E), inwhich E is interpreted as an equality, and thus a countable modelof the originalFormula A .
Indicate which conditions on E are to be added to A_1!