[FOM] Formalization Thesis

joeshipman@aol.com joeshipman at aol.com
Tue Jan 8 17:58:52 EST 2008

On the contrary. The proposed equivalence consists of the following: 
given two formalizations of mathematics A and B, and given a statement 
X in formalization A, there exists a statement Y in formalization B 
such that mathematicians who work in formalization A will agree that a 
B-proof of Y entails the existence of an A-proof of X.

As stated, this is probably false, but if you restrict your attention 
to "classical logic" and "classical mathematics", and replace 
"existence of an A-proof" with "nonexistence of an A-disproof" I think 
it is true for all mathematically interesting X.

What do I mean by "mathematically interesting"? Let me give a 
counterexample. There is a function rank(X) from sets to ordinals 
defined by rank(X) = sup of rank(y) for y in X. "The rank of the 
Riemann Zeta Function is omega_plus_4" is has perfectly well-defined 
truth-value for any given formalization of sufficiently much analysis 
in ZFC, but the truth value depends on the formalization in a totally 
uninteresting way and I do not insist that this sentence have an 
equivalent in an alternate formalization of mathematics.

-- JS

-----Original Message-----
From: hendrik at topoi.pooq.com

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 
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 
remotely in sight.

-- hendrik
FOM mailing list
FOM at cs.nyu.edu

More new features than ever.  Check out the new AOL Mail ! - 

More information about the FOM mailing list