6

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.
God's Drunkest Driver
  • 315

3 Answers3

8

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.

God's Drunkest Driver
  • 315
6

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.

Bram28
  • 100,612
  • 6
  • 70
  • 118
  • would I have to make ~(~p V q) become p & ~q by any chance? fyi, this is the site where the exercise is from http://logic.stanford.edu/intrologic/exercises/exercise_04_11.html – God's Drunkest Driver 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
  • 1
    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. – God's Drunkest Driver Feb 16 '17 at 23:35
  • 1
    @AndrewGuo Hey, good work!! You're clearly getting better at these proofs! – Bram28 Feb 17 '17 at 01:58
0

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.

Community
  • 1
Conor
  • 536