Re: What do you know, and how do you know that you know it?

[hv]

Interesting meditation. :)

As for what I know that I know: I'd limit that to mathematics of a particular formal sort, that I've proved myself, along the lines of "given these axioms, and these rules of logic, this conclusion follows". I'd like to see a project to prove all known maths in this way, using declared rules of logic and steps small enough to permit computer verification - it boils down to nothing but symbolic manipulation. (I even registered "axiomattic.org" for a while, hoping to start the project myself.)

An important aspect of this approach is the definition of 'axiom'. Sometimes axioms are defined as "things that are so obviously true that they need no proof", but that is not how I use the term - if I did I'd have to deny all axioms. Instead, axioms are simply "the things assumed true for the purposes of this proof", and the result of a proof is "assuming these axioms and these rules, this necessarily follows".

Within the realm of programming, I had a very fortunate and salutary experience around 1991, when working on a 6800-based machine with 48K of RAM at a time when I was familiar with every line of code in the O/S. I encountered an unexpected error which halted the machine, and because of the limited RAM saving and printing out the entire core was a practical thing to do.

Tracking back from the location of the error showed that some memory had been corrupted ... by an error elsewhere, in which some memory had been corrupted ... by an error elsewhere, in which some memory had been corrupted ... in a very strange way. It turned out that one instruction had been changed from 0xA8 0x01 (LDAA+ 1 - load register A with the byte pointed to by the pointer register + 1) to 0xA9 xxx, an invalid opcode which nonetheless by symmetry should represent an instruction like 'STS#' - store stack immediate.

The processor had actually skipped a byte, then stored the stack pointer over the following two bytes, and the rest of the mayhem was caused by that. What changed the 0xA8 to 0xA9? Probably an alpha particle: examining that byte of memory showed that it had a parity error. (With the help of a colleague, I was able to account for every byte in memory other than that one.)

That experience in my formative years was very instructive: no matter how defensively you code, the fallibility of hardware means there are no guarantees, ever. This is why important applications use redundancy (see "#8: Why five computers?" under that link).

A couple of years later I learned another important lesson. By now I was writing C code for DOS and Windows, using Microsoft's compiler which was buggy as hell. Every few days I'd track down a problem, contact MS technical support, work my way through the layers of gap-toothed flunkeys determined to point me at a page of a manual I knew better than they, eventually get through to a hallowed programmer who'd (on a good day) look at my test case, confirm that it was a bug, and promise me that it'd be fixed in the next release - which was 6 months away, would cost me more money, and would introduce myriad new bugs.

After a while I noticed that my progress had slowed down purely because of my lack of trust in the tools - whenever my program failed to behave as expected, my first port of call was the debugger's facility to show the C code side by side with the generated assembler, to try and discover how the compiler had screwed up this time. But bad as the compiler was, the majority of the time the bug was in my code, and I wasted an awful lot of time ruling out the compiler each time before examining my own code.

So from this I learnt the importance of good tools (and the value, only realised when I discovered the open source community a few years later, of being able to fix the tools yourself). I also learnt that chances are, it's me that screwed up this time. And I learnt, more generally, that I (and by observation others) will always look first to blame anything other than our own code.

Update: s/cosmic ray/alpha particle/ after reading http://www.science.uva.nl/~mes/jargon/c/cosmicrays.html

Hugo

[thraxil]

I'd like to see a project to prove all known maths in this way, using declared rules of logic and steps small enough to permit computer verification - it boils down to nothing but symbolic manipulation.

it's called the Principia Mathematica. :)

[bunnyman]

As for what I know that I know: I'd limit that to mathematics of a particular formal sort, that I've proved myself, along the lines of "given these axioms, and these rules of logic, this conclusion follows". I'd like to see a project to prove all known maths in this way, using declared rules of logic and steps small enough to permit computer verification - it boils down to nothing but symbolic manipulation. (I even registered "axiomattic.org" for a while, hoping to start the project myself.)

What you describe sounds like Hilbert's Program. Unfortunately, Godel's Incompleteness Theorem states that we can never find an all encompassing axiomatic system which is able to prove all mathematical truths, but no falsehoods.

[tilly]

What he described is less ambitious than Hilbert's Program.

He just wanted to have computers (which hopefully are less fallible than humans) systematically verify known mathematics. While I see this as interesting to attempt, it is also doomed to fail because more math is being produced faster than you can possibly verify it.

Which brings up a dirty little secret of mathematics. You can consider a mathematical proof as being like a computer program that has been specced out in detail, but never run. Yeah, you think that it would work. But if you tried to implement it you'd run into little roadblocks. Most of them you could get around. But you never have any idea what is lurking in there, and no real way to find out.

And no, this is not a trivial problem. In fact entire areas of mathematics have fallen apart because problems were found, and found to be serious. My current favorite example is the classification of finite groups. Nobody has really reviewed the proof. Everyone knows that the proof has flaws. And the situation is serious enough that there is a decades-long effort under way to find a different proof of the result! (The effort was started by some of the people who made their reputation working on the original proof.)

[hv]

It need not necessarily be doomed to fail for that reason, if the software involved could be useful enough that from some point an increasing proportion of new maths were produced using it.

Making the technology sufficiently useful is probably the magic part though; fixing existing proofs is also likely to be a big job, since my impression is that even today they are riddled with informal appeals to reason or analogy in a manner that would in many cases be hard to formalise.

Of course any hard step can be left for later, or for someone else, simply by declaring that step as an axiom.

An interesting aspect of this - though also one with the potential to explode the problem space - is that it could make it much easier to see the overlap in accessibility of theorems under different sets of rules of logic.

I think I first started thinking about this way back when I was first reading Godel, Escher, Bach. I spent a lot of time with the Peano axioms described there, and while I could prove things like commutativity and associativity of addition and multiplication easily enough the lack of axioms for handling negatives meant it was impossible to prove something like "every integer is either even or odd":

 Ax: (Ey: ((x = (SS0 . y) | (x = S(SS0 . y)))))

Hugo

[kabel]

i think the proof problem is due to the application of classical logic. in intuitionistic logic, there is no such thing like an pure existence proof. instead, existence is showed by providing a method of computation -- an algorithm -- which constructs the thing whose existence is to be proofed.

provided that a) existence proofs are the problem and b) i understood your points.