Fitch System Exercise in Propositional Logic

It's a lot of conditionals, but the main thing that you have to notice is that you want to assume everything on the left of the =>, then show that assuming P=>Q then assuming P allows you to derive P=>R, that then means since you derived P=>R from assuming P=>Q you get (P=>Q) => (P=>R).

Chain of implication proofs generally proceed by assuming things on the left, then leveraging the assumption of the implications to get the things on the right, then since you assumed the things on the left they imply the things on the right.

Maybe it's easier to see why this works if you substitute in P is 'this shape is a cube', Q is 'this shape is a cuboid' and R is 'this shape has at least 2 equal sides'. This set of P,Q,R satisfies P=>Q=>R

It's true that if you have a cube (P), then (=>) it's also a cuboid (Q) (this is P=>Q). So (=>) it's true that you have at least two equal sides (R) since you have a cuboid (P) (this is P=>R).

Another way of thinking about it is that implications are machines that take inputs and give you outputs. If P is true on the left as well as (P=>Q =>R), that means that if you have P and P=>Q, you get Q, but if you have P=>Q, you get P=>R since Q=>R.

All right; so, I assumed what was on the left:

1 P => Q => R Assumption
2 P=>Q Assumption
3 P Assumption
4 Q Implication Elimination 2, 3
5 R Assumption
6 P=>R Implication Introduction 3, 5
7 P => Q => R => R Implication Introduction 2, 6
8 ( P => ( Q => R ) ) => (( P => Q ) => ( P => R ) ) Implication Introduction 1, 7

Is this correct? I suspect the Assumption of R in 5 to be incorrect. I thought about deriving Q => R by applying Implication Elimination on the Premise 1 and the Assumption 3 and then by proving R, but I'm not sure that it's possible.
And, by the way, 2 to 6 is a subproof, and 3 to 5 a subproof to that subproof

Line 6 looks wrong. It looks like you are trying to close a subproof commenced on line 3 but you can't do that until you've closed the subproof opened by the assumption on line 5. You can't close a subproof while any subproofs of it are still open.

You can fix that by deducing R on line 5 (maybe needing one or two additional lines), using lines 1, 3 and 4.

1 P => Q => R Assumption
2 P => Q Assumption
3 P Assumption
4 Q Implication Elimination 2, 3
5 Q => R Implication Elimination 1, 3
6 R Implication Elimination 5, 4
7 P=>R Implication Introduction 3, 6
8 P => Q => R => R Implication Introduction 2, 7
9 ( P => ( Q => R ) ) => (( P => Q ) => ( P => R ) ) Implication Introduction 1, 8

In this case, line 2 to 7 is a subproof, and 3 to 6 a subproof of that subproof. I deduced R on line 6 after deriving Q => R on line 5. I hadn't done it before because I thought that I could not apply a rule of inference on elements that were at two removes from each other so to speak. To deduce Q => R in line 5, one has to apply Implication Elimination on 1 and 3. What bothered me is that 3 was a subproof of a subproof of the super-proof in which line 1 is nested, and I thought that this made it impossible to apply the rule; I thought that the two elements on which one applies the rule of inference had to be no more than at one remove from each other as it were. I don't know where I got that idea.
Reply to andrewk And how exactly does one ‘‘close’’ a subproof? Does that mean that it can't end with an assumption?

Can we exit a subproof only by using Implication Introduction?

Reply to Rayan You leave a subproof in Ficht system by discharging the assumption that began it. You can discharge assumptions by negating them (which you can do if the assumption leads to a contradiction) or by making them the antecedent of an implication introduction.

Reply to Rayan This looks correct, except that:

- on line 1 you have written P => Q => R but it should be P => (Q => R)
- on line 8 you have written P => Q => R => R but it should be (P => Q) => (P => R)