The system of Chapter 3 is in some sense a minimal logical system for propositional logic. (See example 7.28.) It is no real surprise that König's lemma arises straightforwardly from the Completeness theorem for this system, but perhaps the manner in doing this appears somewhat artificial. After all, we have used the full strength of König's lemma (and perhaps a bit more) in obtaining from Zorn's lemma the maximal set that cannot derive in the proof of Theorem 3.12. Nevertheless the proof of Theorem 3.13 is slighty curious in that it actually shows that a tree with no infinite paths is finite, and almost - but not quite - gives a bound on the size of the tree (via the number for which contains all strings of size ). I don't know if any more can be said in this direction.
For those that, perhaps rightly, think that there is something suspicious about this proof of König from Zorn, I offer here some alternatives.
First, the application of Zorn in Theorem 3.12 can be replaced by a more straightforward direct argument. We have such that and wish to find a maximal such extending . This can be done by an induction, as follows.
Let and enumerate all as . Now define as follows. Inductively assume and consider . If let and if not let . Of course the inductive assumption holds for too, i.e. , so this construction continues for all . Finally let .
Note that the final set obtained will depend on the particular choice of enumeration of we started with.
Exercise.
Show that, irrespective of the choice of enumeration of , the set is a superset of such that and if then .
Thus the maximal set can be constructed by a rather more direct means other than appealing to Zorn's lemma.
Now for an alternative derivation of König's lemma from the material given.
First, let us modify the definition of semantics for the system.
The intention behind the definition of
is that
traps us at
in the sense
that if we are at in the tree
we have no escape to infinity
which is an infinite
path containing and avoiding all elements of .
To vary this slightly we can modify our idea of a route that
we are willing to escape on.
Definition.
An escape from is an infinite tree containing for which the following holds: for each of length less than the length of , is an initial part of .
Thus an escape from is an infinite tree for which no branching is allowed before . Any infinite path containing is an escape from . In this way, all infinite paths are escapes, but not conversely.
Definition.
Let and . We write ( strongly entails ) to mean that for all escapes from we have .
Since an infinite path is an escape, this clearly implies the previous notion: implies .
Exercise.
Show that the soundness theorem also holds for the notion of strong entailment. That is: implies .
Note too that the completeness theorem as previous stated and proved in the book shows implies , so these three notions, provability and the two semantic entailments, are all equivalent.
Now suppose is an infinite tree. Let be the set of strings not in . Then obviously as there is an escape from , itself, containing that does not meet . It follows by the equivalences just proved that , meaning there is an infinite path containing that does not meet . In other words is an infinite path which is contained in , so König's lemma is proved.
Finally, for this web page, one student has pointed out to me that there is a very easy proof of the completeness theorem for this system, implies , in the special case when is finite. It goes like this. Suppose , that is finite, and that is greater than the length of all and greater than the length of . Suppose has length and has as an initial part. Then any infinite path through contains and cannot contain any of longer length. Since this means that must contain some as an initial part. In other words all such can be obtained from by the Given and Lengthening rules only. Since all such extending can be so derived from , then so can be derived by deriving all these and then using the Shortening rule to get .
It's nice to see that this proof also constructs a proof of from , and one in which all the Given rules come first, then all the lengthening rules, and then all the shortening rules.
Exercise.
Prove directly the assertion just implied, directly by induction on the length of derivations, that if there is a derivation of from consisting of three blocks: the first consisting of all applications of the Given rule; the second (which is possibly empty) consisting of applications of lengthening; and the third (again possibly empty) consisting of applications of the shortening rule.