\( \newcommand\D{\mathrm{d}} \newcommand\E{\mathrm{e}} \newcommand\I{\mathrm{i}} \newcommand\bigOh{\mathcal{O}} \newcommand{\cat}[1]{\mathbf{#1}} \newcommand\curl{\vec{\nabla}\times} \newcommand{\CC}{\mathbb{C}} \newcommand{\NN}{\mathbb{N}} \newcommand{\QQ}{\mathbb{Q}} \newcommand{\RR}{\mathbb{R}} \newcommand{\ZZ}{\mathbb{Z}} \)
UP | HOME

"Compile Anywhere" - Mizar

Table of Contents

1. Overview

Kaliszyk and Pąk have worked on a project over the past decade or so to implement an Isabelle/Mizar environment (that is to say, Mizar as an object logic inside Isabelle). In their paper:

  • Cezary Kaliszyk and Karol Pąk,
    "Semantics of Mizar as an Isabelle Object Logic".
    Journal of Automated Reasoning 63, no.3 (2019) 557–595 Eprint

They present a "HOL Semantics" for Mizar, as well as a "FOL Semantics". This was developed further in:

  • Chad E. Brown, Cezary Kaliszyk, and Karol Pak,
    "Higher-order Tarski Grothendieck as a foundation for formal proof".
    In 10th International Conference on Interactive Theorem Proving (ITP 2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019. Eprint

This picqued my interest, and provoked the following questions:

Can we implement a Mizar clone atop HOL Light in a manner faithful to Mizar's semantics?

To clarify this puzzle, we know of three "Mizar modes" for HOL Light. But these make writing in HOL Light easier; i.e., the formalization is still within the HOL system, rather than within a "Mizar-like system". Instead of a quality-of-life library, could we re-implement Mizar but with HOL working "under the hood" instead of first-order logic…without us ever knowing?

The other question that came to mind was: if we could "swap out" the "engine" from first-order logic to higher-order logic, then what would be stopping us from "swapping in" any other suitably strong foundations?

Can we invent a CIC type theoretic semantics for Mizar?

2. Compile to Types

Let me be more precise in my puzzle. Of course we can "encode" Tarski-Grothendieck set theory in Coq (or Lean or whatever), and probably we could have a "compiler" read in Mizar articles and emit Coq theorems/proofs (albeit horribly inefficiently, perhaps exponentially larger than the original proofs). This is not what I'm asking about.

Could we have Mizar types compile to Coq types, Mizar propositions compile to Coq propositions, and so on?

3. References

  • Cezary Kaliszyk and Karol Pąk,
    "Semantics of Mizar as an Isabelle Object Logic".
    Journal of Automated Reasoning 63, no.3 (2019) 557–595 Eprint
  • Chad E. Brown, Cezary Kaliszyk, and Karol Pak,
    "Higher-order Tarski Grothendieck as a foundation for formal proof".
    In 10th International Conference on Interactive Theorem Proving (ITP 2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019. Eprint

3.1. Mizar Modes

  • For HOL Light
    1. John Harrison,
      "A Mizar Mode for HOL".
      In TPHOLs'96, Eprint
    2. F. Wiedijk,
      "Mizar Light for HOL Light".
      In: Richard Boulton & Paul Jackson (eds.), Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Springer LNCS 2152, 378-393, 2001; Eprint
    3. F. Wiedijk,
      "A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving".
      Logical Methods in Computer Science 8,no.1 (2012) 1-26; arXiv:1201.3601
  • For Coq:
    1. M. Giero and F. Wiedijk,
      "MMode, a Mizar Mode for the proof assistant Coq".
      Tech.report NIII-R0333, University of Nijmegen, 2003; Eprint
    2. Pierre Corbineau,
      "A Declarative Language For The Coq Proof Assistant".
      In: Miculan, M., Scagnetto, I., Honsell, F. (eds) Types for Proofs and Programs. TYPES 2007. Lecture Notes in Computer Science, vol 4941. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68103-8_5

Last Updated 2022-05-02 Mon 08:09.