Home

Welcome to the Gentzen wiki!

Gentzen is an automated propositional logic proof system, using Gerhard Gentzen's algorithm.

Terminology

• Proposition, i.e. well-formed formula - for details, see Syntax.
• Atomic Proposition - a single propositional symbol, e.g. P.
• Sequent - a set of assumptions and conclusions, i.e. S = (A1 && A2 && A3 && A4...) -> (B1 || B2 || B3 || B4...)
• Axiom - a sequent whose assumptions and conclusions share at least one common proposition
• Finished Sequent - an axiom, or a sequent consisting of only atomic propositions

Deduction Trees

The main principle of the Gentzen algorithm is to construct a tree in which each node contains a single sequent, and all child nodes are manipulations of that sequent. Manipulations are formed using one of eight Inference Rules. This lecture from Cornell University does a good job explaining the concept.

Inference Rules

Rule	Sequent	Manipulation
Left And	{ [A && B]; [] }	{ [A, B]; [] }
Right Or	{ []; [A || B] }	{ []; [A, B] }
Right Implication	{ []; [A -> B] }	{ [A]; [B] }
Left Not	{ [!A]; [B] }	{ []; [A, B] }
Right Not	{ [A]; [!B] }	{ [A, B]; [] }
Left Implication	{ [A -> B]; [] }	{ []; [A] }
-	-	{ [B]; [] }
Left Or	{ [A || B]; [] }	{ [A]; [] }
-	-	{ [B]; [] }
Right And	{ []; [A && B] }	{ []; [A] }
-	-	{ []; [B] }

Note that the last three rules result in two possibilities. These three rules are called double-premise rules.

The above rules are listed in an order that roughly provides a minimal size tree. This is because the single-premise rules have the potential to greatly simplify any given sequent, without resulting in any new branches, thus making a "tall" tree with little branching. The rules could be applied double-premise-first, resulting in a "fatter" tree structure with far more branching, which most would agree is more difficult to follow.

Searching for Proofs

The tree is constructed as detailed above. Once the tree is finished (i.e., all of its nodes are finished), the tree's leaves are evaluated.

Any leaves that are not axioms serve as counter-examples. For example, the sequent { [P, Q]; [R] } is clearly a finished sequent, and is not an axiom. Whatever the original proposition, we now know that if P = true, Q = true, and R = false, the original proposition is false as well.

If all leaves of the tree are axioms, then no counter-examples could be found, and the original proposition is a tautology.

Some Theory

Simply put, we are essentially searching for a counter-example to disprove the initial proposition. The only way we can have a counter example is if the assumptions are all true, and any of the conclusions is false (by the definition of a sequent).

Note: Another way to think of a sequent is as a collection of "true" and "false" statements. However, this can quickly become confusing: there is nothing inherently "false" about the conclusions - we are trying to find cases that make the conclusions false. For this reason, sequents are referred to using the Assumptions/Conclusions mentality throughout Gentzen's documentation and implementation.

It can be shown that an axiomatic sequent cannot be falsified, for example:

(P && Q && R) -> P
(P, Q, R) -> P
P -> P
!P || P

In this example, the expression simplifies to "not P or P", which is always true.

Equivalently, a finished, non-axiomatic sequent is always falsifiable. If we view the sequent by its formal definition, (A1 && A2...) -> (B1 || B2...), all we need to falsify the sequent is for any of its conclusions to be valid. In an unfinished sequent, it is not immediately clear if this is possible, but in a finished sequent, no further simplification can be done. To falsify a finished sequent, we simply need to falsify any one of its conclusions, while keeping the assumptions true.

Thus, if at any point we reach an axiom, we do not need to further manipulate the sequent; it is unfalsifiable. If we reach a finished node that is not an axiom, we have found a counter-example. If no such counter-examples exist, then all derived sequents are unfalsifiable, and thus the original proposition is also unfalsifiable.