email@example.com (john baez) wrote: >In article <DsqMAr.firstname.lastname@example.org> Alberto C Moreira <email@example.com> writes:
>>But when you create a formal system, don't you still have to remain >>within the boundaries of a meta-system ?
>Not in any *formal* meta-system, surely: I reason informally until I have >created a formal system with the desired properties. Then I reason >semi-formally within that system to check that it has the desired >properties, and to see what other cool things it spits out. But often >the most fun part, and the really hard work, comes before everything is >formal.
Eventually you will have to build all the formal bridges, except maybe your axioms. Of course, there's a lot of thought that can be done outside the formal frame; but at some time all must be tied down within a meta-system. I'm not disagreeing that one can reason outside the formal system, but that one can't have results outside it.
Also, you're talking at a level far beyond that which I was addressing. When doing mathematical research, one probably has to use whatever tools one has at his/her disposal, but learning it is another story. And when we're talking about teaching students, do we want to emphasize informal thought ? I'm not so sure about this, my computer science bias tells me the opposite, if nothing else because being "informal" inside a computer program quickly leads to chaos: it's too easy to subvert the rules of intuition and insight when we posess the capacity of establishing them to begin with.
>I'm no pure logician, but I certainly pop out of the formal frame >when I am sniffing my way towards interesting formalisms. Call me an >impure logician if you like; I suppose my work on category theory is a >form of logic highly contaminated by applications to mathematical >physics.
Logic itself is your frame, or isn't it ? I'm not at that level, but I have difficulty seeing any kind of mathematics that doesn't anchor itself in a logical frame. I know that category theory people, just like lambda calculus people, like to see category theory as a formal system par with set theory and others. But all three of them are still based on a logic system, or at least I do so far believe.
>What I'm doing is nothing new or surprising, by the way! Just think of >all the nonrigorous calculations Euler did to find nice formulas like > >1 + 1/4 + 1/9 + 1/16 + .... = pi^2/6 > >He wasn't reasoning in any formal system. Indeed, the whole obsession >with formal systems came much later, peaking around the beginning of the 20th >century. Luckily, mathematical physicists today are still no slaves to >formalism. Think of how Ed Witten won the Fields Medal, the biggest >math prize of all! His reasoning was not formal, and in many cases we >still don't know how to make it formal --- but his discoveries were >wonderful.
I hear you, and I don't totally disagree. Still, at some point in time they must come down to earth and grind the nitty-gritty; it's not easy to put out some result without a proof, it becomes a conjecture rather. And what's a proof if it isn't contained within a formal system ? I'm not familiar with the work of Ed Witten, are his proofs "informal", in the sense that they don't fit within a logic system ?