Jape Notes

This is a rough draft in progress.
Some of the information here may be incomplete, inaccurate, or badly worded.

Jape is a software tool for creating proofs and disproofs, by default using natural deduction. The program was designed by Richard Bornat in collaboration with Bernard Sufrin. Bornat notes:

Jape is a lightweight, uncommitted, transparent proof calculator. It’s designed to present an excellent graphical interface and a very short and shallow ‘learning curve’ to all its users, whether novices learning how to make formal proofs or experts — logicians, teachers, sofware engineers, practitioners of any kind — describing inference systems.¹

The name “Jape” is an acronym: “Just Another Proof Editor,” although that's not mentioned in the more recent documentation (perhaps because proof “calculator” sounds a bit different from a proof “editor”).

The prime purpose of this article is so I can keep track of what I'm learning. I find it useful to take notes when trying to learn something even if the existing tutorials are comprehensive. I'll tidy these notes up as I work through the material. I'm not intending to overlap with existing tutorials.

Help and Guidance

Jape.org.uk vs. Other Pages

The main page for Jape is run by Richard Bornat at jape.org.uk. He also mentions Jape with some links on his Middlesex University Web page.

Book vs. Manual

Bornat's book, Proof and Disproof in Formal Logic: An introduction for programmers (Oxford University Press, 2005), incorporates Jape into an explanation of natural deduction, particularly in the field of computer science:

This book concentrates on practical skills: making proofs and disproofs of particular logical claims. The logic it uses, called Natural Deduction, is very small and very simple. Working with it helps you see how large mathematical universes can be built on small foundations. It is a striking example of how it is possible to build useful things, even apparently meaningful things, on top of a meaningless formal system. It teaches you how to focus on syntactic reasoning, and turns you away from the semantic reasoning that dominates mathematics outside computer science. (“ReadMe.Preface,” p. v.)

A just-the-basics user's manual is available as a downloadable PDF. It concentrates on quickly getting up to speed using Jape to explore natural deduction, “Natural Deduction Proof and Disproof in Jape” (2005):

This manual is a how-to for Jape and my Natural Deduction encoding. Earlier versions contained a good deal of logic teaching. That’s been dropped, since now there’s a book (Logic for Programmers, OUP) which says it all a good deal better. You will learn about logic by playing with Jape, so I suppose there’s still teaching in there. (Preface, p. 3)

Chapter five of the manual is particularly useful, providing a brief summary of the intro and elim steps. (Bornat confirms that in section 5.1, p. 23, there are two typos: for “A→B hypothesis” read “A∧B hypothesis,” and for “use ‘→ intro’ ” read “use ‘∧ intro.’ ”)

This and other manuals are available from jape.org.uk.

Jape vs. Natural Deduction

Jape can use any number of theories, including the rules of natural deduction (Bornat capitalizes both words). However, Jape can be used with other systems of logic. See Bornat's “Roll your own Jape logic: Encoding logics for the Jape proof calculator.”

Proof vs. Disproof

Jape in its natural deduction mode can perform proofs and disproofs. The information presented here (so far) is restricted to the proofs.

Notation and Presentation

Rules vs. Claims

As Bornat notes (on p. 22 of his Proof and Disproof): “in inference rules and definitions I use A, B, C, and P(i); in claims I use E, F, G, j, k, R(…), S(…) and T(…).”

So a rule that introduces ^ to A and B in order to produce A^B could be used for an infinite number of various claims including:

• E and F to produce E∧F
• E→F and F→E to produce (E→F) ∧ (F→E)
• E and ¬E to produce E∧¬E.

(I use bold not italics as it shows up better on the screen. Jape also avoids italics in its screen appearance.)

Backward vs. Forward

Backward vs. Forward Menu Items

Here we see two screenshots of menu choices.

The menu headings backward and forward describe the initial direction of your step:

• Going backward from one part of the proof to an earlier part of the proof
• Going forward from one part of the proof to a later part of the proof.

Preferred vs. Other Steps

Under each menu item two horizontal lines group together the first eight choices—considered generally useful—from the later options—which should be used with more caution.

Making another point, Bornat suggests trying backward steps first, despite the novice's tendency to both read and do proofs forward.

Intro/Elim vs. Other Preferred Steps

All preferred backward steps are intro steps except for the last: truth.

