Completeness More about first order logic

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 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. It is proved rather laboriously by showing that none of the rules is capable of introducing an invalid sequent into a proof if all the previous lines represent valid sequents. Trivially, the rule of assumptions cannot introduce an invalid sequent. Now if there were a proof of something invalid then that proof would have to have an invalid line all lines above which were valid. That is, there would have to be a first point at which things went wrong. That "bad" line would have to come by one of the rules from one or more previous lines, so what has to be shown for soundness is that no rule can ever transform valid inputs into an invalid output. This is a matter of grinding through all the cases and is tedious but not difficult.

As an example, consider the most complicated propositional case, the rule ORE. We may suppose all three of its input sequents are valid. That is,

X ⊨ A OR B

Y, A ⊨ C

Z, B ⊨ C

We need to show on these suppositions that the output is valid:

X, Y, Z ⊨ C

Consider, then, any interpretation giving the value 1 to every formula in X, Y or Z. Since this makes everything in X true it must make A OR B true, in which case by the truth table for 'or' it either gives A the value 1 or gives B the value 1. If it gives A the value 1 then it gives 1 to everything in Y and to A, so by the second of our three suppositions it gives 1 to C. Similarly, if it gives 1 to B, by the third supposition it gives 1 to C. Either way C gets the value 1. In sum, any interpretation verifying all of X, Y and Z verifies C which is what we want.

As a second case, consider the rule ALLI. Suppose X ⊨ A and m is a name which occurs in A but not in any formula in X. Let v be a variable not occurring in A. We need to show that X ⊨ ALLv A^v_m. In fact, we argue the other way around, showing that if it is not the case that X ⊨ ALLv A^v_mthen it is not the case that X ⊨ A. Suppose, then that there is an interpretation I which is a model of X but for which ALLv A^v_mis false. By the modelling condition for the universal quantifier, this means that there is some m-variant J of I for which A is false. Since m does not occur in X, and I is a model of X, it follows that J is also a model of X. That is, there is an interpretation for which everything in X is true but A is false, showing that X does not (semantically) entail A. The cases of the other rules are all similar, only simpler. The upshot is that no rule can be responsible for the first invalid line in any proof. Since there is no first invalid line, there are no invalid lines at all. Hence every provable sequent is valid.

Showing completeness for quantified logic is beyond the scope of these notes. The basic technique is to consider an arbitrary unprovable sequent and give a recipe for cooking up an interpretation which invalidates it. In the case of orthodox classical logic this is not really difficult, but it does involve mathematical concepts not assumed as background to the present course, especially to deal with the case of sequents with infinitely many premises. There is a very careful treatment in Geoff Hunter's book Metalogic Hunter which is recommended for those who wish to see the thing done. For the present, my confident assertion that it works will have to serve (Proof by Authority).

Meanwhile, for those who wish to see how completeness proofs are constructed, here is a proof for propositional logic only.

There are several reasons for proving soundness and completeness.

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.

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.

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 unprovable. Mere failure to find a proof in the deductive system cannot show this.

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.

Sequents were so defined that they may have any number of premises.¹ In particular they may have literally no end of them. Since all derivations are finite, clearly a sequent with infinitely many premises is provable iff 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.

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.


¹ Up to the number of formulae in the language, of course!