Hacker News Reader

Comment by practal | Hacker News Reader

I like the way you are thinking about this. And yes, formal math is the future! If you want to check out how to deal with quantification properly, or more generally with operators, without a need to explicitly introduce types, check out https://practal.com .

View on HN

We're looking at this. Some very fascinating stuff. Somewhere at the beginning of "The Calculi of Lambda Conversion" Church talks about the fact that quantification can be reduced to lambdas. I have not read to the end of the paper (still learning these things step by step) and as we have struggled to understand how we should represent quantification, one of the things that became clear is the analogy between functions and quantifiers on the ground that both bind variables, so on the surface what you're talking about has the ring of truth.

Church tried to reduce logic to his invention, the untyped lambda calculus, but failed in a first attempt [1]. He then proceeded later on to invent the simple theory of types, [2], and type theory is pretty much a descendant of that. My argument with abstraction logic is that trying to use lambda+types for logic is actually misguided and overly restrictive. Abstraction logic is simpler, and can nevertheless also express variable binding naturally.

You are kind of lucky that you are relatively fresh to all this, so you can approach both type theory and abstraction logic with an open mind, and see for yourself which you find more appealing.

[1] S. C. Kleene, J. B. Rosser. The Inconsistency of Certain Formal Logics. Annals of Mathematics, 1935.

[2] Alonzo Church. A Formulation of the Simple Theory of Types. Journal of Symbolic Logic, 1940.

How does your system compare to Metamath[0], aside from the obvious difference of not having set theory baked in? I notice both your Abstraction Logic and Metamath's system can state the induction axiom scheme as a single statement, which seems to me like a huge usability advantage over FOL.

[0] https://us.metamath.org/mpeuni/mmset.html

Metamath itself is a logical framework, and doesn't really have a semantics. You can encode rules of a logic with it, and then you have to convince yourself that this encoding is what you want. I believe most of Metamath's content is based on an encoding of first-order logic, and it sounds like they allow some sort of schematic variables, which make it possible to replace axiom schemata by single axioms, but it is still FOL.

Given Metamath has no semantics, there is no built-in notion of soundness with Metamath. I think that has been fixed with Metamath Zero, but as a consequence, Metamath Zero is based on multi-sorted first-order logic only.

On the other hand, Practal uses Abstraction Logic, which can also act as a logical framework, but is itself already a logic with a simple semantics, simpler and more flexible than first-order logic (or any other general logic I know of). An important difference to first-order logic is that Abstraction Logic supports general operators, while first-order logic supports only two operators out of the box: universal quantification ∀, and existential quantification ∃.

Thanks - I hadn't looked into Metamath Zero before, but it sounds like that would be the right thing to compare Abstraction Logic to! Skimming https://arxiv.org/abs/1910.10703 makes it seem like Metamath Zero still operates at the level of schema, but has some other changes compared to Metamath that are too subtle for me to digest in an afternoon.

I just skimmed the paper you linked (I read it before, but forgot its details). So Metamath Zero is still a logical framework, like Metamath, but has a few more tools to ensure soundness of the logics you formulate in it. Nevertheless, just like Metamath, it does not have a semantics, because it operates on a purely syntactic level. You can formulate object logics in it, like FOL, which come with their own semantics, but it is up to you to show that this semantics is actually preserved by your encoding in Metamath Zero.

So I would say that this is the main difference between a logical framework (LF) (like Metamath and Metamath Zero) and Abstraction Logic (AL): the LF is based on proof-theory and syntax only (BYOS, bring your own semantics), while AL gives you in addition to proofs and syntax also a simple semantics.

Some LFs, like Isabelle, are based on intuitionistic type theory, and so they actually DO come with a semantics as well. But I wouldn't describe this semantics as simple (check out for example [1]), so when you describe an object logic with such an LF, you cannot really rely on that semantics to explain your object logic semantics, or prove properties like completeness, but are again left to your own purely syntactic devices, and are back to BYOS.

Does that actually make a difference in practice? Is there a practical benefit to AL having a simple semantics, and other LFs not? I am convinced that yes, it makes a big difference, because it makes it simpler (or even possible) compared to other LFs to implement features which are simple yet general and powerful, and it makes it also simpler to interface with other software like computer algebra software. But in the end, this can only be proven by actually building Practal and showing its practical benefits.

[1] Chad E. Brown. A semantics for intuitionistic higher-order logic .... https://www.ps.uni-saarland.de/iholhoas/msethoas.pdf

Reply on news.ycombinator.com