All preferred forward steps are elim steps except for the last: constructive contradiction (called contra (constructive) in the menu).

In the table below I use the shorthand “we” to refer to the user and the software together, as the software automatically does many of the actions described for each step.

CHOOSE FROM THESE STEPS IF POSSIBLE
Step	Backward Intro	Forward Elim
∧	∧ intro: We move backwards from A∧B to A and B. We introduce ∧ to justify A∧B.	∧ elim: We eliminate ∧ from A∧B to justify A or B (you choose).
→	→ intro: We move backwards from A→B to an assumption box with assumption A and conclusion B. We introduce → to justify A→B.	→ elim: If we have A then we eliminate → from A→B to justify B.
∨	∨ intro: We move backwards from A∨B to either A or B (you choose). We introduce ∨ to justify A∨B.	∨ elim: We eliminate ∨ from A∨B and choose a conclusion C. We put A in one assumption box and B in another (both A and B are assumptions). We conclude C in both assumption boxes. We then justify our original C as following from A∨B. (This is proof by cases.)
¬	¬ intro: We move backwards from ¬A to an assumption box with assumption A and conclusion ⊥ (contradiction). We introduce ¬ to justify ¬A.	¬ elim: We eliminate ¬ from ¬A in order to add A to a later line. (You can insert A into an assumption box by clicking on the box's conclusion.) This step may or may not justify any line right away.
Step	Backward Intro	Forward Elim
∀	∀ intro: We move backwards from ∀x.P(x) to an assumption box with assumption actual i and conclusion P(i). We introduce ∀ to justify ∀x.P(x).	∀ elim: We eliminate ∀ from ∀x.P(x) to justify P(i) in an assumption box. That box requires actual i as an assumption.
∃	∃ intro: We move backwards from ∃(x).P(x) to actual i and P(i). We introduce ∃ to justify ∃x.P(x). (To use an inner assumption box click on the conclusion.)	∃ elim: We eliminate ∃ from ∃x.P(x) to put assumptions P(i) and actual i into an assumption box. We conclude C in that box, hence we jump out of the box and conclude C from ∃x.P(x).
∀ and ∃	As the full menu names suggest, the ∀ and ∃ rules require the assumption actual i. The backwards ∀ intro step and the forwards ∃ elim introduce actual i. The other two steps in this category need actual i but cannot add this line.
Step	Backward Intro	Forward Elim
truth	Adds an open conclusion ⊤.	not available
constructive contradiction	backwards direction not preferred… see below…	Moving forward from a contradiction ⊥ a selected conclusion is justified.
TO BE USED WITH CAUTION
Step	Backward Intro	Forward Elim
classical contradiction	Move back from a conclusion A into an assumption box that has ¬A as hypothesis and contradiction ⊥ as conclusion. (Compare to ¬ intro.)	not available
constructive contradiction	Move back from a conclusion A to a contradiction ⊥ in order to justify A.	forwards direction is preferred… see above…
¬ elim	Move back from contradiction ⊥ to two new lines: _B1 and ¬_B1 (where _B1 is a newly introduced variable). These mutually contradictory lines are then used to justify ⊥.	forwards direction is preferred… see above…
∧ intro	backwards direction is preferred… see above…	Moving forward from A and B we can justify A∧B.
∨ intro	backwards direction is preferred… see above…	Moving forward from A one can justify A∨_B1 or _B1∨A (your choice), where _B1 is a new variable.
Step	Backward Intro	Forward Elim
hypothesis	Convert a variable into a subformula by choosing both.	Convert a variable into a subformula by choosing both.

Constructive vs. Classical Contradiction

Although constructive construction is preferred, classical contradiction is possible within Jape. Classical contradiction sometimes works where constructive construction fails. As a result, sometimes a claim may be both proved and disproved.

Justify vs. Create

Some steps may justify some lines, create others without justification, and create still others with justification.

For instance, we can move backwards from F∧G to create two new lines F and G through ∧ elim. Those two new lines still need to be justified, while the old line F∧G is now justified.

In the end, all lines must be justified.

Backward vs. Forward Justification

Because later lines cannot be used to justify earlier lines, generally backward steps justify the “starting” line, and forward steps justify later lines.

Move Backwards vs. Justify Forwards

Another way to look at the backwards steps is to think of two separate actions: 1) moving backwards from your original “starting” statement to an earlier statement or statements, and 2) moving forwards from those earlier statements to justify the original statement.

