||[Apr. 16th, 2008|10:07 pm]
Hofstadter says that proofs and derivations are different:
A proof is something informal, or in other words a product of normal thought, written in a human language, for human consumption. All sorts of complex features of thought may be used in proofs, and, though they may "feel right", one may wonder if they can be defended logically. That is really what formalization is for. A derivation is an artificial counterpart of a proof, and its purpose is to reach the same goal but via a logical structure whose methods are not only all explicit, but also very simple.
But Wikipedia points them to the same place!
2008-04-17 07:48 am (UTC)
Hofstadter Man says a lotta things.
You're smarter than Wikipedia, Lindsey!
Everyone is both smarter and dumber than Wikipedia!
That's an interesting position to take, and I think one counter to common usage of the word. There's a lot of code out there designed to put together what he'd call "derivations", and they're typically called theorem provers, or something to that effect. Or what about "proof-carrying" code?
Maybe it'd make sense to have non-prose step-by-step proofs that are expanded out to the tiny axioms be called by a different name from the prose ones liberally sprinkled with "without loss of generality, we see that...", but I mean... typically you know what somebody means by context, right?
How do you feel about this?
I think that when he speaks of "derivations" he doesn't just mean non-prose and step-by-step. I think he means entirely mechanical, typographical string manipulation, no reasoning necessary -- in fact, no reasoning allowed.
I think this is kind of the crux of the whole mystery, right here. We act as though "thinking" systems and "not-thinking" systems are as different as night and day. But it turns out that they exist on the same continuum. Like night and day.
*nods* Yeah, totally!
When we say that something is a proof, I think we imagine that, in principle, it contains a derivation, or suggests one -- and if it doesn't, then it's not really a proof. The other direction, I think isn't as clear -- we hope that derivations end up corresponding to proofs that are easily expressible with prose that people can understand, but for a given theorem in a formal system, it might not be clearly expressible with people-friendly language...