10.6092/issn.1972-5787/4596
We present an algorithm for converting proofs from the OpenTheory interchange format, which can be translated to and from any of the HOL family of proof languages (HOL4, HOL Light, ProofPower, and Isabelle), into the ZFC-based Metamath language. This task is divided into two steps: the translation of an OpenTheory proof into a Metamath HOL formalization, hol.mm, followed by the embedding of the HOL formalization into the main ZFC foundations of the main Metamath library, set.mm. This process provides a means to link the simplicity of the Metamath foundations to the intense automation efforts which have borne fruit in HOL Light, allowing the production of complete Metamath proofs of theorems in HOL Light, while also proving that HOL Light is consistent, relative to Metamath's ZFC axiomatization.
application/pdf
1972-5787
4596
1
en
Mario M Carneiro
Journal of Formalized Reasoning
algorithms
Conversion of HOL Light proofs into Metamath
Text.Serial.Journal
https://jfr.unibo.it/
9
QED 20th anniversary
2016-01-29
2014-12-18
2016-01-29
2016-12-23
187-200
JFR
Mario M Carneiro
2016/01/29
10.6092/issn.1972-5787/4596
187
Department of Mathematics, Ohio State University, Columbus OH 43210, USA
1972-5787
1
algorithms
en
200
http://us.metamath.org/downloads/metamath.pdf.
Conversion of HOL Light proofs into Metamath
https://jfr.unibo.it/article/download/4596/5732
9
Conversion of HOL Light proofs into Metamath
MARIO M. CARNEIRO
Department of Mathematics, Ohio State University, Columbus OH 43210, USA


We present an algorithm for converting proofs from the OpenTheory interchange format, which
can be translated to and from any of the HOL family of proof languages (HOL4, HOL Light,
ProofPower, and Isabelle), into the ZFC-based Metamath language. This task is divided into
two steps: the translation of an OpenTheory proof into a Metamath HOL formalization, hol.mm,
followed by the embedding of the HOL formalization into the main ZFC foundations of the main
Metamath library, set.mm. This process provides a means to link the simplicity of the Metamath
foundations to the intense automation efforts which have borne fruit in HOL Light, allowing the
production of complete Metamath proofs of theorems in HOL Light, while also proving that HOL
Light is consistent, relative to Metamath’s ZFC axiomatization.




1.   INTRODUCTION
Metamath is a proof language, developed in 1992, on the principle of minimizing
the foundational logic to as little as possible [Meg07]. The resulting logic has only
one built-in rule of inference, direct substitution, and all syntax and axioms are
input outside the logical core. The most well-developed axiom system in Metamath
is called set.mm, and adds the axioms of classical propositional calculus, first-
order predicate calculus, and ZFC set theory to the Metamath foundations; this
axiom system and associated library of theorems is also sometimes referred to as
Metamath. In contrast, OpenTheory is an interchange format for the HOL family
of proof languages (HOL4, HOL Light, ProofPower/HOL, and Isabelle/HOL) based
on a higher-order logical kernel [Hur11]. All the axioms of HOL are built into the
kernel, and several axioms perform proper substitution, which involves the renaming
of bound variables, as part of their operation. The goal of this paper is to present an
algorithm that transforms valid theorem derivations in OpenTheory into equivalent
theorem derivations in set.mm, as a roadmap for an eventual implementation.
   The main task divides neatly into two parts. First, the axioms and inferences
of OpenTheory are translated into their Metamath equivalents, producing a new
database of axioms which we will call hol.mm. At this stage it is still essentially a
HOL derivation, but the inferences are done “the Metamath way.” The primary
job here is to eliminate proper substitutions and dummy variable renaming, which
must be done over several steps in Metamath, and introduce metavariables in place
of free variables in the final statement.
   The second task is to convert a hol.mm derivation into a set.mm derivation. This
step is done entirely within Metamath, and works by constructing a model of HOL
within ZFC. Types become sets, functions become ZFC functions (sets of ordered
pairs), and the indefinite descriptor becomes a choice function on the HOL universe.
2.   PART I: CONVERSION FROM OPENTHEORY TO hol.mm
In this part, we present a transformation from OpenTheory article file format to
Metamath hol.mm format.
                                     Journal of Formalized Reasoning Vol. 9, No. 1, 2016 Pages 187–200.
188     ·      Mario Carneiro

2.1   OpenTheory
Although the original goal of this research was the translation of HOL Light
proofs to Metamath, the source of the translation was changed to OpenTheory
because it already provides bidirectional translation to HOL Light. Furthermore,
the OpenTheory file format is much simpler than the HOL Light file format, re-
quiring only minimal work to read the derivations into an article reader. But more
importantly, the derivations are all laid out already without needing to be gener-
ated first, since HOL Light “proofs” are not actually derivations but instructions
for searching for derivations. By targeting OpenTheory we are able to skip the step
of deriving the proof to begin with and start from a baseline of a complete proof in
HOL-compatible format.
   An OpenTheory article file works as a stack machine, and the file format is very