Working Order vs. Reading Order

For the most part:

• Working backwards (to earlier lines) eliminates connectives
• Working forwards (to later lines) eliminates connectives.

This is judged by the direction you're working in: from your existing lines (or reasons) to new lines (or reasons).

However, from the point of view of reading the proof from earlier lines to later lines:

• Most backward steps are intro steps: they introduce connectives
• Most forward steps are elim steps: they eliminate connectives.

The distinction can be a bit confusing.

Premise vs. Other

Premise vs. Conclusion

In A$$\vdash$$A∨B the first A is left of the turnstile and does not have to be proved. It is a premise.

To the right of the turnstile is the conclusion A∨B, which does have to be proved.

Premise vs. Assumption

A premise never has to be proved. It can be used to prove other statements.

By contrast, an assumption is temporarily introduced to prove later steps. If an assumption is not proved at some point then it must be discharged later.

According to Bornat ("Manual," sec. 1.5.3, p. 10), “Jape guarantees correct use of assumptions by combining introduction and discharge into a single step.”

For instance, if A→B is an unproved statement we can create an assumption box with A as the assumption and B as the conclusion.

The → intro rule applied to the assumption box then justifies A→B. (The conclusion of the assumption box has to be proved at some point though.)

A→B thus discharges the assumption A in the assumption box.

Default vs. Other Selections

Formula vs. Subformula Selection

A regular mouse click should select an entire formula and place it in a red-coloured outline.

Alt/option plus mouse click highlights a part of the formula—a subformula—and highlights it with yellow.

Conclusion Selection vs. Default Selection

You must choose a target conclusion when using forward ∨ elim and forward ∃ elim.

You may choose a target conclusion when using backward ∃ intro, forward ∧ elim, forward ∨ elim, forward → elim, and forward ¬ elim (for example).

(Double check.)

Hypothesis vs. Unproved Conclusion

In an unfinished proof a hypothesis appears before a line of dots, and a conclusion appears after.

Therefore a line somewhere between two sets of dots might function as an hypothesis or an unproved conclusion.

Choosing the wrong role for that line could prevent you from using a rule that you should be able to use.

For instance, consider this conjecture:

Line 5 has form E∧F and is preceded by E and F, so it makes sense to try backwards ∧ elim. But when I clicked on E∧F and chose ∧ elim from the Backwards menu I got this error message:

What?! It's clearly an unproved conclusion, so why is Jape telling me not to click on an hypothesis?

If you click on the upper half of E∧F the boxy red "U" opens upwards, indicating Jape now considers it an unproved conclusion. (Bornat explains this with examples on pp. 11—12 of his natural deduction manual.)

Backwards ∧ intro now works like a charm:

Obviously clicking on the bottom half of a line with ambiguous function ensures it's considered to be an hypothesis.

---

Footnotes

1. Richard Bornat, “Roll your own Jape logic: Encoding logics for the Jape proof calculator.” 2005 (PDF), “Preface,” p. 3.

---

Still To Do

To Clarify

• When an assumption box is an optional choice for a "target conclusion" (give examples of the choices and a full list of steps that offer that choice)
• How to specify an assumption box
• The difference between how a Jape rule sets up lines vs. how the proof will read in the end. In other words, there's a difference in how a final proof reads (line by line), and how it was constructed (step by step)
• Some Jape actions create no new justifications.

To Add

• The remaining menu items including the two kinds of contradiction
• A clear description of hypothesis vs. conclusion
• Mnemonic "i.e." for backwards/forwards preference for "intro" and "elim" (respectively)
• Subformulas and subformula substitutions
• What is an hypothesis?
• Once a proof is complete then every line must be a premise or a conclusion that follows from an earlier line or lines (a premise has no previous lines)
• Describe the difference between open vs closed conclusion
• More illustrations
• The relationship of natural deduction in general to Bornat's version in particular
• Disproof.

---

Advisory

Please note that I am not a mathematician and so the presentation of proofs that I make may be deeply flawed. I'm using this writing process to figure out what I'm reading. Please consult more authoritative sources as well.

Feel free to contact me by leaving a comment or sending me a private message.