Given p ⇒ q and m ⇒ p ∨ q, use the Fitch System to prove m ⇒ q

Question

I have spent about 6 hours now trying to prove this using the Fitch system and I just keep going in circles! Attached is one of the 500 attempts :) I have a feeling it's done fairly simply and straight-forwardly but I'm not too good at understanding the fitch system clearly... Please help!

Updated: Based on the 2 answers provided, I have managed to get here, but stuck again now! (If I use Implication Introduction for the next step, I get: m => q => q)

Answer 1

Here's a more elegant solution:

I used http://proofs.openlogicproject.org/ to do the proof.

We have M -> P v Q and we have P -> Q this means that if we get P, we also get Q.

Also our conclusion is a conditional which means conditional introduction is a good way to get that form of conclusion.

So we

1. begin by assuming M -- since this is the left side of our conditional.
2. Then we can see we have P v Q by Modus Ponens
3. Now we want to do a constructive dilemma and get rid of the v
4. The left horn (P) will give us Q by Modus Ponens
5. The right horn (Q) is Q, so we just need to repeat it.
6. This gives us Q at the same level as M.
7. We can now conclude that if we have M, we get Q.

Answer 2

This is how I ended up solving it:

Answer 3

m => p|q
So either m => q and it's done, either m => p, and since p => q, m => q.
Given that and the fact that you know how to make a Fitch System (I don't exactly) you can do it easily.

basically, given m at step 3, after step 5 either you assume p and you have q, or you assume q and you have q, so you can say that given m you have q.

I hope I've been clear enough.

Answer 4

You already know p → q. You just need to deduce q → q, enabling you to eliminate the disjunction to conclude q as desired. As: p ˅ q, p → q, q → q Ͱ q

1.|  p → q       : premise
2.|_ m → (p ˅ q) : premise
3.|   |_ m       : assumption
4.|   |  p ˅ q   : conditional elimination (2,3)
5.|   |   |_ q   : assumption
6.|   |  q → q   : conditional introduction (5-5)
7.|   |  q       : disjunction elimination (4,1,6)
8.|  m → q       : conditional introduction (3-7)

The proof writer you are using (Stanford?) should allow this, otherwise you might require the premise to be reiterated into the assumptions scope.

---

Edit: Ah,I thought this looked familiar.   It is indeed exercise 4-4 of the Standford Logic online course.   There is a "Show Answer" button there, which... does pretty much give the above result.