This document describes the definition mechanism of Ghilbert, also providing motivations and an argument for its soundness. ## GoalsOne 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 commanddefthm (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).
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 argumentThe 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.
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. - A note on definitions [Metamath]
- Distinctors vs binders (in which I argue that perhaps distinct variables allow for a richer set of definitions than allowed with explicit free variables - however, I'm now quite satisfied with the richness available in new Ghilbert)
- Principal instances of metatheorems (deeper discussion of the distinction between metavariables and variables in Metamath)
## Comments by Carl WittyAfter I posted the above, Carl sent the following comments by email, reproduced here:
On point (2), I would love to see the example, yes. I can't quite picture what you have in mind. |

Documents >