[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] [Timothy Y. Chow] Re: [FOM] Formalization Thesis



On Sun, 30 Dec 2007, Jesse Alama wrote:


I thought that I would draw the attention of the mizar community to a
discussion now taking place on the FOM (Foundations of Mathematics)
mailing list, in which mizar figures.  The forwarded message is but one
element of the thread; the entire thread can be seen at

 http://cs.nyu.edu/pipermail/fom/2007-December/thread.html

by looking for messages whose subject involve the word "formalization".
I'd be curious to hear the responses of some of the mizar cognoscenti in
connection with these issues.
I think the "mizar cognoscenti" are busy formalizing math, regardless of whether it's considered possible by someone or not :-). One major point about formal math is that it can be transformed very easily. So if someone comes up with new super-cool foundations for math (and this is what various type-theorists tell us twice a day :-), we will very likely just translate the current corpus to it, do some serious debugging of the new (and old) formalism during the process, and continue formalizing. 


I've been trying to make sense of the objections that have been posed to
the Formalization Thesis so far.  There is one strand of argument that
seems to run through several of the responses, which I will call the
"Inexhaustibility Objection."  Roughly speaking, the Inexhaustibility
Objection runs as follows:

"For the Formalization Thesis to be at all interesting, you must fix some
particular formal system.
I'd say that it is already the notion of mathematical proof which requires at least one particular formal system. Without being able to point out to at least one such formal system which fits your proof, you don't really have a mathematical proof (just a bunch of interesting ideas, which may eventually lead to a proof). 


 But whatever formal system you choose, it is
straightforward to write down truths that are not provable in that system.
For example, if you pick ZFC, then we could pick Con(ZFC) or any number of
more mathematically interesting statements.  In addition, if you pick ZFC,
then you commit yourself to translating all mathematics into set theory,
and the process of doing so will inevitably add or subtract some
conceptual content.  Mathematics is inexhaustible both in the sense that
its truths are not computably enumerable, and in the sense that people
come up with completely new concepts all the time.  Therefore there is no
reason to believe in the Formalization Thesis."
From this I'd gather that the claim is something like "there can be no
formal framework for all of math". That surely depends on the definition of "all of math", and also "formal framework". For instance, isn't already natural language in which a "proof" is written a kind of formalism, which might not fit certain "proofs" in e.g. Ramanujan's head? 


Formalization Thesis, "Mizar version": The correctness of anybody's claim
to have proven such-and-such a theorem of ordinary mathematics can be
checked by Mizar.
E.g. for constructive math Mizar is too strong. Then you can obviously model constructive formal system inside set theory. Is it good enough?
From a practical piont of view, I'd say not. If you want to formalize in
special foundations, use a system which is suitable for them (or specify such system in some metasystem like e.g. Isabelle if possible). 

Josef