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$