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:
“If any proof were needed of the progress of the cause for which I have worked, it is here tonight. The presence on the stage of these college women, and in the audience of all those college girls who will some day be the nations greatest strength, will tell their own story to the world.”
—Susan B. Anthony (18201906)
“Ah! I have penetrated to those meadows on the morning of many a first spring day, jumping from hummock to hummock, from willow root to willow root, when the wild river valley and the woods were bathed in so pure and bright a light as would have waked the dead, if they had been slumbering in their graves, as some suppose. There needs no stronger proof of immortality. All things must live in such a light. O Death, where was thy sting? O Grave, where was thy victory, then?”
—Henry David Thoreau (18171862)
“If any doubt has arisen as to me, my country [Virginia] will have my political creed in the form of a Declaration &c. which I was lately directed to draw. This will give decisive proof that my own sentiment concurred with the vote they instructed us to give.”
—Thomas Jefferson (17431826)