# Proof by Fitch System

I need to make a proof for the premise

((p ⇒ q) ⇒ p) ⇒ p

Using only Fitch System. The problem is that I have been trying for at least a week, but I just can't figure it out a way to solve the problem. I tried by assuming (p ⇒ q) ⇒ p and then proving that ~p implies a contradiction, but it's a dead end for me.

I would really apreciate any suggestion.

PD: Sorry for the bad english, It's not my native lenguage.

PD2: I can't use Natural Deduction. I can only use this rules: http://logic.stanford.edu/intrologic/glossary/fitch_system.html

Sorry for the double post, but a tag of "already answered" confused me. The other question is similar, but it makes use of natural deduction, while I can't use natural deduction.

• Your Fitch system is quite similar to the natural deduction, so you can get a Fitch-style proof of the Pierce's law if you change $\bot$s to negation. – Hanul Jeon Jan 26 '17 at 7:32
• Thank you a lot, you're right. – Emilio Ocampo Jan 26 '17 at 7:46
• You will have to use double negation elimination because pierce's law is well known to not be constructively valid. – DanielV Jan 26 '17 at 21:05

Since you have no premises, but only a goal, let's focus on the goal and think about how you can get to something like that. Well, the main connective is a conditional ($\rightarrow$), so the strategy is probably to use $\rightarrow \: Intro$:

OK, so now your (new) goal is to get to $P$, using $(P \rightarrow Q) \rightarrow P$

Well, there is still very little you can do with $(P \rightarrow Q) \rightarrow P$ by itself: $\rightarrow Elim$ requires you to have the antecedent $P \rightarrow Q$, which you don't have. So, let's once again focus on the goal ($P$), and think about how we can prove something like that.

Now, here is a trick to remember: in order to prove an atomic statement like $P$, one strategy is to try and do a proof by contradiction. Here is how that works in Fitch:

OK, so now the (newest) goal is to prove $\bot$ using $(P \rightarrow Q) \rightarrow P$ and $\neg P$. OK, I won't show in detail how to do that, because at this point I want you to just look at the proof skeleton or proof plan that we have right now: do yourself a favor, and make sure to come up with such a proof plan for whatever proof you are working on! ... if your proof plan is good, the details will often pretty much fall out naturally.

For this particular proof, the rest isn't trivial, but it isn't hard either. Just think: "how do I get a $\bot$ given what I have? Well, that requires some statement and its negation. Hmm, I already have a negation $\neg P$. OK, so if I can get to $P$, I would be there. How can I get $P$? Oh, I have a conditional $(P \rightarrow Q) \rightarrow P$ whose consequent is $P$, so if only I could prove the antecedent $P \rightarrow Q$ I would be there. OK, how can I do that, presumably using $\neg P$?"

Well, I'll leave you to that. Good luck, and remember to rely on these proof skeletons!!

When you have the law of the excluded middle at your disposal (or in your case, double negation + this proof), the easy way to prove all of these propositional logic questions is:

• for each variable $v_1 \dots v_n$, infer (or prove) $v_k \lor \lnot v_k$
• for each of the $2^n$ combinations of variables being negated or not, prove the theorem
• combine all cases using or elimination

So for your problem that looks like

$$\begin{array} {rll} (1) & P \lor \lnot P & \text{Proven using the above links} \\ (2) & Q \lor \lnot Q & \text{Proven using the above links} \\ \\ (3) & \quad \quad P & \text{Assumption} \\ & \quad \quad \vdots \\ (4) & \quad \quad ((P \Rightarrow Q) \Rightarrow P) \Rightarrow P & \text{Fill in the dots} \\ \\ (5) & \quad \quad \lnot P & \text{Assumption} \\ (6) & \quad \quad \quad \quad Q & \text{Assumption} \\ & \quad \quad \quad \quad \vdots \\ (7) & \quad \quad \quad \quad ((P \Rightarrow Q) \Rightarrow P) \Rightarrow P & \text{Fill in the dots} \\ \\ (8) & \quad \quad \quad \quad \lnot Q & \text{Assumption} \\ & \quad \quad \quad \quad \vdots \\ (9) & \quad \quad \quad \quad ((P \Rightarrow Q) \Rightarrow P) \Rightarrow P & \text{Fill in the dots} \\ \\ (10) & \quad \quad ((P \Rightarrow Q) \Rightarrow P) \Rightarrow P & \text{Or Elimination of 2, 6 - 7, 8 - 9} \\ (11) & ((P \Rightarrow Q) \Rightarrow P) \Rightarrow P & \text{Or Elimination of 1, 3 - 4, 5 - 10} \\ \end{array}$$

Establishing 9 can be a bit tricky, but the key is to notice that $\lnot P$, $\lnot Q$, and $(P \Rightarrow Q) \Rightarrow P$ is inconsistent so you can establish anything from it, including $P$.

Establishing 7 is straightforward, since if $Q$ is true, then $(P \Rightarrow Q)$ is true, then $(P \Rightarrow Q) \Rightarrow P$ establishes $P$.