Proving a first order logic theorem in equational logic with a term rewriting system

Question

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 sub-logic 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. Finally, I include a proof written in CafeOBJ that uses term rewriting.

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.

Below is the listing in CafeOBJ using TRS. The command red reduces a given term by regarding declared equations as left-to-right rewrite rules. The syntactic details of CafeOBJ are not hugely important. I hope that the relation between the two proofs can be seen in the image below. The trace of the CafeOBJ proof is basically the same as the manual proof in EL+BL+Sk above.