502 – Formal systems (3)

Theorem 2 (Completeness) Whenever {\Sigma\models\tau,} then also {\Sigma\vdash\tau.}

Proof: We prove the contrapositive. Assume that {\Sigma\not\vdash\tau.} We will find an {x\in 2^{\mathbb N}} that extends {\tau} and does not extend any {\sigma\in\Sigma.}

Towards this end, enumerate all finite strings as

\displaystyle \{\sigma_i\mid i\in{\mathbb N}\}.

Let {\Sigma_0=\Sigma.} We define a sequence {\Sigma_0\subseteq\Sigma_1\subseteq\dots} by recursion as follows:

  • Given {\Sigma_i} with the property that {\Sigma_i\not\vdash\tau,} let {\Sigma_{i+1}=\Sigma_i,} unless {\Sigma_i\cup\{\sigma_i\}\not\vdash\tau} either, in which case, let {\Sigma_{i+1}=\Sigma_i\cup\{\sigma_i\}.}

Now let {\Sigma'=\bigcup_i\Sigma_i} and note that {\Sigma'} satisfies the following properties:

  1. {\Sigma'\not\vdash\tau,} by construction and compactness.
  2. For any {\sigma\in2^{<{\mathbb N}},} {\sigma\in\Sigma'} iff {\Sigma'\cup\{\sigma\}\not\vdash\tau.}The left-to-right implication is clear from (1). The other direction holds by construction: If {\sigma=\sigma_i} and {\Sigma'\cup\{\sigma\}\not\vdash\tau,} then certainly {\Sigma_i\cup\{\sigma\}\not\vdash\tau,} and therefore {\sigma\in\Sigma_{i+1}\subseteq\Sigma'.}
  3. In particular, {\tau\notin\Sigma'.}It is actually {\Phi=2^{<{\mathbb N}}\setminus\Sigma'} that interests us. In terms of {\Phi,} property (3) says that {\Phi\ne\emptyset.}
  4. {\Phi} is a tree.To see this, suppose that {\sigma i\in\Phi,} where {i\in2.} Then, by property (2), {\Sigma'\cup\{\sigma i\}\vdash\tau.} But then, certainly, {\Sigma'\cup\{\sigma\}\vdash\tau} so, by (2) again, {\sigma\in\Phi.} This shows that {\Phi} is closed under initial segments.
  5. {\Phi} is actually a branch, i.e., {[\Phi]} is a singleton.To see this, suppose that {\sigma\in\Phi.} We need to show that there is a unique {i\in 2} such that {\sigma i\in\Phi.}

    Since {\sigma\in\Phi,} then {\Sigma'\cup\{\sigma\}\vdash\tau.} Suppose first that both {\sigma 0} and {\sigma 1} are in {\Sigma'.} Then, by compression, {\Sigma'\vdash\sigma,} and therefore {\Sigma'\vdash\tau,} a contradiction.

    Suppose now that neither {\sigma 0} nor {\sigma 1} is in {\Sigma'.} Then {\Sigma'\cup\{\sigma i\}\vdash\tau} for both {i=0} and {i=1.} It then follows, using Fact 3 from last lecture, that {\Sigma'\vdash\tau,} again a contradiction. This gives the result.

Finally, let {x} be the unique element of {[\Phi].} Note that {x} extends {\tau,} since {\tau\in\Phi.} Note also that {x} extends no element of {\Sigma,} since no element of {\Sigma} is in {\Phi,} and the initial segments of {x} are precisely the elements of {\Phi.} This proves that {\Sigma\not\models\tau.} \Box

This is the reason why this formal system is called a tree system; both because of this argument, and because of the relation that it implies between this system and König’s lemma, as we will see below.

To illustrate the interplay resulting from the equivalence of the two relations {\vdash} and {\models,} consider the following two proofs:

Corollary 3 {2^{\mathbb N}} is compact.

Proof: Given a covering of {2^{\mathbb N}} by open sets, let {\Sigma} be the collection of strings {\sigma} such that the basic open set {N_\sigma} is completely contained in one of the open sets in the covering.


\displaystyle 2^{\mathbb N}=N_{\perp}\subseteq\bigcup_{\sigma\in\Sigma}N_\sigma,

and it follows that {\Sigma\vdash{\perp}.} Therefore {\Sigma_0\vdash{\perp}} for some finite subset {\Sigma_0} of {\Sigma,} so {\Sigma_0\models{\perp},} and any finite collection of open sets in the covering that contain the sets {N_\sigma} for {\sigma\in \Sigma_0} constitutes a finite subcovering of {2^{\mathbb N}.} \Box

It is not, of course, that the compactness of {2^{\mathbb N}} is a deep result. But the trivial argument just given helps explain some of the difficulties we found previously, since our results supersede this topological theorem.

Corollary 4 König’s lemma holds for infinite subtrees of {2^{<{\mathbb N}}}.

Proof: Given a tree {T\subseteq2^{<{\mathbb N}},} suppose that {[T]=\emptyset} and let {\Sigma=2^{<{\mathbb N}}\setminus T.} Then {\Sigma\models{\perp}} so, by completeness and Fact 5 from last lecture, there is a finite {\Sigma_0\subset\Sigma} and an {n} such that any {\sigma} of length {n} or larger extends an element of {\Sigma_0.}

Note now that {\Sigma} is closed under extensions, since {T} is a tree. It follows that {\Sigma=2^{<{\mathbb N}}\setminus T} contains all strings of {0}s and {1}s, of length {n} or larger. But then {T\subseteq 2^{<n},} i.e., {T} is finite. \Box

Typeset using LaTeX2WP. Here is a printable version of this post.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: