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:

enter image description here

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?


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

enter image description here

  • $\begingroup$ As mentioned in the answer 'double negation elimination' is not available in JAPE, I guess it must be replaced with some other steps. $\endgroup$ – 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].

| cite | improve this answer | |
  • $\begingroup$ I know the double negation elimination rule, the point is that its not available in JAPE. $\endgroup$ – Kris Oct 14 '15 at 11:06
  • $\begingroup$ 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. $\endgroup$ – Kris Oct 14 '15 at 12:12
  • $\begingroup$ 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. $\endgroup$ – Kris Oct 14 '15 at 14:12

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.