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.
  • $\begingroup$ For "and" : \land; for "or" : \lor; for "not" : \lnot. $\endgroup$ – Mauro ALLEGRANZA Feb 10 '17 at 21:07
  • $\begingroup$ @MauroALLEGRANZA thank you. $\endgroup$ – 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.

| cite | improve this answer | |

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.

| cite | improve this answer | |
  • $\begingroup$ 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 $\endgroup$ – Andrew Guo Feb 10 '17 at 21:34
  • $\begingroup$ @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$ $\endgroup$ – Bram28 Feb 10 '17 at 22:12
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrew Guo Feb 16 '17 at 23:35
  • 1
    $\begingroup$ @AndrewGuo Hey, good work!! You're clearly getting better at these proofs! $\endgroup$ – 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:


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.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.