In the last chapter we learned how to create informal proofs. In this chapter and the next we learn how to create formal ones. This is the final feature we will add to BOOL: a formal proof system.

The final feature we will add to BOOL: * a formal proof system*.

Once we add formal proofs, we’ll have a complete logical system. We’ll then start looking at its applications.

To learn formal proofs, we start with this argument:

1. (P&Q)&R

Thus,

2. P

A formal proof of this argument looks like this:

1. (P&Q)&R

2. P&Q

3. P

Premise

&Elim;1

&Elim;2

Essentially, a formal proof is a table with three columns that follows certain rules.

In its essence, a formal proof is a sort of table with three columns and several rows. In the first column we have a list of line numbers.

In the second column, we have sentences of BOOL. And in the third column, we have a list of citations that justify each sentence.

For example, &Elim is the citation rule that justifies lines 2 and 3.

Justifying premises is easy: Premise

Justifying premises is easy. We just write: Premise!

It is key that every row or line of the proof is numbered, because the numbers are used in the rules, to show what previous lines a rule refers to.

**&Elim: **how to use or “eliminate” a wide-scope conjunction.

The rule used in this example is &Elim, which stands for conjunction “elimination”.

Notice that our premise (P&Q)&R is a & sentence: &Elim is how we use or “eliminate” the & in a conjunction sentence.

Now you try it. Create a proof from ((P&Q&R)&S)&T to R.

Whenever you use &Elim, you must cite exactly one sentence, which is the & sentence you are eliminating. A semicolon always goes between the rule name and the line numbers it cites. Like in the sentences of BOOL, there are never spaces in the citations. So we write, for example: &Elim;1

&Elim allows us to break a & down into its conjuncts, like how in the first proof we infer P&Q on line 2 from (P&Q)&R on line 1.

You might think that “eliminate” is an inaccurate name, since line 2 still has a & in it. But notice that it does not have the & that was wide scope in (P&Q)&R. We used or “eliminated” that one.

&Elim allows you to bring down either conjunct.

But don’t think “elim” means we’ve destroyed line 1 and can’t use it again. If we wanted to, we can use &Elim again to prove the other conjunct, R.

The last line of the proof is always the conclusion. It must also be justified by a rule. In fact, every line of the proof must be justified by a rule, even if that means just stating which lines are the premises by labeling them with “Premise”.

Think of the formal proof as a step-by-step justification of the conclusion from the premises, where the rules like &Elim specify exactly which baby steps are allowed.

Unlike informal proofs, for * formal proofs* we will make explicit what rules are allowed.

Unlike informal proofs, for * formal proofs* we will make explicit what rules are allowed. That’s what all the citations are in the third column of the table.

All the sentences between the premises and conclusion are * intermediary conclusions* which help us get to the final conclusion.

Now it’s your turn to write out a formal proof. Here’s the argument:

1. S&(T&U)

Thus,

2. U

Don’t worry that the line numbering will change. The line number of the conclusion in an argument and proof will only be the same if it’s a one-step proof.

Three lines is the shortest way to do that proof. You cannot just skip to U with &Elim, because of this key fact: all the rules only apply to the main connective.

All formal proof rules only apply to the main connective.

So when you apply &Elim to S&(T&U), you can only get one of the conjuncts of the wide-scope &. Once you get the sentence T&U, then you can use &Elim to get to U.

In long and complicated proofs sometimes it’s easy to get lost or confused. So we’ll show you now a graphical device that will be useful later on.

You learned in Chapter 1 that a horizontal line can be used to separate the premises from the conclusion of an argument. We’ll build that into the graphical version of the proof.

The horizontal line tells us that everything above it is a premise, and everything below it must be justified by one of the other rules like &Elim.

The vertical line indicates how far the premises extend. As long as that vertical line is unbroken, you are allowed to cite any of the line numbers above a sentence.

When you add the graphical lines to a proof, there will always be a vertical line from the premises all the way down to the end of the proof, because the premises are always “live” or available to use. But we’ll see later on that some complicated proofs have additional vertical lines which only govern parts of the proof.

Login

Accessing this textbook requires a login. Please enter your credentials below!