[FOM] Formalization Thesis
wojtek at cs.cornell.edu
Fri Jan 4 19:23:33 EST 2008
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.
More information about the FOM