Rewriting implication als disjunction - equivalence proofs

Question

Given that I have to proof that the following formula is a tautology using equivalence proofs: $$\big(∀x: P(x, C) \to (∀a: P(a, a))\big) ~\to~ ∀b : (∀c : P(c, C)) \to P(b, b)$$

I am aware that I have to rewrite this as a disjunction, but considering the formula contains four implications how do you go about rewriting it?

Is there a Youtube series/site which could help me understand equivalence proofs? I already looked around but it seems the English translation might be different.

Thanks in advance.

Answer 1

$$\big(∀x: P(x, C) \to (∀a: P(a, a))\big) ~\to~ ∀b : (∀c : P(c, C)) \to P(b, b)$$

Under the usual ordering conventions: $A\to B\to C$ is read as $A\to(B\to C)$.

However, usually $\to$ has precedence over quantification, but that would place $P(b,b)$ outside the scope of the universal quantifier ($\forall b$) which I am sure was not intended. (Perhaps they are conceding precedence to the colon?)

So the implicit bracketing would appear to be

$$\Big(∀x: \color{blue}{\big(}P(x, C) \to (∀a: P(a, a))\color{blue}{\big)}\Big) ~\to~ ∀b : \color{blue}{\Big(}\big(∀c : P(c, C)\big) \to P(b, b)\color{blue}{\Big)}$$

Which is indeed a tautology.

---

So begin rewriting one step at a time. $$\Big(\forall x:\big(P(x,C)\to(\forall a: P(a,a))\big)\Big)\to\forall b:\Big(\neg\big(\forall c:P(c,C)\big)\lor P(b,b)\Big)\\~\\\Big(\forall x:\big(P(x,C)\to(\forall a: P(a,a))\big)\Big)\to\forall b:\Big(\big(\exists c:\neg P(c,C)\big)\lor P(b,b)\Big)\\~\\\neg\Big(\forall x:\big(P(x,C)\to(\forall a: P(a,a))\big)\Big)\lor\forall b:\Big(\big(\exists c:\neg P(c,C)\big)\lor P(b,b)\Big)\\~\\\vdots$$