1
$\begingroup$

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.


$\endgroup$
16
  • 2
    $\begingroup$ Ask 'whether' before 'why'. Have you heard of Isabelle? It can encode various formal systems. Notably, Isabelle/HOL, Isabelle/ZFC, etc. etc. $\endgroup$
    – Trebor
    Sep 22 '21 at 6:56
  • 2
    $\begingroup$ Metamath can also encode formal systems. But metamath possesses a much, much weaker meta-logic than Isabelle. $\endgroup$
    – Trebor
    Sep 22 '21 at 6:58
  • 1
    $\begingroup$ Uh, currently AFK, I'm going to add more, and turn it into an answer later. $\endgroup$
    – Trebor
    Sep 22 '21 at 7:00
  • 1
    $\begingroup$ That sounds more like asking for a community than a tool. $\endgroup$
    – Trebor
    Sep 22 '21 at 7:54
  • 2
    $\begingroup$ Metamath, the tool itself, isn't geared towards any formal system -- it is deliberately designed so. But it's community is geared towards ZFC. Is that what you want? $\endgroup$
    – Trebor
    Sep 22 '21 at 8:00
4
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ Thanks for the detailed response. Right now I'm looking at DPO and more general graph-rewriting. The graph production rules handle the meta logical deduduction. But the rules are not hard-coded, they're encoded in the visual language itself. That means it will support any system you encode the axioms / rules for, as long as the category holding your diagrams is adhesive. But there's an even more general 3x3 square pushout-based rewriting (instead of the 2x1 square DPO span rewrite) I'm investigating. It's just that the book containing it costs over $100 USD! :) $\endgroup$ Sep 22 '21 at 21:09
  • 1
    $\begingroup$ @SmokenSieEinBitteChebaHitBits Oh, and, I've written a tiny one. It sort of works, but I abandoned it because my goals turned out to be undecidable. You might find it useful if you want to write your own. Here. $\endgroup$
    – Trebor
    Sep 23 '21 at 1:15
  • 1
    $\begingroup$ Graph rewriting might be too powerful. Usually you just need to deal with syntax trees with binding. $\endgroup$
    – Trebor
    Sep 23 '21 at 1:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.