Structured Typesetting for Metamath

Metamath's set.mm database constructs mathematics from scratch, starting from ZFC set theory axioms, up to algebra, topology, analysis, graph theory and more. It includes over 32,000 formalized proofs, all of them automatically verified.

Metamath itself does not prescribe any syntax, other than the fact that formulas shall be unambiguously parseable: they are basically a string of tokens. The set.mm database defines mathematical symbols as such tokens, so that their ASCII version resembles as closely as possible to their counterpart in mathematical notation. The "GIF" and "unicode" typesettings then renders these tokens one by one. For advanced formulas, this notation is increasingly diverging from the classical mathematical notations. This may be a barrier for people discovering Metamath.

This project, structured typesetting, provides a display of set.mm's formulas as close as possible to the usual mathematical notations, and hopes to enable access to Metamath's set.mm to more people. Here are a few interersting entry points from which to browse on:

Below is an example of how the same formula, the statement of the trirn theorem, is displayed in the different typesettings:

Original Metamath source |- ( ph -> ( sqr ` sum_ k e. A ( ( B + C ) ^ 2 ) )
      <_ ( ( sqr ` sum_ k e. A ( B ^ 2 ) ) + ( sqr ` sum_ k e. A ( C ^ 2 ) ) ) )
GIF typesetting
Unicode typesetting
Structured typesetting

In the cases where it simplifies the display, structured typesetting may however hide the formula's structure. In the example above, for example, the square roots are formalized as the value of the function sqr. This is not directly visible in the structured typesetting.

How does it work?

The MathML markup language is an ISO standard and the W3C recommendation for embedding maths in documents on the Web, therefore it seems a reasonable choice for displaying Metamath's formulas.

Both MathML and Metamath can be seen as using a tree-like representation for formulas. The formula of the example above, for example, can be seen as: (click on the bullets to collapse nodes)

In presentation MathML, the same formula can also be seen as a tree:

The idea of structured typesetting is to transform one structure into the other. One possibility would have been to give the representation for each of set.mm's syntactic axiom, like for csu and wi. However, in order to be even more flexible, it is actually based on rules. The formula to be displayed is matched against that set of rules, and if a match is found, then the same is applied to each of its element, recursively.

Adapted representations:

Metamath's conventions page provides very useful explanations about the notations used in set.mm. Where possible, the notation attempts to conform to modern conventions, with variations due to our choice of the axiom system or to make proofs shorter. However, our notation is strictly sequential (left-to-right). For example, summation is written in the form Σ𝑘 ∈ 𝐴𝐵 (df-sum) which denotes that index variable 𝑘 ranges over 𝐴 when evaluating 𝐵. Thus, Σ𝑘 ∈ ℕ (1 / (2↑𝑘)) = 1 means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum). Structured typesetting and MathML on the other hand, allow to display formulas using underscripts, overscripts, subscripts ans superscripts. See df-sum and geoihalfsum for the representation of the same formula wiht structured typesetting.

Formulas displayed with structured typesetting will not differ much from formulas displayed in the Unicode typesetting, until more complex constructs are introduced. Most of the propositional calculus, predicate calculus and work ZFC abstract class building will look very similar in both typesettings. However, staring with functions, structured typsetting for set.mm will displays formulas differently, to get as near as possible to the classical math representation.

Function values, to start with, may surprise new users by the way they are represented in set.mm. In set.mm, the value of the function F applied at X is written ( F ` X ). Structured typesetting allows to write is as the more conventional F X

The table below provides a comparison of several mathematical constructs, with their representation in set.mm and in structured typesetting.

Construct name ASCII Representation in set.mm Structured typesetting Example theorems
Function value ( F ` X ) F X f1ofveu
Image of a set ( F " A ) F X unipreima
Inverse functions `' F F -1 unpreima
Sums, products, unions, intersections iterating over sets sum_ x e. A ( F ` x )
prod_ x e. A ( F ` x )
U_ x e. A ( F ` x )
|^|_ x e. A ( F ` x )
xA F x xA F x 0.999...
risefacval
Sums, products, unions, intersections iterating over integer intervals sum_ x e. ( 1 ... N ) ( F ` x )
prod_ x e. ( 1 ... N ) ( F ` x )
U_ x e. ( 1 ... N ) ( F ` x )
|^|_ x e. ( 1 ... N ) ( F ` x )
x=1 N F x pcfac
Fractions ( 1 / 2 ) 12 geoihalfsum
Intervals ( 0 [,) 1 ) 01 icoun
Absolute values
Set cardinal
( abs ` A )
( # ` A )
A hashun
Square roots ( sqr ` x ) x sqrdiv
Complex conjugate ( * ` z ) z addcj
root1cj
Decimal numerals ; ; 3 6 5 365 birthday
1kp2ke3k
Binomial coefficient ( M _C N ) ( M N) bcp1n
Exponential notation ( A ^ B )
( A ^c B )
( exp ` X )
A Be X efadd
Factorials ( ! ` N ) N ! facp1
Integrals S_ [ A -> B ] ( F ` x ) _d x
S. E ( F ` x ) _d x
A B F X dx E F X dx ditgsplit
Derivatives ( RR _D F )
( RR _D ( x e. A |-> B ) )
F dx A B d x mvth
divlip
dvexp3

Brackets/parenthesis

TBC

Invisible times

TBC

What is kept the same:

In set.mm, there is a major difference between set variables, written in red lowercase, and class variables, written in pink uppercase. For example, quadratic equations, which are usually written with all variables in lower case ax2 + bx + c, are written in uppercase in Metamath if class variables are used. We keep the set.mm notation for class variables, so the same equation may be rendered AX2 + BX + C.