[FOM] Formalization Thesis

[hendrik@topoi.pooq.com]

On Fri, Jan 04, 2008 at 10:39:11AM +0100, Andrej Bauer wrote:
> 
> And just a quick comment: Timothy picked ZFC as an example. People who
> actually work on formalization know that having powerful type-theoretic
> infrastructure is absolutely necessary to keep things organized (imagine
> having 3000 lemmas...). So they use type theory instead. For example,
> pairs are typically a primitive notion, because that is just more
> convenient. Because most modern proof asistants (Coq, Isabelle) can
> easily encode ZFC, as well as ZFC + your favorite large cardinals, as
> well as intuitionistic mathematics, temporal logic, etc., it would be
> better to discuss the formalization thesis in terms of such type
> theories. I am just pointing out that the practice of formalization
> requires a great deal of "logic engineering" (that logicians are not
> used to) that is invisible in ZFC.

This variety of inequivalent formalizations is, I think, the weak point 
in the informalism.  The Formalization Thesis is evidently named by 
analogy with Church's thesis.  But the point of Church's Thesis was that 
although many formalisations of the idea of "computation" had been 
proposed, they all turned out to be equivalent.  No such equivalence 
between different formalization of mathematics seems evident here.
On the contrary, we have many inequivalent formalizations, and no 
agreement on the truth of some canonical or maximal one seems to be even 
remotely in sight.

-- hendrik