[FOM] Formalization Thesis
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.
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.
FOM mailing list
FOM at cs.nyu.edu
More new features than ever. Check out the new AOL Mail ! -
More information about the FOM