# [FOM] Formalization Thesis

Wojtek Moczydlowski 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.

Wojtek Moczydlowski