During the beginning of my Logic class, my professor wrote a theorem on the board as an example, saying that it would be something we could easily prove after a few weeks in the course. I wrote it down and have tried solving it, but no luck. Last week, I asked him about it, and he said that yes, we have learned enough rules to sufficiently prove the theorem. Only problem is, I'm struggling.
At this point, it doesn't really matter (not for a grade or anything) but it's bugging me that I can't figure it out, and the professor has kind of turned this into a game/challenge for me to figure it out (I think he enjoys seeing me struggle since I'm usually one of the better performing students).
The theorem is as follows:
: (A → B) ∨ (B → C)
The thing is, I can clearly see why it's true in my mind, but I can't figure out a way to use the given rules to solve it. As of right now, the only tools we've learned are conjunction I/E, disjunction I/E, Biconditional I/E, Conditional Proofs/Assumptions, MP, MT, Double Negation I/E, and RAA. (I/E is for introduction/elimination). I've read ways to do it using truth tables, but that's not available to us at the moment.
Any help on this, anything from a starting point hint to a full proof, would be much appreciated!
Edit: According to the professor, the proof he's expecting should be within 20-25 lines, and we're not using logical equivalences or truth tables.
With Natural Deduction, we need LEM or the equivalent DN, because the formula is not intuitionistically valid.
1) $B$ --- assumed [a]
2) $B \lor \lnot B$ --- by $\lor$-intro
3) $\lnot (B \lor \lnot B)$ --- assumed [b]
4) $\bot$ --- contradiction: 2) and 3)
5) $\lnot B$ --- by $\lnot$-intro, discharging [a]
6) $B \lor \lnot B$ --- by $\lor$-intro
7) $\bot$ --- contradiction: 3) and 6)
8) $B \lor \lnot B$ --- by DN, discharging [b].
Up to now, we have proved (classically) : $\vdash B \lor \lnot B$ (no open assumptions left).
Now we will start from 8) :
9) $B$ --- assumed [$c_1$] from 8) for $\lor$-elim
10) $A \to B$ --- from 9) by $\to$-intro
12) $\lnot B$ --- assumed [$c_2$] from 8) for $\lor$-elim
13) $B$ --- assumed [d]
14) $\bot$ --- contradiction
15) $C$ --- from 14) by $\bot$-elim
16) $B \to C$ --- by $\to$-intro, discharging [d]
Having derived $(A \to B) \lor (B \to C)$ from assumptions $B$ and $\lnot B$, we may apply $\lor$-elim: