my philosophy about expressivity

[gusl]

I wouldn't want to prove the Jordan Curve Theorem (a visually "obvious", but hard-to-prove theorem).

for the same reason that

a mathematician wouldn't want to *constructively* prove the Fundamental Theorem of Algebra.

(Freek interestingly likes the idea of the first project, but not the second one) (nice thoughts here... he expresses his vision of a natural medium for doing mathematics, analogous to a "Word Processor")


The reason is: for me, there is no reason to bend over backwards, just for the sake of minimality. If we have tools, why not use them?

While it's philosophically interesting to be able to derive everything from a minimal set of axioms, if you're trying to do practical things (whether they be science or phenomenology :-), so perhaps I shouldn't say "practical" ), and as long as you know your math is consistent (and truth-preserving?) it's irrelevant how many axioms you use.

This is analogous to finding the shortest possible way of coding a program, just to get a tight bound on the Kolmogorov Complexity of the problem: the tight bound may be a theoretically nice result, but you end up with an ugly hack: at least from the cognitive point of view, you've made things unintuitive / hard to understand and unwieldy.

This is my philosophy, and I think it's also the TUNES Philosophy.

Comments

[gustavolacerda.livejournal.com]

I'll be the first to admit that if I refuse to prove the Jordan Curve Theorem, then I should choose a set of higher-level axioms that will "easily" prove not just the JCT, but also similar problems.

I want an axiom system which reflects the simplicity of human reasoning in this domain (as well as other domains... this is a general interest of mine): if my thoughts are simple, the proof should be simple.

If to express my simple thoughts I need write complex code, then I consider this language to not be "expressive" enough.

simple: but wrong?

[bram.livejournal.com]

[This is similar to what rdore writes below.]

I think you may be in trouble here. Human intuition may not always be a good guide. We put together all the ingredients we think make sense, and out pops something like the Tarski-Banach theorem. Euclid's 5th postulate seems intuitive, but not intuitive enough. It seems like the kind of thing to prove from the other postulates or from a more basic postulate. It doesn't seem as if it should be independent from the axioms, a pick-and-choose semi-intuitive result, but it is.

My working guess is that our intuitive math is not reliable, that although in many cases someone might think something is obvious, other things we think obvious might just be wrong. Formalization was not only a way to prove things, it was a common ground for people with differing intuition to explore the exact consequences of their ideas.

Resolution to the Banach-Tarski paradox

[gustavolacerda.livejournal.com]

Well, I consider the Axiom of Choice to be "true", so I have to accept Banach-Tarski. But some people think it's not so bad:

from http://www.kuro5hin.org/story/2003/5/23/134430/275:

...
In fact, if we assume that spheres are not infinitely divisible, then the Banach-Tarski paradox doesn't apply, because each of the "pieces" in the paradox is so infinitely complex that they are not "measurable" (in human language, they do not have a well-defined volume; it is impossible to measure their volume)
...
Bingo! There is no paradox here after all. We are merely seeing the logical consequence of mathematical sets like S being infinitely dense. In fact, if you think about it, this is not any stranger than how we managed to duplicate the set of all integers, by splitting it up into two halves, and renaming the members in each half so they each become identical to the original set again. It is only logical that we can continually extract more volume out of an infinitely dense, mathematical sphere S.
...

If you had a constructive proof AND measurable sets (i.e. a sphere being partitioned (even if infinitely) into *measurable* sets), then I would certainly be in trouble. If you had an existence proof I'm not sure... I'll confess being insecure in my intuition here.

Re: Resolution to the Banach-Tarski paradox

[bram.livejournal.com]

Heh, I think that's similar to the way Feynman "solved" it in Surely You're Joking Mister Feynman--there he has a rant about self-satisfied mathematicians and their "counterintuitive" results that are not so counterintuitive. The example he gives is IMHO a thinly veiled Tarski-Banach "paradox".

