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!