4

Given the following axioms $$\begin{aligned}&1. p\Rightarrow (q\Rightarrow p)\\&2. [p\Rightarrow (q\Rightarrow r )] \Rightarrow [(p\Rightarrow q)\Rightarrow (p\Rightarrow r)]\\&3. \neg\neg p \Rightarrow p \end{aligned}$$ and the deduction rule of modus ponens, I want to prove that $$p\vdash \neg\neg p$$ and should therefore use the Deduction Theorem.

Has anyone a hint how to start?

Peter
  • 3,383
  • This isnt true at all... it depends about what logic are you talking about. Exist a lot of different negations in logic. – Masacroso Sep 16 '14 at 06:28

3 Answers3

3

I will outline the basic idea of the proof, but you can formalize it. We set, $q\equiv(\neg \neg p \to p)$ and, $r \equiv (\neg \neg p)$ and let $p \equiv p$. Then, by axiom 2, we have that

$$[p \to (q \to r)] \to [(p \to q)\to (p \to r)]$$

is equivalent to

$$[p \to ((\neg \neg p \to p) \to (\neg \neg p))] \to [(p \to (\neg \neg p \to p))\to (p \to (\neg \neg p))]$$

On the LHS, since we assumed $p$, we now have $(\neg \neg p \to p) \to (\neg \neg p)$. By axiom 1, this also holds. Therefore, the RHS of the sentence must also hold.

Now, we consider the RHS. The LHS of the RHS holds by axiom 1 as well. Hence, we then get the RHS of the RHS must hold, which is $(p \to \neg \neg p)$, i.e. the statement we are trying to prove.

Note: If this post is too confusing, I will be glad to rewrite it in the morning.

Kyle Gannon
  • 6,363
  • Thanks for your answer, I also thought of the same starting point but got stuck as I don't see how to get the following: ${p,q}\vdash p\Rightarrow q$. But now I see that this follows from axiom 1. Thanks! – Peter Sep 15 '14 at 09:37
  • @Peter: This stuff is really tricky. I remember doing problems similar to this and getting stuck all the time. It just takes practice and patience. You're Welcome! – Kyle Gannon Sep 15 '14 at 09:41
  • One question regarding this topic: In another problem, I have to show that $\perp \Rightarrow p$. I don't know how to implement $\perp$ in the syntactic deduction. I only know that $v(\perp) = 0$ but I am not allowed to use that. – Peter Sep 15 '14 at 10:04
  • @KyleGannon by axiom 1 you have $\neg \neg p \to (p\to \neg \neg p)$ – Snufsan Sep 16 '14 at 08:26
  • I think that the first part does not work. In order to "detach" $(¬¬p→p)→(¬¬p)$ from Axiom 1, you have to assume $¬¬p$, and not $p$. – Mauro ALLEGRANZA Sep 16 '14 at 08:34
  • 2
    @MauroALLEGRANZA: Sorry for the delay, I have been travelling. I will respond to your comments tomorrow. – Kyle Gannon Sep 16 '14 at 08:54
  • @Snufsan: (as well as yours. See ^) – Kyle Gannon Sep 16 '14 at 08:57
3

To solve questions like these in general, it may help to reverse engineer the proof. Suppose we had a proof of $\vdash p \Rightarrow \lnot \lnot p$. There must be a first such occurrence of $p \Rightarrow \lnot \lnot p$ within the proof.

Notice that this first such occurrence cannot be in the conclusion of a modus ponens application. This is because if modus ponens was applied on $\{A, A \Rightarrow B\}$ to infer the conclusion $B$ and if the $B$ contains an occurrence of $p \Rightarrow \lnot \lnot p$, then another occurrence must also occur in the RHS of the premise $A \Rightarrow B$.

Therefore, the first such occurrence of $p \Rightarrow \lnot \lnot p$ must be the rightmost subexpression from an axiom. Here are the forms of all viable candidates:

  • From the first axiom schema $A \Rightarrow (B \Rightarrow A)$, they are:
    1. $\lnot \lnot p \Rightarrow (p \Rightarrow \lnot \lnot p)$
    2. $(p \Rightarrow \lnot \lnot ~p) \Rightarrow (B \Rightarrow (p \Rightarrow \lnot \lnot ~p))$
  • From the second axiom schema $[A \Rightarrow (B \Rightarrow C)] \Rightarrow [(A \Rightarrow B) \Rightarrow (A \Rightarrow C)]$, they are:
    1. $[p \Rightarrow (B \Rightarrow \lnot \lnot p)] \Rightarrow [(p \Rightarrow B) \Rightarrow (p \Rightarrow \lnot \lnot p)]$
    2. $[A \Rightarrow (B \Rightarrow (p \Rightarrow \lnot \lnot p))] \Rightarrow [(A \Rightarrow B) \Rightarrow (A \Rightarrow (p \Rightarrow \lnot \lnot p))]$
  • From the third axiom schema $\lnot \lnot A \Rightarrow A$, it is:
    1. $\lnot \lnot (p \Rightarrow \lnot \lnot ~p) \Rightarrow (p \Rightarrow \lnot \lnot ~p)$

(Note: For the sake of clarity, I used the letters $A$, $B$, and $C$ to denote arbitrary formulas.)

Now, which one of these are actually useful to include in the proof? Since the premise of (1) is logically invalid, it cannot be that. Since using modus ponens on (2) would require that $p \Rightarrow \lnot \lnot p$ was a premise, it cannot be that.

Since the premise of (4) and the premise of (5) both include $p \Rightarrow \lnot \lnot p$ as a subexpression, I would not recommend trying those candidates first.

Thus, as a hint, try to include candidate (3).

Moh
  • 461
3

Here is the proof.

We can prove it also with a "Natural Deduction-like" proof, using the definition :

$\lnot p := p \rightarrow \bot$.

Axioms 1 and 2 are enough to prove : $\vdash \varphi \rightarrow \varphi$ as well as the Deduction Theorem.

With the above definition, the proof is quite simple :

i) $p$ --- assumed

ii) $\lnot p$ --- assumed

iii) $p \rightarrow \bot$ --- from ii) by definition of $\lnot$

iv) $\bot$ --- from i) and iii) by modus ponens

v) $\lnot \lnot p$ --- from ii) and iv) by DT and definition of $\lnot$, "discharging" assumption ii).

$\vdash p \rightarrow \lnot \lnot p$ --- from i) and v) by DT.

Note

This poof does not use Axiom 3, as expected, due to the fact that $p \rightarrow \lnot \lnot p$ is intuitionistically valid, while Axiom 3 : $\lnot \lnot p \rightarrow p$ is not.

Community
  • 1
Mauro ALLEGRANZA
  • 94,169