Deductive Proof

We now look at the general idea of deductive systems, collections of inference rules that allow us to derive new facts from existing ones.

This is a radically different approach to the “enumerate all possible truth values” approaches we have taken so far by writing out truth tables or by using a SAT solver.

Instead, we construct sequences (or, more generally, trees) of rules connected together that lead us step by step from some assumptions to a conclusion.

Video

Slides for the video (PDF)

The key idea in the video is that of a proof rule which allows us to deduce a conclusion from zero or more premises:

The rule is read top to bottom: if we can prove all the premises (possibly using other rules), then we can use this rule to deduce the conclusion. Often, we will write a collection of rules as one rule by putting in variables (usually X, Y, Z) to stand for other symbols. See below for multiple examples of this. Rules (or rule collections) are usually given names, which are written to the right of the premises (sometimes off the end of the line).

Rules with no premises are called axioms, and are needed to be able to prove anything. The axioms are things that we can assume without proof.

Proofs are constructed from rules by arranging them into trees, which we usually construct bottom up, applying rules to transform a goal statement to be proved into (hopefully) simpler subgoals that will eventually be proved by means of axioms. The rest of this page uses a small proof editor to interactively build proofs.

Example: Mammalian Biology

Rules

Here are the proof rules used for the small mammalian biology proof system given in the video. There are four axioms A1-A4 that tell us basic facts about bears and coconuts, and two rules R1 and R2 that allow us to make further deductions.

Example 1

Enter the name of the rule you want to apply in the input box and press enter (for example, A1 for the “furry(bear)” axiom. If the rule does not apply, because the conclusion of the rule does not match the statement to be proved, the system will not let you apply it. Continue until the proof has no more branches that need proof.

If you get stuck, click on a statement in the proof tree to reset it to that point.

Example 2

Example: Arithmetic

We can also represent arithmetic on whole numbers as proof rules. For the purposes of this proof system we use a representation of whole numbers starting from 0 in unary. This means that we represent 0 as the symbol “z” and every other number n as n uses of the successor function “s”. For example, 5 is represented as “s(s(s(s(s(z)))))”. Think of using “s” as adding one (or taking the successor of a number).

We have two judgement forms:

1. If we can prove add(x,y,z) then that means that x + y = z.

2. If we can prove mul(x,y,z) then that means that x * y = z.

The rules are:

The best way to see how these rules is to use them. As above, type the name of the rule into the box to use it.

Addition by repeated succession

Addition works by stripping successors from the first number and the third number until we get down to zero in the first number and the second and third are equal (because 0 + y = y).

Let's try 2 + 2 = 4:

And 3 + 2 = 5:

Note that if we try to prove an equation that doesn't hold, such as 2 + 2 = 2, then we will not be able to complete the proof:

The soundness property of this system is that if we can prove add(x,y,z) then it is actually the case that x + y = z. This system is also complete, meaning that if x + y = z, then it is possible to prove add(x,y,z). (Note that this only holds for numbers we can represent using zero and successor, the system has nothing to say about negative numbers, or fractions, or any other kind of number.)

Multiplication by repeated addition

Multiplication is the process of repeated addition. We use the first number to tell us how many times to repeat the addition of the second number:

For example, 2 * 3 = 0 + 3 + 3 = 6:

And 3 * 2 = 0 + 2 + 2 + 2 = 6:

As for addition, the soundness property of this system is that if we can prove mul(x,y,z) then it is actually the case that x * y = z. And this system is also complete, meaning that if x * y = z, then it is possible to prove mul(x,y,z). (Again, this only holds for whole numbers starting from 0).

Example: Haggis Migration

For many proof systems, there can often be more than one proof for a single statement. One way to think about this is as different "paths" leading to the same conclusion. For some purposes we may only care that the conclusion is reached (so we know that it is justified by our rules). For other purposes, we may care about the exact route taken (often shorter proofs are preferred over longer rules, but sometimes a longer proof may be more meaningful or useful in some way).

Let's take the idea of paths to a conclusion literally, and look at a proof system for describing the migration patterns of haggis. There is one judgement migrates(X,Y), meaning that it is possible for haggis to migrate from X to Y.

Here are the rules:

(I am not claiming whether or not this system is sound or complete for real haggis migration patterns.)

There are three proofs of migrates(glasgow, inverness). Can you find them all? If you get stuck, clicking on a part of the proof tree resets the proof to that point.

Proof 1

Proof 2

Proof 3

Proof Systems for Logic

The systems of proof rules we have looked at above are all for specific cases. In the remainder of the course we will look at a general proof system for Propositional and, later, Predicate Logic. These proof systems are powerful enough that other proof systems can be encoded in them by using implication to move proof rules "into" the logical formulas. We will see an example of this when we come to look at arithmetic inside Predicate Logic.

There are many ways of giving proof systems for Propositional and Predicate Logic. The way that we will use is a variant of Natural Deduction, called Focused Natural Deduction. There are other proof systems such as Sequent Calculus. One of the simplest, in terms of number of rules and not in terms of constructing proofs, are “Hilbert” style proof systems which usually only have one rule (“Modus Ponens” or “MP”) and some axioms.

For a minimal logical system that only includes implication the rule and axioms are: (implication is written as implies(a,b) here, due to limitations with the tool).

In more normal notation, the S axiom is written (A → B → C) → (A → B) → (A → C) and the K axiom is written A → B → A. The rule MP (“Modus Ponens”) says that if we know A implies B and we know A, then we know B. We can see MP as a way of incorporating the idea of applying a proof rule directly into the logic.

This system has its roots in Gottlob Frege's book Begriffsschrift published in 1879, which was the first attempt to write down a systematic proof system for logic by itself. The idea was later developed by David Hilbert and are often called Hilbert Systems. It is closely related to Combinatory Logic, one of the many systems that can be used to describe what is computable.

This system is surprisingly expressive, and can be extended to all of propositional logic just by adding extra axioms. Even with just these two rules, it is sound and complete for Intuitionistic Logic when the only connective is implication (see the page on Soundness & Completeness & Philosophy for more on Intuitionistic Logic). Because the logic can be easily changed just by using different axioms, systems like these are often used by logicians experimenting with alternative logical systems.

However, actually constructing proofs in this system can be very difficult.

As an example, try to prove that “a” implies “a”. Have a look at the Wikipedia page on Hilbert Systems if you get stuck.

(You'll get at least one of the formulas in the proof being left unresolved as Xnn, because the proof isn't enough to fully determine exactly how the variables in the axioms are used.)

This proof system is hard to use because it does not allow explicitly for reasoning where we temporarily make assumptions that we later include into our formulas. Every statement in the proof needs to explicitly list all of its assumptions. Indeed, looking at the S axiom, we can see that it has the same form as MP, except that (a) it uses implication instead of being a rule, and (b) it has an extra assumption A throughout.

Natural Deduction is an alternative proof system that incorporates temporary assumptions into the logic directly, making it much easier to use. Natural Deduction is the kind of system we will use in this course.