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:


*

*$p ⇒ q$ (premise)

*(tab)|$¬q$ (assumption)

*(tab)| (tab) |$p$ (assumption)

*(tab)| (tab) |$¬q$ (reiteration: 2)

*(tab)|$p ⇒ ¬q$ (implication introduction: 3, 4) 

*(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.

 A: 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.
A: 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:


*

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

*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$

*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. 
A: 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.
