Proof
Let f: N→N be the function defined by:
- f(#(θ)) = #(θ(#(θ))
for each T-formula θ in one free variable, and f(n) = 0 otherwise. The function f is computable, so there is a formula δ representing f in T. Thus for each formula θ, T proves
- (∀y) ,
which is to say
- (∀y) .
Now define the formula β(z) as:
- β(z) = (∀y) ,
then
- β(#(θ)) ⇔ (∀y) ,
which is to say
- β(#(θ)) ⇔ ψ(#(θ(#(θ))))
Let φ be the sentence β(#(β)). Then we can prove in T that:
- (*) φ ⇔ (∀y) ⇔ (∀y) .
Working in T, analyze two cases:
1. Assuming φ holds, substitute #(β(#(β)) for y in the rightmost formula in (*), and obtain:
- (#(β(#(β)) = #(β(#(β))) → ψ(#(β(#(β))),
Since φ = β(#(β)), it follows that ψ(#(φ)) holds.
2. Conversely, assume that ψ(#(β(#(β)))) holds. Then the final formula in (*) must be true, and φ is also true.
Thus φ ↔ ψ(#(φ)) is provable in T, as desired.
Read more about this topic: Diagonal Lemma
Famous quotes containing the word proof:
“Right and proof are two crutches for everything bent and crooked that limps along.”
—Franz Grillparzer (1791–1872)
“The insatiable thirst for everything which lies beyond, and which life reveals, is the most living proof of our immortality.”
—Charles Baudelaire (1821–1867)
“a meek humble Man of modest sense,
Who preaching peace does practice continence;
Whose pious life’s a proof he does believe,
Mysterious truths, which no Man can conceive.”
—John Wilmot, 2d Earl Of Rochester (1647–1680)