## 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) 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.

### 4 Responses to 502 – Formal systems (2)

1. 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?

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

• Matt O'Dell says:

Did you mean to make this assignment due the 11th, or today?

• Matt O'Dell says:

Just a comment so I can get follow up emails.