Formalization is a rationality technique

post by Johnicholas · 2009-03-06T20:22:39.032Z · LW · GW · Legacy · 27 comments

Contents

27 comments

We are interested in developing practical techniques of rationality. One practical technique, used widely and successfully in science and technology is formalization, transforming a less-formal argument into a more-formal one. Despite its successes, formalization isn't trivial to learn, and schools rarely try to teach general techniques of thinking and deciding. Instead, schools generally only teach domain-specific reasoning. We end up with graduates who can apply formalization skillfully inside of specific domains (e.g. electrical engineering or biology), but fail to apply, or misapply, their skills to other domains (e.g. politics or religion).

A side excursion, to be used as an example:

Is it true that a real-world decision can be perfectly justified via a mathematical proof? No.

Here is one reason: Any real-world "proof", whether it is a publication in a math journal or the output of a computer proof-checker, might contain a mistake. Human mathematicians routinely make mistakes in publications. The computer running the proof-checker is physical, and might be struck by a cosmic ray. Even if the computer were perfect, the proof-checker might have a bug in it.

Here is another reason: Even if you had a proof known to be mistake free, mathematical proof always reasons from assumptions to conclusions. To apply the proof to the real world, you must make an informal argument that the assumptions apply in this real-world situation, and a second informal argument that the conclusion of the proof corresponds to the real-world decision. These first and last links in the chain will still be there, no matter how rigorous and trusted the proof is. The problem with duplicating real-world spheres with Banach-Tarski isn't that there's a mistake in the proof, it's that the real-world spheres don't fit the assumptions.

If you were fitting this argument into your beliefs, you might produce a number, a "gut" estimate of how likely this informal argument is wrong. Can we improve on that using the technique of formalization? What would a formalization of this argument look like? One possible starting point might be to rename everything. We're confident (via philosophy of logic) that renaming won't increase or decrease the quality of the argument. We will reason better about the correctness of the form if we hide the subjects of the argument.

Is it true that A? No.

Here is one reason: B is true (and B implies not A). Intuition pump. Intuition pump. Intuition pump.

Here is another reason: Even assuming B were false, C is true (and C implies not A). Intuition pump.

Note: there are many choices in this renaming process. It's not a trivial, thought-free operation at all. Someone else might get a completely different "underlying structure" from the same starting point. This particular structure suggests an equation, something like:

P( whole argument is wrong ) = P( first subargument is wrong ) * P( second subargument is wrong | first subargument is wrong )

The equation allows you to estimate the probability of the whole argument being wrong, using two "gut" estimates instead of one. This is probably an improved, lower-variance estimate.

The point is:

27 comments

Comments sorted by top scores.

comment by HalFinney · 2009-03-06T23:08:28.709Z · LW(p) · GW(p)

It's a start, but I don't know that this rather superficial level of formalization really gets you anywhere useful. I think in practice you will need to learn the domain specific formalization techniques to make real progress. I know Robin has occasionally asked people making comments on economics to offer a formal model, and I for one would have no idea how to begin. In my own field of computer security, sometimes a proposal is met with a challenge to define a threat model, and again this often serves to silence the amateurs.

In fact there is a danger that demands for formalization end up being a way of excluding those who are not members of the club.

Replies from: John_Maxwell_IV
comment by John_Maxwell (John_Maxwell_IV) · 2009-03-07T02:04:46.063Z · LW(p) · GW(p)

Perhaps a better response to the forays of amateurs would be to define a formal model that represents your understanding of their argument, explain it to them, and see if they agree that it's accurate.

Replies from: jimrandomh
comment by jimrandomh · 2009-03-07T02:43:45.481Z · LW(p) · GW(p)

That's a lot of work to respond to an amateur's argument with. Probably at least an order of magnitude more work than went into the original argument. And the formal argument is likely to end up being very different from the original, informal one; it would be very frustrating to take someone's informal argument, formalize it, show that the formal version of the argument is incorrect, and then be told that your formalization missed some important insight.

Replies from: John_Maxwell_IV
comment by John_Maxwell (John_Maxwell_IV) · 2009-03-07T04:55:26.347Z · LW(p) · GW(p)

Really? Maybe I'm just naive. Could you give me an example of an argument and its formalization?

Replies from: Tyrrell_McAllister
comment by Tyrrell_McAllister · 2009-03-09T19:01:03.566Z · LW(p) · GW(p)

