(no subject)

[gusl]

To summarize my recents philosophical thoughts about formal mathematics & intuition:

(see http://www.livejournal.com/users/gustavolacerda/156135.html?nc=7 and http://www.livejournal.com/users/gustavolacerda/155299.html?nc=7)


* If we have tools, why not use them?

For the same reason that a mathematician wouldn't want to find a *constructive* proof of the Fundamental Theorem of Algebra, I wouldn't want to find a proof of the Jordan Curve Theorem (a visually "obvious", but hard-to-prove theorem).
(Freek interestingly likes the idea of the first project, but not the second one)


* While minimality is nice, "expressivity" is more important:

If in order to express my simple thoughts I need to write complex code, then I consider this language to not be "expressive" enough. The Jordan Curve Theorem is a good example of this: the standard mathematical foundation is not "expressive" enough: it takes a lot of work to prove that which we can see intuitively. Of course, this is a criticism of standard mathematical practice in general, not of any specific formalization programs. Grounding the JCT into foundations (i.e. proving it follows from the foundations) is necessary to maintain the minimality of the axioms, and thereby the "elegance" of the system.


WAYS IN WHICH FORMAL MATHEMATICS DOESN'T CORRESPOND TO REAL HUMAN MATHEMATICS

There are many languages for formal mathematics, but they often don't correspond to mathematicians' cognitive structures.

This is for the following reasons:

* These proofs are currently too low-level (proof plans, proof sketches are possible solutions to this)

* They don't model multiple representations, or semantics (while humans integrate symbolic & visual reasoning)

* They work from absolute mathematical foundations. As we know, real mathematics existed way before it was given good foundations. Human mathematicians work with relative foundations, and (sometimes) try to ground them later.


My vision: tag formal proofs with "chunks" / high-level concepts, analogous to the way texts are semantically tagged.
Create multiple, parallel formal proofs using different foundations, and hook them into each other (I suspect we will need something like Logical Frameworks to accomodate different foundations in a standard form. I think "faithful interpretations" may have a role to play here).

Comments

[gustavolacerda.livejournal.com]

A constructive proof of FTA has already been formalized in Coq, and in fact its PX was a notorious failure (the first approximation took a few hours, and was a "0"... the second approximation took even more hours and was "0" to a greater precision... and that was the last iteration it reached).

Then this might be incredibly satisfying then: a constructive proof of FTA without using the rationals.

[jcreed.livejournal.com]

Oh, wow! These look really cool. Thanks for the links.