I am trying to translate and prove a sentence that was originally written in first order logic (FOL) into a combination of equation logic (EL) and Boolean logic (BL) (more precisely, a model of Boolean algebra). The target language also allows skolemization (Sk). The translation task is therefore from FOL to EL + BL + Sk. My motivation is that if my translation and the subsequent proof in EL + BL + Sk are correct, I should be able to provide such proof using a term rewriting system ( TRS). TRS can be used to prove equation theories. Since EL + BL is a sublogic of FOL and Skolemization leads to an equivalent system, it is to be 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 to prove it with natural derivatives. This is followed by my attempt to translate and test in EL + BL + Sk. See notes on translation / proof below.
My questions are:
Is the preliminary translation from FOL to EL + BL + Sk correct?
Is the preliminary proof in EL + BL + Sk correct?
Does the proof in EL + BL + Sk count as proof for the original FOL theorem? I am not sure how conclusive the theoretical consequence is ($ vdash $) in FOL refers to semantic enttailment ($ models $) in EL + BL + Sk. Tut ($ Gamma models_ {EL + BL + Sk} varphi iff Gamma vdash_ {FOL} varphi $) stop?
ExampleFOL formulas
At least one person likes each person: $ exists y for all x: Likes (x, y) $
Every person likes at least one person: $ ( forall x exists y: Likes (x, y)) $
I want to prove: $ ( exists y for all x: Likes (x, y)) vdash ( exists for all x exists y: Likes (x, y)) $
Natural Deduction (ND) proof
The ND proof uses syntactic consequences $ Gamma vdash varphi $ means the sentence $ varphi $ can be demonstrated from the assumptions $ Gamma $,
begin {align *}
& textbf {FOL Theorem} ~~ ( exists y for all x: Likes (x, y)) vdash ( for all x exists y: Likes (x, y)) \
& \
& textbf {notation for EL + BL + Sk} \
& x ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
& c ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~
& d ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~
& mathtt {skFun} ~~~~~~~~~~~~~~~~~~ text {Skolem function} \
& mathtt {Likes} ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~
& mathtt {true} ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~
& \
& textbf {Translation of the sentence according to EL + BL + Sk:} \
& ( forall x: ( mathtt {skFun} (x) = c, mathtt {Like} (x, c))) models ( forall x: mathtt {Like} (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} ~~ for everyone 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 evidence } \
& textbf {4} = ~~~~~ mathtt {Likes (d, c)} ~~~~~~~~~~~~~~~~~~ text {Apply 2 to the second argument of 3 to}
& textbf {5} = ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~ text {Apply 1 at 4} \
end {align *}
Instructions for translation / proofing.

The EL + BL + Sk proof is based on an interpretation, so that the translation requires a semantic correspondence $ models $, In general, this can be written as $ Gamma models_ {EL + BL + Sk} varphi $, which means that under $ EL + BL + Sk $ logically the sentence $ varphi $ is true in all models of $ Gamma $,

In the EL, all variables are considered to be universally quantified.

Existence variables in FOL that are not in the range of universals are translated into Skolem constants.

Existence variables in FOL that are in the range of universals are translated into Skolem functions, e.g. $ mathtt {skFun} (x) $ with a universal argument from $ x $, The original existential was within the scope $ x $,

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

In EL, expressions are different unless they are made the same or the same by equations.
Below is the listing in CafeOBJ with TRS. The command red
Reduces a specific term by viewing declared equations as rewriting rules from left to right
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 .
red Likes(d,skFun(d)) .
> Gives true