quotes: Babylonian vs Euclidean method, why physicists dread precision

[gusl]

There are two kinds of ways of looking at mathematics... the Babylonian tradition and the Greek tradition... Euclid discovered that there was a way in which all the theorems of geometry could be ordered from a set of axioms that were particularly simple... The Babylonian attitude... is that you know all of the various theorems and many of the connections in between, but you have never fully realized that it could all come up from a bunch of axioms... Even in mathematics you can start in different places... In physics we need the Babylonian method, and not the Euclidian or Greek method.
— Richard Feynman

The physicist rightly dreads precise argument, since an argument which is only convincing if precise loses all its force if the assumptions upon which it is based are slightly changed, while an argument which is convincing though imprecise may well be stable under small perturbations of its underlying axioms.
— Jacob Schwartz, "The Pernicious Influence of Mathematics on Science", 1960, reprinted in Kac, Rota, Schwartz, Discrete Thoughts, 1992.

When I say I'm an advocate of formalization, I'm not saying we need to understand all the precise details of what we're arguing for (although this usually is the case in mathematics, at least more so than in physics). What I want to do is to formalize the partial structure that does exist in these vague ideas. Favoring a dynamic approach, I hold that we must accept formalizing theories in small steps, each adding more structure. We will need "stubs", and multiple, parallel stories to slowly evolve into a formal form. The point is that a vague, general idea *can* be formalized to a point: this is evidenced by the fact that we humans use precise reasoning when talking about them.
Again, the idea is about doing what humans do, formally. If the humans' idea is irremediably vague, we don't hope to do any better, but we do hope to formalize it as far as the ideas are thought out / understood (even if vaguely). To the extent that there exists a systematic (not necessarily "logical", but necessarily normative) in the way we reason and argue, it will be my goal to formalize this in a concrete form.

Regarding the normative aspect, the reason we need one is: not all ideas make sense! For fully-formalized mathematics (i.e. vagueness-free mathematics), it's easy to come up with a normative criterion: a mathematical idea or argument is fully-formalized if it corresponds to a fully-formal definition or a fully-formal proof. One of the challenges of this broader approach is to define what it means for an idea to "make sense": what does it attempt to do? What is its relation with related concepts?

The "natural" medium expression of these ideas is English. The idea is to connect English words to concepts in the formal knowledge system. We say an English sentence makes sense in a given context iff it addresses the goal / there is sound reasoning behind it (not all may be applicable).

Comments

[gustavolacerda.livejournal.com]

That is, just because a physicist's favorite argument for proposition X turns out to be incorrect under close formal scrutiny, if X is really true, then it probably has a proof in a reasonable formal system, barring, of course, some sort of Gödelian weirdness.

I'm pretty confident that Gödelian weirdness wouldn't get in the way here. Do you have any reason to believe it would?

[jcreed.livejournal.com]

No, I just fear the gods of formal logic will strike me down for hubris when I get dangerously close to saying something like "everything that's really true ought to be provable" :)

[jcreed.livejournal.com]

Although, maybe an intuitionsit would say that Gödel's theorem is not true: the setup of the proof gives you a sentence G that has the shape

¬∃n.(n is the gödel-number of a proof of this proposition)

So you reason that if G is provable, then the sentence (call it H for which G = ¬H)

∃n.(n is the gödel-number of a proof of this proposition)

is provable, and you can derive ⊥. And supposing ¬G is provable, well, by double-negation-elimination, then H is true, so G has a proof, so you get ⊥ also.

So if your logic is intuitionistic, it might be that ¬G ( = ¬¬H) is provable, but H is not. Probably other people have throught this through more thoroughly than I am thinking about it off the cuff right now. The other point to make is that even working in a logic that has classical axioms, the intuitionist may see no problem with neither G nor ¬G being provable despite G being 'true', because to her G isn't really true. The content of G is that it is a contradiction for G to be provable. Being able to show that adding ¬G is relatively consistent, we know that it is not a contradiction. The state of affairs where neither G nor ¬G are provable also has the property that neither proposition is (intuitionistically) true!

[jcreed.livejournal.com]

Whoops, I didn't mean to say that an intuitionist wouldn't think his theorem is true (if it's applied to a classical logic) but that it isn't perhaps as interesting.

tangent about Gödel's incompleteness

[gustavolacerda.livejournal.com]

Speaking as someone who knows little about this stuff, I want to say that I (currently) find Gödel's theorems unremarkable... All they say is that if you want to have a model of arithmetic, any sound theory of the model will be incomplete (i.e. there will be sentences true of the model which are not in the theory), which is fine with me. To be honest, I don't see why we want to have models at all...

I am really a formalist. So, by definition, the true things are those that follow from your axioms. So we have completeness by definition. I guess this is like a kind of intuitionism, since T |= A does not follow from ~ (T |= ~A) (analogous to intuitionism's "double negation is not affirmation"), which is equivalent to saying that it's not the case that forall A, T |= A or T |= ~A (analogous to intuitionism's "no excluded middle"). The Gödel sentences would be undecidable here, i.e. neither it nor its negation is true/provable.

How does the enumeration which you use to build the Gödel sentence connect to models of arithmetic? I'm gonna try to look this up.