More on the König-lemma system

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 ${\Sigma }^{+}$ that cannot derive $\sigma$ 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 $n$ for which $\Sigma$ contains all strings of size $n$). 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 $\Sigma \subseteq 2^{*}$ such that $\Sigma ⊬\sigma$ and wish to find a maximal such ${\Sigma }^{+}$ extending $\Sigma$. This can be done by an induction, as follows.

Let ${\Sigma }_0=\Sigma$ and enumerate all $\tau \in 2^{*}$ as ${\tau }_0,{\tau }_1,\dots$. Now define ${\Sigma }_{i+1}$ as follows. Inductively assume ${\Sigma }_i⊬\sigma$ and consider ${\tau }_i$. If ${\Sigma }_i\cup \left\{{\tau }_i\right\}⊬\sigma$ let ${\Sigma }_{i+1}={\Sigma }_i\cup \left\{{\tau }_i\right\}$ and if not let ${\Sigma }_{i+1}={\Sigma }_i$. Of course the inductive assumption holds for $i+1$ too, i.e. ${\Sigma }_{i+1}⊬\sigma$, so this construction continues for all $i$. Finally let ${\Sigma }^{+}={\bigcup }_{i\in \mathbb{N}}{\Sigma }_i$.

Note that the final set ${\Sigma }^{+}$ obtained will depend on the particular choice of enumeration of $\tau \in 2^{*}$ we started with.

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 $\Sigma \models \sigma$ is that $\Sigma$ traps us at $\sigma$ in the sense that if we are at $\sigma$ in the tree $2^{*}$ we have no escape to infinity $P$ which is an infinite path containing $\sigma$ and avoiding all elements of $\Sigma$. To vary this slightly we can modify our idea of a route that we are willing to escape on.

Thus an escape from $\sigma$ is an infinite tree for which no branching is allowed before $\sigma$. Any infinite path containing $\sigma$ is an escape from $\sigma$. In this way, all infinite paths are escapes, but not conversely.

Since an infinite path is an escape, this clearly implies the previous notion: $\Sigma {\models }^{+}\sigma$ implies $\Sigma \models \sigma$.

Note too that the completeness theorem as previous stated and proved in the book shows $\Sigma \models \sigma$ implies $\Sigma ⊢\sigma$, so these three notions, provability and the two semantic entailments, are all equivalent.

Now suppose $T$ is an infinite tree. Let $\Sigma =T^c$ be the set of strings not in $T$. Then obviously $\Sigma {⊭}^{+}\perp$ as there is an escape from $\perp$, $T$ itself, containing $\perp$ that does not meet $\Sigma$. It follows by the equivalences just proved that $\Sigma ⊭\perp$, meaning there is an infinite path $P$ containing $\perp$ that does not meet $\Sigma$. In other words $P$ is an infinite path which is contained in $T$, 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, $\Sigma \models \sigma$ implies $\Sigma ⊢\sigma$, in the special case when $\Sigma$ is finite. It goes like this. Suppose $\Sigma \models \sigma$, that $\Sigma$ is finite, and that $n\in \mathbb{N}$ is greater than the length of all $\tau \in \Sigma$ and greater than the length of $\sigma$. Suppose $\rho \in 2^{*}$ has length $n$ and has $\sigma$ as an initial part. Then any infinite path through $\rho$ contains $\sigma$ and cannot contain any $\tau \in \Sigma$ of longer length. Since $\Sigma \models \sigma$ this means that $\rho$ must contain some $\tau \in \Sigma$ as an initial part. In other words all such $\rho$ can be obtained from $\Sigma$ by the Given and Lengthening rules only. Since all such $\rho$ extending $\sigma$ can be so derived from $\Sigma$, then so can $\sigma$ be derived by deriving all these $\rho$ and then using the Shortening rule to get $\sigma$.

It's nice to see that this proof also constructs a proof of $\sigma$ from $\Sigma$, and one in which all the Given rules come first, then all the lengthening rules, and then all the shortening rules.