# JAPE double negation handling

I'm trying to prove a simple conjecture using JAPE application. There must be some 'magic trick' in JAPE to get rid of double negation statements but I have no idea how to handle it properly. The point where it all makes sens to me is:

I have started from line 5 and then going backwards I did implication intro twice. Could anyone (who knows JAPE) tell me how to get --E to E and from --F to F so the implication E -> F holds?

EDIT:

After Mauro's suggestions I'm at the point were I have a contradiction but JAPE still wants smth more in it:

• As mentioned in the answer 'double negation elimination' is not available in JAPE, I guess it must be replaced with some other steps. – Kris Oct 14 '15 at 11:09

The 'magic trick' in the Natural Deduction proof is to use Double Negation elimination rule :

$\lnot \lnot \varphi \vdash \varphi$.

If not available, you must have a "contradiction" rules; see : Richard Bornat, Proof and Disproof in Formal Logic : An Introduction for Programmers (2005), that is a reference for Jape software, page 43 :

if $\Gamma \vdash \bot$, then $\Gamma \vdash \varphi$ --- contradiction (constructive)

and :

if $\Gamma, \lnot \varphi \vdash \bot$, then $\Gamma \vdash \varphi$ --- contradiction (classical).

In this case, they are not necessary :

The derivation is :

1) $E \to F$ --- premise

2) $\lnot \lnot E$ --- assumed [a]

3) $\lnot F$ --- assumed [b]

4) $E$ --- assumed [c]

5) $F$ --- from 1) and 4) by $\to$-elimination

6) $\bot$ --- from 3) and 5) by $\lnot$-elimination

7) $\lnot E$ --- from 4) and 6) by $\lnot$-intro, discharging [c]

8) $\bot$ from 2) and 7) by $\lnot$-elim

9) $\lnot \lnot F$ --- from 3) and 8) by $\lnot$-intro, discharging [b]

10) $\lnot \lnot E \to \lnot \lnot F$ --- from 2) and 9) by $\to$-intro, discharging [a].

• I know the double negation elimination rule, the point is that its not available in JAPE. – Kris Oct 14 '15 at 11:06
• pls see my edit where I've posted new image, it looks like JAPE has some peculiar own rules to solve this and even if your solution looks ok to me I cannot translate it directly into JAPE interface/commands. – Kris Oct 14 '15 at 12:12
• Hey @Mauro, still no luck, I really appreciate your efforts, the problem is with putting your proof to JAPE itself, it just cannot be done in a form you posted. – Kris Oct 14 '15 at 14:12