sequents and theorems

In proving the Law OfExcluded Middle in section 1 of chapter 10 we saw an example of a proof of a statement—or more accurately, a statement form—from no premises. This can occur because we can begin a proof with a supposition, which is discharged by the step of reductio ad absurdum at the end.

The existence of such proofs raises some interesting questions. First, we cannot have an argument with no premises, so what shall we say that such a proof has proved valid? Sec­ond, all we have done in this proof is to take a valid argument, show that the conjunction of all its premises entails its conclusion, and then Conditionalize the conclusion on this conjunction. Couldn’t we do that with any valid argument?

The answer to the second question is, yes, indeed we could. What this shows is that there is a very close relationship between an argument and the corresponding conditional whose antecedent is the conjunction of the argument’s premises, and whose consequent is the argument’s conclusion: if the conditional is logically true, the argument is formally valid; and if the conditional is logically false, the argument is formally invalid. Differently put, the argument is formally valid iff the conditional is true. (Can you prove that? Exercise 10).

done by introducing a symbol for entailment, the turnstile: H. This is to be read as asserting that the statements on the left of the Ή entail the statement on the right, or equivalently, that the statement to the right of the Ή follows from those (if any) on the left.

Thus the proof of the Hypothetical Syllogism (see chapter 7) establishes that

whilst the above conditional proof establishes that

The formulas (1) and (2) are called sequents. The two formulas on the left of the in (1) (which we may call the premises of the sequent) validly entail the one on the right (which we may call its conclusion); in such a case, we may call that sequent valid.

A sequent is an assertion that one statement or wff (the conclusion, written to the right of a turnstile) follows from a sequence of zero or more statements or wffs (the premises, written to the left of the turnstile and separated by commas).

Again, we know that (1) and (2) are valid sequents whatever statements might be sub­stituted for P, Q, and R, so long as they are consistently substituted. So, by analogy with the distinction between argument and argument form, we may define a sequent form:

A sequent form is an array of logical symbols containing statement variables rather than statements, such that a sequent is produced when statements are consistently

Thus (1) is an instance of the valid Sequentform

and (2) is an instance of the valid sequent form

Thus we have extended the meaning of validity so that it not only applies to arguments and argument forms, but also to sequents and sequent forms.

In a sequent form like (4), with nothing to the left of thethe statement form to the right of theis logically true, or, in logicians’ parlance, a tautology. (We shall examine tautologies in the next chapter, on truth tables.) The way we have set up statement logic, all such formulas are derivable by application of our rules of inference alone. They can therefore be regarded as theorems, as can any of the derived rules of inference.

A theorem is a sequent form with no premises, validly derived entirely by using the rules of inference.

12.2.2