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:
“It comes to pass oft that a terrible oath, with a swaggering accent sharply twanged off, gives manhood more approbation than ever proof itself would have earned him.”
—William Shakespeare (1564–1616)
“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 nation’s greatest strength, will tell their own story to the world.”
—Susan B. Anthony (1820–1906)
“If some books are deemed most baneful and their sale forbid, how, then, with deadlier facts, not dreams of doting men? Those whom books will hurt will not be proof against events. Events, not books, should be forbid.”
—Herman Melville (1819–1891)