I'd claim not so much that you're wrong but that guided by intuition it's easy to set up a mathematical system and say, "This expresses my intuition," then look at the detailed consequences and say, "Oh, back up, this sphere lacks a special property that the spheres in my imagination have."
...
So you slice something up, the intermediate states after slicing have no defined volume, and then they are put together to have a defined volume that is larger than the original sphere. Still, I think most people have an intuition that doing something (even if it's infinitely delicate) to a sphere can't result in a sphere with twice that volume.

Re: Resolution to the Banach-Tarski paradox

[gustavolacerda.livejournal.com]

Re: Feynman, I remember reading that... the mathematicians where foolish enough to call it an "orange".

Indeed, our intuition is sometimes logically inconsistent (btw, I had dreams about math and physics a couple of times, and the math one was total nonsense... I wish I could have this sort of dream again), but what I am concerned with is being able to express them anyhow.

I do think, though, that intuition can be "debugged", even before it is expressed formally. You can look at things more carefully in your minds' eye, or you can rotate your point of view, whatever.

This, of course, is evidence that intuition exists, and that people reason at that level.

Of course, writing things a formal language, gives a better guarantee of correctness.

I'm wondering if the concept of "faithful interpretation" has something to do with multiple representations in mathematics.

[rdore.livejournal.com]

Are you saying your ability to visualize is good enough that you can see any simple closed curve? Maybe you can only visualize curves which are say piecewise smooth or something.

That something seems obvious does not mean that it's true.

[gustavolacerda.livejournal.com]

Maybe you're right. But even for piecewise smooth curves, it seems that if you want to prove it from a standard foundation, you will need a way to express geometrical concepts symbolically. While this can be done rather easily, it's not clear that the intuitions can be naturally translated as well. (I thought that the JCT was a good example of this, but now I'm not sure)

What bothers me about it is not being able to talk simply about simple concepts, not being able to easily formalize what I see right in front of me.

[(Anonymous)]

So it's not clear to me whether you don't think the Jordan Curve Theorem deserves a mathematical proof in the traditional style (like the proof that you can read under http://www.cs.kun.nl/~freek/jordan/newman/ (http://www.cs.kun.nl/~freek/jordan/newman/). Or that you agree that that traditional proof has its place, but that you don't think it's interesting to formalize it. Because those are two different things!

I think most mathematicians will take the second position. But your blog entry sounds like the first.

Freek

[gustavolacerda.livejournal.com]

Ok. This has nothing to do with formalization.
So I'm indeed defending a radical position. Zeilberger might agree with me, but maybe nobody else.

I think the proof of the JCT has its place, but only because it assures a minimality of axioms. We would like to be able to automatically add all "obvious" things to our mathematics, but if we add them as axioms this is not very elegant.

So here I'm assuming that it's safe to say that that the JCT is a priori true, i.e. that you would be reasonable in claiming its truth even if you didn't know that a proof had been found. But we believe that a geometric interpretation is faithful, don't we?


MY REASONING IS ROUGHLY...

INTUITION FORMAL MATHEMATICS (i.e. normal mathematics)

JCT-geometric ---C--> JCT-formal
^ ^
| |
B D
| |
axioms of
visual <-----A------ axioms of mathematics
system

Given A, B, C
A: interpretation
B: visual theorem, obtained by intuitive reasoning (visual logic?)
C: reinterpretation
D: provability relation

The idea is that humans are equipped with graphics-acceleration... so our visual reasoning serves as an oracle for certain mathematical statements about geometry.

I wish these ideas were worked out. Maybe it's what I should do!

[(Anonymous)]

Gustavo:
So here I'm assuming that it's safe to say that that the JCT is a priori true, i.e. that you would be reasonable in claiming its truth even if you didn't know that a proof had been found.


I don't agree. I think that if the JCT was not provable, then the counterexamples to it would show where our intuition was "wrong".

It's like saying that obviously a surface has two sides, that that doesn't need proof. And then a Moebius strip or a Klein bottle really are interesting, aren't they?

Or, different example, there was this Kant character who claimed that space (the real space of reality out there) obviously had to be Euclidean, no possibility for it to be otherwise. To bad for him that Einstein showed him to be wrong :-)

Freek

[gustavolacerda.livejournal.com]

I don't agree. I think that if the JCT was not provable, then the counterexamples to it would show where our intuition was "wrong".

You seem to be assuming that if the JCT were not provable, there would be a counterexample. What about when the system is too weak to prove it?

My view is that in our mathematical world, it is *necessarily* the case (i.e. in all possible worlds where geometry/topology are interpreted the way they are now) that the JCT cannot have a counterexample. (though I'll grant that perhaps I don't understand the JCT very well)
What I'm saying is that there's something fundamental about geometry... that there exist "geometric truths" independent of which foundation you choose (of course you can have weird geometries, but then this violates the condition that "geometry/topology are interpreted the way they are now").

Mathematicians, however, seem to be slaves to formalism: the truth only exists in the realm of formalism. My view, instead, is that the role of formalisms is model the "physical truth" of geometry, etc. (so I'm more like a scientist here, but this view also reflects the development of real mathematics: discoveries first, justifications (i.e. proper proofs) later)


It's like saying that obviously a surface has two sides, that that doesn't need proof. And then a Moebius strip or a Klein bottle really are interesting, aren't they?

ok. So we need to be *very*careful* when using intuitions. It's too easy for us to imagine a prototypical case, and rule out all other possibilities.
An "intuitive proof" is different from a "mathematical proof" because there's no way for the individual to communicate his knowledge. And self-skepticism is always healthy too, so maybe we can't really call it "knowledge"... But I also want to maintain that "intuititive mathematical knowledge" exists. I believe there is something fundamentally logical about intuitions, that they are more than mere heuristics.

[(Anonymous)]

You seem to be assuming that if the JCT were not provable, there would be a counterexample. What about when the system is too weak to prove it?

Of course that might happen too, but I consider that highly unlikely. 99.99% of the potential theorems that mathematicians consider can be proved or have a counter-example. Or at least, that's the way I experience it.

My view is that in our mathematical world, it is *necessarily* the case (i.e. in all possible worlds where geometry/topology are interpreted the way they are now) that the JCT cannot have a counterexample.

I don't share that intuition. Do you consider it possible to divide the plane in three parts such that the boundaries of those three parts are all the same? That happens to be the case (it's a theorem of Brouwer, I think), and that does not sound so different from having the possibility of a closed curve that divides the plane in n parts with n different from two. Which of course is not possible (that's the Jordan Curve Theorem): but my intuition about those two things is more or less the same.

Freek

[gustavolacerda.livejournal.com]

Ok. This has nothing to do with formalization.
So I'm indeed defending a radical position. Zeilberger might agree with me, but maybe nobody else.

I think the proof of the JCT has its place, but only because it assures a minimality of axioms. We would like to be able to automatically add all "obvious" things to our mathematics, but if we add them as axioms this is not very elegant.

So here I'm assuming that it's safe to say that that the JCT is a priori true, i.e. that you would be reasonable in claiming its truth even if you didn't know that a proof had been found. But we believe that a geometric interpretation is faithful, don't we?


MY REASONING IS ROUGHLY...

INTUITION FORMAL MATHEMATICS (i.e. normal mathematics)

JCT-geometric ---C--> JCT-formal
   ^                     ^
   |                     |
   B                     D
   |                     |
axioms of                |
visual <-----A------ axioms of
system               mathematics

Given A, B, C
A: interpretation
B: visual theorem, obtained by intuitive reasoning (visual logic?)
C: reinterpretation
D: provability relation

The idea is that humans are equipped with graphics-acceleration... so our visual reasoning serves as an oracle for certain mathematical statements about geometry.

I wish these ideas were worked out. Maybe it's what I should do!