simple—a sequence of commands that manipulate the stack, separated by newlines
[Hur11]. An article reader maintains a stack, a dictionary for backreferencing pre-
vious computations and theorems, and a list Γ of assumptions and an export list
∆ of theorems. The result of the computation after all instructions in the file are
executed is a “theory” Γ . ∆ that states that the theorems in ∆ are derivable
from the axioms in Γ. Figure 1 shows the inference rules supported by the logi-
cal kernel. The base syntax involves two types of variables: t, u, f, g, x, y denote
term metavariables (and φ, ψ denote term metavariables of type bool), while α, β
are type metavariables. By “metavariable” we mean that an application of any
of these axioms will not involve a literal t but will have t replaced by some term,
which is itself constructed by application of these rules (by contrast to another
notion of “metavariable” used in Metamath presentations; see section 2.2). The
built-in constants are the type constant bool, the function type operator α → β,
and the equality operator = : α → (α → bool) (the term (= x) y is presented as
x = y for clarity). Each term variable v is constructed from a name (a string) and
a type, and two variables are considered equal only if the name and type are equal.
   A derivation is structured as a list of theorems of the form Γ ` φ, where φ is a
term of type bool, and Γ is a finite set of terms of type bool. The set unions and
differences in deductAntisym treat terms that are α-equivalent as equal, where two
terms are considered to be α-equivalent if there is a consistent mapping of bound
variables that transforms one term into the other. More precisely:
Definition 2.1. Given a map σ of variables to variables, terms t, u are said to be
α-equivalent with respect to σ if one of the following conditions is met:
  — t = u = c for some constant term c
  — t = u = v for some variable term v not in the domain of σ
  — t = v and u = σ(v) for some variable term v in the domain of σ
  — t = f x and u = g y, and f, g and x, y are α-equivalent with respect to σ
  — t = (λw. x) and u = (λv. y), and x, y are α-equivalent with respect to
σ[w 7→ v], where σ[w 7→ v] represents the map σ with σ(w) = v added to the map,
replacing any mapping for w if it exists.
Two terms t, u are said to be α-equivalent if they are α-equivalent with respect to
an empty map.

Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
                                  Conversion of HOL Light proofs into Metamath             ·     189


                                     t:β                             f :α→β x:α
           varTerm v 1                         absTerm v 1                      appTerm
    v:α                        (λv. t) : α → β                           f x:β

    t:α                           φ : bool                           Γ ` φ0 = ψ ∆ ` φ
         refl                              assume                                     eqMp2
    `t=t                          {φ} ` φ                                Γ∪∆`ψ

    f :α→β      x:α Γ`f =g ∆`x=y                                     Γ`t=u
                                 appThm                                              absThm v 3
                Γ∪∆`f x=g y                                    Γ ` (λv. t) = (λv. u)

            Γ`φ ∆`ψ                                                ((λv. t) u) : α
                                  deductAntisym                                       betaConv
    (Γ − {ψ}) ∪ (∆ − {φ}) ` φ = ψ                              ` (λv. t) u = t[v → u]

      Γ`φ                                                                t:α
                subst σ                                                         defineConst c
    Γ[σ] ` φ[σ]                                                    c:α     `c=t

                    t:α `φt
                                                defineTypeOp A[vs] abs rep 4
    ` abs (rep a) = a ` φ r = (rep (abs r) = r)



                            Fig. 1.   The OpenTheory logical kernel.5

  The term φ0 in eqMp is required to be α-equivalent to φ. This definition is related
to the definition of a proper substitution, used in rule subst.
Definition 2.2. Given a map σ of term variables to terms and a term t, the proper
substitution t[σ] is defined by structural induction as follows:
   — For a constant term t = c or a variable term t = v not in the domain of σ,
t[σ] = t.
   — For a variable term t = v in the domain of σ, t[σ] = σ(v).
   — If t = f x, then t[σ] = f [σ] x[σ].
   — If t = (λv. x) and some variable present as a subterm of t (this includes v)
is also in the domain of σ, then t[σ] = (λw. x[v 7→ w][σ]), where w is a dummy
variable distinct from variables in subterms of t of the same type as v, otherwise
t[σ] = (λv. x[σ]).
For a set Γ of terms, Γ[σ] = {t[σ] : t ∈ Γ}. We use the same notation t[σ] for a
substitution of type variables to types, but in this case the substitution is direct
(distributes through all term and type construction operators).

1 The variable v is assumed to be of type α in these rules.
2 The terms φ, φ0 are required to be α-equivalent.
3 The variable v must not be free in Γ. Equivalently, Γ must be α-equivalent to a set of terms Γ0

that do not have v as a subterm.
4 The list of variables vs must match the set of free variables in φ; this defines a type operator

A[vs] and constants abs : α → A[vs], rep : A[vs] → α.
5 The astute reader will notice that this table is more detailed than figure 2 of [Hur11], upon which

it was based. This is due to the inclusion of explicit term formation axioms varTerm, absTerm,
appTerm; these were elided in the presentation of [Hur11] but are included in later versions of the
specification (see http://gilith.com/research/opentheory/article.html).
                                                 Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
190       ·     Mario Carneiro

   The OpenTheory stack machine also contains a command axiom that accepts a
list of terms Γ and a term φ and produces the theorem Γ ` φ, while also adding
Γ ` φ to the list of assumptions, and a command thm that takes as input Γ and φ
and also a theorem Γ0 ` φ0 where Γ0 and φ0 are α-equivalent to Γ and φ, and adds
Γ ` φ to the list of exported theorems. These rules are sufficient to completely
describe the OpenTheory logical kernel.
   In addition to the above axioms, there are three axioms that are appended in
order to develop the full HOL foundations:
extensionality ` ∀t. (λx. t x) = t
choice         ` ∀p, x. p x ⇒ p (p)
infinity       ` ∃f ind→ind . (injective f ∧ ¬surjective f )
   However, these require more advanced definitions such as ∀ and ⇒, and their
