Transforming FOL sentences

76 Views Asked by At

Can the implications (1a) and (1b) be derived from the equivalence (1)?

$\forall x \forall y : (overlap(x,y) \equiv (\exists z : part(z,x) \land part(z,y)))$                (1)

$\forall x \forall y : (overlap(x,y) \Rightarrow (\exists z : (part(z,x) \land part(z,y)))) $            (1a)

$\forall x \forall y : ((\exists z : part(z,x) \land part(z,y)) \Rightarrow overlap(x,y)) $                (1b)

Further, if I can prove (1b') does that count as a proof of (1b).

$\forall x \forall y \forall z : ((part(z,x) \land part(z,y)) \Rightarrow overlap(x,y)) $                   (1b')

In words, can I change the existentially quantified $z$ in the antecedent of 1(b) to be universally quantified variable in (1b') and use a proof of (1b') as a proof of (1b)?

1

There are 1 best solutions below

0
On BEST ANSWER

Yes and yes. Here are some general equivalence principles involving quantifiers you can use to show this:

Distribution $\forall$ over $\land$

$$\forall x (\phi(x) \land \psi(x)) \Leftrightarrow \forall x \ \phi(x) \land \forall x \psi(x)$$

Prenex Laws

Where $\varphi$ is any formula and where $x$ is not a free variable in $\psi$:

$$ \exists x \ \varphi \rightarrow \psi \Leftrightarrow \forall x (\varphi \rightarrow \psi)$$

Applied to your case:

$$\forall x \forall y : (overlap(x,y) \equiv (\exists z : part(z,x) \land part(z,y))) \Leftrightarrow \text{ (Equivalence)}$$

$$\forall x \forall y : ((overlap(x,y) \rightarrow (\exists z : part(z,x) \land part(z,y))) \land ((\exists z : part(z,x) \land part(z,y))\rightarrow overlap(x,y))) \Leftrightarrow \text{ (Distribution } \forall \text{ over } \land \text{)}$$

$$\forall x(\forall y ((overlap(x,y) \rightarrow (\exists z : part(z,x) \land part(z,y))) \land \forall y((\exists z : part(z,x) \land part(z,y))\rightarrow overlap(x,y))) \Leftrightarrow \text{ (Distribution } \forall \text{ over } \land \text{)}$$

$$\forall x \forall y ((overlap(x,y) \rightarrow (\exists z : part(z,x) \land part(z,y))) \land \forall y \forall y((\exists z : part(z,x) \land part(z,y))\rightarrow overlap(x,y)))$$

So $(1)$ is equivalent to the conjunction of $(1a)$ and $(1b)$, meaning that the latter two can indeed be derived from the former.

And, once you have $(1b)$:

$$\forall y \forall y((\exists z : part(z,x) \land part(z,y))\rightarrow overlap(x,y))) \Leftrightarrow \text{ (Prenex Law)}$$

$$\forall y \forall y \forall z((part(z,x) \land part(z,y))\rightarrow overlap(x,y))) $$

So $(1b)$ is equivalent to $(1b')$, meaning that the latter logically follows from the former as well.