![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
guslThere 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).
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
(no subject)
Date: 2005-02-28 11:59 pm (UTC)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.
Perhaps English is irremediably vague
Date: 2005-03-01 01:07 am (UTC)I also like your overall goal here. Metaphorically, it sounds a lot like some of the thought processes that happen in my head when going from an idea of what I want a computer program to do, to actually writing the program.
This is an open problem in computer science (or, if you like, "computer engineering"). The complaint is that too much of software development is an art when it (or at least parts of the process) could be formalized into something that you'd call engineering.
If you are interested a concrete example of an almost "provable" method of software development, I'll suggest a book called Database Design for Mere Mortals by Michael J. Hernandez. I have actually used the methods outlined in this book to train a non-programmer, non-technical person to do database application development! The process described by the book begins with gathering information in conversational English, and then applying small, mechanical, formal steps to that input in a way that transforms and reduces it to an idealized, relational database model, which can then be used as the core of the desired application.
I think that computer code and the English language are difficult tools to use to build anything formalized, and for the same reason: too many choices, too many different ways to do the same thing. I think that by the time you get part of the way through "connecting English words to concepts in the formal knowledge system", what you'll really have done is invented a new intermediate language between English and a formal knowledge system. (Not that that's a bad thing.)
But maybe there's another natural language out there that it would be better to start from instead of English. Translating ideas into that language would be a step towards formalizing them.
Re: Perhaps English is irremediably vague
Date: 2005-03-01 07:22 am (UTC)Dijkstra quote
Date: 2005-03-01 05:24 pm (UTC)Being abstract is something profoundly different from being vague... The purpose of abstraction is not to be vague, but to create a new semantic level in which one can be absolutely precise. -- E. Dijkstra
What you're looking for is the correct abstraction for a logical argument. Now, the core of logic is probably pretty well established and extensively studied, I believe. What might be more interesting, and has to date been untractable, is the way that arguments ramify when you take into consideration the fact that manipulated representations are dynamically found to not match the represented reality closely enough. Even in classical logic, you get some ramification. Just imagine having to add subjective evaluations to the matter. They add a whole new world of potential break downs, and it would be interesting to exhibit the structure of the space of such break downs (and ways to cope with them).
My bet is that when you take the mismatch into account, you end up having few universal things to say anymore. Basically, logical tautologies and praxeological truths. The rest depends deeply on subjective evaluations for which you have no universal meter -- except action in the real world. Now, that does not mean that there is no possible universal processes for reasoning, that may be approximated on computer. Things like Solomonoff induction might be good models for building generic intelligences able to argue meaningfully. But even these models won't free you from having to commit to subjective choices concerning the way you evaluate arguments.
(no subject)
Date: 2005-03-02 02:38 am (UTC)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.
(no subject)
Date: 2005-03-02 02:57 am (UTC)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.
(no subject)
Date: 2005-03-02 05:16 am (UTC)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.
(no subject)
Date: 2005-03-05 05:51 pm (UTC)I'm pretty confident that Gödelian weirdness wouldn't get in the way here. Do you have any reason to believe it would?
(no subject)
Date: 2005-03-05 05:57 pm (UTC)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.
(no subject)
Date: 2005-03-05 10:39 pm (UTC)(no subject)
Date: 2005-03-05 10:48 pm (UTC)¬∃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!
(no subject)
Date: 2005-03-05 10:49 pm (UTC)tangent about Gödel's incompleteness
Date: 2005-03-06 02:33 am (UTC)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.
Re: Dijkstra quote
Date: 2005-03-06 02:56 am (UTC)What does reverse mathematics have to do with ramification? The fact that it's more "Babylonian"?
Cool quote
Date: 2008-05-09 10:09 am (UTC)Show me a man who is a good loser and I'll show you a man who is playing
golf with his boss.
----------------------------------------------------------------------------------------------------
http://blurty.com/users/arturocaseygq