How to prove this tautology using equivalences?

Question

I am trying to prove that the following is a tautology:

$(A \implies (B \implies C)) \implies ((A \implies (C \implies D)) \implies (A \implies (B \implies D)))$

To make progress, I thought I'd eliminate all the arrows. After that, and some de Morgan, I've arrived at:

$(A \land B \land ¬C) \lor (A \land ¬C \land ¬D) \lor (¬A \lor B \lor D) $

At this point, I don't know how to carry on, though. I feel like I'm missing some rule -- I get stuck in trying to expand this and don't get anywhere.

I'd be really grateful for help / hints!

EDIT:

Thank you Henning Makholm and Mauro ALLEGRANZA for spotting mistakes in my reformulations. The rewritten form should read:

$(A \land B \land ¬C) \lor (A \land C \land ¬D) \lor (¬A \lor ¬B \lor D) $

Answer 1

There must be something wrong with your rewritings -- what you have arrived at is false when all of the propositional variables are true (as well as when they're all false), whereas the original formula is true in that case.

Answer 2

(If anyone wants a proof by the deduction theorem)

Suppose $(A\implies (B\implies C))$. Then not $A$ or $(B \implies C)$.

Case 1: If not $A$, then $(A⟹(B⟹D))$. So $((A⟹(C⟹D))⟹(A⟹(B⟹D)))$ is true.

Case 2: $A$ is true. So $(B \implies C)$, then not $B$ or $C$.

Case a) If not $B$, then $(A⟹(B⟹D))$ is true.

Case b) $B$. So $C$.

Case bi) If $D$ is false, $C⟹D$ is false, so $(A⟹(C⟹D))$ is false. So $((A⟹(C⟹D))⟹(A⟹(B⟹D)))$ is true.

bii) If $D$ is true, $B⟹D$ is true. So $(A⟹(B⟹D))$ is true. So $((A⟹(C⟹D))⟹(A⟹(B⟹D)))$ is true.

So $(A⟹(B⟹C)) \implies ((A⟹(C⟹D))⟹(A⟹(B⟹D)))$.

Answer 3

excuse my unfamiliarity with the formal expression of propositional calculus, but i hope the following reasoning may be of assistance

suppose the proposition false. then we have: $$ (A \to (B \to C)) \land ¬ ((A \to (C \to D) \to (A \to (B \to D))) = \\ (A \to (B \to C)) \land ((A \to (C \to D)) \land ¬(A \to (B \to D)) = \\ (A \to ((B \to C) \land (C \to D)) \land (A \land ¬(B \to D)) = \\ ((B \to C) \land (C \to D)) \land (B \land ¬D) =\\ C \land (C \to D) \land ¬D = \\ D \land ¬D $$

Answer 4

To use equivalences to find the solution, we will profit from the equivalence scheme: $$\phi\implies(\psi\implies\chi) \quad\equiv\quad \neg\phi\lor\neg\psi\lor\chi$$ for arbitrary formulas $\phi,\psi,\chi$. This can be obtained by applying the rule of material implication $\phi \implies \psi \equiv \neg\phi \lor \psi$ twice.

Applying it to the three innermost formulas, one obtains:

$$(\neg A \lor \neg B \lor C) \implies ((\neg A \lor \neg C \lor D) \implies (\neg A \lor \neg B \lor D))$$

The entire formula, however, also fits our scheme, leading to:

$$\neg(\neg A \lor \neg B \lor C) \lor \neg(\neg A \lor \neg C \lor D) \lor (\neg A \lor \neg B \lor D)$$

Applying De Morgan on the first two entries yields the expression mentioned in your edit: $$(A \land B \land \neg C) \lor (A \land C \land \neg D) \lor \neg A \lor \neg B \lor D$$

How do we go from here? The key is expanding e.g. $\neg B$ to: $$(\neg B \land A \land \neg C) \lor (\neg B \land \neg A) \lor (\neg B \land C)$$

and then regrouping the first term with $(A \land B \land \neg C)$ to yield $A \land \neg C$. We can then continue eliminating the conjunctions with the most terms until we arrive at e.g. a canonical $A \lor \neg A$.

---

This indicates a way in which you could establish the formula is a tautology with equivalences. It should be clear, however, that this is not a very efficient way to go about it. One would be better off using e.g. the deduction theorem or truth tables.