Proofs as structured lists and proof trees

1. How to write a proof

This web page gives information on what a proof is, i.e. what sort of a mathematical object it is and how it might be manipulated mathematically. The details here are intended for propositional logic particularly, but may easily be adapted to any of the systems in The Mathematics of Logic.

There are two views of what a proof is, both perfectly correct. The approaches are: proofs as structured lists, as used in most of the printed text; and proofs as trees, as used by many other authors of logic texts. Since most people working in logic will see tree-proofs sooner or later, this web page explains this view and how it relates to the previous one. There are some advantages and disadvantages of each, as we shall see.

2. Structured lists of statements

The first approach is the one emphasised in The Mathematics of Logic: a proof is considered to be a structured list of statements written down in a linear fashion on the page. The structure is given by the idea of subproof which I indicate using indentation and a vertical line down the left margin.

In this view, a proof (from set of given assumptions $Σ$ ) is a list of statements and subproofs following various rules. All of the rules take the form, if certain formulas or subproofs preceed the current position and are in scope then some further expression may occur at the current position. Thus the idea of the set of preceding formulas or subproofs that are in scope is essential for work with this view. This idea was explained in some detail on page 67 of The Mathematics of Logic with respect to propositional logic.

The advantages of proofs written as structured lists of statements are

Proofs written in this system are similar to proofs written in ordinary mathematical texts.
The idea of subproof makes rigorous and explicit the idea of a temporary assumption or short sub-argument with limited scope that is often already implicit in natural language proofs anyway.
Proofs are written in a linear fashion, so can be read from top to bottom.

The disadvantages of proofs written as structured lists of statements are

Some proof rules must be formulated in terms of all previous statements and subproofs that are in scope, and not just a small number of them. (For example, the ∃-elimination rule requires a variable that does not occur free in any preceding formula which is in scope, the the rule can be modified to avoid this problem to a certain extent.)
Some assertions in a proof relate to a particular thread of the argument; other assertions relate to a different thread. It is not always so easy to see what is required for each of the separate threads, only that they are all needed when the various threads are combined.

3. Proof trees

An alternative approach is emphasised in other logical textbooks, especially books treating Natural Deduction Systems or Gentzen's Sequent Calculus.

The idea here is that a proof is a finite tree. Each node of the tree is labelled by some assertion, and the proof is a proof of the assertion at the bottom-most node (which is the root of the tree, so these trees are drawn upside down compared to the trees in Chapter 1 of The Mathematics of Logic, or if you prefer the right way up compared to real biological trees). The pre-conditions required to make a proof step are the labels of the immediately preceding node or nodes, and there will be finitely many of these.

There are many different types of assertions that label nodes in proof trees. Some systems label nodes with single formulas, some with sets of formulas, yet others with assertions of the kind $Σ ⊢ Π$ where $Σ, Π$ are sets of formulas. The simplest and most natural way of converting our particular proof-as-structured-list picture of proof to proof-as-tree is to label the nodes of the proof-tree with assertions of the form $Σ_{0} ⊢ σ$ where $Σ_{0}$ is a finite sequence of formulas and $σ$ is a further formula. (In this context, the $Σ_{0}$ is often called a sequent and is regarded as an unordered set, so the order of its elements and any repetitions of its elements are ignored, so for example the sequent $γ, α, β, α$ is equivalent to $α, β, γ$ .) Most of the rules are easy to convert into this form.

It is common to write rules in the form

\frac{Σ_{0} ⊢ σ_{0}}{Σ_{1} ⊢ σ_{1}}

to indicate that from $Σ_{0} ⊢ σ_{0}$ one may deduce $Σ_{1} ⊢ σ_{1}$ in a single step, and

\frac{Σ_{0} ⊢ σ_{0} Σ_{1} ⊢ σ_{1}}{Σ_{2} ⊢ σ_{2}}

to indicate that from both $Σ_{0} ⊢ σ_{0}$ and $Σ_{1} ⊢ σ_{1}$ one may deduce $Σ_{2} ⊢ σ_{2}$ in a single step. We may also write

\frac{}{Σ ⊢ σ}

to indicate that $Σ ⊢ σ$ can be proved in a single step without any preceding assertions.

The tree nature of proof is now evident: by combining several such steps we build a rooted tree with root at the bottom and branches going upwards. In the presentation I am about to give, the leaf nodes will all be empty, and there will be rules that make it possible to get a proof started.

