5
$\begingroup$

There are 3 basic formalisms of the mathematical knowledge (and their respective theorem provers/libraries):

  1. Axiomatic set theory (Mizar)
  2. Higher order logic (Isabelle/HOL)
  3. Constructive Type Theory (Coq)

The translations among formalisms is big open problem according to https://jfr.unibo.it/article/view/4570. There are translations from HOL to Set theory and Type Theory (see resp. https://link.springer.com/chapter/10.1007%2F978-3-642-14052-5_22 and https://link.springer.com/chapter/10.1007/978-3-642-14052-5_23), but I have not managed to find translation from Set theory to Type Theory (importing Mizar into Coq). There is one work about Mizar mode in Coq, but it explicitly states, that such mode is not importing Mizar into Coq.

So - I am asking for references and ideas - how to import Mizar in Coq or how to express (translate into) axiomatic set theory into constructive type theory?

$\endgroup$
1
$\begingroup$

This is less of an answer and more of an explanation on why it is hard, why it will probably never exist usefully, and why you probably wouldn't want to use any system that purported to do this anyway.

First, I'll say what is easy relatively speaking. You can formalize Tarski-Grothendieck set theory (TG) in Coq. Jonas Kaiser axiomatizes TG in Formal Construction of a Set Theory in Coq mentioned in the mailing list post. Another paper mentioned in the same mailing list post, Semantical Investigations in Intuitionistic Set Theory and Type Theories with Inductive Families by Bruno Barras, formalizes the closely related ZFC+U but does so in a somewhat different way. Kaiser simply postulates a type $\mathsf{set}$ and a relation ${\in} :\mathsf{set}\to\mathsf{set}\to\mathsf{Prop}$ and the TG axioms. This approach is basically just using Coq as a logical framework and doesn't "reduce" TG to CIC at all. Barras, on the other hand, while also introducing a type $\mathsf{set}$, does so by definition rather than postulation in which case some of the axioms and notions of set theory can be derived, though some axioms still need to be postulated to go all the way. This provides a more proper reduction of ZFC+U to CIC plus some axioms which aren't doing all of the work as they are in Kaiser's case.

With either approach, the key thing for us is that anything you might talk about in either of these systems is a value of type $\mathsf{set}$. If all you cared about is verifying Mizar proofs with Coq, then this would be relatively straightforward. Certainly, as far as the TG axioms, you'd be able to translate those one-to-one. The Mizar meta-language is actually not that different from a dependent type theory and should be able to be translated without too much trouble. The hardest part is likely to be some of the built-in reasoning of Mizar's proof language. With sufficiently fancy Ltac programming, you should be able to produce tactics that mimic these proof rules, allowing a simple translation.

The problem is: you probably don't just want to verify a Mizar proof; you want to use results proved in Mizar in your Coq proofs. This is where everything falls apart. If you're familiar with programming, the problem is basically exactly the same as programming language interoperability. Even more specifically, it's very closely analogous to getting a (statically) typed language to interoperate with an untyped/"dynamically typed" language. The issue is while it is easy to ignore structure, it is not easy to recover it.

The issues and solutions to programming language interoperability have direct parallels. First, we need a way to embed values of arbitrary types into $\mathsf{set}$ and to project them out. But for a type $T$, there is not a unique or canonical embedding $T\to\mathsf{set}$. We'd likely more prefer something like $T\cong\Sigma s\!:\!\mathsf{set}.\varphi(s)$ where $\varphi(s)$ states that $s$ is a set-theoretic representation of $T$. This isomorphism is not unique and neither $\varphi$ nor the isomorphism can be automatically, let alone uniformly, derived. However, you could derive a $\varphi$ and isomorphism of this form in a type-directed manner (using meta-programming techniques or possibly "type classes"), but the problem there is that the set-theoretic representation, i.e. $\varphi$, quite likely won't be the representation the Mizar proofs were written against. You could resolve this by proving in Mizar (or in Coq) that the two set-theoretic representations were isomorphic. This can't be automated. You then need to insert these conversions all over the place. This can be partially automated. However, you can only prove things using the Mizar proofs with respect to a representation, and you have no way of verifying that you've used the correct representation. If I define $<$ on naturals as $\in$, from Coq that's just a $\mathsf{set}\to\mathsf{set}\to\mathsf{Prop}$ predicate. If I use the wrong representation, I just get seemingly false theorems. Adding proofs to validate the representations and wrapping things to produce a more idiomatic interface can't be automated. Finally, the proof checking of the translated Mizar proofs is likely to be far less efficient than a more idiomatic direct encoding. (Yes, mathematicians in the not distant future [it's already happening now] will have to care about performance just like us programmers.)

All of this is extremely tedious, especially without tooling (beyond the translator). The tooling is usually fairly complicated and/or underwhelming in its usefulness. You have to really be getting something to go through this hassle, and it needs to be less hassle than just reproving the results (perhaps guided by the Mizar proof). I'm pretty confident that in virtually all cases that will not be the case. For a lot of reasons, going the other way, i.e. embedding Coq into Mizar, is likely to be much easier though quite possibly still not worth the hassle. With regards to the above discussion, the main difference is that since Coq is more structured, it provides more information, and it doesn't require you to recover structure just conform to it which is a much more well-defined problem. Judging from experience in programming, this kind of interoperability will not be implemented without some significant pay-off (and often not even then). There's been an impressive effort to get Haskell to run in the browser (i.e. interoperate with JavaScript) and a far less successful effort to get Haskell to run on the Java Virtual Machine, but no one is putting out any effort to make it easier for Haskell and Go to talk to each other. One of the more successful ways of getting Haskell and Java to interoperate is to embed Java source code into Haskell but ultimately build each with their own respective toolchains and have the resulting programs communicate. The result is fairly seamless, at least from a source code perspective. This approach also makes sense for proof assistants. We can simply add a "call out to Mizar" proof rule to Coq. This approach solves almost all the issues mentioned above. Lean is more oriented to this sort of thing than Coq. A dramatic solution to this problem would be to implement and prove correct a Mizar verifier in Coq and then use reflection techniques. This is the "principled" way of effectively adding a "call out to Mizar" proof rule. It's likely completely impractical.

$\endgroup$

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.