Progress: bound variables

[Raph Levien]

As of the latest commit, the Rust prototype now handles bound variables (with lambda syntax) and "not free in" constraints, with syntax of "x y F/ A, z F/ B" appearing (without parentheses) after the last hypothesis of an axiom or theorem.

Consequently, the prototype should now have enough power to handle a translation of set.mm. There are of course still a lot of rough edges that need to be polished before it becomes usable, not least of which is the unhelpful error reporting. I also want to put infix syntax in place to show more accurately what proof files will look like.

It's also missing two key features of the original Ghilbert: safe definitions and modules. I think definitions can be added readily enough, but I'm going to hold back on modules for a bit, as I plan a total overhaul.

The implementation was interesting, I think. I basically allow terms to have a "type" such as "val->wff", which is the argument to the universal quantifier term (A.). It wouldn't be a big stretch to allow variables to have these kinds of types too, then one could write:

var P: val->wff;

theorem 19.2 : -> (A. P) (E. P) ::( ... )

I'm not sure what this buys you, though.

The metalanguage lets you write lambda expressions to construct terms of these higher "types", but doesn't contain a mechanism to apply them. Similarly, I'm not sure exactly what that would buy, as it seems possible to derive everything you need from axioms (and this is most consistent with the Metamath tradition).

As always, feedback is welcome. I think the system has arrived at the point where it might be fun to play with.

Raph