[FOM] Formalization Thesis

[Wojtek Moczydlowski]

On Thu, 3 Jan 2008 joeshipman at aol.com wrote:

> I repeat my earlier challenge: can anyone who disputes Chow's
> Formalization Thesis respond with a SPECIFIC MATHEMATICAL STATEMENT
> which they are willing to claim is not, despite its expressiblity in
> English text on the FOM discussion forum, "faithfully representable" or
> "adequately expressible" as a sentence in the formal system ZFC?
>
> -- JS

"The program/lambda expression \lambda x. x, given any number n, returns 
the same number". A formalization in ZFC (though not in IZF, its 
constructive counterpart) takes away its computational nature: the 
possibility of actually running the program on the input.

As far as proofs are concerned, last time I checked, a faithful 
formalization of all proofs using Barendregt's convention (allowing one to 
pick in the proof a "fresh" bound variable when necessary, different from 
everything else in the context), was still an open problem.

Wojtek Moczydlowski