# Given $p$ ⇒ $q$, use the Fitch System to prove ¬p ∨ q.

Disclaimer: I'm a complete newbie to the site, and I haven't fully figured out how to format properly. I do not have enough reputation to use the meta sandbox thread, so in addition to asking my question, I may use some space below to test some stuff out...

edit: I now have enough reputation to use the meta forums

Here's what I've done so far, with regards to the question:

1. $p ⇒ q$ (premise)
2. (tab)|$¬q$ (assumption)
3. (tab)| (tab) |$p$ (assumption)
4. (tab)| (tab) |$¬q$ (reiteration: 2)
5. (tab)|$p ⇒ ¬q$ (implication introduction: 3, 4)
6. (tab)|$¬p$ (negation introduction: 1,5)

I thought of "Or-ing" $¬p$ with $q$ (Or introduction: 6) but that would not be a complete proof, because I would still be within a subproof. What steps am I missing? Or, perhaps, was I going in the wrong direction in the first place?

Also, please do not edit the format of my question. Instead, I would appreciate formatting suggestions, especially including the following:

• how do I format a tab?
• how do I format logic symbols like "and"/"or", without using copy+paste.
• how do I format Fitch-style logic problems. I don't want to use "|" as a substitute for the solid line going down.
• For "and" : \land; for "or" : \lor; for "not" : \lnot. – Mauro ALLEGRANZA Feb 10 '17 at 21:07
• @MauroALLEGRANZA thank you. – Andrew Guo Feb 10 '17 at 21:11

A bit long winded, due to the logic software's inability to do a contradiction intro:

1.  p => q            Premise
2.    ~(~p | q)       Assumption
3.      ~p            Assumption
4.      ~p | q        Or Introduction: 3
5.    ~p => ~p | q    Implication Introduction: 3, 4
6.     ~p             Assumption
7.     ~(~p | q)      Reiteration: 2
8.    ~p => ~(~p | q) Implication Introduction: 6, 7
9.    ~~p             Negation Introduction: 5, 8
10.   p               Negation Elimination: 9
11.   q               Implication Elimination: 1, 10
12.   ~p | q          Or Introduction: 11
13. ~(~p | q) => ~p | q        Implication Introduction: 2, 12
14.  ~(~p | q)                 Assumption
15. ~(~p | q) => ~(~p | q)     Implication Introduction: 14, 14
16. ~~(~p | q)                 Negation Introduction: 13, 15
17. ~p | q                     Negation Elimination: 16


Bam, done.

I am not sure why you start by assuming $$\neg q$$ ...

Instead, try a proof by contradiction: assume $$\neg (\neg p \lor q)$$, and derive a contradiction between that and your premise.

In general, if your goal is ever a disjunction $$A \lor B$$, there are basically 3 strategies:

1. If you're lucky, you already have (or can get to) $$A$$ or $$B$$ by itself ... so then you can just do $$\lor \: Intro$$

2. If you have some other disjunction (e.g $$C \lor D$$) to work with, then a fruitful approach may be to do a proof by cases on the $$C \lor D$$: So do one subproof assuming $$C$$, and a second subproof assuming $$D$$: chances are that one of them leads to $$A$$, and that the other one leads to $$B$$. And then in either case you can do $$\lor \: Intro$$ at the end of the subproof to get $$A \lor B$$, which you can then pull out using $$\lor \: Elim$$

3. Finally, you can try to do a proof by Contradiction, i.e. assume $$\neg (A \lor B)$$ and try to get a contradiction. The nice thing about this strategy is that after assuming $$\neg (A \lor B)$$, you can (with some work) derive $$\neg A$$ as well as $$\neg B$$, so you get some nice 'small stuff' that you can use to combine with other premises you have on your way to a contradiction.

• would I have to make ~(~p V q) become p & ~q by any chance? fyi, this is the site where the exercise is from logic.stanford.edu/intrologic/exercises/exercise_04_11.html – Andrew Guo Feb 10 '17 at 21:34
• @AndrewGuo You should be able to infer $p$ by itself from $\neg (\neg p \lor q)$, and the same is true for $\neg q$. And with $p$ and $p \to q$ you get $q$, so that will contradict the $\neg q$ – Bram28 Feb 10 '17 at 22:12
• The software I use for Fitch Proofs cannot do a contradiction intro, so it costed me many more steps. I answered my own question with the proof that works but seems a bit long winded but works. – Andrew Guo Feb 16 '17 at 23:35
• @AndrewGuo Hey, good work!! You're clearly getting better at these proofs! – Bram28 Feb 17 '17 at 1:58

# Annotation of Andrew Guo's proof

These proofs require us to work backwards from our conclusion (goal) to our premises.

Our goal is find ~p|q. We do not have access to ~p or q.

We only know that p => q.

Thus we have to proceed by reductio ad absurdum. We assume the opposite (the negation) of our goal. From this assumption we try to derive a contradiction.

1.  p => q              Premise
2.      ~(~p | q)       Assumption


A contradiction will be something similar to:

~(~p | q) =>  p
~(~p | q) => ~p


Andrew Guo uses

~(~p | q) =>  (~p | q)
~(~p | q) => ~(~p | q)


Most of Andrew's proof is concerned with deriving the :

~(~p | q) =>  (~p | q)


Here is Andrew's proof of this lemma:

Subproof

1.   ~(~p | q)          Premise
2.        ~p            Assumption
3.        ~p | q        Or Introduction: 3
4.    ~p => ~p | q      Implication Introduction: 3, 4
5.        ~p            Assumption
6.        ~(~p | q)     Reiteration: 2
7.    ~p => ~(~p | q)   Implication Introduction: 6, 7
8.    ~~p               Negation Introduction: 5, 8
9.    p                 Negation Elimination: 9
10.   q                 Implication Elimination: 1, 10
11.   ~p | q            Or Introduction: 11


These proofs have a recursive nature. Inside the sub proof, Andrew uses another instance of proof by contradiction.

He starts by assuming ~p. He proceeds to show that this results in a contradiction:

~p =>   ~p | q
~p => ~(~p | q)


If ~p results in a contradiction, then by the law of the excluded middle p must hold.

Andrew uses p to get q via our (almost forgotten) premise p=>q.

From q he can get ~p | q.

After this fractal-ing deep dive we can finally break out of our sub proof with a Negation introduction.