Show HN: i2forge – A Platform for Verified Reasoning

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 ∃.

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