Definitions in Mizar

The main parts of a Mizar article are:

1. Definitions
   • <Definitional-Items>
   • <Function>
   • <Predicate>
   • <Mode>
   • <Structure>
   • <Attribute-Definition>
2. <Theorems>
3. <Schemes>

Constructors are the real, unambiguous functions, predicates, types, and attributes to which the patterns are translated before any checking takes place.

Patterns are mapped to the constructors; they accomodate the need for having different symbols for the same constructor or vice-versa.

The process, mapping patterns to constructors, is done separately for each Mizar article depending on its <Environment-Declarations>. It is usually quite nontrivial.

(I suppose this is somewhat analogous to a macro system?)

The possible choices were TPTP, DFG (for SPASS), and Otter formatting. Urban went with DFG for SPASS.

The basic approach to translation was the following:

1. The Mizar Parser and Analyzer translated Mizar articles to the constructor level
2. Absolute (i.e., context independent) names are given to all constructors
3. Definitions of constructors translate usually to several first-order formulas
   • We have to translate both the type hierarchy information given in the definition, and the actual <Definiens>
4. Sometimes additional properties of the defined constructor are stated inside the definition (e.g., commutativity, transitivity, etc.).
   • They are also translated into corresponding first-order formulas.
5. All formulas are relativized with respect to the typed variables occurring in them; so for x being Real holds x-x = 0 translates to Real(x) implies x-x=0

The syntactic structure of <Mode-Definition> is:

<Mode-Definition> =
	"mode" <Mode-Pattern> ( [ <Specification> ] [ "means" <Definiens> ] ";"
<Correctness-Conditions> | "is" <Type-Expression> ";" ) { <Mode-Property> } .

<Mode-Pattern> = <Mode-Symbol> [ "of" <Loci> ] .
<Mode-Symbol> = <Symbol> | "set"

<Loci> = <Locus> { "," <Locus> }
<Locus> = <Variable-Identifier>

An example of this might be:

definition let X;
  mode Element of X means
  :Def2: it in X if X is non empty
    otherwise it is empty;
  existency by BOOLE:def 1;
  consistency;
end;

• We have the <Loci-Declaration> be the first statement after the definition, i.e., the "let X;" is such a declaration. It declares the variables occurring in the definition.
• The <Specification> part is missing for this example. (If it were present, it gives the "mother type" for the newly defined mode. If not, the largest type set is used as the mother type.)
• The <Definiens> after the keyword means consists of an optional <Label-Identifier> and either (a) a simple sentence, or (b) several sentences separated by the keywords if and otherwise. The latter condition (<Conditional-Definiens>) is used for "per cases" definitions.
  • In our example, the <Conditional-Definiens> separates the case when the mode argument X is non-empty from the case when it is empty.
    • For the first case states, for any it (special variable used in definitions) being of type Element of X means that it in X
    • The second case, in the degenerate case when X is empty, being of the type Element of X means to be empty too.
• <Correctness-Conditions> in our example is given by the existence and consistency conditions.
  • The existence condition states the extension of the defined type is non-empty
  • The consistency condition states the disjunction of all the cases into which the definition was split, is true.

(Note, Element of transforms a given set into a "soft type".)

Types in Mizar may be translated as predicates. So n-ary types become n+1-ary predicates. So, the Mizar type qualification X is Element of Y will be translated as m1_subset_1(X,Y).

The definiens translates as m1_subset_1(X,Y) iff ( (not(empty(Y)) and in(X,Y)) or (empty(X) and empty(Y)) ).

The existence condition translates to: forall([Y], exists([X], m1_subset_1(X,Y)))

Another couple examples, from binop_1.miz:

definition
  let A be set; :: loci-declaration
  :: defines a unary operation on A
  mode UnOp of A is Function of A,A;
  :: defines a binary operation on A, note that [:A,A:] is the Cartesian product of A with A
  mode BinOp of A is Function of [:A,A:],A;
end;

The syntactic structure to a <Predicate-Definition> is:

