Is $\forall_x\forall_y\forall_z\Big(P(x,x)\wedge(P(x,z)\implies\big(P(x,y)\vee P(y,z)\big)\Big)\implies\exists_x\forall_y P(x,y)$ tautology?

Question

Is formula $$ \forall_x\forall_y\forall_z\Big(P(x,x)\wedge(P(x,z)\implies\big(P(x,y)\vee P(y,z)\big)\Big)\implies\exists_x\forall_y P(x,y) $$ a tautology?

What's method to check this? Do I need to try to construct model which would be counterexample and try to take some conclusions from it or is there some easier way?

Answer 1

Let's re-write the formula : $$\forall_x\forall_y\forall_z\Big(P(x,x)\wedge(P(x,z)\implies\big(P(x,y)\vee P(y,z)\big)\Big)\implies\exists_x\forall_y P(x,y)$$ $$\leftrightarrow \text{Because} \ (A \implies B) \equiv (\lnot A \lor B)$$ $$\forall_x\forall_y\forall_z\Big(P(x,x)\wedge( \lnot P(x,z)\lor\big(P(x,y)\vee P(y,z)\big)\Big)\implies\exists_x\forall_y P(x,y)$$ $$\leftrightarrow \text{Using the distributivity}$$ $$\forall_x\forall_y\forall_z\Big(\big(P(x,x)\wedge \lnot P(x,z)\big)\lor\big((P(x,x)\wedge P(x,y)\big)\lor\big((P(x,x)\wedge P(y,z)\big)\Big)\implies\exists_x\forall_y P(x,y)$$ $$\leftrightarrow \text{Using} \ (A \implies B) \equiv (\lnot A \lor B)$$ $$ \lnot\Bigg(\forall_x\forall_y\forall_z\Big(\big(P(x,x)\wedge \lnot P(x,z)\big)\lor\big((P(x,x)\wedge P(x,y)\big)\lor\big((P(x,x)\wedge P(y,z)\big)\Big)\Bigg)\lor\exists_x\forall_y P(x,y)$$ $$\leftrightarrow \text{Using de Morgan on $\lnot\forall_{x,y,z}$}$$ $$ \Bigg(\exists_x\exists_y\exists_z\lnot\Big(\big(P(x,x)\wedge \lnot P(x,z)\big)\lor\big((P(x,x)\wedge P(x,y)\big)\lor\big((P(x,x)\wedge P(y,z)\big)\Big)\Bigg)\lor\exists_x\forall_y P(x,y)$$ $$\leftrightarrow \text{Using $\lnot( A \lor B) \equiv (\lnot A \land \lnot B) $}$$ $$ \Bigg(\exists_x\exists_y\exists_z\Big(\lnot\big(P(x,x)\wedge \lnot P(x,z)\big)\land\lnot\big((P(x,x)\wedge P(x,y)\big)\land\lnot\big((P(x,x)\wedge P(y,z)\big)\Big)\Bigg)\lor\exists_x\forall_y P(x,y)$$ $$\leftrightarrow \text{Using $\lnot( A \land B) \equiv (\lnot A \lor \lnot B) $}$$ $$ \Bigg(\exists_x\exists_y\exists_z\Big(\big(\lnot P(x,x)\lor P(x,z)\big)\land\big((\lnot P(x,x)\lor \lnot P(x,y)\big)\land\big((\lnot P(x,x)\lor \lnot P(y,z)\big)\Big)\Bigg)\lor\exists_x\forall_y P(x,y)$$ $$\leftrightarrow \text{Using $(\exists_x A) \lor (\exists_x B) \equiv \exists_x (A \lor B)$}$$ $$ \exists_x\exists_y\exists_z\Bigg(\Big(\big(\lnot P(x,x)\lor P(x,z)\big)\land\big((\lnot P(x,x)\lor \lnot P(x,y)\big)\land\big((\lnot P(x,x)\lor \lnot P(y,z)\big)\Big)\lor \big(\forall_y P(x,y)\big)\Bigg)$$

If you want to prove a tautology here you just need to prove that $\big(\forall_y P(x,y)\big)$ is true for a fixed x.

Answer 2

Whenever I am confronted with this kind of question, I will first scan the statement and see if I can quickly make sense of it being a tautology (so in this case: if the consequent does indeed logically follows from its antecedent).

If I don't find a quick justification for that, I'll try to produce a counterexample ... if I find one then it's not a tautology, and if there isn't one, then presumably I can see why I wasn't able to find one, and hopefully will be able to translate that into a proof that it is a tautology after all.

Also, my search for counterexamples (especially when binary predicates are involved) typically goes something like this:

First, I go through a list of the 'usual suspects': for the domain I consider the natural numbers, integers, or real numbers, and for the binary predicate I'll try things like $=$, $<$, or $\le$.

If that doesn't quickly work, I'll move on to very simple but completely abstract domains, where there are $1$, $2$, or $3$ objects $a$, $b$, and $c$, and just play around with those.

If I don't get a quick answer there either, I'll try some more systematic method, like truth trees.

Fortunately for you, in this case the first method for finding a counterexample works just fine ... (yes, that's a big HINT)