I am studying the relationship between First Order Logic (FOL) specification methods (e.g. CASL) and equational based specification (e.g. CafeOBJ). My question is:

Is it generally possible to transform a FOL theory into a an equivalent theory that consists of an equational theory with conditional equations plus Boolean Algebra?

By equivalent I mean that the theories in both logics should denote the same class of models. The intended models are algebras that include predicates as Boolean valued functions. Boolean algebra includes the normal logical operators and can be interpreted as propositional logic. Lets call this combined logic CEQL+BOOL, if indeed it is a logic. CEQL+BOOL admits Skolem functions. In CEQL all variables are assumed to be universally quantified.
In conditional equations, denoted as $(t_1 = t'_1 \land \dots \land t_n = t'_n) \Rightarrow (t_0 = t'_0)$, 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:

$((x \times y = 1) \Rightarrow (x \times x^{-1} = 1))$ (implicit universal quantification)

is equivalent to the formula

$\forall x : ((\exists y : (x \times y = 1)) \Rightarrow (x \times x^{-1}=1))$

in ordinary first-order logic.
I believe that conditional equational logic is an extension of equational logic and both are sub-logics of FOL.

In the example below I am trying to show that the models described by Theory 1 (FOL) can be described using Theory 2 (CEQL+BOOL). I attempt to prove Theorem 1 in each logic. I do not know if these proofs really provide any evidence of equivalent models. If I can show that the sentences in both logics have the same set of theorems, is that sufficient evidence that they have the same set of models? Of course my approach, example, transformation and proofs may be flawed.

Example

Theory 1 (FOL) uses FOL notation and Theory 2 (CEQL+BOOL) uses (CEQL+BOOL) notation to describe relation $R$. My intention is that Theory 1 and Theory 2 should describe the same class of models. I provide Theorem 1 on reflexivity which I attempt to prove separately in each logic. Using the theorem prover Prover9 I can prove that if Theory 1 (FOL) holds then so does Theory 2 (CEQL+BOOL), but not vice versa.

Theory 1 (FOL) First order theory for relation R.

[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 (CEQL+BOOL) Relation R 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: show that R is reflexive: $\vdash (R~x~x) = \top$

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.1.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*}

Proof of Theorem 1 using using Natural deduction in FOL

To prove a universal property we need to set up a $\forall$-Intro sub-proof with $\fbox{a}$ as an arbitrary object. We also need $\fbox{b}$ for existential elimination

Formal proof of $\forall x (R~x~x)$ \begin{array} {rll} (1) & \forall x,y,z ((R~x~y) \land ((R~y~z)\Rightarrow (R~x~z))) & \text{(Premise: Transitivity)} \\ (2) & \forall x,y (R~x~y \Rightarrow R~y~x) & \text{(Premise: Symmetry)} \\ (3) & \forall x, \exists y R~x~y & \text{(Premise: Existence)} \\ (4) & | \quad \fbox{a} & \text{(Set up for universal introduction)}\\ (5) & | \quad \exists y (R~a~y) & \text{($\forall$-elim 3)}\\ (6) & | \quad | \quad \fbox{b}~(R~a~b) & \text{(Set up for existential elimination)} \\ (7) & | \quad | \quad (R~a~b) \Rightarrow (R~b~a) & \text{($\forall$-elim 2)} \\ (8) & | \quad | \quad (R~b~a) & \text{($\Rightarrow$-elim 6,7)} \\ (9) & | \quad | \quad R~a~b \land R~b~a & \text{($\land$-Intro 6,8)} \\ (10) & | \quad | \quad R~a~b \land R~b~a \Rightarrow (R~a~a) & \text{($\forall$-elim 1)} \\ (11) & | \quad | \quad R~a~a & \text{($\Rightarrow$-elim 9,10)} \\ (12) & | \quad R~a~a & \text{($\exists$-elim 5,6-11)} \\ (13) & \forall x (R~x~x) & \text{($\forall$-intro 4-12)} \\ \end{array}

This question is a generalisation of my previous question on the Mathematics forum.

Your Answer

 
discard

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.