<Predicate-Definition> =
  "pred" <Predicate-Pattern> [ "means" <Definiens> ] ";" <Correctness-Conditions> { <Predicate-Property> } .

Functors are parametrized constants in Mizar. For example, if G is a group, then its identity element is 1_G which is parametrized by G. The cyclic group \(\mathbb{Z}/n\mathbb{Z}\) is INT.Group(n) parametrized by a positive integer n (this is defined in GR_CY_1:def 5).

Functions must define the types of their arguments and the type of their result. Several <Functor-Properties> (like commutativity) can be associated with them. The syntax is:

<Functor-Definition> =
 "func" <Functor-Pattern> [ <Specification> ] [ ( "means" | "equals" ) <Definiens> ] ";"
 <Correctness-Conditions> { <Functor-Property> } .

<Specification> = "->" <Type-Expression>

Mizar demands that every functor be accompanied by a proof of existence and uniqueness.

The example given:

definition let x be real number;
  func -x -> real number means :Def1: x + it = 0;
  existence by AXIOMS:19;
  uniqueness by Th10;

Lets analyze this definition.

• The <Loci-Declaration> declares a variable x for the type number with the adjective real
  • The type number is now just a convenient synonym for the larget type set, and real is also defined in the same Mizar article arytm.
• The <Functor-Pattern> is -x here
• The <Specification> is -> real number, which tells us the result type of the function (a real number).
• The <Definiens> here is :Def1: x + it = 0.
• The <Correctness-Condition>, we have 2 of them which the system always checks:
  • "existence" states there exists an object (of the desired type real number) conforming to the <Definiens>
  • "uniqueness" says it is unique (proven, in fact, by a previous theorem, Th10)

The definition creates one new pattern, and one new constructor.

Intuitively, a structure is a tuple with named components.

From algstr_0.miz, we have:

:: Multiplicative structures
definition
  struct (1-sorted) multMagma (# carrier -> set,
                                 multF -> BinOp of the carrier
  #);
end;

:: multiplication is later defined as:
:: 
:: definition
::   let M be multMagma;
::   let x,y be Element of M;
::   func x*y -> Element of M equals
::   (the multF of M).(x,y);
::   coherence;
:: end;

This introduces a multMagma structure, which inherits the 1-sorted structure. Loosely, structures are analogous to classes (they define new types, they have a constructor — in this case, it's multMagma(# X, op #), and so on). We can access the fields of the structure by writing things like the multF of M to get the multF field, and the carrier to get its underlying set.

(This is a common Mizar idiom, using carrier as the name of the underlying set of a mathematical gadget.)

Our intuition should be that a struct is how Mizar encodes stuff and structure (in the Baez–Dolan sense). Indeed, idiomatic Mizar will encode a mathematical gadget in this manner, with a Gadget-like attribute for a GadgetStr structure, then we will find a mode Gadget means Gadget-like GadgetStr type definition.

Another example of a structure (from VECTSP_1), this time using over:

:: VECTSP_1
definition
  let F be 1-sorted;
  struct(addLoopStr) ModuleStr over F (#
      carrier -> set,
      addF -> BinOp of the carrier,
      ZeroF -> Element of the carrier,
      lmult -> Function of [:the carrier of F, the carrier:], the carrier
  #);
end;

For details about structures in Mizar, see:

• Gilbert Lee and Piotr Rudnicki,
  "Alternative aggregates in Mizar."
  In Towards Mechanized Mathematical Assistants, pp. 327-341. Springer, Berlin, Heidelberg, 2007.

There are several types of cluster registrations:

• Existential registration: asserts an attributed type is non empty (and thus permits us to use an attribute as an adjective)
• Conditional registration: propagates types (for example, every characteristic subgroup is also a normal subgroup; conditional registration makes this association automatic)
• Functorial registration, another propagation mechanism

For further reading about attributes, see:

• Christoph Schwarzweller,
  "Mizar attributes: A technique to encode mathematical knowledge into type systems."
  Studies in Logic, Grammar and Rhetoric 10, no. 23 (2007) pp.387–400.