502 – Formal systems (2)

August 31, 2009

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

Read the rest of this entry »