I'm trying to prove $\vdash((p\rightarrow q)\rightarrow p)\rightarrow p$.

The best attempt I can come up with is as follows:

  1. $((p\to q)\to p)$ Assumption
  2. $p\to q$ Assumption
  3. $p$ $\to$ Elimination 1,2
  4. $((p\to q)\to p)\to p$ $\to$ Introduction 1,2-3

But I'm sure it's completely invalid as the ways the implications are eliminated and introduced don't match the way they are in other examples I've seen.

Also, am I correct in saying that this is a tautology? Or is it a theorem? I get the two confused.


I'll start answering from the bottom.

The mathematical object $((p\rightarrow q)\rightarrow p)\rightarrow p$ is both a tautology and a theorem. In principle they are different concepts (check the definitions), but the completeness theorem for propositional calculus tells you that every tautology is a theorem and vice-versa.

As for the proof, what you're doing doesn't work. The second assumption isn't wrong per se, but it's odd. The very last step is wrong because the $p$ you inferred on the third step is 'inside' yet another assumption, it's not at the same level as the first assumption which is what you desire.

Here's an idea for proving it. The details will depend on which rules you have available. Start by assuming $(p\to q)\to p$. Next, hoping to find a contradiction, suppose $\color{red}{\neg p}$ holds. From this new assumption prove that $p\to q$ holds, then eliminate $\to$ in $(p\to q)\to p$ and get $p$. Careful, this $p$ you infer here is not at the appropriate level. Here you get a contradiction and are able to deduce $\neg \neg p$ from the red assumption.

  • $\begingroup$ Im lost as to how prove that $p\rightarrow q$ holds after supposing $\neg p$, as $(p \rightarrow q) \rightarrow p, \neg p \vdash \neg(p\rightarrow q)$ by modus tollens right? $\endgroup$ – Charles Del Lar Feb 23 '15 at 11:18
  • $\begingroup$ @CharlesDelLar If MT is one of the available rules, then that's right, that's your contradiction right there and you don't need to go further. What I had in mind was the following. To prove $p\to q$, start by assuming $p$. Since you have $\neg p$, you also get a contradiction, from a contradiction you can derive anything, in particular you can infer $q$, therefore $p\to q$. $\endgroup$ – Git Gud Feb 23 '15 at 11:23
  • $\begingroup$ My initial assumption is $(p \rightarrow q) \rightarrow p$. So I'm going to assume $\neg p$ then inside that assumption I'm going to assume $p$ to create a contradiction against $\neg p$ which allows me to infer $q$. Then outside the assumption of $p$ I can say $p \rightarrow q$ which by the initial assumption implies $p$ - this contradicts my assumption of $\neg p$ providing $\neg \neg p$. Then a simple finish. Does this seem correct? I'm not familiar with the fact you can derive anything from a contradiction, I'll read up on it. $\endgroup$ – Charles Del Lar Feb 23 '15 at 12:03
  • $\begingroup$ That is correct. If you're not familiar with that rule, perhaps you're not supposed to use it. Where does this question come from? Is it from a book or class? In either case, check what rules you have available at the moment. Different formal systems use different rules. I can give a more exact answer once you state exactly what rules you have. If you decide to do this, add this information directly to the question and let me know about it in a comment. $\endgroup$ – Git Gud Feb 23 '15 at 12:07
  • $\begingroup$ It's from a class. I found the rule in my notes, "Ex Falso Quodlibet" scribbled next to it. So I guess I'm finished here, thanks for your help! $\endgroup$ – Charles Del Lar Feb 23 '15 at 12:22

Here's the proof you are looking for. You can find more information here.

((a->b) -> a )-> b proof

This proof was constructed using the Panda Proof assistant.

Or in Fitch format: $$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{}{\fitch{~~1.~~(p\to q)\to p\hspace{8ex}:\text{assumption}}{\fitch{~~2.~~\lnot p\hspace{8ex}:\text{assumption}}{\fitch{~~3.~~p\hspace{8ex}:\text{assumption}}{~~4.~~p\land\lnot p\hspace{8ex}:\text{conjunction introduction}\\~~5.~~q\hspace{8ex}:\text{explosion (ex falso quodlibet}}\\~~6.~~p\to q\hspace{8ex}:\text{conditional introduction}\\~~7.~~p\hspace{8ex}:\text{conditional elimination (modus ponens)}\\~~8.~~p\land\lnot p\hspace{8ex}:\text{conjunction introduction}}\\~~9.~~\lnot\lnot p\hspace{8ex}:\text{negation introduction}\\10.~~p\hspace{8ex}:\text{double negation elimination}}\\11.~~((p\to q)\to p)\to p\hspace{8ex}:\text{conditional introduction}}$$


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.