# Prove distribution of or over implies knowing the implication is always true

I was given a task to construct a Hilbert-style proof for the following:

$$A → B ⊢ C ∨ A → C ∨ B$$

I figured I could use the axiom $$A→B≡A∨B≡B$$, but this leads me nowhere since I don't think I can use the consequent anywhere.

The theorem is intuitively true to me (since we know $$A→B$$, adding a true $$C$$ in there will give $$⊤→⊤$$, obviously true, and a false $$C$$ gives the original $$A→B$$), but I do not know how to prove this.

I'm using Tourlakis' Mathematical Logic and all axioms contained within it.

• What you're doing there $A→B≡A∨B≡B$ is neither hilbert-caluclus nor sequent-calculus ... . If you want help on this one, you'll first have to tell us exactly what rules you have to work with, because there are many logical proof systems. – Bram28 Feb 19 '19 at 18:39
• I am using Tourlakis' Mathematical Logic (2008) and the axioms contained within it. – Bill Feb 19 '19 at 19:57
• Which doesn't help anyone who doesn't have that book on hand. – Graham Kemp Feb 19 '19 at 22:32
• Looked at that book ... ugh, that's not a very user-friendly system for beginners. Do you have to use that book? – Bram28 Feb 19 '19 at 23:20
• Yeah, it's what the class is using @Bram28 – Bill Feb 20 '19 at 0:12

Here are the relevant Hilbert Axiom Schemas...(your book may label them differently, or treat disjunction as a substitution.)

$$\begin{array}{rl}\mathrm A2.&\phi\to(\psi\to\phi) \\ \mathrm A3.&(\phi\to(\psi\to\xi))\to((\phi\to\psi)\to(\phi\to\xi)) \\ \lor\mathrm {IL}.&\phi\to(\phi\lor\psi) \\ \lor\mathrm {IR}.&\phi\to(\psi\lor\phi) \\ \lor\mathrm E.&(\phi\to\xi)\to((\phi\to\xi)\to((\phi\lor\psi)\to\xi)) \\\hdashline \mathrm P1.&A\to B \\\hline 2.&\lower{2ex}\ddots\end{array}$$

• Unfortunately, Tourlakis' axioms look nothing like this .... – Bram28 Feb 21 '19 at 3:38

1) $$A \to B \ \ \ \ \ \langle \text { assumption } \rangle$$

2) $$C \lor A \ \ \ \ \ \ \langle \text { assumption } \rangle$$

3) $$C \lor A \equiv \lnot C \to A \ \ \ \ \langle 2.4.11 \rangle$$

4) $$\lnot C \to A \ \ \ \ \langle (2,3) + \text {Eqn} \rangle$$

5) $$\lnot C \to B \ \ \ \ \langle (2.5.9 \text { Coroll. - Transitivity of} \to) \rangle$$

6) $$C \lor B \equiv \lnot C \to B \ \ \ \ \langle 2.4.11 \rangle$$

7) $$C \lor B \ \ \ \ \langle (5,6) + \text {Eqn} \rangle$$

8) $$C \lor A \to C \lor B \ \ \ \langle (2.6.1 \text { Deduction Theorem}) \rangle$$