Good examples of this include the efforts of posters on the newsgroup sci.math to make sense of arguments by math cranks who believe that they've proved the denumerability of the reals or what have you.

comment by Annoyance · 2009-03-07T15:11:41.492Z · LW(p) · GW(p)

An argument need not be formal if it is precise and specific and clear. Those are the properties that formalism attempts to bring to arguments. The traditional forms are fine and good, and even better because they're generally understood, but they're not strictly necessary.

If you can be precise, specific, and clear, in a way that isn't traditionally formal, that's just fine.

Replies from: Johnicholas
comment by Johnicholas · 2009-03-07T16:15:26.695Z · LW(p) · GW(p)

Suppose someone was striving to be precise, specific and clear, but didn't have any good ideas for moving in that direction. Would you suggest "try to formalize it" as an idea-generator?

Replies from: Annoyance
comment by Annoyance · 2009-03-07T16:24:52.491Z · LW(p) · GW(p)

No. The set of precise, specific, and clear ways to express an idea is much, much larger than the set of formal ways (which are arguably a subset of the larger group). Generally, it's easier to hit a very large target than a narrow one. And if you don't know how to hit the set, hitting a subset will probably be even harder.

Precision and clarity precede the formal versions of themselves, in the same way that people used the principles of logic long before they were explicitly recognized and formalized. If Aristotle didn't already understand those principles, he could never have generated formal logic, which is the rational examination of them. If you don't understand the ideas clearly, you won't be able to formalize them.

Replies from: Johnicholas
comment by Johnicholas · 2009-03-07T16:52:11.068Z · LW(p) · GW(p)

I have had good experiences sharpening my ideas by striving to formalize them, into propositional or predicate logic, into running code, or (more recently) into bayesian networks.

Of course, formalization as a technique for improving arguments may not be useful for everybody.

comment by GregRansom · 2009-03-09T01:27:57.628Z · LW(p) · GW(p)

There is a DEEP fallacy here, discussed in the work of Thomas Kuhn, Ludwig Wittgenstein and the work of philosopher Larry Wright on formal and informal reasoning, and in the work of Friedrich Hayek on explanation in economics.

Think about how formalization gave Carnap a massively false view of science and knowledge. Think how formalization made math economists believe that socialism was possible, and the an equilibrium construct was an "economy" or somehow provided an explanation (there are many more examples of how formalism made philosophers of science and economists stupid, but those should be enough for an educated person to "get it".)

Formalize also massively falsified the nature of language, mind, and reasoning for most analytic philosophers over the last 100+ years -- a bit of reading of Wittgenstein should help one understand this.

Wright shows the strengths -- and limitations -- of formalization in argument, and points out at the bottom is something identified in Kuhn and Wittgenstein, i.e. experience, training, good judgment, practice, etc., all stuff NOT formalizable -- there is no 'ultimate' math or logical metric that can capture everything in a number or in a formalism.

On all this I might in particular recommend Larry Wright, "Argument and Deliberation: A Plea for Understanding", Journal of Philosophy.

Replies from: michael_webster, Johnicholas, Tyrrell_McAllister
comment by michael_webster · 2009-03-27T15:52:16.501Z · LW(p) · GW(p)

Greg, I don't think we are given enough information here to call this a fallacy.

However, I probably side with your overall skepticism about how formalism is used and abused.

The foundations of mathematical modeling are simple to state.

A good model is: a) a formal translation of informal language, of b) truth functional elements, that c) preserves validity of the home language inference.

Unfortunately, many thinkers leave out c) all together, are ignorant of b)'s limitations, and do not think about a).

Some conscious effort along the lines of a-c would improve our modeling in general.

If anyone wants to see a concrete but tinker toy example of a-c, consult any introductory text on formal logic and the rational reconstruction of material implication as a translation of the English "if, then." All the elements are shown clearly.

comment by Johnicholas · 2009-03-09T19:26:45.794Z · LW(p) · GW(p)

Would you recommend trying to formalize an argument, as a way of making it more precise, specific, and clear? Contrariwise, would you recommend avoiding formalization?

comment by Tyrrell_McAllister · 2009-03-09T18:55:33.103Z · LW(p) · GW(p)

On all this I might in particular recommend Larry Wright, "Argument and Deliberation: A Plea for Understanding", Journal of Philosophy.

Here's a link to that article on JSTOR.

