How do I reason with Skolem functions?

Question

Given the first-order sentence.

$\forall x \forall y : (Overlap(x,y) \iff (\exists z Part(z,x) \land Part(z,y)))~~~~~~~~~~~~~~~~$ (1)

Here is an outline (partial) proof that $Overlap$ is symmetric:

Proof 1 \begin{align} & \text{1}~~\forall x \forall y : (Overlap(x,y) \iff (\exists z Part(z,x) \land Part(z,y))) & \tag{Axiom}\\ & \text{2}~~~~~~~Overlap(a,b) \tag{Assume} \\ & \text{3}~~~~~~~\exists z (Part(z,a) \land Part(z,b)) \tag{1,2}\\ & \text{4}~~~~~~~\exists z (Part(z,b) \land Part(z,a)) \tag{3}\\ & \text{5}~~~~~~~Overlap(b,a) \tag{1,2,4}\\ & \text{6}~~\forall x \forall y : (Overlap(x,y) \implies Overlap(y,x)) \tag{$\forall$-Intro 2-5} \\ \end{align} Note in line 4 the same existential $z$ is used.

Now I wish write the axiom (1) in an equisatisfiable form that can be proved using equational logic and term rewriting. This usually requires Skolemization. Sentence (1) can be Skolemized as follows:

$\forall x \forall y : (Overlap(x,y) \iff (Part(Sk(x,y),x) \land Part(Sk(x,y),y))~~~~~~~~~~~$ (2)

Now I try to prove symmetry using (2) with a similar approach as in Proof 1:

Proof Attempt 2 \begin{align} & \text{1}~~\forall x \forall y : (Overlap(x,y) \iff (Part(Sk(x,y),x) \land Part(Sk(x,y),y))& \tag{Axiom}\\ & \text{2}~~~~~~~~Overlap(a,b) \tag{Assume} \\ & \text{3}~~~~~~~~Part(Sk(a,b),a) \land Part(Sk(a,b),b) \tag{1,2}\\ & \text{4}~~~~~~~~Part(Sk(a,b),b) \land Part(Sk(a,b),a) \tag{3}\\ & \text{5}~~~~~~~~Overlap(b,a)\tag{XX}\\ & \text{6}~~\forall x \forall y : (Overlap(x,y) \implies Overlap(y,x)) \tag{XX} \\ \end{align}

I am stuck at lines 4-5 in Proof Attempt 2.By following the approach of Proof 1 there is an issue with the order of arguments to Skolem functions.

Answer 1

This is a sketch of the main idea. The axiom is the same if the universal quantifiers are interchanged.

Skolemization of this gives $$\exists Sk \forall y \forall x \; Overlap(x, y) \Leftrightarrow Part(Sk(y, x), x) \land Part(Sk(y, x), y) \tag{a}\label{eqa}$$

which is equivalent to

$$\exists Sk \forall x \forall y \; Overlap(y, x) \Leftrightarrow Part(Sk(x, y), y) \land Part(Sk(x, y), x) \tag{b}\label{eqb}$$

by changing the names of the variables.

We can also show similarly from the Axiom that

$$\exists S \forall x \forall y \; Overlap(x, y) \Leftrightarrow Part(S(x, y), y) \land Part(S(x, y), x) \tag{c}\label{eqc}$$

From (\ref{eqb}) and (\ref{eqc}) and the assumption on the Skolem functions that $\exists Sk \exists S \forall x \forall y \; Sk(x, y) = S(x, y)$, it follows

$$\forall x \forall y \; Overlap(x,y) \Leftrightarrow Overlap(y, x) $$

Answer 2

We can translate the original bi-conditional axiom into three implications. Using the quantifier equivalence, $\exists x (Q(x) \implies P) \equiv \forall x Q(x) \implies P $, the existential in the original (1) can be replaced by a universal $z$, so line 3 below does not need a Skolem function. I believe these 3 sentences and the FOL sentence (1) are equisatisfiable. I believe breaking (1) into three parts makes the proof fairly straightforward.

Proof \begin{align} & \text{1}~~\forall x \forall y : (Overlap(x,y) \implies Part(Sk(x,y),x)) & \tag{Axiom1}\\ & \text{2}~~\forall x \forall y : (Overlap(x,y) \implies Part(Sk(x,y),y))& \tag{Axiom2}\\ & \text{3}~~\forall x \forall y \forall z : ((Part(z,x) \land Part(z,y)) \implies Overlap(x,y))& \tag{Axiom3}\\ & \text{4 (a,b)}~~Overlap(a,b) \tag{Assume} \\ & \text{5}~~~~~~~~~~~~~(Part(Sk(a,b) ,a) \land Part(Sk(a,b) ,b)) \implies Overlap(a,b) \tag{$\forall$-Elim 3}\\ & \text{6}~~~~~~~~~~~~~Overlap(a,b) \implies Part(Sk(a,b),a) \tag{$\forall$-Elim 1}\\ & \text{7}~~~~~~~~~~~~~Overlap(a,b) \implies Part(Sk(a,b),b) \tag{$\forall$-Elim 2}\\ & \text{8}~~~~~~~~~~~~~Part(Sk(a,b),a) \tag{$\implies$-Elim 4,6}\\ & \text{9}~~~~~~~~~~~~~Part(Sk(a,b),b) \tag{$\implies$-Elim 4,7}\\ & \text{10}~~~~~~~~~~~~~Part(Sk(a,b),b) \land Part(Sk(a,b),a) \tag{$\land$-Intro 8,9}\\ & \text{11}~~~~~~~~~~~~~(Part(Sk(a,b) ,b) \land Part(Sk(a,b) ,a)) \implies Overlap(b,a) \tag{$\forall$-Elim 3}\\ & \text{12}~~~~~~~~~~~~~Overlap(b,a) \tag{$\implies$-Elim 10,11}\\ & \text{13}~~\forall x \forall y : (Overlap(x,y) \implies Overlap(y,x)) \tag{$\forall$-Intro 4-12} \\ \end{align}