How this works

There are seven exercises to solve (use the "Select exercise" button on the top left to check your progress). An exercise is made of two elements:

• A (possibly empty) set of premises
• A proposition

Your job is to prove propositions by building proof trees for them. To set the focus to a specific node in your tree, simply click on it (there is always one focused node and it is outlined in bold). You can then apply any of the rules compatible with that node using the buttons in the other panel. Note that some of the rules can be applied to any node (e.g., ⊥-elim), whereas others are context-dependent (e.g., the last step in a proof tree for A ∧ B can not be ∨-intro-l). The system only shows rules compatible with the node under focus. If that node is a leaf, applying a rule will turn it into a branch node with one leaf per premise of the corresponding natural deduction inference rule. Otherwise, the branch node gets turned into a leaf node (the system clears everything above it) and the rule gets applied to it.

Different rules act in different ways. Some of them expect an user-provided expression: in that case, just input something sensible in the panel that automatically opens. Some (such as →-intro) implicitly introduce local premises that can be used in the rest of the branch. Use an external reference for the moral justification as to why the inference rules behave the way they do.

Warning: the rules implemented here are a slight departure from those given by Van Dalen, though the resulting systems are equivalent (i.e., anything that can be proven with Van Dalen's rules can be proven here, and vice versa; proving that is an optional exercise left to the reader). The differences are:

• The classical logic inference rule DNE (double-negation elimination) is provided
• Several rules (such as ∨-elim) work with explicit implications instead of introducing branch-local hypotheses; if what this means is not clear to you, just click the button and see how it differs from what the book says. To get back to the version of the book, just use an explicit →-intro: you can view Van Dalen's version as syntactic sugar for that
• No distinction is made between ⊥-elim and RAA (reductio ad absurdum): ⊥-elim behaves like the more powerful RAA (this does not change much in practice; you just get a hypothesis for free in the ⊥-elim case)

I will change the system so as to make it match the book after submissions (I don't want to make breaking changes while people are still working on this).

A leaf is automatically marked as done by the system whenever a matching premise or a local hypothesis (as implicitly introduced by →-intro or RAA) is found. Leaves that are done turn green. Branch nodes such that all the nodes sitting directly atop them are done are themselve marked as done and turn green. Focusing a done leaf nodes highlights a justification for it being done in yellow: either a premise or a node/subexpression lower in the same branch. The whole exercise is done when the root node is marked as done, in which case the entire background turns green.

If you get stuck, I advise to do proofs with pen-and-paper first and to port them to this system later. Also remember that you are welcome to submit pen-and-paper proofs.