To avoid having lots of screenshots I'll represent a Jape proof by this kind of table:

1: E∧(F∧G) premise
2: F∧G ∧ elim 1
3: F ∧ elim 2
4: E ∧ elim 1
5: E∧F
6: G
7: (E∧F)∧G ∧ intro 5,6

The first column shows line numbers (as does the Jape software). I have bolded line 7 because that line was selected (clicked on) before the backwards ∧ intro rule was executed. (It had a different line number when selected, and selection is turned off once the step is implemented.)

In the next two columns I have highlighted new material: lines 5 and 7 were added, and the justification for line 7 was added. (I have not highlighted lines.)

An assumption box is represented here by the > symbol:

1: > E assumption
> …
2: > F
3: E→F → intro 1-2

In the actual Jape presentation an assumption box looks like an actual box.


Feel free to leave a comment. A general log-in will be required, but you don't have to be a member of the Echolocation wiki. You may wish to read recent comments too (two at this point, including one from me).

Add a New Comment
Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-ShareAlike 3.0 License