I was asked to prove $\vdash p\to\neg\neg p$ in this system.

$(\mathcal A_1)\vdash p\to(q\to p)$
$(\mathcal A_2)\vdash (p\to(q\to r))\to((p\to q)\to (p\to r))$
$(\mathcal A_3)\vdash \neg\neg p\to p$

I have tried to use axiom 2 and find a proper proposition $x$ such that $\vdash (p\to(x\to\neg\neg p)) \to ((p\to x)\to (p\to \neg\neg p))$ holds, but I couldn't find one.

Any help would be appreciated.

Note from a comment on a deleted answer: there is also a rule that $\lnot P$ may be replaced by $P \to \bot$.

  • $\begingroup$ For a system like this, trying to solve individual propositional expressions is like trying to build a house with a blindfold on. You should first learn truth tables, then translate the process of proving something with truth tables into the language of this logic. This is usually hidden as a "proof of completeness". Figuring out how to solve every propositional expression is much much easier than figuring out how to solve 1 propositional expression. $\endgroup$ – DanielV May 19 at 3:14
  • $\begingroup$ If modus ponens is the only rule of inference, this isn't possible. $\endgroup$ – Doug Spoonwood May 20 at 14:21

Okay.. I've known how to solve this — by employing the Deduction Theorem:

If $A$ is a set of propositions, $p$, $q$ are propositions, then $A \vdash p\to q$ is equivalent to $A \cup \{p\} \vdash q$.


$$\{p,\neg p\}\vdash p\tag{1; assumed}$$ $$\{p,\neg p\}\vdash \neg p=(p\to\bot)\tag{2; assumed}$$ $$\{p,\neg p\}\vdash \bot\quad\tag{3; MP,1,2}$$ $$\{p\}\vdash (\neg p\to \bot)=\neg\neg p\tag{4; DT}$$ $$\vdash (p\to \neg\neg p)\tag{5; DT}$$

  • $\begingroup$ This is correct. You might want to replace F with $\bot$ for clarity since F looks like a propositional variable. Also you can use \tag to name expressions. $\endgroup$ – DanielV May 20 at 5:15

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.