I am trying to translate and prove a theorem, originally written in first order logic (FOL), in a combination of equitable logic (EL) and Boolean logic (BL) (more precisely a model of Boolean algebra). The target language also allows Skolemization (Sk). Then the translation task is from FOL to EL + BL + Sk. My motivation is that if my translation and the subsequent test in EL + BL + Sk are correct, then I should be able to perform such tests using a Rewrite System of Terms (TRS). TRS can be used to test equitable theories. Because EL + BL is a sublogic of FOL and Skolemization results in an equisatisfactable system, a valid proof in EL + BL + Sk is expected to be a valid proof of the original FOL theorem. Below is an example of FOL and my attempt at a natural deduction test. This is followed by my translation attempt and test in EL + BL + Sk. See translation / test notes below.
My questions are:
Is the tentative translation of FOL to EL + BL + Sk correct?
Is the tentative test correct in EL + BL + Sk?
Does the proof in EL + BL + Sk count as proof of the original FOL theorem? I'm not sure how it proves the theoretical implication ($ vdash $) in FOL refers to semantic linking ($ models $) in EL + BL + Sk. Does ($ Gamma models_ {EL + BL + Sk} varphi iff Gamma vdash_ {FOL} varphi $) to hold?
Examples of FOL formulas
At least one person likes each person: $ exists y for all x: I like (x, y) $
Each person likes at least one person: $ ( forall x exist y: Like (x, y)) $
I want to try: $ ( exist y forall x: Like (x, y)) vdash ( forall x exist y: Like (x, y)) $
Natural deduction test (ND)
The ND test uses syntactic consequence where $ Gamma vdash varphi $ means that prayer $ varphi $ is demonstrable from the set of assumptions $ Gamma $.
begin {align *}
& textbf {FOL theorem} ~~ ( exist y forall x: Likes (x, y)) vdash ( forall x exist 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 removal} \
& mathtt {skFun} ~~~~~~~~~~~~~~~~ text {Skolem function} \
& mathtt {Like} ~~~~~~~~~~~~~~~~ text {Boolean Value Function} \
& mathtt {true} ~~~~~~~~~~~~~~~~~~ text {Boolean constant} \
& \
& textbf {Translation of the theorem into EL + BL + Sk:} \
& ( forall x: ( mathtt {skFun} (x) = c, mathtt {Like} (x, c))) models ( forall x: mathtt {Like} (x, mathtt { skFun} (X))) \
& \
& textbf {Test in EL + BL + Sk} \
& textbf {1} ~~ forall x: mathtt {Like} (x, c) = true ~~~~~~ text {Assumption, with constant Skolem $ c $} \
& textbf {2} ~~ forall x: mathtt {skFun} (x) = c ~~~~~~~~~~~~~~~ text {Interpretation of Sk. work with Sk. constant $ c $} \
& textbf {3} ~~ mathtt {Like} (d, mathtt {skFun} (d)) ~~~~~~~~~~~~ text {Universal deletion and Skolemization of the term to be tested } \
& textbf {4} = ~~~~~ mathtt {Like (d, c)} ~~~~~~~~~~~~~~~~ text {Apply 2 to the second argument of 3}
& textbf {5} = ~~~~~~ true ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ text {Apply 1 to 4 } \
end {align *}
Notes on translation / proof.

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

In EL, all variables are considered universally quantified.

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

Existential variables in FOL that are in the field of universals are translated into functions of Skolem, p. $ mathtt {skFun} (x) $ with unique universal argument of $ x $. The original existential was in scope $ x $.

Each predicate in FOL translates to an operation of Boolean value in EL + BL + Sk, p. predicate $ Like $ becomes a boolean operation $ mathtt {Like} $.

In EL terms, they are different, unless they are made identical or equal by equations.
Below is the list in CafeOBJ using TRS. The command red
reduce a given term by considering the declared equations as rewrite 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