THE LOGIC NOTES

7   Metalogic: The View from Above

In this chapter, we take a fresh look at reasoning by considering the theory of logic itself as an object of study. We ask whether it is fit for purpose, and sharpen this question to the one of whether the systyem of derivations is formally correct, and whether it is strong enough to capture all the inference forms it should capture. The material here is more mathematically sophisticated than that in the other chapters, so it is not expected that every reader will want to venture here, but for those who do, the proofs are not as hard as they may seem, and the rewards in terms of understanding are great.

So far, we have developed first order logic in two ways: syntactically by means of a proof system and semantically using a system of models. The question that arises immediately is whether the two are in fact one, whether the same sequents are valid semantically as are provable by means of the rules. The answer is 'yes'. This answer comes in two parts. Firstly, every provable sequent is valid. This fact is called the soundness of the proof system with respect to the semantic definition of validity. It amounts to the correctness of the rules IMPI, ORE, etc. given the model-theoretic account of what the expressions mean. Secondly, and conversely, every (semantically) valid sequent is also derivable in the proof system. This is the completeness of the rules, for it amounts to their having left nothing out.

Soundness is much easier to show than completeness, and is treated first. Completeness, however, is our main goal. In fact, we like it so much that we prove the completeness of propositional natural deduction four times! Following that, we consider extending the completeness proof to full first order logic, though the complexity of the quantified case is such that the proof is not easy to read in one pass.

There are several reasons for proving soundness and completeness.

  1. Since the two notions of entailment coincide, any rationale supporting one can be enlisted in support of the other. Thus on the one hand the truth table for inclusive disjunction which is obviously correct can be used to justify the rule ORE which might otherwise be rather obscure, while on the other hand the truth table for implication which is somewhat under-motivated is supported by whatever lent credibility to the rules IMPI, ANDI, RAA etc.

  2. In the propositional case, truth tables give an easy decision procedure for validity of sequents. This transfers via the completeness theorem to a decision procedure for provability, giving us a way of checking whether sequents are derivable or not.

  3. Even in the quantified case, although there is no decision procedure, semantic methods such as tableaux enable us to show in many cases that sequents are invalid, and hence unprovable. Mere failure to find a proof in the deductive system cannot show this, as it could always be because we didn't think of all the clever ways the proof might have gone, or because we gave up too soon.

  4. In particular, soundness assures us that the proof system is in several senses consistent. Minimally, not everything can be proved in it! More strongly, there are formulas (such as contradictions) none of whose substitution instances are theorems.

  5. Sequents were so defined that they may have any number of premises (up to the number of formulae in the language). In particular they may have literally no end of them. Since all derivations are finite, clearly a sequent with infinitely many premises is provable only if there is some finite subset of its premises from which the conclusion follows. On the semantic definition of validity, it is not obvious that every valid sequent has a valid finite sub-sequent. The completeness theorem, however, delivers this useful result for free.

  6. A test for validity, especially a slick one such as a semantic tableau, often gives information not just as to whether a sequent is valid but also why it is valid. We find out what prevents it from having a falsifying interpretation, and by studying this we may get hints as to how it might be proved. Proofs often simulate semantic reasoning in a way which must be picked up from examples.

The sequent calculus also stands in need of a proof of completeness. As noted in the earlier chapter, this comes in the form of a proof that the cut rule is admissible—completeness follows, as every natural deduction rule can be emulated quite easily in the sequent calculus, so every sequent with a natural deduction proof also has a sequent calculus proof. We close this chapter with a proof of cut elimination, the Hauptsatz of proof theory.

The Cut Elimination Theorem was called the Hauptsatz, the "main proposition", by Gerhard Gentzen (1909—1945), the originator of the sequent calculus, in recognition of its fundamental importance.