502 – Formal systems (2)

Here is a different (more direct) presentation of the argument for Fact 2; the algorithm in the previous proof can be extracted from here as well:

Proof: We proceed by induction on the length of the proof to show that for all {n,} whenever a string has a proof from {\Sigma} of length at most {n,} then it has a proof of the required form.

This is clear if {n=1.} Suppose {\tau} has a proof {s} of length {n+1} and the result holds for all proofs of length at most {n.} If {\tau} is an axiom, it has a proof of length {1.} If in {s,} {\tau} is the result of applying the extension rule to some {\sigma,} then {\sigma} has (by the induction hypothesis) a proof {t} of the required form, and {t{}^\frown(\tau)} is a proof of {\tau} of the required form.

Finally, suppose that in {s,} {\tau} is the result of applying compression to {\tau0} and {\tau1.} By the induction hypothesis, {\tau0} and {\tau1} have proofs {s_0} and {s_1,} respectively, of the required form. If in {s_0} the extension rule is used, then it must in particular be used at the last step, so {\tau} appears in {s_0.} Restricting {s_0} to its initial segment that ends in {\tau} gives us a proof of {\tau} of the required form. Similarly with {s_1.}

We can then assume that extension is neither used in {s_0} nor in {s_1.} So, for {i\in2,} {s_i=t_i{}^\frown r_i,} where {t_i} consists of applications of the axioms rule, and {r_i} consists of applications of compression. Then {t_0{}^\frown t_1{}^\frown r_0{}^\frown r_1{}^\frown(\tau)} is a proof of {\tau} of the required form. \Box

Fact 2 is a key technical lemma; it will prove very useful in what follows.

Fact 3 Suppose that {\Sigma\cup\{\tau i\}\vdash\sigma} for both {i=0} and {i=1.} Then in fact {\Sigma\vdash\sigma.}

Proof: For {i\in 2} let {s_i} be a proof of {\sigma} from {\Sigma\cup\{\tau i\}} that follows the pattern described in Fact 2. If it exists, consider the first string in {s_0} that is the result of applying either compression or expansion to {\tau 0.}

If it is compression that is applied, then {\tau 1} is also a string in {s_0,} and it must appear in {s_0} before the first time {\tau 0} is used. This means that a suitable subsequence of {s_0} witnesses that {\Sigma\vdash \tau 1.} Since {\Sigma\cup\{\tau 1\}\vdash \sigma,} then in fact {\Sigma\vdash \sigma,} as we wanted to show.

A similar reasoning shows the same conclusion if compression is invoked the first time that {\tau 1} is used in {s_1.}

If {i\in 2} and {\tau i} is not used in {s_i,} then the subsequence obtained from {s_i} by removing from it the occurrences of {\tau i} due to the axioms rule, is a proof of {\sigma} from {\Sigma.}

The only remaining case is that {\tau i} is used in {s_i} for both {i=0} and {i=1,} and that the first such use is by applying the expansion rule. Recall now that both {s_0} and {s_1} are in the form dictated by Fact 2. This means that either both {\tau 0} and {\tau 1} are initial segments of {\sigma,} which is clearly impossible, or else for some {i,} both {\tau i} and the strings obtained from it by expansion, can be eliminated from {s_i} and still obtain a proof of {\sigma.} But then this is a proof from {\Sigma,} and we are done. \Box

Fact 4 If {\Sigma\vdash{\perp},} then there is a proof of {{\perp}} from {\Sigma} that only uses the axioms and compression rules.

Proof: If {\Sigma\vdash{\perp},} there is a proof of {{\perp}} from {\Sigma} as described in Fact 2. But then no applications of the expansion rule can occur in this proof, since {{\perp}} has no proper initial segments. \Box

Fact 5 If {\Sigma\vdash{\perp},} then there is an {n} and a {\Sigma_0\subseteq\Sigma\cap 2^{\le n}} such that {\Sigma_0\vdash\tau} for any {\tau} of length at least {n.} Moreover, there is a proof of {\tau} from {\Sigma_0} that only uses the axioms and extension rules.

Proof: Let {\Sigma_0} be a finite subset of {\Sigma} such that {\Sigma_0\vdash{\perp},} and let {n} be the maximum of the lengths of strings in {\Sigma_0.} To show that {n} and {\Sigma_0} are as required, it is enough to show that {\Sigma_0\vdash\tau} whenever {\tau\in2^n,} with a proof as required. Any larger string can then be deduced as well, by repeatedly applying the extension rule.

In order to show this, consider the set {\Sigma_1} consisting of all those strings derivable from {\Sigma_0} by proofs that use only the axions and compression rules. Note that {\Sigma_1\subseteq2^{\le n},} and that {{\perp}\in\Sigma_1,} by Fact 4. Given {\tau\in2^n,} let {\sigma\sqsubseteq\tau} be the largest initial segment of {\tau} that belongs to {\Sigma_1.} Note that there is such a {\sigma,} since {{\perp}\in\Sigma_1.}

