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.
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:
A formal proof of the argument looks like this:
The horizontal and vertical lines indicate that this is a formal proof. Sentences above the horizontal line are premises, and every sentence below the line must follow from the premises by a rule, such as &Elim.
Every row or line of the proof is numbered. The numbers are used in the rules, to show what previous lines a rule refers to.
The rule used in this example is &Elim, which stands for conjunction "elimination". Notice that our premise is a & sentence: &Elim is how we use or "eliminate" the & in a conjunction sentence.
Whenever you use &Elim, you must cite exactly one sentence, which is the & sentence you are eliminating.
&Elim allows us to break a & down into its conjuncts, like how 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.
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 below the premise line (the horizontal line) must be justified by a rule.(The premises need no justification, since they are assumed in the proof.)
Think of the formal proof as a step-by-step justification of the conclusion from the premises, where the rules specify exactly which baby steps are allowed.
Unlike informal proofs, for formal proofs we will make explicit what rules are allowed.
All the lines between the premises and conclusion are intermediary conclusions which help us get to the final conclusion.
Now it's your turn to do a formal proof. Here's the argument:
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.
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.