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.

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 $\Sigma $)
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

. 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 *in scope* then some
further expression may occur at the current position*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.

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 $\Sigma \u22a2\Pi $ where $\Sigma ,\Pi $ 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 ${\Sigma}_{0}\u22a2\sigma $ where ${\Sigma}_{0}$ is a finite sequence of formulas and $\sigma $ is a further formula. (In this context, the ${\Sigma}_{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 $\gamma ,\alpha ,\beta ,\alpha $ is equivalent to $\alpha ,\beta ,\gamma $.) Most of the rules are easy to convert into this form.

It is common to write rules in the form

$$\frac{{\Sigma}_{0}\u22a2{\sigma}_{0}}{{\Sigma}_{1}\u22a2{\sigma}_{1}}$$to indicate that from ${\Sigma}_{0}\u22a2{\sigma}_{0}$ one may deduce ${\Sigma}_{1}\u22a2{\sigma}_{1}$ in a single step, and

$$\frac{{\Sigma}_{0}\u22a2{\sigma}_{0}{\Sigma}_{1}\u22a2{\sigma}_{1}}{{\Sigma}_{2}\u22a2{\sigma}_{2}}$$to indicate that from both ${\Sigma}_{0}\u22a2{\sigma}_{0}$ and ${\Sigma}_{1}\u22a2{\sigma}_{1}$ one may deduce ${\Sigma}_{2}\u22a2{\sigma}_{2}$ in a single step. We may also write

$$\frac{}{\Sigma \u22a2\sigma}$$to indicate that $\Sigma \u22a2\sigma $ 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 ${\sigma}_{0}\in {\Sigma}_{0}$ then the step $\frac{\text{}}{{\Sigma}_{0}\u22a2{\sigma}_{0}}$ is allowed
- Top: for any ${\Sigma}_{0}$ the step $\frac{\text{}}{{\Sigma}_{0}\u22a2\top}$ is allowed
- $\wedge $-Introduction: the step $\frac{{\Sigma}_{0}\u22a2\varphi {\Sigma}_{0}\u22a2\psi}{{\Sigma}_{0}\u22a2(\varphi \wedge \psi )}$ is allowed
- $\vee $-Introduction: the steps $\frac{{\Sigma}_{0}\u22a2\varphi}{{\Sigma}_{0}\u22a2(\varphi \vee \psi )}$ and $\frac{{\Sigma}_{0}\u22a2\psi}{{\Sigma}_{0}\u22a2(\varphi \vee \psi )}$ are allowed
- $\wedge $-Elimination: the steps $\frac{{\Sigma}_{0}\u22a2(\varphi \wedge \psi )}{{\Sigma}_{0}\u22a2\varphi}$ and $\frac{{\Sigma}_{0}\u22a2(\varphi \wedge \psi )}{{\Sigma}_{0}\u22a2\psi}$ are allowed
- $\vee $-Elimination: the step $\frac{{\Sigma}_{0}\u22a2(\sigma \vee \tau ){\Sigma}_{0}\u22a2\neg \sigma}{{\Sigma}_{0}\u22a2\tau}$ is allowed
- $\neg $-Elimination: the step $\frac{{\Sigma}_{0}\u22a2\neg \neg \sigma}{{\Sigma}_{0}\u22a2\sigma}$ is allowed
- Contradiction Rule: the step $\frac{{\Sigma}_{0}\u22a2\sigma {\Sigma}_{0}\u22a2\neg \sigma}{{\Sigma}_{0}\u22a2\perp}$ is allowed
- Reduction Ad Absurdum Rule: the step $\frac{{\Sigma}_{0},\sigma \u22a2\perp}{{\Sigma}_{0}\u22a2\neg \sigma}$ is allowed

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

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

- $\to $-Elimination: the step $\frac{{\Sigma}_{0}\u22a2(\sigma \to \tau ){\Sigma}_{0}\u22a2\sigma}{{\Sigma}_{0}\u22a2\tau}$ is allowed
- $\to $-Introduction: the step $\frac{{\Sigma}_{0},\sigma \u22a2\tau}{{\Sigma}_{0}\u22a2(\sigma \to \tau )}$ 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.

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{{\Sigma}_{0}\u22a2\sigma}{{\Sigma}_{0},\tau \u22a2\sigma}$$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 $\tau $ 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{{\Sigma}_{0}\u22a2\sigma {\Sigma}_{0},\sigma \u22a2\tau}{{\Sigma}_{0}\u22a2\tau}$$(Hint: modify a proof of ${\Sigma}_{0},\sigma \u22a2\tau $ inductively starting at the root and working upwards by removing the assumption $\sigma $ on the left. The only place this can't be done is at the leaf nodes $\frac{\text{}}{{\Sigma}_{0},\sigma \u22a2\sigma}$ but these can be replaced with copies of the proof of ${\Sigma}_{0}\u22a2\sigma $.)

Exercise.

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

$$\frac{{\Sigma}_{0},\sigma \u22a2\tau {\Sigma}_{0},\neg \sigma \u22a2\tau}{{\Sigma}_{0}\u22a2\tau}$$