I am trying to understand the relationship between arbitrary FOL theories and theories that consist of conditional equations plus Boolean algebra (CEQL+BOOL). For example:
Given the following first order theory for relation R expressed using FOL:
Theory 1
[Symmetry] $\forall x,y : ((R~x~y) \Leftrightarrow (R~y~x))$
[Transitivity] $\forall x,y,z : (((R~x~y) \land ((R~y~z)) \Rightarrow R~x~z)$
[Existence] $\forall x \exists y : (R~x~y)$
Theory 2 ,below, represents my efforts to transform theory Theory 1 into a conditional equational theory (CEQL). I permit Boolean Algebra in the language, so we have CEQL+BOOL. Boolean algebra includes the normal logical operators and can be interpreted as propositional logic. CEQL+BOOL admits Skolem functions. All variables are assumed to be universally quantified. In conditional equations, variables in the conditions $(t_1 = t'_1 \land \dots \land t_n = t'_n)$ that do not appear in the consequent $(t_0 = t'_0)$ can be seen as existentially quantified in a FOL context. For example:
$\forall x,y : t \bullet ((x \times y = 1) \Rightarrow (x \times x^{-1} = 1))$
is equivalent to the formula
$\forall x : t \bullet ((\exists y : t \bullet (x \times y = 1)) \Rightarrow (x \times x^{-1}=1))$
in ordinary first-order logic.
Theory 2 expressed in CEQL+BOOL
[Symmetry] $(R~x~y) = (R~y~x)$
[Transitivity] $((R~x~y) = \top) \land ((R~y~z) = \top)) \Rightarrow (R~x~z = \top$)
[Existence] $(R~x~skolem(x)) = \top$
Theorem 1 Using Theory 2 show that R is reflexive: $\vdash (\forall x (R~x~x))$
Proof of Theorem 1 using CEQL+BOOL
\begin{align*} &~~~~\{\text{Transitivity Axiom\}} \\ &(1)~~~~((R~x~y) = \top) \land ((R~y~z) = \top) \Rightarrow (R~z~x = \top)\\ & \text{ \{Substitution, z = x \}} \\ &(2)~~~~((R~x~y) = \top) \land ((R~y~x) = \top) \Rightarrow (R~x~x = \top)\\ &= \text{\{Symmetry Axiom at term (2.2.1)\}} \\ &(4)~~~~((R~x~y) = \top) \land ((R~x~y) = \top) \Rightarrow (R~x~x = \top)\\ &= \text{\{Substitution, y = skolem(x) \}}\\ &(5)~~~~((R~x~skolem(x)) = \top) \land ((R~x~skolem(x)) = \top) \Rightarrow (R~x~x = \top)\\ &= \text{\{Existance axiom \}} \\ &(6)~~~~(\top \land \top)\Rightarrow (R~x~x = \top)\\ &= \text{\{ Boolean Algebra: Idempotency of $\land$\}}\\ &(7)~~~~\top \Rightarrow (R~x~x = \top)\\ &= \text{\{Boolean Algebra: Left identity of $\Rightarrow$\}}\\ &(8)~~~~(R~x~x = \top) \end{align*}
Are the transform and proof reasonable?
This question uses same theorem proved in Prove reflexivity using Fitch software