Documents‎ > ‎

Definitions

This document describes the definition mechanism of Ghilbert, also providing motivations and an argument for its soundness.

Goals

One goal of Ghilbert relative to Metamath is to provide a safe definition mechanism, while at the same time preserving the richness of definitions enjoyed by Metamath. In particular, the Ghilbert definition mechanism should allow creation of new binding terms (this feature is missing from Mizar), including the full richness of proper substitution - [A / x] ph. Note that x may appear free in A in such a term, and also that x is considered free in [A / x] ph if so (and only if so). Thus, defined terms may have interesting behavior with respect to free variables even if the underlying terms in the axioms only describe simple binding. [This motivates the new optional free variable clauses in the term command, not yet properly documented, but if you want to understand it, the TestFv cases in verify_test.py in the ghnew prototype are a good place to start. todo: replace with reference to appropriate section in documentation]

In Metamath, new definitions are essentially axioms. By convention, most such definitional axioms follow the form definiendum = definiens or definiendum <-> definiens, where the definiens is an expression containing no free variables not appearing in the definiendum, and also where the definiendum does not appear in the definiens. (Definitions which would most naturally be written as recursive are instead stated in terms of explicit recursion operators such as df-rdg.) However, these conventions are nowhere enforced, and, indeed, the constraint on free variables is not directly expressible in the Metamath metalogic.

The defthm command

defthm (label
  kind definiendum
  free-variable-conditions
  hyps
  conclusion
  proof)

Here's a simple example, for concreteness:

defthm (df-or
  wff (\/ ph ps)
  () ()
  (<-> (\/ ph ps) (-> (-. ph) ps))
  (-> (-. ph) ps) pm4.2)

Note that, syntactically, this is the same as thm with the kind and definiendum fields added. Note also that these new fields are the same as would appear in a term command in an interface file. This is not a coincidence - a defthm in a proof file will generally export that term and also a stmt corresponding to the thm in the usual way.

The definiens follows the same syntax as in the term command: the term name comes first, followed by a list of variables (both term and binder allowed) without duplicates.

Unlike thm, the proof stack at the end of evaluating the proof is not identical to the conclusion. Rather, it matches. The definiendum appears one or more times in the conclusion. Where it appears, a term of matching kind (the definiens) must appear in the term at the end of the proof stack. If the definiendum appears more than once, all corresponding terms must be identical. (The main motivation for allowing more than one is allowing df-bi).

Binding variables which appear in the definiens but not the definiendum are definition dummies. These variables are special, and treated considerably different than other variables. These variables are subject to the following additional constraints:

  • They must not appear in either the conclusion or the hypotheses.
  • They must not appear free in the definiens (i.e. they are always bound).
The usual consequence of these rules is that the theorem justifying a definition that involves a definition dummy generally takes the form of an alpha conversion. Note that the metalogic of Ghilbert does not assume that alpha conversions are true - rather, they must be proved from the axioms of the logic.

[todo: put another example here containing an alpha conversion]

Soundness argument

The above rules were very carefully crafted to ensure that definitions are conservative, i.e. after being expanded out they do not add to the set of theorems that can be proved. This section will give an argument that this is so.

First consider the Ghilbert fragment not including definitions. A proof tree can be expanded by replacing each reference to a thm with the body of that thm, applying relevant substitutions, and instantiating all dummy variables with fresh variables. (Recall that a dummy variable is one that occurs in the proof of a thm but not in the hypotheses or conclusion). When done repeatedly until no longer possible, a proof tree is fully expanded, and refers only to axioms (whether simple axioms with no hypotheses or inference rules given as axioms, such as ax-mp). One of the soundness obligations of the Ghilbert metalogic is that this fully expanded proof is valid. Most important for this discussion, each free variable constraint of every instance of an axiom is respected. (These constraints include explicitly stated constraints that certain binding variables not appear free in the expressions substituted for certain other term variables, and also the implicit assumption that any two binding variables in an axiom have two distinct binding variables).

Metamath makes a distinction between the metavariables appearing in Metamath proofs and the simple variables that may appear in instantiations. Of course, in Metamath there is no implicit assumption that binding variables be unique, and such distinctness constraints need to be explicitly stated. For example, in Metamath "A. x A. y ph <-> A. y A. x ph" is a theorem (alcom) that, in fact, is still valid when the variables are not disjoint, so it can be instantiated both ways. In Ghilbert, these would have to be represented as two different theorems. Thus, in Metamath the distinction between metavariable and variable is important.

