Sorts and terms

An .mm0 file declares a theory: the syntax of its expressions, its axioms, and the theorems to be proved. A verifier checks the compiled .mmb proof against this declaration. The .mm0 file is the specification that an .auf proof development must satisfy.

An .mm0 file contains a sequence of statements, each ending in a semicolon. This chapter explains the statements that declare a theory’s syntax.

Sorts

A sort is a syntactic category, declared with sort:

sort tm;

Every expression belongs to exactly one sort.

Sort declarations can carry modifiers. The most common is provable:

provable sort wff;

provable means expressions of this sort can be asserted: they may appear between $ signs as an axiom’s conclusion, a theorem’s statement, or a proof line’s goal. Most theories have exactly one provable sort. The opening Hilbert theory used wff as its only sort. The natural deduction examples also used sorts for contexts and sequents.

Term constructors

A term statement declares a way to build expressions.

term imp (a b: wff): wff;

imp takes two expressions of sort wff and produces another wff. Within a math string (text between $ signs), write the constructor before its arguments. Parenthesize any argument that is itself an application:

$ imp a (imp b a) $

Constructors and variables are the only syntactic forms that MM0 supports. The -> in earlier chapters was notation for the imp constructor. Here is the implication fragment from earlier chapters without that notation.

Proofs using the notation-free syntax differ only in how their formulas are written.

Argument names are used only for dependencies between binders (the subject of the next chapter). A constructor whose argument names are never referred to can be declared with an arrow type instead:

term imp: wff > wff > wff;

Delimiters

Theories generally open with something like this:

delimiter $ ( ) $;

The parser normally splits math strings into tokens at whitespace. Characters listed in this form of delimiter also create token boundaries wherever they occur. Without this declaration, (imp is one unknown token rather than ( followed by imp. Notation explains the other delimiter options.

Several sorts

A theory can declare as many sorts as it needs. A first-order theory usually has two: one for the objects it talks about and one for the statements it makes about them.

tm is not provable, which is why a numeral is not a valid assertion. Add axiom bare (n: tm): $ suc n $; to the theory cell and it reports that the math string does not have a provable sort. In this theory the only assertions available are equations.

Sorts also provide the signatures for constructors. For example eq takes two tms, so eq a (eq a a) is rejected — the inner equation is a wff, and a wff is never a tm.

Coercions

A coercion lets the parser convert an expression from one sort to another. It names a one-argument constructor that the parser inserts when the surrounding expression requires the target sort.

hyp turns a formula into a one-element context. The coercion lets us omit it: ax is written nd a a, although nd requires a ctx as its first argument. After the parser inserts the coercion, this is nd (hyp a) a. Writing the constructor out gives the same expression:

These declarations make a formula by itself denote a one-element context in the natural-deduction theory used in Proof search.

A coercion may also be what makes a sort assertable. If the arithmetic theory above declared term holds (t: tm): wff; and coerced tm > wff, then $ suc zero $ would be a statement after all, meaning holds (suc zero).

The parser can chain coercions when several conversions are needed. To prevent ambiguity, there must be at most one path between any two sorts, even when the direction of each coercion is ignored.

Sort modifiers

MM0 provides three other sort modifiers.

Modifiers are written before sort and can be combined. Most theories need only provable. The other three govern how the sort interacts with variables; Variables, binders, and dependencies gives the details.