← Back to the calculator

Manual

DeDucktion

A Natural Deduction Calculator

Leander Herter · Rasmus Buurman

2026-06-12  ·  Version 0.1.0  ·  github.com/DeDucktion

1. Overview

This manual provides an introduction to the relevant formal definitions and to the usage of our calculator. In general, this calculator is designed to offer an opportunity for visually creating deduction trees step by step.

Thus, the main focus is to make the process of creating such a tree more accessible. For this reason, the major spotlight is given to the design of the webpage. However, we are also interested in a fast and clean backend that proof-checks all the deduction trees.

Some functionality which might also be interesting for people who are more advanced in logic is the converting tool. Everyone who deals with logic comes sooner or later in touch with deduction trees. Typesetting such deduction trees remains an issue: although there are very useful packages, it is still time-consuming. For this reason, the calculator offers to convert every tree you create into ready-to-use LaTeX or Typst code.

It is still a challenge to agree on a general syntax and definition of a natural deduction proof system. Since DeDucktion is an open-source project, we invite everyone to integrate their own syntax and formal definition of their natural deduction proof system. For now, we start with the formal notions oriented at the lecture "Einführung in die formale Logik" (Introduction to Formal Logic) from Tübingen. So far the calculator is only usable for propositional logic.

2. Formal Notions

2.1. Syntax

We start with the definition of the syntax of propositional logic.

Definition 2.1.1 (Language)

The language of our propositional logic contains only the following symbols:

  1. Propositional symbols: P, Q, R, P_1, Q_1, R_1, P_2, \ldots
  2. Connectives: \lnot,\ \land,\ \lor,\ \rightarrow,\ \leftrightarrow
  3. Parentheses: (\ ,\ )

This is followed by the inductive definition of a formula.

Definition 2.1.2 (Formula)

  1. Every propositional symbol is a formula.
  2. If \varphi is a formula, then \lnot\varphi is a formula.
  3. If \varphi and \psi are formulas, then (\varphi \land \psi) is a formula.
  4. If \varphi and \psi are formulas, then (\varphi \lor \psi) is a formula.
  5. If \varphi and \psi are formulas, then (\varphi \rightarrow \psi) is a formula.
  6. If \varphi and \psi are formulas, then (\varphi \leftrightarrow \psi) is a formula.
  7. Nothing else is a formula.

With this said, we can provide a few examples of formulas that are allowed in our calculator.

Example

  • (P \land (Q \lor P_2))
  • P_{999}
  • ((P \leftrightarrow R) \rightarrow (R \land R_1))

Remark

We do not allow any propositional symbols other than P, Q, R and P_i, Q_j, R_l for i, j, l \in \mathbb{N}.1

A parenthesis-saving convention is not included either. Therefore, there is no defined hierarchy between the connectives.

2.2. Natural Deduction System

For every connective we define at least one introduction and one elimination rule.

Definition 2.2.1 (Deduction Rules)

\land Conjunction

Introduction

\varphi\psi
\land\mathrm{I}
(\varphi \land \psi)

Elimination 1

(\varphi \land \psi)
\land\mathrm{E}1
\varphi

Elimination 2

(\varphi \land \psi)
\land\mathrm{E}2
\psi

\lor Disjunction

Introduction 1

\varphi
\lor\mathrm{I}1
(\varphi \lor \psi)

Introduction 2

\psi
\lor\mathrm{I}2
(\varphi \lor \psi)

Elimination

(\varphi \lor \psi) [\varphi]\vdots\chi [\psi]\vdots\chi
\lor\mathrm{E}
\chi

\rightarrow Conditional

Introduction

[\varphi]\vdots\psi
\rightarrow\mathrm{I}
(\varphi \rightarrow \psi)

Elimination

(\varphi \rightarrow \psi)\varphi
\rightarrow\mathrm{E}
\psi

\lnot Negation

Introduction

[\varphi]\vdots\psi [\varphi]\vdots\lnot\psi
\lnot\mathrm{I}
\lnot\varphi

Elimination

[\lnot\varphi]\vdots\psi [\lnot\varphi]\vdots\lnot\psi
\lnot\mathrm{E}
\varphi

\leftrightarrow Biconditional

Introduction

[\varphi]\vdots\psi [\psi]\vdots\varphi
\leftrightarrow\mathrm{I}
(\varphi \leftrightarrow \psi)

Elimination 1

(\varphi \leftrightarrow \psi)\varphi
\leftrightarrow\mathrm{E}1
\psi

Elimination 2

(\varphi \leftrightarrow \psi)\psi
\leftrightarrow\mathrm{E}2
\varphi

Remark

In this calculator the order of the premises matters. That means the calculator will not accept instances of:

\varphi(\varphi \rightarrow \psi)
\rightarrow\mathrm{E}
\psi

Another important remark is that the discharging brackets are obligatory.2

With these rules one can define the derivability relation \Gamma \vdash \varphi.

Definition 2.2.2 (Derivability)

Let \Gamma be a set of propositional logic formulas and let \varphi be one such formula. Then \Gamma \vdash \varphi holds iff \varphi is the result of using the rules of Definition 2.2.1 with only the formulas of \Gamma as open assumptions.3

Example 1 (P \rightarrow Q),\ (Q \rightarrow R) \vdash (P \rightarrow R)

(Q \rightarrow R)
(P \rightarrow Q) [P]
\rightarrow\mathrm{E}
Q
\rightarrow\mathrm{E}
R
\rightarrow\mathrm{I}
(P \rightarrow R)

Example 2 (P \lor Q),\ (P \rightarrow R_1),\ (Q \rightarrow R_2) \vdash (R_1 \lor R_2)

(P \lor Q)
(P \rightarrow R_1) [P]
\rightarrow\mathrm{E}
R_1
\lor\mathrm{I}1
(R_1 \lor R_2)
(Q \rightarrow R_2) [Q]
\rightarrow\mathrm{E}
R_2
\lor\mathrm{I}2
(R_1 \lor R_2)
\lor\mathrm{E}
(R_1 \lor R_2)

3. Using the Calculator

You now know the rules of our proof system (Section 2.2). In this chapter we provide an explanation on how to turn such a proof tree in a DeDucktion tree in the calculator and after that how to proof-check it. The calculator is built around one idea: you state a claim \Gamma \vdash \varphi, then you build up the proof tree bottom up, starting with the last inferential step, and build the proof upwards by applying one rule at a time. Similarly to the two examples above.

The Interface

The calculator has five areas. This is shown in the schematic graphic below; the numbers point to the sections that follow.

The calculator’s five areas
  1. 1Rule sidebar — one button for each deduction rule.
  2. 2Action bar — validate, clear, undo, export, and view controls.
  3. 3The claim — the premises, the turnstile \vdash, and the conclusion you want to derive.
  4. 4Proof canvas — the canvas in which you can build your tree.
  5. 5Result, Input Help & Convert Help — shows the verdict of the proof-check, input shortcuts, and package import helpers for export.

3.1. The Rule Sidebar

At the moment the Rule Sidebar shows a list of every rule defined in Definition 2.2.1, with the same label, e.g. \land\mathrm{I}, \rightarrow\mathrm{E}, \lnot\mathrm{I}. By clicking on such a rule button you apply the rule either to the empty canvas or with respect to a selected node.

Clicking a rule does one of two things:

  1. Empty canvas. The clicked rule becomes the root of a new tree: a conclusion box, the inference line with the rule’s label, and one empty premise slot per premise of that rule.
  2. A node is selected. That node is turned into the conclusion of the rule: the line and label appear above it, and fresh empty premise slots are added on top. Whatever formula was already in the box is kept.

For example, if you click on \rightarrow\mathrm{E}, an empty deduction tree appears in the canvas (one empty node for the conclusion and one empty node for each premise).

Rule button

\rightarrow\mathrm{E}

Schema on the canvas

\rightarrow\mathrm{E}

Now you can fill in the empty nodes. For each premise, you either type in a formula or press another rule. At the end every conclusion and premise node must be filled with exactly one (maybe discharged) formula.

3.2. The Action Bar

Above the canvas and the claim you find the action bar. For every crucial functionality there is a button. The following lists every button:

Validate Clear Tree Clear Input Undo Convert to Typst Convert to LaTeX Practice Fit View
Validate
Runs the proof checker on the current tree against the claim in the bar, and writes the verdict into the result panel.
Clear Tree
Removes the whole tree from the canvas.
Clear Input
Empties the premise and conclusion fields.
Undo
Steps back through your edits (applied rules, typed formulas, and the view) up to the last 100 changes.
Convert to Typst
Exports the current tree as ready-to-paste Typst code.
Convert to LaTeX
Exports the current tree as ready-to-paste LaTeX code.
Practice
Loads a practice claim. The problems are taken from The Natural Deduction Pack by Alastair Carr.4
Fit View
Zooms and re-centres so the entire tree fits the canvas.

3.3. Claim: Premises & Conclusion

The bar under the buttons states the claim you are trying to prove, \Gamma \vdash \varphi:

Premises (P \rightarrow Q),\ P
\vdash
Conclusion Q
  • Premises: The formulas \Gamma you are allowed to use as open assumptions, separated by commas.
  • Conclusion: The single formula \varphi your tree must end in.

This is what Validate checks: the conclusion at the bottom of your tree must match the right field, and every open assumption left in the tree must appear among the premises on the left.

3.4. The Canvas

The canvas is the working area where the tree grows. You can scroll as far as you want in any direction. You can also zoom in and out.

If you select an input field of a tree-node you can selct another rule or type in a formula with the shortcuts like -> or imp. If you type in an invalid formula the input field gets a red stroke.

If a proof scrolls off the screen, the Fit View-Button resets the zoom and position so the whole tree is visible and centred again.

3.5. The Result, Input Help & Convert Help Panels

The right-hand column has three stacked panels.

Result

Correct proof.

Incorrect proof.

No validation yet.

Result stays muted until you press Validate. A correct proof turns it to Correct proof; a broken step turns it to Incorrect proof.

Input Help

and, & for \land

or, | for \lor

not, ~ for \lnot

imp, -> for \rightarrow

biimp, <-> for \leftrightarrow

Input Help shows keyboard shortcuts: type any sequence in a formula field and it is replaced by the logical symbol as you go.

Convert Help

curryst Typst
bussproofs LaTeX

Convert Help provides a ready-to-copy import command for either curryst for Typst or bussproofs for LaTeX.

4. Demo

To see the calculator in action, watch the two short demos:

Demo 1 (P \rightarrow Q),\ (Q \rightarrow R) \vdash (P \rightarrow R)

Demo 2 (P \land (Q \lor R)) \vdash ((P \land Q) \lor (P \land R))

Service Contact:
Found a bug, an error, or another problem? Contact leander.herter@student.uni-tuebingen.de.