Note that the rules for defthm, while not explicitly stating the definiens, allow it to be inferred. Thus, there is a well defined mapping from definiendum to definiens. This is almost enough to fully describe the operation of expanding a definition ("unfolding" in GrafZahl's terminology). The missing bit is (as is not surprising) the definition dummies.

One traditional approach would be to use fresh variables, just as for ordinary dummies. However, this has the problem that the expansion of a definition would no longer be unique. If the two expansions in E! x ph <-> E! x ph got distinct fresh variables, then a proof of this theorem using pm4.2 would not be sound. Of course, in standard the expanded theorem would still be provable through an alpha conversion, but that violates the spirit and the letter of the goal of definitions being conservative.

Other authors have struggled with this. Margaris [todo: proper cite, p. 109] introduces E! thusly:

Statements of the following forms are very common in mathematics:

 There is one and only one u such that P(u)
 There is exactly one u such that P(u)
 ...

We translate each of them as

E. u P(u) /\ A. u A. v (P(u) /\ P(v) -> u = v)            (1)

where P(v) is P(v/u) and v is the first variable in the alphabetic list of variables that does not occur in P(u). Then we abbreviate (1) as

E! u P(u)                      (2)

We have chosen v in (1) to be a specific variable to make sure that (2) has a unique unabbreviation. In practice, v can be any variable such that P(u) is similar [alpha-convertible] to P(v).

We have no qualms about reusing variables (some logicians do; see df-sb for a bit of discussion). Even if v does occur in P(u), as long as it is not free, it can be used as a dummy variable. And the rules for defthm insist that the definition dummy variables almost never appear free in terms (the exception is within the proof of the justifying theorem itself, and all theorems invoked in that proof are unable to reference the definition). Thus, for the purpose of expanding definitions, we use the following rules:

  • Each occurrence of an ordinary dummy is instantiated to a distinct, fresh variable.
  • Each occurrence of a definition dummy is instantiated to the same variable. Of course, variables from multiple definitions are considered distinct (so just the identifier is not sufficient, and if a definition has more than one binding variable, they are also distinct.
Note that if def and thm were separated (as was the case in earlier drafts of Ghilbert), there would be opportunity for unsoundness. Two different proofs could expand the definition, and the second one could invoke the first, instantiating an ordinary binding variable in the first theorem with a def dummy. Then, in the fully expanded theorem, the same variable would appear twice, once as the instantiation of that variable and again as the def dummy. [todo: this is pretty confusing, might be clearer as an actual example]

A full proof of soundness, including definitions, is a fairly substantial task, and a careful specification of Ghilbert is of course a necessary precondition. In the meantime, one important invariant can be stated:

The set of free variables in a term is invariant when definitions are expanded.

The desire to maintain this invariant has had extremely profound effects on the design of Ghilbert. Among other things, it means that the concept of variable freeness must be built into the metalogic. This, combined with the ugliness of dealing with (cv x) terms in previous Ghilbert drafts, is the main motivation for the change.

Other discussions:

Some relevant links:

An earlier draft of Ghilbert (draft spec) had an unsound definition mechanism. Dan Kresje discovered the unsoundness a while ago, and GrafZahl recently discovered another example. There are several attempts in the JHilbert world to fix this. See Definitions in JHilbert for the master discussion, and also Carl Witty's proposal. For historical background, also see GrafZahl's Botched attempt to prove JHilbert definition soundness.
Plus there's some more discussion about the unsoundness of earlier Ghilbert attempts that's probably mostly in email threads.

Comments by Carl Witty

After I posted the above, Carl sent the following comments by email, reproduced here:

1) Basically, you're saying that every definition is expanded exactly
once -- after a defthm, the verifier never again makes use of the
definition.  This requires that everything you would ever want to know
about a definition can be captured in a single theorem.  This is fine
for set.mm, but might be a problem for weaker object logics.  For
example, I'm imagining a version of HOL that has no formalized concept
of type equality (types are equivalent only if they are syntactically
identical); I think it would not be feasible to use this definition
mechanism at the type level in such a formalization.

2) I think that your proof of conservativity is going to want to use
levels.  The only way I can think of to prove conservativity is to
prove that every proof that uses definitions can be translated to an
equivalent proof with all definitions expanded; if expanding a
particular definition always uses the same variable for its dummy
variable, then this is not necessarily true.  (The idea is to consider
a particularly weak object logic, where you can prove some
alpha-equivalences -- enough to construct the definitions -- but not
all alpha-equivalences.  I can provide an example if you want.)

With your somewhat weak definitions (definitions are only folded in
the corresponding defthm), you don't need levels in the verifier, only
in the proof of conservativity.

On point (1), my feeling is that, yes, in order to axiomatize such an HOL, you would need to have explicit axioms of type equality. But I'm open to making the definition mechanism more powerful if it's still simple and I believe the soundness argument.

On point (2), I would love to see the example, yes. I can't quite picture what you have in mind.

Comments