Replies from: Cameron_Taylor
comment by Cameron_Taylor · 2009-03-10T15:50:44.256Z · LW(p) · GW(p)

Thanks, I'll take a look.

comment by grobstein · 2009-03-07T01:39:06.275Z · LW(p) · GW(p)

Formalizations that take big chunks of arguments as black boxes are not that useful. Formalizations that instead map all of an argument's moving parts are very hard.

The reason that specialists learn formalizations for domain-specific arguments only is because formalizing truly general arguments[FN1] is an extremely difficult problem -- difficult to design and difficult to use. This is why mathematicians work largely in natural language, even though their arguments could (usually or always) be described in formal logic. Specialized formal languages are possible and useful only because they describe radically stripped-down models of the world.

Overall, this means that -- while moves like the example in the post probably are helpful -- we shouldn't expect to go much further in this direction.


[FN1]To be precise, formalizing truly general arguments in a way that simplifies and clarifies is hard. There is a trivial formalization for every argument, since the class of arguments is equinumerous with the natural numbers; the decision process can be a symbolic representation of a bunch of experts' brains or something like that.

comment by Cameron_Taylor · 2009-03-08T04:39:34.000Z · LW(p) · GW(p)

like it

comment by John_Maxwell (John_Maxwell_IV) · 2009-03-07T00:48:10.108Z · LW(p) · GW(p)

Let's say I believe that proposition A has probability Pa of being true. Then I am informed of an argument B which has a probability P~b~ of being true. Although argument B implies proposition A, proposition A does not imply argument B. How should I adjust P~a~ for various values of P~b~?

comment by Cyan · 2009-03-06T22:24:04.755Z · LW(p) · GW(p)

P( whole argument is wrong ) = P( first subargument is wrong ) * P( second subargument is wrong | first subargument is wrong )

P( whole argument is wrong ) is not P( first subargument is wrong AND second subargument is wrong), so the above conditional probability decomposition is incorrect.

Replies from: Johnicholas
comment by Johnicholas · 2009-03-06T22:37:13.780Z · LW(p) · GW(p)

Could you expand? I don't follow you.

Replies from: John_Maxwell_IV, John_Maxwell_IV
comment by John_Maxwell (John_Maxwell_IV) · 2009-03-07T00:37:26.003Z · LW(p) · GW(p)

Let's say I am arguing that the sky is blue because the aliens have landed and that's the color they painted it. The probability of the aliens having landed is very low, and the probability of the aliens painting the sky blue given that they've landed is also fairly low, but the probability of the sky being blue is quite high.

In other words, incorrect arguments in favor of a proposition don't make the proposition less likely.

comment by John_Maxwell (John_Maxwell_IV) · 2009-03-07T00:42:33.109Z · LW(p) · GW(p)

For the argument to be wrong, only one of its subarguments has to be wrong. So the correct equation is

P(whole argument is wrong) = 1 - P(first subargument is right) * P(second subargument is right | first argument is right)

Replies from: MBlume, jimrandomh, Cameron_Taylor
comment by MBlume · 2009-03-07T02:18:48.007Z · LW(p) · GW(p)

I don't believe he's speaking of two subarguments which together imply the main argument, but two subarguments each of which independently implies the main argument. Thus, they would both have to be false

Replies from: Cameron_Taylor, Cyan
comment by Cameron_Taylor · 2009-03-10T15:53:14.172Z · LW(p) · GW(p)

That's right. Unless one has negative relevance. Happens all to often.

comment by Cyan · 2009-03-07T02:36:18.183Z · LW(p) · GW(p)

The logical operator between the two subarguments was ambiguous -- I assumed the total argument would be something like a lemma and a theorem that depends on the lemma, not a disjunction of propositions.

comment by jimrandomh · 2009-03-07T02:45:24.110Z · LW(p) · GW(p)

If the arguments are chained together, then this is true, but the original poster was talking about independent lines of reasoning leading to the same conclusion. For arguments which are truly independent, then his formulation is correct.

Replies from: John_Maxwell_IV
comment by John_Maxwell (John_Maxwell_IV) · 2009-03-07T04:59:33.997Z · LW(p) · GW(p)

Alrighty, I gotcha.

comment by Cameron_Taylor · 2009-03-10T15:52:09.368Z · LW(p) · GW(p)

Not quite. You can combine the arguments together in all sorts of ways.