10 Gentzen-Prawitz Natural Deduction
The TreeDeduction class indicates that a code block will contain Gentzen-Prawitz natural deduction exercises, which require the production of a Gentzen-Prawitz deduction tree.
These problems use ProofJS for their user interface. An initial click may be required to select a node. Once a node is selected, Enter will create a sibling premise (on any node but the root), Ctrl-Enter will create a new premise above the focused node, and Ctrl-Shift-Enter will create a new conclusion node below the focused node (on any node but the root node). Nodes can be selected by either pressing Tab and Shift-Tab to cycle, or by using the mouse. Changes can be undone and redone with Ctrl-Z and Shift-Ctrl-Z respectively. The subtree above a selected node can be deleted with Ctrl-Backspace, and subtrees can be cut-copy-pasted with Shift-Ctrl-X, Shift-Ctrl-C and Shift-Ctrl-V respectively.
10.1 Available Systems
At the moment, four systems are available:
| System | Description |
|---|---|
| propNK | A system based on the propositional fragment of Gentzen’s NK |
| propNJ | A system based on the propositional fragment of Gentzen’s NJ |
| openLogicNK | The propositional fragement of the Open Logic project’s natural deduction |
| openLogicFOLNK | The full (first-order with equality) Open Logic project natural deduction |
| openLogicArithNK | openLogicFOLNK for the language of arithmetic |
| openLogicExArithNK | openLogicFOLNK for the language of arithmetic with arbitrary predicates and functions |
| openLogicSTNK | openLogicFOLNK for the basic language of set theory with arbitrary predicates and functions |
| openLogicExSTNK | openLogicFOLNK for the basic language of set theory |
| openLogicESTNK | openLogicFOLNK for an extended language of set theory |
| openLogicExESTNK | openLogicFOLNK for an extended language of set theory with arbitrary predicates and functions |
| openLogicSSTNK | openLogicFOLNK for an extended language of set theory with separation abstracts |
| openLogicExSSTNK | openLogicFOLNK for an extended language of set theory with separation abstracts and arbitrary predicates and functions |
Exercises are given by specifying the system, and the sequent to be proved. So an exercise can be constructed like so:
```{.TreeDeduction .propNK}
1.1 P\/Q, ~P :|-: Q
```which produces:
Instead of .propNK etc, you can also use system="propNK".
(Remember to click on a node in order to interact, and to press Ctrl-Enter to create the first child node)
A completed proof will look like this:
With rule names to the right of inference lines, and assumptions labeled to the right of the rule citation (with or without parentheses). Discharged assumptions are marked using an inference with empty premise, and the assumption label on its own to the right of the inference line.
10.2 Rules for .propNJ and .propNK
Here’s a brief summary of NJ’s propositional rules. The notation [ψ]/φ indicates that an assumption ψ can be discharged from the subproof establishing φ
| Rule | Premises | Conclusion |
|---|---|---|
∧I |
φ, ψ | φ∧ψ |
∧E |
φ∧ψ | φ OR ψ |
∨I |
φ | φ∨ψ OR ψ∨φ |
∨E |
φ∨ψ, [φ]/χ, [ψ]/χ | χ |
→I |
[φ]/ψ | φ→ψ |
→E |
φ,φ→ψ | ψ |
¬I |
[φ]/⊥ | ¬φ |
¬E |
φ, ¬φ | ⊥ |
¬E |
⊥ | φ |
NK results from the addition of one more rule:
| Rule | Premises | Conclusion |
|---|---|---|
LEM |
φ∨¬φ |
The syntax of formulas accepted for is that for the propositional systems for Kalish & Montague/The Carnap Book in the Systems Reference.
10.3 Rules for Open Logic Systems
For the systems .openLogicNK, etc., the rules are:
| Rule | Premises | Conclusion |
|---|---|---|
∧I |
φ, ψ | φ∧ψ |
∧E |
φ ∧ ψ | φ OR ψ |
∨I |
φ | φ∨ψ OR ψ∨φ |
∨E |
φ∨ψ, [φ]/χ, [ψ]/χ | χ |
→I |
[φ]/ψ | φ→ψ |
→E |
φ,φ→ψ | ψ |
↔︎I |
[φ]/ψ, [ψ]/φ | φ↔︎ψ |
↔︎E |
φ↔︎ψ, φ | ψ |
| φ↔︎ψ, ψ | φ | |
¬I |
[φ]/⊥ | ¬φ |
¬E |
φ, ¬φ | ⊥ |
X |
⊥ | φ |
IP |
[¬φ]/⊥ | φ |
For the first order systems, we also have the rules:
| Rule | Premises | Conclusion |
|---|---|---|
∀I |
φ(a) | ∀x φ(x) |
VE |
∀x φ(x) | φ(t) |
∃I |
φ(t) | ∃x φ(x) |
∃E |
∃x φ(x), [φ(a)]/ψ | ψ |
=I |
t=t | |
=E |
φ(t),t=s | φ(s) |
The syntax of accepted for the Open Logic systems is described in the Systems Reference. The natural deduction systems for arithmetic and set theory only differ in the syntax; there are no axioms.
Here is an example of a derivation in the language of arithmetic:
10.4 Advanced Usage
10.4.1 Options
In addition to the standard points=VALUE and submission="none" options, Gentzen-Prawitz natural deduction exercises allow for you to set init="now" to have proofchecking begin as soon as the proof is loaded (rather than waiting for input) as well as the following allowed arguments to options="…":
| Option name | Effect |
|---|---|
prepopulate |
Prepopulates the endformula of an exercises with the conclusion to be shown |
displayJSON |
Ctrl-? will toggle display of an editable JSON representation of the proof |
10.4.2 Runtime Axioms and Rules
The “extended” mathematical systems, openLogicExArithNK openLogicExSTNK openLogicExESTNK and openLogicExSSTNK can be equipped with extra axioms and rules. To set an axiom or a rule for a system, include an option of the form axiom-NAME="RULEVARIANTS" where NAME is the name that you want your axiom or rule to have, and RULEVARIANTS is a semicolon-separated list of sequents representing the variant schematic forms of the rule. The rule should be cited as Ax-NAME. Axiom names are case-insensitive, so don’t rely on upper or lower-case variants of names to distinguish rules.
When entering the schematic sequents representing the forms of a rule, you should indicate which sentence letters, constants, and function symbols are to be read as schematic by preceding each such symbol with a prime, like so: 'P. So, for example:
~~~{.TreePlayground .openLogicExArithNK init="now" axiom-flip="'P('a*'b) :|-: 'P('b*'a); 'P('a+'b) :|-: 'P('b+'a)"}
{ "ident": 13, "label": "a+b=c", "rule": "Ax-flip", "forest": [
{ "ident": 15, "label": "b+a=c", "rule": "", "forest": [] }
]}
~~~will produce:
10.4.3 JSON Serialization
Here’s an incomplete proof, showing how to use the displayJSON option:
To show the JSON representation, click to focus one of the input areas in the proof and press Ctrl-?. To edit the deduction by editing the JSON, try replacing one of the Qs in the JSON panel with a P. The deduction will update to reflect the JSON, so long as the JSON is a well-formed representation of a deduction.
The above was generated with
```{.TreeDeduction .propNK init="now" options="displayJSON"}
1.1 P\/Q, ~P :|-: Q
| {"ident":12,"label":"Q","rule":"\\/E", "forest":[
| {"ident":13,"label":"P\\/Q","rule":"", "forest":[]},
| {"ident":14,"label":"Q","rule":"(1)", "forest":[
| {"ident":17,"label":"","rule":"","forest":[]}
| ]},
| {"ident":15,"label":"Q","rule":"?","forest":[
| {"ident":18,"label":"?","rule":"","forest":[]}
| ]}
| ]}
```The displayJSON option is useful for saving and communicating proofs, since one can reproduce a proof by pasting its JSON representation into the panel where the JSON representation is displayed. It’s also useful for creating exercises in which the problems are partially completed, since, as in the example above, one can prefill an exercise by supplying a JSON representation below the statement of the problem.
10.4.4 Playgrounds
One can generate a Gentzen-Prawitz playground (where there is no goal, but where what you’ve proved is displayed) using something like the following:
```{.TreePlayground .propNK init="now" options="displayJSON"}
| {"ident":12,"label":"Q","rule":"\\/E (1) (2)","forest":[
| {"ident":13,"label":"P\\/Q","rule":"","forest":[]},
| {"ident":14,"label":"Q","rule":"(1)","forest":[
| {"ident":17,"label":"","rule":"","forest":[]}
| ]},
| {"ident":15,"label":"Q","rule":"-E","forest":[
| {"ident":18,"label":"!?","rule":"-E","forest":[
| {"ident":24,"label":"P","rule":"(2)","forest":[
| {"ident":27,"label":"","rule":"","forest":[]}
| ]},
| {"ident":25,"label":"-P","rule":"","forest":[]}
| ]}
| ]}
| ]}
```The result, in this case, will be:
Try editing the proof to see how the displayed sequent changes!