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 )
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
The disadvantages of proofs written as structured lists of statements are
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 where is a finite sequence of formulas and is a further formula. (In this context, the 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
to indicate that from one may deduce in a single step, and
to indicate that from both and one may deduce in a single step. We may also write
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.
Proofs are finite, so any label in a proof must have finite set . For infinite sets we define to mean that there is a finite subset of such that there is a tree-proof following the above rules of the assertion where the bottom-most node is labelled with .
For systems that involve the symbol we add the following rules.
The advantages of proofs written as trees are
The disadvantages of proofs written as trees are
These exercises all relate to the system of propositional logic as trees defined earlier. Most introduce useful metarules that make the system more managable.
Prove that the weakening rule
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.)
Prove that the following is a metarule of the system
(Hint: modify a proof of 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 but these can be replaced with copies of the proof of .)
Prove that the following cut rule is a meta rule of the system