Metablog

As an exercise, to get some experience with Metamath’s formal system, I’ve been working on a formalization of the Lambda Calculus. (That article should provide more than enough background for this post.) I’ve run into a little issue, though. When defining combinators (certain fixed expressions with special meaning), one needs to use dummy variables. For instance, the S combinator is λxyz.xy(xz), where “x”, “y”, and “z” could be any three letters. You could choose them as needed not to collide with any other variables you’re using. However, when expanding these definitions in Metamath, it becomes impossible to avoid having to prove things like “x is not free in M”, even though of course it’s not free. For example, through beta reduction, we have

As the next step, we’d like to substitute y for N, yielding (MN(Mz))[z := L]. But we can’t do this without also proving that y is not free in M, because, expanding the steps in more detail, we have

There is no way to eliminate the [y := N] after the M without proving that doing so would not change the meaning of the term. Of course, I could eliminate that requirement from the axiom, but I fear the system would become unsound. Now, we know that this is a fine step to do, because we know that in the definition of the S combinator the variables x, y, and z are postulated not to match any of the other variables in the terms you’re substituting for them. The problem, however, is representing this notion in the formal system.

The paper I’m working on, available here, provides a fairly thorough and rigorous introduction to the subject, and so is pretty much ideal for what I’m using it for. However, it deal with the problem presented here by postulating that bound variables and free variables are drawn from two distinct sets. I don’t believe this approach is practical for Metamath.

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.