Metablog

Also published at Less Wrong.

So, you wanna be a rationalist, huh? Then it’s more than likely that at some point you’ve had the thought: “I should be completely honest with everyone. I shouldn’t hide any truth.” And it’s likely you’re a bit more honest than the average human. (Robin Hanson might take issue here.) And it’s likely you’re nothing like completely honest with everyone. So where, and why, do these ideals fall short?

First, strict honesty is a form of vulnerability. You’re bound to say a particular thing in any given situation, regardless of how it may work to your advantage or disadvantage. You pass up opportunities to manipulate or obfuscate that could work to your advantage. In the game of life, you’re conceding ground. Now, this is made up for, to some extent, by the reputational advantages of honesty. Is the balance positive? Not hardly, in my opinion. (And we haven’t even considered the “telling it like it is” problem yet.)

Second, it takes a lot of active effort to stay honest with someone. And that effort needs to pay off for honesty to be worthwhile. Strict honesty can only pay off with particular people. You say you want honesty. No, what you want is honesty from someone who thinks rather highly of you and is committed to your well-being. Someone who doesn’t have much negative to say about you at all, compared to the positive.*

Really, I think what people are searching for with these honesty impulses is reciprocal honesty. Reciprocal honesty is much more practicable than strict honesty. You can be reciprocally honest in limited ways, with specific people on certain topics. You can pick and choose. (Do you feel an obligation to tell the truth to those who lie to you?)

Continue reading »

Great name for a song. (I wouldn’t drink it that way myself, obviously. I take it neat. (I wouldn’t drink it that way, obviously. I take it intravenously.))

Thanks to drinking a tiny bit of Everclear in my PowerCitrus! soda and listening to Katamari On The Rocks, the a capella version of the main Katamari Damacy theme in the Moon level (the last level).

Isabelle is a program that checks your math. You tell it, in a very technical computer language, how to prove that some line of mathematical reasoning is correct, and it verifies that you’ve told it right. It’s also a great help in searching for proofs to begin with, because it has powerful techniques to simplify and transform mathematical statements into simpler or just different versions that help you understand the statements.

Isar is a language built on top of Isabelle. Unlike most computer proof languages, It allows steps in a proof to be done without mentioning the theorem being used by name in certain circumstances, allows explicit naming and reference of statements, and allows backwards and forwards proof to be mixed together arbitrarily. (In these respects it’s similar to the difference between assembly language and higher-level programming languages.) You can state subgoals explicitly on your way to proving the main goal if you like (similar to subroutines). A key strength of Isar is its flexibility—you can state a given proof in many different ways, which means that you can usually find a way that’s fairly easy to read.

What’s more, the ideas behind Isar don’t have a whole lot to do with the underlying logical or even metalogical framework. In other words, Isar is to a large extent orthogonal to Isabelle. Isabelle/Isar uses unification and resolution in an intuitionistic metalogic as its principles, but they could be substantially different while keeping Isar useful.

Metamath is a system that’s quite similar to Isabelle at heart, but much, much, much simpler. It’s correspondingly less powerful (practically speaking, not formally) and harder to use. Its main advantage is that its proofs, while longer, are very explicit and thus possible to follow with a minimum of prior knowledge. (And, as far as I’m concerned, the simplicity is also quite nice in that I can easily use Metamath ideas to design my own math system and have a lot more confidence in the results than I would with a system of my own design or a system that imitated the design of a more complex system like Isabelle.)

Continue reading »

I’ve been doing a lot of mathy things recently, and one of them has been playing with Metamath, which is step by step formalizing a whole bunch of mathematics. You can see what real numbers really are, how recursion and induction can be defined using only basic set theory, what a function really is, and a million other neat things. It has proofs for all of its theorems that can be verified by a very simple program, or by hand if you like. It’s just a whole bunch of substituting A for B and matching.

The only problem with it is that it’s kind of low-level. It’s hard to follow the proofs and even sometimes the definitions. Now, on the one hand, it’s probably good to become more fluent in formal mathematical language if you want to learn a lot of math. But on the other hand, part of the difficulty I was encountering was entirely avoidable, due to not including enough information about the proof when it’s displayed. In particular, to know what substitution is being made at any given point, you have to open the theorem being used at that step, and then go back to the proof. If the theorem is quite large, you might have to go back and forth quite a bit to get it in your head enough to understand what’s going on. And further, for very long equations, it can be completely impossible to do this in your head.

So I made it all happen on the screen, right there in front of you. Proofs still aren’t easy to follow, but they’re quite a bit easier than they were. Perhaps as easy as they’re going to get with Metamath. We’ll see if I get any better at reading them now. (By the way, this is done along with shrinking the site quite a bit by having it all done in javascript.)

Unfortunately, I don’t currently replicate all of the features of the Metamath site, since that would be hard and kind of boring. So you need to really start here, and then type in http://pdf23ds.net/projects/Metamath/theory-name.htm when you have a theorem whose proof you want to follow.

I invite your comments.

Hi, google!

And hi, searcher! If you’re looking for a .NET or C# or VB version (really, just the output part) of the Rats! PEG parser, I can probably help! I have written such a thing, and could be persuaded to assist with its use. It isn’t in the main distribution of Rats!, for various reasons, though could be in the future if there’s any demand for it. There is a Bazaar repository with my changes here (though this might not be the latest–check with me).