Date: Jun 13, 1996 8:22 PM
Author: Alberto C Moreira
Subject: Re: Concrete and Abstract in Mathematics, was "What's wrong with education..." (john baez) wrote:
>In article <> Alberto C Moreira <> 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

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

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

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 ?