translations are straightforward, so can be safely ignored for Part I. These defini-
tions also implicitly introduce the type constant ind (the intended model is as any
infinite set) and the “indefinite descriptor”  : (α → bool) → α, which is the HOL
equivalent of a global choice function. We will consider these constructs in more
detail in Part II.
2.2     hol.mm
The primary features of the OpenTheory system (see section 2.1) that are not avail-
able in Metamath-based axiomatizations are proper substitution and α-equivalence,
the “not free in” predicate, and set manipulation of the contexts (the Γ in Γ ` φ).
To address the last problem, we introduce a new term constructor, the “context
conjunction”, which takes as input terms φ and ψ of type bool and produces a term
(φ, ψ), also of type bool. When ∧ is defined, it becomes possible to prove that
(φ ∧ ψ) = (φ, ψ), but before this it is necessary to introduce this as part of the
axiomatization for the “bootstrapping” phase. After taking > as axiomatic, it be-
comes possible to represent Γ ` φ as simply ψ ` φ by using the context conjunction
to put all the terms in Γ into one term, and use ψ = > if Γ = ∅.
  Figure 2 shows the axiomatization that is used in hol.mm.1 A comparison with
the axioms of OpenTheory (figure 1) shows several differences. The most obvi-
ous difference is the increase in the number of axioms, from 14 to 23, but this
comparison is deceptive, because this increase must be weighed against the more
complicated explanation of α-equivalence and proper substitution that must be de-
scribed in order to fully explain when the axioms are applicable. In the hol.mm
axiomatization, the only “asterisks” are the distinct variable provisos that come
with leq, ax-17, and distrl.
  There are three kinds of variables in these axioms: “type”, “var”, and “term”
variables. Term variables are represented by capital letters, type variables are
represented with greek letters, and “var” variables (referred to henceforth as vars)
are represented by lowercase letters. The reason for the division of OpenTheory
term variables into two different types has to do with the way which Metamath
handles substitutions. Metamath is designed to have “pluggable” axioms, with the
only built-in axiom being the direct substitution of a (meta)variable with a term.

1A    version of hol.mm is available for download at http://us.metamath.org/metamath/hol.mm.
Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
                                    Conversion of HOL Light proofs into Metamath               ·      191


                         R : bool S : bool                  F :α→β T :α
               wtru                        wct                            wc                        wv
    > : bool                (R, S) : bool                      (F T ) : β                  xα : α

           T :β                    R : bool             R`S S`T                    R`S R`T
                       wl                   id                          syl                         jca
    (λxα . T ) : α → β             R`R                    R`T                       R ` (S, T )

                                            R : bool S : bool                 R : bool S : bool
                            weq                               simpl                             simpr
    = : α → (α → bool)                          (R, S) ` R                        (R, S) ` S

    R : bool                           A:α                                R`A      R`A=B
             trud                           refl                                         eqmp
    R`>                               >`A=A                                       R`B

    (R, S) ` T (R, T ) ` S                         F :α→β      A:α R`F =G                R`A=B
                           ded                                                                      ceq
          R`S=T                                                 R`F A=GB

          R`A=B                                                       A:γ B:α
                              leq1                                                            hbl1
    R ` (λxα . A) = (λxα . B)                               > ` (λxα . λxβ . A) B = (λxβ . A)

                    B:α F :β→γ                                            A:β B:α
                                                       distrc                              ax-172
    > ` (λxα . (F A)) B = ((λxα . F ) B) ((λxα . A) B)                 > ` (λxα . A) B = A

                     A:γ B:α                                                   A:β
                                                  distrl3                                    beta
    > ` (λxα . λy β . A) B = λy β . ((λxα . A) B)                       > ` (λxα . A) xα = A


                      > ` (λxα . B) y α = B         xα = C ` A = B
                                                                        R`A
                      > ` (λxα . S) y α = S         xα = C ` R = S
                                                                                  inst
                                                 S`B



                                  Fig. 2.    The hol.mm axiomatization.

This substitution process happens for every application of every theorem, and the
only restriction on substitutions is that the substitution must be with a term, and
the distinct variable provisos must be honored.
   Unlike OpenTheory, vars in hol.mm do not come with built-in type information,
so a variable term takes a var as well as a type; this is represented as a superscript
in figure 2 (e.g. xα ). Metamath often refers to its variables as “metavariables”,
because they can be interpreted as variables which stand in for expressions of their
type in some lower object language. Note that even vars like x are metavariables
in this sense, but they can only be substituted with other vars (because the only
expressions of type “var” are other vars). The capital term variables, on the other
hand, can be substituted with other terms, like xα or (λxα . A). In Metamath, it
is easier to work with term variables than vars because they admit direct substitu-
tion, but only vars can be bound in constructs like lambda abstractions, so both

1 The variable x is required to not be present in the (expression substituted for) R.
2 The variable x is required to not be present in A.
3 The variable y is required to be distinct from x and not present in B.



                                                     Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
192     ·      Mario Carneiro

variable types are necessary in the Metamath interpretation. However, since this
conflicts with our terminology we will stick to calling these variables, and referring
to variables ranging over Metamath expressions as “metavariables”. For simplicity
of presentation, we will stick to using only vars during a derivation and keep the
term variables to just the axioms themselves.
   Most of the axioms have direct equivalents, but a few deserve extra explanation.
The axioms wtru, wct, id, syl, jca, simpl, simpr, trud are necessary in order to handle
context manipulation: doing the set unions in OpenTheory axioms like eqMp (this
is discussed in more detail in section 2.4). The axioms hbl1, distrc, distrl, ax-17 are
used to define the properties of the “not free in” predicate, which is used in inst.
Definition 2.3. Let NF(xα , A) denote the statement that > ` (λxα . A) y α = A is
derivable (with explicit metavariable y). We can read this as “x is not free in A”.
  Then ax-17 asserts that NF(xα , A) whenever A is a term that is distinct from x,
and hbl1 asserts that NF(xα , (λxβ . A)), while distrc and distrl can be used to show
that NF(xα , A) and NF(xα , B) imply NF(xα , A B) and NF(xα , (λy β . A)) (when
x and y are distinct). Thus this predicate allows one to represent the structural
property “x is not free in A” faithfully within the logic. (This same trick is used
in set.mm to represent the not-free predicate, although there it is expressed more
naturally as (ϕ → ∀x ϕ). The name ax-17 is borrowed from set.mm, where an
axiom by the same name asserts (ϕ → ∀x ϕ) when x is distinct from ϕ.)
  The three additional axioms in HOL are translated to the following three axioms:
eta > ` ∀f α→β . (λxα . f α→β xα ) = f α→β
ac > ` ∀pα→bool . ∀xα . (pα→bool xα ⇒ pα→bool (pα→bool ))
inf > ` ∃f ind→ind . (injective f ind→ind ∧ ¬surjective f ind→ind )
  These axioms are exactly what you would expect from the earlier listing on
page 190. Also, the following simple theorems of the system will be useful:

                                      >`A
                                              a1i
                                      R`A
                                  R`A=B
                                              eqcomi
                                  R`B=A
                             R`A=B R`B=C
                                                     eqtri
                                   R`A=C
                    A : bool C : bool R ` A = B R ` C = D
                                                           cteq
                               R ` (A, C) = (B, D)
                                 NF(xα , A) NF(xα , B)
                                                       hbct
                                    NF(xα , (A, B))
                               xα = y α ` A = B
                                                       cbv
                            > ` (λxα . A) = (λy α . B)
  In the last theorem, y must not be present in A and x must not be present in
B. This theorem is curious because although it is true using only OpenTheory core
theorems (trivially, since (λxα . A) and (λy α . B) are α-equivalent), it (provably)
requires eta for its hol.mm proof.
Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
                                 Conversion of HOL Light proofs into Metamath             ·     193

2.3   Language embedding
Our first step in defining the conversion from OpenTheory to hol.mm is to define
the embedding of formulas in one language into formulas in the other. We denote
this function as F.
Definition 2.4. The map F operates on statements, terms, and types of the
OpenTheory language, and outputs statements, terms, and types of the hol.mm
language.
   — For a constant term or type c, F(c) = c, where a constant named c is defined
in the file if it is not already present.
   — For a variable term v of type α, F(v) = v F (α) and F(λv. x) = (λv F (α) . F(x)),
where a var named v is defined in the file if it is not already present.
   — For a type variable α, F(α) = α, where a type variable named α is defined in
the file if it is not already present.
   — F(f x) = F(f ) F(x)
   — F(t : α) = F(t) : F(α)
   — F(α → β) = F(α) → F(β)
   — If A[α1 , . . . , αn ] is a type operator of arity n, then F(A[α1 , . . . , αn ]) =
A[F(α1 ), . . . , F(αn )], and A[β1 , . . . , βn ], with literal type variables β1 , . . . , βn , is
added as a syntax constructor if it is not already present (and β1 , . . . , βn are added
as type variables if not present).
   — F({φ1 , φ2 , . . . , φn } ` ψ) = ((F(φ1 ), F(φ2 )), . . . , F(φn )) ` F(ψ), unless n = 0
in which case F(` ψ) = > ` F(ψ).
Remark 2.1. Since sets are unordered but the context conjunction is, F(Γ ` φ)
is not uniquely defined. However, any of the choices of ordering of Γ produce
equivalent statements, and internally Γ is usually stored as a list anyway, so one
may as well use this ordering. Alternatively, one can define a total order on terms
and insist that the listing be done in increasing order to ensure uniqueness. In any
case, the ordering chosen will not be relevant to later developments.
   In the course of “evaluating” this function on the statements of an OpenTheory
derivation, at various points certain variables and constants will be added to the
logical system. This is necessary because all variable and constant names need to be
predeclared in a Metamath file, so this ensures that the predefinitions are made and
allows an OpenTheory file to use variables that may not have been defined in the
hol.mm core (which only defines variables that are used in the axioms themselves,
such as x, y, A, B, α, β. Any other variable names, like v, will need to be declared
before their use in a theorem).
   We assume that all term variable names in an OpenTheory derivation are dis-
tinct from type variable names and hol.mm core axiom and theorem labels, and no
variable is used multiple times in the same theorem statement with different types,
because OpenTheory will consider these distinct while hol.mm will consider them
the same (i.e. NF(xβ , (λxα . xβ )) even though OpenTheory would consider xβ as
free in that expression). This can be ensured with suitable preprocessing of the
OpenTheory article file.

                                                Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
194     ·      Mario Carneiro

  Now we are finally capable of stating the main goal of this part, although the
proof will be postponed to the next section.
Theorem 2.1. If the statement Γ ` φ is derivable in OpenTheory, then F(Γ ` φ)
is derivable in a conservative extension of hol.mm.
  The reason for the “conservative extension” caveat is because in addition to
the variables and constants being added to the system by F, our transformation
will also need to add definitions coming from defineConst and defineTypeOp, and
Metamath does not support a special definition construct. Instead, definitions and
axioms are treated on equal footing, and an external tool can be used to show that
the axioms that claim to be definitions are actually conservative.
2.4   Proving the embedded OpenTheory axioms
Our proof of theorem 2.1 will proceed by defining an explicit map from OpenThe-
ory derivations to hol.mm derivations. First, we show that proper substitution,
simplification, and α-equivalence are derivable.
Lemma 2.1. If A is a nested context conjunction containing B as a conjunct, then
A ` B is provable.
Proof. By induction on the length of A. If A = B, then id proves A ` B. If
A = (A1 , A2 ) and B is a conjunct of A1 , then simpl proves A ` A1 and by induction
A1 ` B is provable, so syl proves A ` B. The case of B a conjunct of A2 is similar
(using simpr instead).
Lemma 2.2. If A does not contain x and C = B[A/x] is the result of the proper
substitution of A for xα in B (where proper substitution of hol.mm terms is defined
similarly to OpenTheory proper substitution), then xα = A ` B = C is provable,
and NF(xα , C).
Proof. By induction on the length of B.
   — If B does not contain xα , then C is identical to B and so refl, a1i proves
x = A ` B = B and ax-17 proves NF(xα , B).
 α

   — If B = xα , then C = A so id proves xα = A ` xα = A and ax-17 proves
NF(xα , A).
   — If B = B1 B2 , then C = B1 [A/x] B2 [A/x], so the induction hypothesis gives
proofs of xα = A ` B1 = B1 [A/x] and xα = A ` B2 = B2 [A/x], and ceq proves
xα = A ` B = C and distrc, ceq prove NF(xα , C) from NF(xα , B1 [A/x]) and
NF(xα , B2 [A/x]). (The same is true when B = (B1 , B2 ), with cteq in place of ceq
and hbct for the proof of NF(xα , C).)
   — If B = (λxα . B1 ), then NF(xα , B), so C is identical to B and so again refl,
a1i proves xα = A ` B = B and NF(xα , B) is given.
   — If B = (λy β . B1 ) where x, y are distinct, then C = (λy β . B1 [A/x]) and distrl,
leq, eqtri proves NF(xα , C). If A does not contain y, then leq proves the goal. If
A does contain y, then leq is not directly applicable, and the proper substitution
for C = (λz β . C1 ) includes a dummy variable z. In this case, use the induction
hypothesis to prove y β = z β ` B1 = B1 [z/y], and then apply cbv, a1i to get
xα = A ` B = (λz β . B1 [z/y]). Using the induction hypothesis once more to prove
Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
                            Conversion of HOL Light proofs into Metamath            ·     195

xα = A ` B1 [z/y] = C1 , leq gives xα = A ` (λz β . B1 [z/y]) = C and eqtri proves
the goal theorem.


Lemma 2.3. If A is α-equivalent to B (where α-equivalence of hol.mm terms is
defined similarly to OpenTheory α-equivalence), then > ` A = B is provable.
Proof. By induction on the length of A.
   — If A is a variable or constant, then A = B and refl proves the goal.
   — If A = A1 A2 , then B = B1 B2 and ceq proves the goal.
   — If A = (A1 , A2 ), then B = (B1 , B2 ) and cteq proves the goal.
   — If A = (λxα . A1 ) and B = (λxα . B1 ), then leq proves the goal.
   — If A = (λxα . A1 ) and B = (λy α . B1 ), then let A01 = A1 [y/x] and A0 =
(λy α . A01 ). Then A is α-equivalent to A0 and B, so by the third clause > ` A0 = B
is provable, and by lemma 2.2 xα = y α ` A1 = A01 is provable, so cbv gives
> ` A = A0 and eqtri proves the goal.


Lemma 2.4. If A is α-equivalent to B and C is α-equivalent to D, then A ` C
implies B ` D.
Proof. Lemma 2.3 applied twice gives us > ` A = B and > ` C = D, and id,
a1i, eqmp, eqcomi turn these into B ` A and C ` D, and then syl gives B ` D as
desired.
  In order to prove Theorem 2.1, we cast it as a special case of a more general
theorem, using an invariant property which we’ll call reduction.
Definition 2.5. Given an OpenTheory term φ and a hol.mm term A, we say that
A reduces to φ if there is a φ0 α-equivalent to φ with F(φ0 ) = A, and given an
OpenTheory statement Γ ` φ and a hol.mm statement A ` B, we say that A ` B
reduces to Γ ` φ if there is a type variable substitution σ such that B reduces to
φ[σ] and for every ψ ∈ Γ either A reduces to ψ[σ] or A = (A1 , A2 ) and at least one
of A1 , A2 reduces to ψ[σ].
Remark 2.2. Note that F(Γ ` φ) always reduces to Γ ` φ.
   Intuitively, the notion of reduction from A ` B to Γ ` φ means that Γ is equiva-
lent to a subset of the conjunction of terms in A, and B and φ are equivalent. Thus
if Γ ` φ is provable, then A ` B has only added irrelevant antecedents, so it ought
to be provable as well. This forms our main invariant across the derivation.
Theorem 2.2. If Γ ` φ is derivable in OpenTheory and A ` B reduces to Γ ` φ,
then A ` B is derivable in a conservative extension of hol.mm, and if t : α is
derivable in OpenTheory, then F(t : α) is derivable in a conservative extension of
hol.mm.
Proof. The proof is by induction on the length of the proof of the OpenTheory
statement. We break the proof into cases based on the last inference rule in the
derivation tree.
                                          Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
196     ·      Mario Carneiro

   2.4.1 Direct conversions. Many of the axioms are converted directly into equiv-
alent axioms. Specifically:
  —    varTerm → wv
  —    absTerm → wl
  —    appTerm → wc
  —    refl → refl
  —    eqMp → eqmp
  —    appThm → ceq
  —    deductAntisym → ded
  —    extensionality → eta
  —    choice → ac
  —    infinity → inf
  Given derivations of all the hypotheses to one of these inferences, apply the
transformed step to the transformed hypotheses (and a1i to the result if A 6= >) to
get an α-equivalent statement, and the lemma 2.4 finishes the job.
 2.4.2 assume. This axiom is an application of lemma 2.1 to prove A ` B 0 where
  0
B is the conjunct of A that is α-equivalent to B, followed by lemma 2.4.
  2.4.3 absThm. This axiom is almost a direct application of leq, but the require-
ment is only that Γ not have v free in it, not that v be completely disjoint from
Γ. However, if v is not free in Γ, then there is a Γ0 that is disjoint from v and
α-equivalent to Γ, so leq proves F(Γ0 ) ` (λxα .A) = (λxα .B) from F(Γ0 ) ` A = B
and lemma 2.4 applied before and after turn the Γ0 into Γ in this inference.
   2.4.4 subst. There are two kinds of substitution performed by subst—type vari-
able substitution and term variable substitution. If a type variable substitution is
performed, so that Γ = Γ0 [σ] and φ = φ0 [σ], then Γ0 ` φ0 is also reducible to A ` B,
so A ` B is provable.
   If σ = [x1 7→ A1 , . . . , xn 7→ An ] is a term variable substitution, then by writing
this as a composition of [x1 7→ y1 , . . . , xn 7→ yn ] with [y1 7→ A1 , . . . , yn 7→ An ] where
yi are dummy variables, we can reduce this to the case when no Ai contains any
xj . Then we can rewrite it again as the composition of σ1 = [x1 7→ A1 ], . . . , σn =
[xn 7→ An ], so that we can reduce to the case of a single variable substitution. And
this case is handled by axiom inst, with the hypotheses filled by lemma 2.2.
   2.4.5 betaConv. This axiom is an application of beta followed by the same sub-
stitution process described in section 2.4.4 (and a1i, lemma 2.4).
  2.4.6 Definitions. Lastly, we have the two definitional axioms, defineConst and
defineTypeOp. In this case, we simply introduce all the output statements as axioms.
We can do a little better, though; by introducing the axioms
                                  B:α      R`A=B
                                                 eqtypri
                                           A:α

                          > ` F B TDβ,A,R (F, B)
                                                                               typedef
 A:α→β           R : β → α > ` (A; (R xβ ) = xβ , F y α = (R (A y α ) = y α ))
Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
                            Conversion of HOL Light proofs into Metamath           ·     197

we can set it up so that the only axiom needed for defineConst is a single axiom
> ` c = t for the constant’s definition, and the only axiom needed to define a new
type is TDβ,A,R (F, B) (which is a new kind of statement designed solely for input to
typedef). However the checking that the constant does not appear in the definition,
the typedef’s type constant β lists all free type variables in use, etc. must still
be checked outside the system. Nonetheless, as long as the original OpenTheory
derivation followed these consistency rules, the transformed definition will also be
conservative, for the same reasons, so it does not interfere with this proof.
Proof of Theorem 2.1. Follows immediately from Remark 2.2 and Theorem 2.2.

3.   PART II: CONVERSION FROM hol.mm TO set.mm
In this part, we have the remaining job of transforming our Metamath representa-
tion of a HOL axiomatic system into ZFC. Although the foundations are changing,
the basic functions of substitution and the like are the same on both the start and
endpoint of the transformation, so we can focus on the mathematical content of the
sentences without worrying as much about the exact representation of the formula.
We begin by describing the model of HOL that we will build in ZFC:
Definition 3.1. A type α is a pair hια , bα i of a witness and a base set such that
bα ∈ Vω+ω (where Vω+ω is the second limit step of the cumulative hierarchy) and
ια ∈ bα . Let Ch() denote that either  is a choice function on Vω+ω or there is no
such function, and define a map S from types, terms and statements of hol.mm to
sets and wffs of set.mm.
   — For the two constant types, we take S (bool) = h1, 2i := h1, {0, 1}i and
S (ind) = h0, ωi, and define S (>) = 1.
   — For type variables, S (type α) ↔ α ∈ Type, where α ∈ Type is defined to
mean that α is a type in the sense above; this hypothesis is implicit in all axioms
that involve type variables.
   — For convenience, define the wff predicate toWff(A) ⇐⇒ A = 1, and the
function toBool(ϕ) = if(ϕ, 1, 0).
   — A variable is mapped to S (xα ) = if(x ∈ bα , x, ια ).
   — For the function type, we take S (α → β) = h(x ∈ bα 7→ ιβ ), bbβα i, the set of
all ZFC functions from α to β, with a constant function as witness.
   — Function application is represented by function application:
S (F A) = (F ‘A).
   — Lambda abstraction is represented by the mapping operator
S (λxα . A) = (x ∈ bα 7→ A).
   — Context conjunction is represented by conjunction:
S ((A, B)) = toBool(toWff(A) ∧ toWff(B)).
   — For a term, S (A : α) ↔ A ∈ bα .
   — For a theorem, S (A ` B) ↔` (Ch() ∧ toWff(A)) → toWff(B).
   — The equality operator =α is mapped, depending on its type, to S (=α ) =
(x ∈ bα 7→ (y ∈ bα 7→ toBool(x = y)))


                                         Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
198     ·      Mario Carneiro

  — The indefinite descriptor α itself is mapped, depending on its type, to
      S (α ) = (f ∈ b{0,1}
                       α     7→ if(∀x ∈ bα . f (x) = 0, ια , ({x ∈ bα : f (x) = 1}))).
  — A defined type S (TDβ,A,R (F, B)) asserts that β = hB, {x ∈ bα : toWff(F (x))}i,
A = (x ∈ bα 7→ if(x ∈ bβ , x, B)), and R = (x ∈ bβ 7→ x).
   Most of these definitions are exactly what you would expect—functions are func-
tions, and types and terms map to sets and their elements. The unusual part of
the definition deals with the indefinite descriptor . HOL is based on a version of
the Axiom of Choice that is stronger than the usual one in ZFC. Instead of as-
serting that for any set there exists a choice function on that set, it asserts that
a specific function is a choice function on the universe. If the HOL universe were
a proper class, this would be problematic, but luckily it can be entirely contained
within Vω+ω , which is a set in ZFC, and thus the ZFC axiom of choice gives us
a single choice function  on all of Vω+ω . We pass this in as a parameter to S,
so that we can give meaning to the various pieces of the formula that use , and
theorems assert the choice behavior of , so that it can be used in derivations. The
reason for the “or if there is no such function” proviso is to allow the proof of
` S (> ` A) =⇒ ` toWff(A) to avoid choice, so that the ZFC choice axiom never
gets invoked unless ac does. Since we also require a term variable to have uncondi-
tional closure, we are forced to add witnesses so that we don’t need to invoke choice
by using  to select elements.
   The construction here is performed using Vω+ω , but of course it is also possible
to use Vδ for any limit ordinal δ > ω, and this can be passed in as an extra
parameter to make a translation Sδ, which depends on δ. However, as this makes
the translation process more cumbersome to describe, we will assume δ = ω + ω
and leave the extension process to those who need the extra power this affords.
3.1   Proving the hol.mm axioms
Theorem 3.1. If A ` B is derivable in hol.mm, then ` S (A ` B) is derivable
in set.mm. In particular, if A ` B does not contain , then ` S(A) → S(B) is
derivable (where the  has been dropped from the notation to indicate that the
action of S does not depend on ).
Proof. Here we merely need to verify that each of the axioms is preserved under
wrapping by S . Note that S can actually be defined in set.mm, so that each of
the axioms, in S -wrapped form, can be proven as theorems within set.mm, and
then the transformation will be one-to-one in terms of proof length. Also, keep in
mind that there are implicit hypotheses that α, β, etc. are types; these become
explicit hypotheses during this translation. Abbreviated proofs for each axiom are
presented, using theorem labels for existing set.mm proofs when necessary [col14].
  — type bool: 1 ∈ 2 ∈ Vω+ω
  — type ind: 0 ∈ ω ∈ Vω+ω
  — type (α → β): If rank(bα ) = m < ω + ω and rank(bβ ) = n < ω + ω, then
rank(bbβα ) ≤ max(m, n) + 3 < ω + ω
  — wtru: 1 ∈ 2
  — wct: toBool of anything is in 2
Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
                               Conversion of HOL Light proofs into Metamath            ·     199

  — wc: If f : α → β and x ∈ α, then f (x) ∈ β
  — wv: If x ∈ bα , then if(x ∈ bα , x, ια ) = x ∈ bα , otherwise ια ∈ bα
  — wl: If for all x, T ∈ bβ , then (x ∈ α 7→ T ) : bα → bβ
  — id: theorem simpr2
  — syl: theorem syldan
  — jca: theorem jca
  — weq: use the definition and two applications of wl
  — simpl,simpr: theorem simpl,simpr
  — trud: theorem a1i,tru
  — refl: theorem eqidd
  — eqmp: theorem mpbid after showing toWff(A = B) ↔ (toWff(A) ↔ toWff(B))
by case analysis)
  — ded: theorem impbid,expr
  — ceq: theorem fveq12d
  — leq: theorem mpteq2dv
  — hbl1: theorem hbmpt1
  — distrc,distrl: short proof using vtoclg,fvmpt2
  — ax-17: theorem fvmpt,eqidd
  — beta: theorem fvmpt2
  — inst: theorem vtoclf
  — eta: theorem dffn5v
  — inf: short proof using (x ∈ ω 7→ x + 1)
  — ac: By definition, α (p) = if(∀x ∈ bα . p(x) = 0, ια , ({x ∈ bα : p(x) = 1})),
but since p(x) = 1, the if-condition is false, so α (p) = ({x ∈ bα : p(x) = 1})).
Assuming ax-ac,  is a choice function on Vω+ω , and {x ∈ bα : p(x) = 1} is a
nonempty subset of bα ∈ Vω+ω , so ({x ∈ bα : p(x) = 1}) ∈ {x ∈ bα : p(x) = 1},
and thus p(α (p)) = 1.
   For the final statement, observe that no S transformation depends on  except
S (α ), so if  is not in A or in B then it will not be in the right hand side of Ch() →
(S(A) → S(B)), and theorem exlimiv turns this into ∃. Ch() → (S(A) → S(B)).
But ∃. Ch() is provable, because if there is a choice function  on Vω+ω then Ch()
for that choice of  and if not then Ch(0) is true.

4.   FUTURE WORK
We stopped at Part II here, but one can argue the existence of a part III to this
translation project, where notations such as the HOL Light natural numbers are
mapped via the natural isomorphisms to the set.mm natural numbers, so that a
statement like the Prime Number Theorem, which is (as of this writing) proven in
HOL Light but not in set.mm, can be said to be proven in its “natural form”, rather

2 This and the other theorem names mentioned here refer to theorem labels in set.mm. There are

individual web pages for these, for example simpr is found at http://us.metamath.org/mpegif/
simpr.html.

                                             Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
200       ·      Mario Carneiro

than in some model. This process is much less formulaic, however, and requires
individual considerations of each mathematical concept in order to identify the
proper isomorphisms.

ACKNOWLEDGMENTS
The author wishes to thank Norman Megill, Bob Solovay, and Raph Levien for their
work on investigating Part II in many email discussions, as well as John Harrison
for creating HOL Light and Joe Leslie-Hurd for creating OpenTheory and providing
the source material for figure 1.

References
[col14]       Metamath collaboration.      Metamath Proof Explorer.        http://us.
              metamath.org/mpegif/mmset.html, 2014. [Online; accessed 18-Dec-
              2014].
[Far08]       William M Farmer. The seven virtues of simple type theory. Journal of
              Applied Logic, 6(3):267–286, 2008.
[Har09]       John Harrison. HOL Light: An overview. In Stefan Berghofer, Tobias
              Nipkow, Christian Urban, and Makarius Wenzel, editors, Proceedings of
              the 22nd International Conference on Theorem Proving in Higher Order
              Logics, TPHOLs 2009, volume 5674 of Lecture Notes in Computer Science,
              pages 60–66, Munich, Germany, 2009. Springer-Verlag.
[Hur11]       Joe Hurd. The OpenTheory standard theory library. pages 177–191, 2011.
[Kun11]       Ondřej Kunčar. Proving valid quantified boolean formulas in HOL Light.
              Lecture Notes in Computer Science, 6898:184–199, 2011.
[Meg07]       Norman D. Megill.       Metamath: A Computer Language for Pure
              Mathematics.     Lulu Publishing, Morrisville, North Carolina, 2007.
              http://us.metamath.org/downloads/metamath.pdf.




Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
