Item — HN Reader

I think you're overstating the case against ZFC as a practical basis for proof formalization. The Metamath project has got pretty far even without powerful tactics and so on, and has an appealingly simple kernel. That work continues in Mario Carneiro's Metamath Zero, which does add some pretty basic automation, and is able to prove a simple C-like compiler among other things.

Of course I admit that Lean is pretty much cleaning everybody else's clock, but it's not clear to me that's because of the inherent superiority of type theory over set theory. It's equally plausible that it's just well engineered, and there's been a lot more attention on automating type theory by computer scientists.

3 comments

Lean is well engineered, is also marketed as a programming language, and expressive enough to do proper math in it. Type theory is more elegant to implement than set theory based on first-order logic. That's about it.

Nevertheless, first-order logic is not the last word when it comes to formalising set theory, I think Abstraction Logic (AL)[1] is. When you start formalising set-like and type-like things in AL, the border between sets and types disappears. That border is just an artefact of history, useful for foundational studies, but will lose its importance for anything practical.

[1]: https://obua.com/publications/philosophy-of-abstraction-logi...

If you want to "automate" set theory, you pretty much have to build a type theory on top of it. This is what Mizar does (one of the oldest projects in formalized math, but still going strong). It also starts by assuming extremely strong set-theoretic axioms, to make this more convenient.

The type theoretic approach is ultimately more elegant; the basic foundation is a bit more complex than material set theory, but the complexity is of a kind that's used basically everywhere in a practical formalization. It avoids the pattern of building complicated stuff on top of an overly simple axiomatic basis.

You are probably confusing "automation" with "mechanisation" here, and maybe also with "computing".

It is very easy to automate set theory, at least when it is just embedded in first-order logic, and at least compared to type theory. Automation of first-order logic is MUCH further and MUCH easier than automation of type theory, which is usually not much automated at all apart from a few tactics here and there.

Furthermore, the prevalent use of type theory for mechanised interactive theorem proving is based on the work of Church on simple type theory, and extensions of that into dependent types. Computer scientists like the lambda calculus and types, and it gives a nice and general way for implementing binding. It also is straightforward to compute in it, but that is also easy to implement for set theory if you are interested in it (most people doing set theory are not).

Ultimately, though, both set theory and type theory are just specific mathematical theories. This became apparent to me after I discovered what is probably the best foundational logic, Abstraction Logic (AL) [1], in which you can represent both as mathematical theories. AL is like first-order logic, but plus operators (and therefore binding), and like higher-order logic, but minus static types.

What is missing for AL is an actual system implementing it, but that is in the works.

[1]: https://obua.com/publications/philosophy-of-abstraction-logi...

> ...in which you can represent both as mathematical theories...

There are many logical frameworks (LF's) that are targeted at this same space. They're especially useful for exploring automated conversions of high-level "theories" to different axiomatic systems.

Yes, I know. The reason why you call them "frameworks" instead of logics is because they don't have a model-theory based semantics, but are justified via proof theory. Abstraction logic on the other hand is a logic with its own model-theory based semantics.

To further elaborate why this is important: When you implement a logic in some LF, then it is up to you to do a pen and paper argument of what the semantics of your logic is, and why it is faithfully represented via the constructs of the LF, which itself has no semantics. On the other hand, to implement a logic in AL, you just write down its axioms, and the semantics of AL automatically gives a semantics for your logic, including soundness and completeness results. Of course, you still need to do a pen and paper argument that the semantics of your logic via AL is faithful to the semantics of your standalone logic. But this will only be done for the first few logics you implement in AL, future logics will just inherit their semantics from AL, and that will be their semantics then by definition.

Yes, it's not so clear to me either. But I'm willing to grant this point for the sake of the argument.