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 whenever a string has a proof from of length at most then it has a proof of the required form.
This is clear if Suppose has a proof of length and the result holds for all proofs of length at most If is an axiom, it has a proof of length If in is the result of applying the extension rule to some then has (by the induction hypothesis) a proof of the required form, and is a proof of of the required form.
Finally, suppose that in is the result of applying compression to and By the induction hypothesis, and have proofs and respectively, of the required form. If in the extension rule is used, then it must in particular be used at the last step, so appears in Restricting to its initial segment that ends in gives us a proof of of the required form. Similarly with
We can then assume that extension is neither used in nor in So, for where consists of applications of the axioms rule, and consists of applications of compression. Then is a proof of of the required form.
Fact 2 is a key technical lemma; it will prove very useful in what follows.
Proof: For let be a proof of from that follows the pattern described in Fact 2. If it exists, consider the first string in that is the result of applying either compression or expansion to
If it is compression that is applied, then is also a string in and it must appear in before the first time is used. This means that a suitable subsequence of witnesses that Since then in fact as we wanted to show.
A similar reasoning shows the same conclusion if compression is invoked the first time that is used in
If and is not used in then the subsequence obtained from by removing from it the occurrences of due to the axioms rule, is a proof of from
The only remaining case is that is used in for both and and that the first such use is by applying the expansion rule. Recall now that both and are in the form dictated by Fact 2. This means that either both and are initial segments of which is clearly impossible, or else for some both and the strings obtained from it by expansion, can be eliminated from and still obtain a proof of But then this is a proof from and we are done.
Proof: If there is a proof of from as described in Fact 2. But then no applications of the expansion rule can occur in this proof, since has no proper initial segments.
Proof: Let be a finite subset of such that and let be the maximum of the lengths of strings in To show that and are as required, it is enough to show that whenever 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 consisting of all those strings derivable from by proofs that use only the axions and compression rules. Note that and that by Fact 4. Given let be the largest initial segment of that belongs to Note that there is such a since
We claim that If this is the case, we are done, since then can be derived from by a proof as required. To see the claim, note that otherwise, and are also in and therefore In particular, and we must have that one of and is an initial segment of But this contradicts the maximality of
Note that, thanks to the compression rule, the converse also holds: If for some proves every string of length then
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 and we write
which can be read as “ is true of ” or “ models ,” or a variant of these expressions, iff whenever and then there is a such that
This can be expressed topologically by saying that iff
where for all
We want to relate the two relations and
Here are some easy examples:
- Something is true of iff
- iff for all there is an initial segment that belongs to
Note that the above also holds of by Fact 5. In fact, we will show:
Whenever a formal system satisfies the implication 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 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 then also
Proof: The argument is by induction on the length of proofs.
Suppose that has a proof from of length Then and it is clear that Assuming that any string provable from in at most steps is true of we show the same for if it has a proof of length
If we have the result. So we may assume that comes from extension or compression. Suppose where and has a proof in of length at most By the induction hypothesis, Let and suppose that Then also and since there is then some that is an initial segment of This means that
Suppose now that comes from compression. Then both and have proofs from of length at most and therefore for Let and suppose that Then for either or In both cases, there is then some with This proves again that and we are done.
We will study the completeness theorem next lecture.
Typeset using LaTeX2WP. Here is a printable version of this post.