Thread: Abstract reasoning/natural deduction with Fitch

I'm practicing natural deduction, using a system similar to Fitch. I'm wondering if what I'm doing is legal, especially the => intro @ 5.

I've to prove is a tautology. I've set my reasoning up as follows:

Code:

1, H:                              (P => Q) => P
2, H:                                 P
3, => elim on 1 & 2                      P => Q
4, => elim on 2 & 3                      Q
5, => intro on 3 & 4                  (P => Q) => Q
6, => intro on 1 & 5               ((P => Q) => P) => ((P => Q) => Q)

Is this approach correct? I think not, because I'm not actually using the hypothesis (2) in my conclusion (5).

Am I allowed to do this?

Code:

1, H:        P
2, H:             Q
3, ^I 1,2              P ^ Q
4, =>I 3,2       (P ^ Q) => Q
     || ||

I've a new way to solve the first one:

Code:

1, H:       (P => Q) => P
2, H:           P => Q
3, =>E 1,2:         P
4, =>E 2,3:         Q
5, =>I 2,4:     (P => Q) => Q
6, =>I 1,5: ((P => Q) => P) => ((P => Q) => Q)

I think this is correct, any advice?

Regarding the second part, the question was to prove P => ((P ^ Q) => Q) is a tautology, now I've set up my reasoning as follows

Code:

1, H:       P
2, H:           Q
3, ^I 1,2:          P ^ Q
4, ^E 3:            Q
5, =>I 3,4:    (P ^ Q) => Q
6, =>I 1,5: P => ((P ^ Q) => Q

Furthermore I'm trying to prove (P => Q) => ((P ^ R) => (Q ^ R)) and having some trouble introducing the R, my current train of thought leaves me with an assumption i can't get rid of.

Code:

1, H:       P => Q
2, H:           P
3, =>E 1,2:         Q
4, H:                    R
5, ^I 2,4:                    P ^ R
6, ^I 3,4:                    Q ^ R
7, =>I 5,6:              (P ^ R) => (Q ^ R)
8, =>I 1,7: (P => Q) => ((P ^ R) => (Q ^ R))

As you see, I'm left out with an assumption too many. I guess I'm introducing the R (4) incorrect, any pointers?

Originally Posted by Lepzed

Code:

1, H:                              (P => Q) => P
2, H:                                 P
3, => elim on 1 & 2                      P => Q
4, => elim on 2 & 3                      Q
5, => intro on 3 & 4                  (P => Q) => Q
6, => intro on 1 & 5               ((P => Q) => P) => ((P => Q) => Q)

Step 3 is wrong because MP gives you the conclusion of an implication, not the premise. Step 5 is also wrong because =>I can only close an assumption and never a formula that is a conclusion of a subderivation, like formula 3.

Originally Posted by Lepzed

Code:

1, H:        P
2, H:             Q
3, ^I 1,2              P ^ Q
4, =>I 3,2       (P ^ Q) => Q
     || ||

=>I cannot close P ^ Q since it's not an assumption.

Originally Posted by Lepzed

I've a new way to solve the first one:

Code:

1, H:       (P => Q) => P
2, H:           P => Q
3, =>E 1,2:         P
4, =>E 2,3:         Q
5, =>I 2,4:     (P => Q) => Q
6, =>I 1,5: ((P => Q) => P) => ((P => Q) => Q)

This is correct.

Originally Posted by Lepzed

Regarding the second part, the question was to prove P => ((P ^ Q) => Q) is a tautology, now I've set up my reasoning as follows

Code:

1, H:       P
2, H:           Q
3, ^I 1,2:          P ^ Q
4, ^E 3:            Q
5, =>I 3,4:    (P ^ Q) => Q
6, =>I 1,5: P => ((P ^ Q) => Q

Cannot close P ^ Q: not an assumption. You need to assume P ^ Q (along with a vacuous assumption P) and deduce Q by ^E.

Originally Posted by Lepzed

Furthermore I'm trying to prove (P => Q) => ((P ^ R) => (Q ^ R)) and having some trouble introducing the R, my current train of thought leaves me with an assumption i can't get rid of.

Code:

1, H:       P => Q
2, H:           P
3, =>E 1,2:         Q
4, H:                    R
5, ^I 2,4:                    P ^ R
6, ^I 3,4:                    Q ^ R
7, =>I 5,6:              (P ^ R) => (Q ^ R)
8, =>I 1,7: (P => Q) => ((P ^ R) => (Q ^ R))

As you see, I'm left out with an assumption too many. I guess I'm introducing the R (4) incorrect, any pointers?

Same mistake: you need to assume P ^ R instead of proving it. From it you get P and (using another assumption P => Q) Q. From P ^ R you also get R and hence Q ^ R.

Hmm, I see. Is there some sort of 'algorithm' I should follow when trying to solve questions like this?
Currently I try to work from bottom to top and fill in blanks when needed and apparantly I'm not quite sure what's allowed to be used as a hypotheses..

At least when the formula has only conjunctions and implications and its proof uses only the rules for those connectives (no reasoning by contradiction, for example), then the principle is pretty simple. Each branch in the shortest derivation starts with a series of elimination rules and ends with a series of introduction rules. So, going bottom up, you introduce all assumptions and split all conjunctions, and then see what you can get with the assumptions you collected.

After reading your answer regarding

Code:

1, H:       P
2, H:           Q
3, ^I 1,2:          P ^ Q
4, ^E 3:            Q
5, =>I 3,4:    (P ^ Q) => Q
6, =>I 1,5: P => ((P ^ Q) => Q

Cannot close P ^ Q: not an assumption. You need to assume P ^ Q (along with a vacuous assumption P) and deduce Q by ^E.

I'm not sure if I follow, instead of assuming Q, I should've assumed P ^ Q as follows:

Code:

1, H:       P
2, H:           P ^ Q
3, ^E 2:            Q
4, =>I 2,3:    (P ^ Q) => Q
5, =>I 1,4: P => ((P ^ Q) => Q

Is this correct? If so then I think I understand this part now.
I'm going to spend the evening practicing (at work now, 40 hour job next to uni is hard work, especially if you cant attend lectures because of it :<) and then ND with negation, disjunction and quantifiers is next Thanks again!

Originally Posted by Lepzed

Code:

1, H:       P
2, H:           P ^ Q
3, ^E 2:            Q
4, =>I 2,3:    (P ^ Q) => Q
5, =>I 1,4: P => ((P ^ Q) => Q

Yes, this is correct.

I can't help but trying to work on (P => Q) => ((P ^ R) => (Q ^ R)) during lunch break

Code:

1, H:       P => Q
2, H:           P ^ R
3, ^E 2:            P   
4, =>E 1,3:         Q
5, ^E 2:            R
6, ^I 4,5:          Q ^ R 
7, =>I 2,6:    (P ^ R) => (Q ^ R)
8, =>I 1,7: (P => Q) => ((P ^ R) => (Q ^ R))

I'm having some doubts about the long list of conclusions starting at 3, is this allowed?

Yes, you are absolutely right. Good work.

I've been working on some examples and exercises, and I think I'm getting there, there are however 4 exercises I'm having some difficulties with, I was hoping I could get soms feedback on them, since they're a bit harder than the rest. I think I've done 2 of them reasonably well, the other 2 not so much Still, just implication and conjunction.

1) (P => Q) => (P => (P ^ Q))

Code:

1, H:        P => Q
2, H:             P
3, => E 1,2:           Q
4, ^I 2,3:             P ^ Q
5, =>I 2,4:       P => (P ^ Q)
6, =>I 1,5: (P => Q) => (P => (P ^ Q))

Seems sound, right?

2) ((P => Q) ^ (R => S)) => ((P ^ R) => (Q ^ S))

Code:

 1, H:           (P => Q)  ^ (R => S)
 2, H:                (P ^ R)
 3, ^E 1:                   P => Q
 4, ^E 1:                   R => S
 5, ^E 2:                   P
 6, ^E 2:                   R
 7, =>E 3,5:                Q                
 8, =>E 4,6:                S
 9, ^I 5,6:                 P ^ R
10, ^I 7,8:                 Q ^ S
11, =>I 9, 10:             (P ^ R) => (Q ^ S)
12, =>I 1, 11: ((P => Q) ^ (R => S)) => ((P ^ R) => (Q ^ S))

I think I did this okay, I have no idea how to do this otherwise.

3) (P => Q) => ((R => (P => Q)) ^ ((P ^ R) => Q))

Code:

 1, H:         P => Q
 2, H:              P ^ R
 3, ^E 2:               P
 4, ^E 2:               R
 5, =>E 1,3:            Q
 6, =>I 4,1:            R => (P = > Q)
 7, H:              P ^ R
 8, ^E 7:               P
 9, =>E 1,8             Q
10, =>I 7,9:        (P ^ R) => Q
11, ^I 6, 10: (R => (P => Q)) ^ ((P ^ R) => Q)
12, =>I 1, 11: (P => Q) => ((R => (P => Q)) ^ ((P ^ R) => Q))

This one I'm not so sure about. Seems a bit redundant to assume P ^ Q twice for example, but I'm not sure how else I can get to the ^I I need to connect the two parts.

And lastly:
4) (P => (Q => R)) => ((P => Q) => (P => R))
And this one I get stuck, doing too many assumptions.
I tried the following

Code:

 1, H:         P => (Q => R)
 2, H:              P ^ Q
 3, ^E 2:               P
 4, ^E 2:               Q
 5, =>I 2,3:        P => Q
 6, H:              P ^ Q
 7, ^E 6:               P
 8, ^E 6                Q
 9, =>E 1,7:            Q => R
10, =>E 8,9:            R
11, =>I 7, 10:       P => R

Im stuck here, again, assuming the same thing twice just seems wrong. I can't really wrap my head around it, any tips? I seem to miss an assumption as well, but if I would assume P, well think im being twice as redundant :P May be it's super easy, but I think this is rather harder than the other exercises hehe

Originally Posted by Lepzed

1) (P => Q) => (P => (P ^ Q))

Code:

1, H:        P => Q
2, H:             P
3, => E 1,2:           Q
4, ^I 2,3:             P ^ Q
5, =>I 2,4:       P => (P ^ Q)
6, =>I 1,5: (P => Q) => (P => (P ^ Q))

Correct.

Originally Posted by Lepzed

2) ((P => Q) ^ (R => S)) => ((P ^ R) => (Q ^ S))

Code:

 1, H:           (P => Q)  ^ (R => S)
 2, H:                (P ^ R)
 3, ^E 1:                   P => Q
 4, ^E 1:                   R => S
 5, ^E 2:                   P
 6, ^E 2:                   R
 7, =>E 3,5:                Q                
 8, =>E 4,6:                S
 9, ^I 5,6:                 P ^ R
10, ^I 7,8:                 Q ^ S
11, =>I 9, 10:             (P ^ R) => (Q ^ S)
12, =>I 1, 11: ((P => Q) ^ (R => S)) => ((P ^ R) => (Q ^ S))

Line 9 is not needed, and line 11 should close line 2.

Originally Posted by Lepzed

3) (P => Q) => ((R => (P => Q)) ^ ((P ^ R) => Q))

Code:

 1, H:         P => Q
 2, H:              P ^ R
 3, ^E 2:               P
 4, ^E 2:               R
 5, =>E 1,3:            Q
 6, =>I 4,1:            R => (P = > Q)
 7, H:              P ^ R
 8, ^E 7:               P
 9, =>E 1,8             Q
10, =>I 7,9:        (P ^ R) => Q
11, ^I 6, 10: (R => (P => Q)) ^ ((P ^ R) => Q)
12, =>I 1, 11: (P => Q) => ((R => (P => Q)) ^ ((P ^ R) => Q))

Line 6 closes line 4, which is not an assumption. Should be like this.

Code:

 1, H:        P => Q
 2, H:              R
 3, =>I 1,2:        R => (P => Q)
 4, H:              P ^ R
 5, ^E 4:               P
 6, =>E 1,5:            Q
 7, =>I 4,6:        P ^ R => Q
 8, ^I 3, 7:        (R => (P => Q)) ^ ((P ^ R) => Q)
 9, =>I 1, 8: (P => Q) => ((R => (P => Q)) ^ ((P ^ R) => Q))

I am not sure if the hypothesis 1 should be repeated between lines 2 and 3 (probably not). In a tree-form derivation, the hypothesis P => Q occurs twice, but in Fitch style it should probably be declared just once.

Originally Posted by Lepzed

4) (P => (Q => R)) => ((P => Q) => (P => R))
And this one I get stuck, doing too many assumptions.
I tried the following

Code:

 1, H:         P => (Q => R)
 2, H:              P ^ Q
 3, ^E 2:               P
 4, ^E 2:               Q
 5, =>I 2,3:        P => Q
 6, H:              P ^ Q
 7, ^E 6:               P
 8, ^E 6                Q
 9, =>E 1,7:            Q => R
10, =>E 8,9:            R
11, =>I 7, 10:       P => R

In the shortest derivation, all formulas should be subformulas of open assumptions or of the conclusion. (If I remember correctly, this is true when double-negation elimination is not used.) So, P ^ Q is not needed; one can do with implication only.

There are three levels. You assume P => (Q => R)), (P => Q), and P, and then you derive in turn:

Q => R
Q
R

and close everything.

Also, note that rule #8 in this sticky thread says not to ask more than two questions in one thread.