In this picture, the rules of propositional logic (page 65) are written as follows.

Given statements: if $σ_{0} \in Σ_{0}$ then the step $\frac{}{Σ_{0} ⊢ σ_{0}}$ is allowed
Top: for any $Σ_{0}$ the step $\frac{}{Σ_{0} ⊢ ⊤}$ is allowed
$\land$ -Introduction: the step $\frac{Σ_{0} ⊢ ϕ Σ_{0} ⊢ ψ}{Σ_{0} ⊢ (ϕ \land ψ)}$ is allowed
$\lor$ -Introduction: the steps $\frac{Σ_{0} ⊢ ϕ}{Σ_{0} ⊢ (ϕ \lor ψ)}$ and $\frac{Σ_{0} ⊢ ψ}{Σ_{0} ⊢ (ϕ \lor ψ)}$ are allowed
$\land$ -Elimination: the steps $\frac{Σ_{0} ⊢ (ϕ \land ψ)}{Σ_{0} ⊢ ϕ}$ and $\frac{Σ_{0} ⊢ (ϕ \land ψ)}{Σ_{0} ⊢ ψ}$ are allowed
$\lor$ -Elimination: the step $\frac{Σ_{0} ⊢ (σ \lor τ) Σ_{0} ⊢ \neg σ}{Σ_{0} ⊢ τ}$ is allowed
$\neg$ -Elimination: the step $\frac{Σ_{0} ⊢ \neg \neg σ}{Σ_{0} ⊢ σ}$ is allowed
Contradiction Rule: the step $\frac{Σ_{0} ⊢ σ Σ_{0} ⊢ \neg σ}{Σ_{0} ⊢ ⊥}$ is allowed
Reduction Ad Absurdum Rule: the step $\frac{Σ_{0}, σ ⊢ ⊥}{Σ_{0} ⊢ \neg σ}$ is allowed

Proofs are finite, so any label $Σ_{0} ⊢ σ$ in a proof must have finite set $Σ_{0}$ . For infinite sets $Σ$ we define $Σ ⊢ σ$ to mean that there is a finite subset $Σ_{0}$ of $Σ$ such that there is a tree-proof following the above rules of the assertion where the bottom-most node is labelled with $Σ_{0} ⊢ σ$ .

For systems that involve the $\to$ symbol we add the following rules.

$\to$ -Elimination: the step $\frac{Σ_{0} ⊢ (σ \to τ) Σ_{0} ⊢ σ}{Σ_{0} ⊢ τ}$ is allowed
$\to$ -Introduction: the step $\frac{Σ_{0}, σ ⊢ τ}{Σ_{0} ⊢ (σ \to τ)}$ is allowed

The advantages of proofs written as trees are

The conditions for a proof step are clearer: they are often only conditions applied to the previous line.
The various paths through the proofs are emphasised.

The disadvantages of proofs written as trees are

There is no longer a single way of reading the proof from top to bottom, and it may be more difficult to convert such a proof to natural language.
Often tree proofs will be much longer and will require repetitions of the same proof steps.
Many readers, especially beginners, may fail to recognise a proof written as a tree as a traditional mathematical proof.

4. Exercises

These exercises all relate to the system of propositional logic as trees defined earlier. Most introduce useful metarules that make the system more managable.

Exercise.

Prove that the weakening rule

\frac{Σ_{0} ⊢ σ}{Σ_{0}, τ ⊢ σ}

is a metarule of the system. (Hint: Given a proof using this rule at some point, go up the branch or branches starting from this rule adding $τ$ to all sequents on the left-hand side. Observe that the resulting proof is correct and does not require the weakening rule.)

Exercise.

Prove that the following is a metarule of the system

\frac{Σ_{0} ⊢ σ Σ_{0}, σ ⊢ τ}{Σ_{0} ⊢ τ}

(Hint: modify a proof of $Σ_{0}, σ ⊢ τ$ inductively starting at the root and working upwards by removing the assumption $σ$ on the left. The only place this can't be done is at the leaf nodes $\frac{}{Σ_{0}, σ ⊢ σ}$ but these can be replaced with copies of the proof of $Σ_{0} ⊢ σ$ .)

Exercise.

Prove that the following cut rule is a meta rule of the system

\frac{Σ_{0}, σ ⊢ τ Σ_{0}, \neg σ ⊢ τ}{Σ_{0} ⊢ τ}