This is problem 3.5 of Johnstone's Notes on logic and set theory:
Let $\mathscr L$ be a first-order language having sets $\Omega$ and $\Pi$ of primitive operations and predicates. Let $\mathscr L^*$ be the language obtained from $\mathscr L$ on replacing each primitive operation $\omega$ by a primitive predicate $\omega^* $. If $\mathscr T$ is a theory in $\mathscr L$, show how to construct a theory $\mathscr T^*$ in $\mathscr L^*$ in the sense that it has 'the same models'.
(Hint: first write down axioms to express "$[\omega]^*$ is the graph of a function".)
Definitions:
Terms: terms are defined inductively:
Any variable is a term.
If $\omega\in \Omega$ is an $n$-ary operation and $t_1,...,t_n$ are terms, then $\omega t_1...t_n$ is a term.
$n$-ary predicate: Something whose intended interpretation in a structure $A$ is a subset of $A^n$; thus if $a_1,...,a_n \in A$, $\phi(a_1,...,a_n)$ will be the assertion that the $n$-uple $(a_1,...,a_n)$ belongs to the subset which interprets $\phi$.
Atomic formulae: there are two kinds:
- If $s$ and $t$ are terms, then $(s=t)$ is an atomic formula.
- If $\phi\in \Pi$ and $t_1 ,...,t_n$ are terms, then $\phi(t_1,...,t_n)$ is an atomic formula.
Formulae are defined inductively:
- Atomic formulae are formulae.
$\bot$ is a formula, and if $p$ and $q$ are formulae so is $(p\Rightarrow q)$.
If $p$ is a formula and $x$ is a variable which occurs free in $P$ then $(\forall x)p$ is a formula.
Sentence: a formula without free variables.
First order theory in a language $\mathscr L$: a set of sentences, called axioms of the theory.
Here is what I have done so far. We start by replacing each $n$-ary primitive operation $\omega$ by the $(n+1)$-ary primitive predicate $\omega^*$ whose interpretation in a structure $A$ is the subset of $A^{n+1}$ such that $(a_1,...,a_{n+1})\in \omega^*$ if $a_{n+1}=\omega a_1 ... a_n$.
Let $\mathscr T$ be a theory in $\mathscr L$. Then its axioms may or may not have operations $\omega \in \Omega$ in them. We let the axioms without operations invariant and for the axioms that have operations I have thought of explicitly turning them into predicate axioms. For example:
If an axiom is of the type $(t=s)$ and $t,s$ are terms of the form $t=\omega_1 t_1,...,t_n$ and $s=\omega_2 s_1,...,s_m$ then we can express $(s=t)$ equivalently as a predicate axiom by writing:
$$\bigl({\omega_1}^*(t_1,...t_{n+1}) \land {\omega_2}^*(s_1,...s_{m+1}) \Rightarrow (t_{n+1}=s_{m+1})\bigr)$$
which would mean:
$$\text{if} \ \ t_{n+1}=\omega_1 t_1,...,t_n \ \ \text{and} \ \ s_{m+1}=\hat\omega_2 s_1,...,s_m \ \ \text{then} \ \ t_{n+1}=s_{m+1}$$
If $\phi\in \Pi$ and $t_1 ,...,t_n$ are terms, we again turn the terms into predicates by doing:
$$\text{for each} \ \ t_i=\omega_ì {t_i}^1,...,{t_i}^m \ \ \text{replace} \ \ t_i \ \ \text{by} \ \ {\omega_i}^*({t_i}^1,...,{t_i}^{m+1}) \ \ \text{where} \ \ {t_i}^{m+1}=\omega {t_i}^1,...,{t_i}^m $$
and we get the predicate atomic formula:
$$\phi \bigl({\omega_1}^* \bigl({t_1}^1,...,{t_1}^{{m_1}+1}\bigr),...,{\omega_n}^* \bigl({t_n}^1,...,{t_n}^{{m_n}+1}\bigr)\bigr)$$
Now all the other formulae would be constructed form the atomic formulae and thus would also be predicate formulae, so we would be done.
I'm not sure if what I have done is correct, especially the construction of the second atomic axiom. I don't know if we can just plug predicates instead of terms into a relation $\phi$. Also, I'm not sure either if this would finish the algorithm or if I have to consider more cases, or if there's a more elegant approach to the problem, so any advice is welcome.
The first thing you would want to do, which you haven't mentioned here, is ensure that our new relation symbols actually give us functional relations. So step one is to add axioms to the effect that $$\forall\bar{x}\exists y(\omega^*(\bar{x},y)\wedge\forall z(\omega^*(\bar{x},z)\Rightarrow z=y)).$$ Otherwise the reinterpretations of our axioms may not actually ensure that our "functions" are defined or single-valued.
For your other starts so far, (2) needs to be addressed the most, since you cannot put relation symbols in place of terms, and since (1) is a special case of this anyway. I'll assume here that $\phi$ is a two place relation symbol to save some typing. You still want to look at putting terms as your arguments in $\phi$, but you want to think about building up a new formula that would mean the same thing as $\phi(\omega_1(\bar{x}),\omega_2(\bar{y}))$ did in our original language. Observe that this formula is equivalent to $$\exists x',y'(\omega_1(\bar{x})=x'\wedge\omega_2(\bar{y})=y'\wedge\phi(x',y')),$$ which gives us some hint as to what to do instead. Simply think of $\omega^*(\bar{x},x')$ as meaning "$\omega(\bar{x})=x'$" and anywhere $\phi(\omega_1(\bar{x}),\omega_2(\bar{y}))$ occurred in your old theory, substitute $$\exists x'\exists y'(\omega_1^*(\bar{x},x')\wedge\omega^*_2(\bar{y},y')\wedge \phi(x',y')),$$ renaming the quantified variables as needed. The existential quantifiers may look redundant since we already know such things exist from our functionality axioms above, but the point is that back in our functional language no variables were free in $\phi(\omega_1(\bar{x}),\omega_2(\bar{y}))$ beyond the variables $\bar{x},\bar{y}$. This is a problem with your (1), since you could put it in place of a closed formula and get an open one (and since all our old axioms were closed, we certainly want our new ones to be).
Of course, in full detail you also need to account for any instances where only some of the arguments of $\phi$ are not variables, but that's not hard.