Every axiom, definition, and theorem in Metamath is actually a template where no matter what you plug in for the free variables, you get a statement that's considered true in the system. So, for example:
Q → (P → Q)
Allows you to write sentences like
(A = 0) → ((∀ x ∈ R (0 < x → A < x)) → (A = 0))
This is kind of like a Scheme macro, but a really surprising thing about Metamath is that the sort of substitution it employs is not hygienic. If you happen to be using a local variable x, and you plug in a formula that has x free, the formula will “capture” the x in its new context.
In Scheme, if you plug a bit of code into another bit of code this way, and both bits of code are using a variable named x, Scheme behaves as though it's silently renaming one of the variables so the two don't conflict... unless the two x's actually refer to the same global variable or something—you can see it gets rather complicated. Lisp doesn't bother. It just plugs in the code. If variables get crossed, they get crossed.
Apparently doing it the Lisp way makes the Metamath proof-checker a lot simpler. Interesting.
2 comments:
It the variable does not occure in a bound context, and if the context is not bound by the variable either or the substituent does not contain the context variable either, than no harm can happen.
Or symbolically
(lambda x.t)[y/s] =
lambda x.(t[y/s])
for x<>y and x not in s
Bye
Yep. Metamath uses something called "disjoint variables" to make sure that "x not in s".
See the follow-up post for more details.
Post a Comment