# 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.

## 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.

`.propNJ`

and `.propNK`

Rules for 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.

## 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:

## Advanced Usage

### 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 |

### 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:

### 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 `Q`

s 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.

### 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!