I am trying to translate and prove a theorem, originally written in first order logic (FOL), into a combination of equational logic (EL) and Boolean logic (BL) (more precisely a model of Boolean Algebra). The target language also permits Skolemization (Sk). So the translation task is from FOL to EL+BL+Sk. My motivation is that if my translation and subsequent proof in EL+BL+Sk are correct, then I should be able to perform such proofs using a Term Rewriting System (TRS). TRS can be used to prove equational theories. Because EL+BL is a sublogic of FOL and Skolemization results in an equisatisfiable system, it is hoped that a valid proof in EL+BL+Sk is a valid proof of the original FOL theorem. Below is a FOL example and my attempt at a proof using natural deduction. This is followed by my attempt at translation and proof in EL+BL+Sk. See notes on translation/proof below.
My questions are:
Is the tentative translation from FOL to EL+BL+Sk correct?
Is the tentative proof in EL+BL+Sk correct?
Does the proof in EL+BL+Sk count as a proof of the original FOL theorem? I am not sure how proof theoretic entailment ($ \vdash$ ) in FOL relates to semantic entailment ($ \models$ ) in EL+BL+Sk. Does ($ \Gamma \models_{EL+BL+Sk} \varphi \iff \Gamma \vdash_{FOL} \varphi$ ) hold?
Example FOL formulae
At least one person is liked by every person: $ \exists y \forall x :Likes(x,y)$
Every persons likes at least one person: $ (\forall x \exists y: Likes(x,y)) $
I want to prove: $ (\exists y \forall x: Likes(x,y)) \vdash (\forall x \exists y : Likes(x,y)) $
Natural Deduction (ND) proof
The ND proof uses syntactic consequence where $ \Gamma \vdash \varphi$ means that the sentence $ \varphi$ is provable from the set of assumptions $ \Gamma$ . \begin{align*} &\textbf{FOL Theorem}~~(\exists y \forall x :Likes(x,y)) \vdash (\forall x \exists y :Likes(x,y)) \ &\ &\textbf{Notation for EL+BL+Sk}\ &x~~~~~~~~~~~~~~~~~~~~~~~~~\forall x~~\text{Universally Quantified variable}\ &c~~~~~~~~~~~~~~~~~~~~~~~~~~\text{Skolem Constant}\ &d~~~~~~~~~~~~~~~~~~~~~~~~\text{Arbitrary $ Person$ , for universal elimination}\ &\mathtt{skFun}~~~~~~~~~~~~~~~~\text{Skolem Function}\ &\mathtt{Likes}~~~~~~~~~~~~~~~~\text{Boolean valued function}\ &\mathtt{true}~~~~~~~~~~~~~~~~~~\text{Boolean constant}\ &\ &\textbf{Translation of Theorem to EL+BL+Sk:}\ &(\forall x :(\mathtt{skFun}(x)=c ,\mathtt{Likes}(x,c)))\models(\forall x:\mathtt{Likes}(x,\mathtt{skFun}(x))) \ &\ &\textbf{Proof in EL+BL+Sk}\ &\textbf{1}~~\forall x:\mathtt{Likes}(x,c) = true~~~~~~\text{Assumption, with Skolem constant $ c$ }\ &\textbf{2}~~\forall x:\mathtt{skFun}(x) = c~~~~~~~~~~~~~~~\text{Interpretation of Sk. function with Sk. constant $ c$ }\ &\textbf{3}~~\mathtt{Likes}(d,\mathtt{skFun}(d))~~~~~~~~~~~~\text{Universal elim & Skolemization of term to be proved}\ &\textbf{4}=~~~~~\mathtt{Likes(d,c)}~~~~~~~~~~~~~~~~\text{Apply 2 to second argument of 3}\ &\textbf{5}=~~~~~~true~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\text{Apply 1 at 4}\ \end{align*} Notes on translation/proof.

The EL+BL+Sk proof relies on an interpretation, so the translation needs semantic entailment $ \models$ . In general, this can be written as $ \Gamma \models_{EL+BL+Sk} \varphi$ , which means that under $ EL+BL+Sk$ logic the sentence $ \varphi$ is true in all models of $ \Gamma$ .

In EL all variables are considered to be universally quantified.

Existential variables in FOL that are not in the scope of universals are translated to Skolem constants.

Existential variables in FOL that are in the scope of universals are translated to Skolem functions e.g. $ \mathtt{skFun}(x)$ with single universal argument of $ x$ . The original existential was in the scope $ x$ .

Each predicate in FOL is translated to a Boolean valued operation in EL+BL+Sk, e.g. predicate $ Likes$ becomes Boolean operation $ \mathtt{Likes}$ .

In EL terms are distinct, unless they are made identical or equal by equations.
Here is the listing in CafeOBJ using TRS.
mod LIKES { [Person] pred Likes : Person Person } op c : > Person . ops d : > Person . op skFun : Person > Person .  Hypothesis eq [assumption] : Likes(x:Person,c) = true . eq [skolem] : skFun(x:Person) = c . reduce Likes(d,skFun(d)) . > Gives true