(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

[jcreed.livejournal.com]

can you parse this for me? Is this the core of the paragraph: "The ability to discriminate is a "tool" that the constructivists don't want to cast aside." ?

Yeah, sorry for writing such dense sentences :) You got the core right, yes. I'm trying to claim that actually there's no easy way to tell whether constructive or nonconstructive logic is more "right" by applying the principle "let's use all the tools we can". This is because a constructivist can tell you the ability to discriminate between things that are true constructively and things that are true only nonconstructively is a "tool", and a classicist will tell you the extra axioms are "tools".

Then it comes down to a sort of question of whether it's mathematics' job to prove fewer things, or more things. In the extreme, it's neither. We don't want to include all of our axioms A in every statement, publishing long-titled papers like, "if you assume the axioms of blah, bloo, blee, and so forth, then 1 = 1". We also don't want to include so many axioms that we derive false statements --- but now we're back arguing whether excluded middle and AC are "true".

It seems very reminiscent to me of arguments between languages with very strict typing disciplines, and languages with "lots of language features", I'm thinking in particular objects, aspects, macros, etc., things that let you do "more things" to existing programs. The people that advocate the former are interested in being able to write fewer wrong programs, and the people that advocate the latter are interested in being able to write more programs.

Ideally we want to write more, and more correct programs, and write more, and more certain proofs, but I'm not sure how to do this.

[gustavolacerda.livejournal.com]

I'm trying to claim that actually there's no easy way to tell whether constructive or nonconstructive logic is more "right" by applying the principle "let's use all the tools we can". This is because a constructivist can tell you the ability to discriminate between things that are true constructively and things that are true only nonconstructively is a "tool", and a classicist will tell you the extra axioms are "tools".

Which is why we need Logical Frameworks :-) Since neither classical logic nor intuitionistic logic will give you all the information, it may become necessary to look at it from the meta-level.