We claim that {\sigma\in\Sigma_0.} If this is the case, we are done, since then {\tau} can be derived from {\Sigma_0} by a proof as required. To see the claim, note that otherwise, {\sigma0} and {\sigma1} are also in {\Sigma_1,} and therefore {{\rm lh}(\sigma)<n.} In particular, {\sigma\ne\tau,} and we must have that one of {\sigma 0} and {\sigma 1} is an initial segment of {\tau.} But this contradicts the maximality of {\sigma.} \Box

Note that, thanks to the compression rule, the converse also holds: If for some {n,} {\Sigma} proves every string {\sigma} of length {n,} then {\Sigma\vdash{\perp}.}

So far we have only studied the syntactic part of the tree system. Now we want to assign a meaning to the rules and strings. This corresponds to the semantic part of logic.

Given {\Sigma\subseteq 2^{<{\mathbb N}}} and {\tau\in 2^{<{\mathbb N}},} we write

\displaystyle \Sigma\models\tau,

which can be read as “{\tau} is true of {\Sigma}” or “{\Sigma} models {\tau},” or a variant of these expressions, iff whenever {x\in2^{\mathbb N}} and {\tau\sqsubset x,} then there is a {\sigma\in\Sigma} such that {\sigma\sqsubset x.}

This can be expressed topologically by saying that {\Sigma\models\tau} iff

\displaystyle \bigcup_{\sigma\in\Sigma} N_\sigma\supseteq N_\tau,

where {N_\sigma=\{x\in2^{\mathbb N}\mid \sigma\sqsubset x\}} for all {\sigma\in2^{<{\mathbb N}}.}

We want to relate the two relations {\vdash} and {\models.}

Here are some easy examples:

  • Something is true of {\Sigma} iff {\Sigma\ne\emptyset.}
  • {\Sigma\models{\perp}} iff for all {x\in2^{\mathbb N}} there is an initial segment {\sigma\sqsubset x} that belongs to {\Sigma.}

Note that the above also holds of {\vdash,} by Fact 5. In fact, we will show:

\displaystyle \Sigma\vdash\tau\quad\mbox{ iff }\quad\Sigma\models\tau.

Whenever a formal system satisfies the implication {\Rightarrow,} we say that it admits a soundness theorem. The idea is that the system is “sound” in the sense that everything that one can prove is actually true.

The direction {\Leftarrow} is called the completeness theorem. The system is “complete” in the sense that everything true is provable.

These are important properties, also shared by first order logic.

Theorem 1 (Soundness) Whenever {\Sigma\vdash\tau,} then also {\Sigma\models\tau.}

Proof: The argument is by induction on the length of proofs.

Suppose that {\tau} has a proof from {\Sigma} of length {1.} Then {\tau\in\Sigma,} and it is clear that {\Sigma\models\tau.} Assuming that any string provable from {\Sigma} in at most {n} steps is true of {\Sigma,} we show the same for {\tau} if it has a proof of length {n+1.}

If {\tau\in\Sigma,} we have the result. So we may assume that {\tau} comes from extension or compression. Suppose {\tau=\rho i} where {i\in 2} and {\rho} has a proof in {\Sigma} of length at most {n.} By the induction hypothesis, {\Sigma\models\rho.} Let {x\in 2^{\mathbb N}} and suppose that {\tau\sqsubset x.} Then also {\rho\sqsubset x,} and since {\Sigma\models\rho,} there is then some {\sigma\in\Sigma} that is an initial segment of {x.} This means that {\Sigma\models\tau.}

Suppose now that {\tau} comes from compression. Then both {\tau 0} and {\tau 1} have proofs from {\Sigma} of length at most {n,} and therefore {\Sigma\models\tau i} for {i=0,1.} Let {x\in 2^{\mathbb N}} and suppose that {\tau\sqsubset x.} Then {\tau i\sqsubset x} for either {i=0} or {i=1.} In both cases, there is then some {\sigma\in\Sigma} with {\sigma\sqsubset x.} This proves again that {\Sigma\models\tau,} and we are done. \Box

We will study the completeness theorem next lecture.

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

Advertisement

This entry was posted on Monday, August 31st, 2009 at 12:54 pm and is filed under 502: Logic and set theory. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.

4 Responses to 502 – Formal systems (2)

  1. Andrew Misseldine says:
    September 1, 2009 at 12:43 pm

    I’m completely stumped on exercise 3 part 4. I assume you want us to construct a function \sigma like in part 3, but I’ve tried and tried and can’t find the appropriate analog. Can we have some kind of hint?

    Reply
  2. andrescaicedo says:
    September 1, 2009 at 6:36 pm

    Hi Andrew, I’ve posted a hint as a separate entry.

    Reply

Leave a Reply

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

Gravatar
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 )

Cancel

Connecting to %s

%d bloggers like this: