Sequent Calculus App

What is this?

The app is designed to help students of mathematical logic learn how a sequent calculus works. A sequent calculus is a formal system of mathematical proof.

This sequent calculus is roughly based on these lecture notes by Peter Koepke.

Each derivation consists of a formula to the right of the turnstile which has been successfully proven from the assumptions on the left side of the turnstile \(\vdash\). A new derivation comes from applying one of the rules to earlier derivations.

You have to start with either the assumption rule \(\begin{matrix} & & \\\hline \Gamma & \varphi & \varphi \end{matrix}\) (click on it and then on "Use with \(\Gamma=\{\}\)") or the \(=\)-introduction rule \(\begin{matrix} & \\\hline \Gamma & t = t \end{matrix}\).

Sometimes it is necessary to build or complete a formula. This can be done through the formula builder. Build a formula from its outermost operation down to the innermost atomic formula and then build a term if necessary.

This is still work in progress!