Axioms, theorems, and definitions

Besides declaring a theory’s syntax, an .mm0 file states its axioms and theorems and introduces definitions.

Axioms

An axiom states a rule that the theory accepts without proof.

axiom ax_k (a b: wff): $ a -> b -> a $;

Hypotheses go ahead of the conclusion, separated by >:

axiom mp (a b: wff): $ a $ > $ a -> b $ > $ b $;

The last formula is the conclusion and every formula before it is a hypothesis, so mp says b is derivable whenever a and a -> b are. Every formula in an axiom must have a provable sort.

An axiom’s binder list gives the sorts with which the rule may be instantiated and any restrictions described in Variables, binders, and dependencies.

Hypotheses as binders

A hypothesis can also be written as a binder with a formula for its sort.

axiom mp (a b: wff) (h1: $ a $) (h2: $ a -> b $): $ b $;

This declares the same rule as the arrow form above. The two can be combined, and hypotheses are taken in the order they appear either way.

Ordinary binders may follow a hypothesis binder, but a hypothesis can only mention variables already declared to its left, so in practice the variables come first.

Proof lines cite hypotheses with a # reference: positionally as #1 and #2 under either spelling, or by name as #h1 and #h2 when the hypothesis is a named binder.

Theorems

A theorem is written like an axiom.

theorem id (a: wff): $ a -> a $;

Unlike an axiom, a theorem requires a proof block in the .auf file.

The .mm0 file gives a human-readable specification of what the compiled .mmb file must prove. The verifier checks the binary proof against that specification.

Definitions

A def introduces a new constructor that abbreviates a different expression.

A defined term such as not is still a constructor and can carry notation. Definitions are conservative: replacing each defined term with its body removes the definitions without changing what is provable.

Definitions are transparent at rule applications. The folded and unfolded forms are the same expression as far as matching is concerned, so each line can be written in whichever form is clearer.

weaken_not is ax_k instantiated at a -> F., unfolded on the left of the arrow and folded on the right. not_elim gives mp the folded term ~ a for its second, implication-shaped hypothesis; it unfolds automatically.

Dummy variables

A definition’s body may use variables that are not among its arguments. A dot in the binder list indicates that the variable is hidden and not among the required arguments of the definition.

uniq takes x and p. Its y is internal to the body. A proof that unfolds uniq may instantiate it with any variable that does not clash. The free sort modifier described in Sorts and terms forbids hidden dummies of a sort.

Definition checking

A definition’s result type must declare every variable that remains free in its body: that is, every variable not captured by a binder in the body.

definition body has free variables that the result type does not declare

The body eq x x has x free, and the bare sort wff does not declare any dependencies. The fix is to declare the dependency the body really has. A def may carry dependencies on its result type in the same way as a term.

Here’s the fixed version:

def refl_of {x: tm}: wff x = $ eq x x $;

Every refl_of x now counts as having x free — as it must, since unfolding it produces eq x x.

Binders inside the body capture free variables. uniq from the previous section is accepted with a bare wff because ex y and all x between them capture everything:

FV(eq x y)                        = {x, y}
FV(iff p (eq x y))                = {x, y}
FV(all x (iff p (eq x y)))        = {y}
FV(ex y (all x (iff p (eq x y)))) = {}

FV(p) is {x} because uniq declares p as wff x. What makes all x subtract that x again is all’s declaration, term all {x: tm} (p: wff x): wff: the x on the argument p says that this constructor binds x within that argument. If you declare it as (p: wff) then all does not bind anything.

This free-variable computation occurs only during definition checking. At rule applications, the restrictions from Variables, binders, and dependencies use plain occurrence: an expression counts as mentioning a variable if the variable appears anywhere in it, even under a binder. all x (eq x y) cannot instantiate an argument whose dependency list excludes x, although x is not free in it. Binding structure counts when a definition is checked, and never when a rule is applied.

Definitions without a body

The body of a definition may be omitted.

def nand (a b: wff): wff;

The .mm0 interface declares that the connective exists without specifying its body. Theorems about the connective can specify its required properties. The proof file must supply a body and prove those theorems, as described in Lemmas and definitions in proofs.