quotes: Babylonian vs Euclidean method, why physicists dread precision

[gustavolacerda]

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

Comments

[jcreed]

I pretty much agree with everything you're saying. There's a bit of a fallacy in Schwartz's comment --- maybe more than one.

First of all the idea that a heuristic for accepting or rejecting arguments is better the more permissive it is, is ridiculous. Though I want to believe that I'm just setting up a straw man, Schwartz does say "rightly dreads" not "rightly apporaches with caution" or something. Of course I acknowledge that we may, by demanding more formal, more rigorous proofs, throw out some arguments that (by our new standard) wrongly reach what were actually right concluisions. But there is always tension between (to use fundamentally like terminology from several fields) soundness and completeness, (from formal language transformations) between "safety" and "expressiveness" (from programming language design) between type one and type two errors, (from experimental psychology) between precision and recall (from machine learning).

There's always an opportunity for making mistakes saying "yes" when you should say "no" to an argument, and vice-versa.

So I claim he can't tout informal methods just because they allow more good arguments, because they allow more bad arguments too, but symmetrically I can't push formal methods just because they allow fewer arguments, because they may allow fewer good arguments, too.

The reason formal methods win, I think, is because the people working with them are actually succeeding at not trading off between "safety" and "expressiveness", but making progress increasing the former while maintaining the latter.

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. In any event, this strict completeness demand that Schwartz seems to want --- that every argument we accepted yesterday we had better accept in any new system --- is crap anyhow. What we really want is that every proposition that's really true "today" to still be just as provable "tomorrow" once we accept a new, more demanding standard of proof.

Now the thing is, I don't have much hope for showing that some formal system is propositionally complete in this sense, relative to the informal system of proofs that physicists, say (or any other such disciplinarians) use. But you could forge ahead and try to prove all the things you care about, and if you succeed, you know for sure you've proven at least "that much" completeness.

This is the move I want to make: to tighten your belt from a more informal system to a more formal system. Saftey/soundness ought to increase by design, and the fact that expressiveness/completeness is maintained (to a degree) can be shown, if true, constructively, by exhibiting proofs of all the important old theorems.

Compare this to the move the strawman physicist wants to make:
to relax from a more formal system to a more informal system. Expressiveness/completeness increases by design, by what in the world can be said about safety/soundness?? The physicist can exhibit a thousand proofs that were fallacious in the formal system and that are still fallacious to her informal intuition, but this does not convince me that there is no informal argument yet to be discovered that passes her intuitive test, but cannot be correctly formalized.

I believe this partial notion of completeness --- knowing we got at least so far in proving finitely many useful things --- and real soundness is far more useful than real completeness and "partial soundness", knowing only that we can think up some bad examples that indeed a system rejects.

[pbrane]

The physicist can exhibit a thousand proofs that were fallacious in the formal system and that are still fallacious to her informal intuition, but this does not convince me that there is no informal argument yet to be discovered that passes her intuitive test, but cannot be correctly formalized.

I think the point for physics is that we don't rely on "proofs" at all, really. We often 'prove' things to some degree of satisfaction using formal systems (renormalization of the Standard Model being a good example - Physics Nobel 2000), but we know that the real final arbiter of correctness for a theory is *experiment*: regardless how hokey and seemingly inconsistent a theory seems (mathematicians are pretty sure that QFT as a whole is inconsistent on numerous levels: each term in the perturbation theory is ill defined, even once regulated, the sum of the series diverges, and the defining generating function of the whole system is an integral with a completely undefined measure over an infinite dimensional space), if it produces predictions which are verified by precision experiments (like the 14 decimal places of accuracy that the standard model agrees to), we call it "right".

Continuing the analogy, mathematicians have been trying to formalize QFT for 50 years, without much success, and without any real contribution to finding new "truths" - at best, they've found slightly more reasonable proofs that some little piece of the edifice can be given another (more rigorous) definition which reproduces the same results as the old ill-defined one.

Formal systems are great - for mathematics, linguistics, computer science. But not for the physical sciences.

[jcreed]

So, I don't dispute that consistency with experiment is the right thing to be looking for. However, isn't there still a process that takes the a proposed model and derives what experimental predictions it actually makes? I think that process could (or, really, already does) benefit from improving and deploying more formal understanding. Just because QFT produces formal objects that are foreign to how mathematicians usually think about calculus doesn't mean that there isn't some consistent formal system that encapsulates our current physical theory in that domain.

If the mathematics is irreparably inconsistent (which I doubt) then it falls to mere intuition and the community social dynamics of physicists to even decide what the theory is predictably and what it isn't. But I bet instead that it's a very well-behaved formal system that just hasn't been exactly delineated yet.

[pbrane]

But I bet instead that it's a very well-behaved formal system that just hasn't been exactly delineated yet.

Certainly, I agree with you on this. My point is just that for all the work that mathematicians have done on trying to make advances in finding this well-behaved formal system, we've gained pretty much *no* new insights about physics, and have made no new predictions, and don't really have any new way of seeing what's going on.

There may be a perfectly consistent and well-defined formal system for QFT, but it may also not be as *useful* as the kludgey shorthand set of mnemonics we have now. I'm not saying that formal systems aren't interesting, or that physical law can't be encapsulated in one, I'm just saying that it may not be terribly efficient or productive (in discovering new physics or understanding old).

This is not to say, of course, that *abstraction* isn't useful in physics - it's *immensely* useful, as it allows the condensing of messy systems into more basic components. But making sure that these basic components are all well defined and interact consistently has historically not been that necessary for the gains that are made by the initial ill-defined abstraction process.

[gustavolacerda]

There may be a perfectly consistent and well-defined formal system for QFT, but it may also not be as *useful* as the kludgey shorthand set of mnemonics we have now.

We can, of course, have formal systems that are less mathematically elegant (for example, using redundant axioms)... my dream is precisely to make such systems are natural as possible to use in practice: make them correspond to intuition.

Once formal systems match the way physicists do their thing (i.e. when formal language is close to natural language), then the machines can be used to support scientists in their reasoning... and maybe eventually take over their job.

[gustavolacerda]

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]

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]

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]

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]

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.