Why isn't there an app that allows you to enter in all the rules of a given formal system so that the app supports all formal systems of math?

Question

I'm jumping around between articles about ETCS to Simple TT to Calculus of Constructions wondering what my app should focus on.

I'm wondering, why there isn't yet a software app in which you can encode (using a mathematical language) any formal system that is given as a finite set of logical rules.

Thus Coq / Lean had to say "our software is based upon / makes use of Calculus of Constructions" in their documentation. But I'm looking for an app that can simply encode any and all of the formal systems.

I know, you're saying well that would be the programming language you choose. E.g. C++ fits the bill because it's a Turing complete language. However, this type of software won't count to answer this question. A programming language is overkill. I'm looking for a UX with an almost zero learning time for mathematicians. Learning C++ would take months.

---

Reason for asking.

Say I had a visual language which supports parenting of nodes, arrows between any two nodes (all arrows are parentless), and any number of text labels on a node or an arrow.

Suppose that I had a general subgraph isomorphism-based searcher (implemented in say C++ for speed) that would search for every subgraph in the drawn diagram of a user in a large graph (the database or "library") and try to match that user's subgraph to the input of a diagram rule (drawn by another user using the same language). Diagram rules get special arrows - they are two-lined arrows such as $\implies$ because they mean essentially logical implication. But we could also just label them with a keyword phrase such as "diagram rule". Anyway, if a match is made, the whole rule shows up in the library search widget allowing the user to click the "Apply rule" button which would glue in the result of the rule (and delete any nodes / arrows as needed) in place into the users graph, and create a proof step. So going one step back in the proof would show their original diagram. But the current view now shows the diagram with the logical rule applied. That rule can be part of an axiom, definition, or theorem. For example a theorem might have many associated rules so I say "part of".

Anyway, given that, clearly you can express any logical theory doing things like $x:X$ is synonymous with a node labeled $X$ with a child node labeled $x$. And an arrow can be a map of types or a diagram rule.

Okay, given that base system that is hard-coded. The theories that it has the ability to encode are any given one. The fact that we needed a graph search is only because the language is visual, and not textual, and so naturally supports commutative diagrams & graphs. Converting the language to text before doing a search seems like more work than just doing a subgraph isomorphism search.

---

Answer 1

Perhaps its best to clarify one thing: The distinction of formal systems and meta-logic.

When you conclude from $A$ and $A \to B$ (in Hilbert's formalization of logic) that $B$ is provable, what is it that verifies your conclusion? It is undoubtedly some sort of logic, but definitely not the logic that you are formalizing --- that would result in circular definition. In fact, we call the logic that you use to study another logic meta-logic.

Meta-logic does not have to be connected in any way with the logic under investigation. For example, you can use ZFC to prove things (like Lindelof's theorem) about first order logic. You can use Coq (or the Calculus of Constructions) to do that as well. You can prove theorem schemes (i.e. For every formula $\phi$, $\phi \to \phi$; this is not one theorem but a bunch of them, each for a well-formed formula $\phi$) with Metamath, Isabelle or NFU (Quine's New Foundations, with Urelements). The meta-logic is up to you to choose.

No matter which meta-logic you decide upon, as long as it is consistent, the concrete theorems that you prove (like $\forall x. x=x$ in first order logic or $n{:} \mathbb N \vdash n+1=1+n$ in Martin-Lof's type theory) will be the same. However, a concrete theorem is just a very specific property about the formal system under investigation: "$\forall x. x=x$ is provable in FOL." We can prove other properties: "The axiom of choice is not refutable in ZF." You can't do that in Metamath, because the meta-logic would be too weak. But you can do it in Martin-Lof type theory with enough universes. These properties are called meta-theorems.

From what you have described, you probably don't need too many meta-theorems. But you will know that it is crucial if you want to do anything practical, especially in systems like plain first-order logic: You definitely want the deduction theorem (it's a meta-theorem, but unfortunately named a theorem), or you probably won't get anything done! HOL (a.k.a. STT) and Martin-Lof-style type systems circumvent that by allowing higher order constructs, so in theorem provers like Coq, the logic is the Calculus of Constructions, and the meta-logic (a.k.a. type-checker) is so simple that it doesn't deserve a name: just syntax-tree substitutions according to typing rules, and nothing else.

That said, you should now realize that you can actually use (say) Coq to study any formal system you want. And it's pretty cool to encode proofs in dependent type theories, because the types enforce invariants miraculously, and you don't need to write proof-checkers at all; the type-checker in the meta-logic automatically does that for you! [Reminder: Now Coq is the meta-logic, and Coq's meta-logic (meta-meta-logic?) is the very simple type-checker.] You will encounter bad stuff like coherence problems when you try to prove more powerful theorem-schemes, though. But it's off topic here.

Now, for recommendations. You may want to check out LCF (logic for computable functions), which is Lisp-based and very extensible. Isabelle does have a few small libraries for Isabelle/ZF and Isabelle/FOL. But indeed, the majority of the work goes to Isabelle/HOL, including powerful proof-automation and counterexample-finding tools. Metamath is focused on ZFC (actually NBG (actually with an additional Grothendieck axiom, dedicated for developing category theory)), but has a decent set of material on NF, ZFI (intuitionistic ZF), HOL, and many more. You can have a graphical view, as linked to in the comments.

If what you want is a tool with many approximately equal-sized formal system libraries, I think you will not find anything. This is arguably caused by human nature: What's more developed will attract more attention, and thus quickly become the monopoly. Also, a stable community must have a united direction to work at. And that's probably why the "other" systems in Metamath isn't nearly as developed as one tenth of the Metamath/ZFC system.