"Formalization of Science"

[gusl]

When your placeholders are #6 and #7 on Google and the placeholder on your old page is #10, you know there's a lot of work to be done in this area.

There seem to be plenty of people saying that formalization projects aren't interesting or worthwhile, so I'll give them a chance to convince me. The reason I left physics (and much of the reason I "left" mathematics) is because we didn't have a formal way of talking about things. Since there was no logical calculus to appeal to, I could never ultimately convince my teacher that she was wrong (this was in high school). About one year later, my classmate Eivind managed to out-rhetoric me and convince her.

This same sort of thing could be happening in top-level scientific debates today. If we did have formal logic in science, we probably wouldn't have so many controversies.

Comments

[spoonless.livejournal.com]

he reason I left physics (and much of the reason I "left" mathematics) is because we didn't have a formal way of talking about things.

What do you mean by "there's no formal way?" I thought mathematical proofs were about as formal as you can get.

I agree with you that formalization is often important--I often think about how we ought to clean up philosophy and make it as formal as physics and math. The first step would be to agree on a more consistant vocabulary, instead of each philosopher using his/her own terms to define things. Does this fit in to anything you're saying? Or is it unrelated?

[gustavolacerda.livejournal.com]

99% of proofs in mathematics are informal, and so are most logic proofs. In formal proofs, every step is a direct consequence of things that have been derived before / assumed (be they axioms, hypotheses or more direct consequences of the two above).

The problem is exactly capturing the semantics. A consistent vocabulary is a good place to start. Eventually maybe you can develop a system for talking about a lot of physics in logical form.

One professor of mine believes that while it's possible to formalize very specific domains, physics theories are not integrated / don't have a clear interface, so formalizing a general theory is not possible. I think he's a pessimist, but then again I'm an optimist.

The idea of formalizing a general theory is that you could feed a problem in the logical language and the logic (hopefully embodied in a computer) has a derivation for your solution. Existing physical theories already tell you (to some extent) how to solve problems, so it's a matter of making them formal, so that the computer can do the problems for you.

Look up "qualitative physics".

Aside about formal theories:
If you encode set theory into your system, all theorems of mathematics can be derived. There is an algorithm which is complete (all theorems get derived), while the theory still being undecidable, since there is no bound on the size of proofs (unprovable true statements are not theorems)

[spoonless.livejournal.com]

99% of proofs in mathematics are informal, and so are most logic proofs. In formal proofs, every step is a direct consequence of things that have been derived before / assumed (be they axioms, hypotheses or more direct consequences of the two above).

When you say informal, do you mean done by a human rather than theorem-proving software? I was under the impression that a proof in math was not a proof, unless every step is a consequence of previously derived theorems... even if the application of the theorems are expected to be known already to the reader.
Are you just arguing that there are too many in-between steps ommitted? If there's anything ommitted, I think it's usually because it's obvious. Physicists aren't nearly as rigorous, of course. But the focus in physics isn't really on proving things, it's on explaining things.

One professor of mine believes that while it's possible to formalize very specific domains, physics theories are not integrated / don't have a clear interface, so formalizing a general theory is not possible. I think he's a pessimist, but then again I'm an optimist.

Theories in physics have definitely become more and more integrated. As to whether they will ever be fully integrated formally, I can't say--but I too am an optimist.

The idea of formalizing a general theory is that you could feed a problem in the logical language and the logic (hopefully embodied in a computer) has a derivation for your solution. Existing physical theories already tell you (to some extent) how to solve problems, so it's a matter of making them formal, so that the computer can do the problems for you.

Most of the work done in physics, though, isn't deduction. That would be fine for taking an existing well-laid-out theory and getting a computer to solve computationally-intensive problems--but mostly that works well already. The difficult part of physics is in creatively coming up with new axioms and new laws to explain new observations. Computers will not be able to do anything like that for a long time--and I don't think it's because of a lack of formalization, it's because induction is fundamentally different from deduction--the idea of revising your axioms to have new, better ones, is not likely something that could be done within a formal logic system.