The sethood property is introduced into the Mizar system to declare that objects of a given type or possessing given properties represented as adjectives belong to some universes. It is applied to control whether such objects can be used in definitions of sets by so called Fraenkel operators. In this paper we propose an extension of the Mizar system including its language and functionality with a possibility of application of those universes not only within Fraenkel operators, but also by other Mizar modules to reason about types of objects with the sethood property declared.
Copyright © by the paper’s authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). definition let x1 be 1; x2 be 2; : : : ; xn be n; mode of x1; x2; : : : ; xn -> means :ident:
(x1; x2; : : : ; xn; it); existence; sethood proof
thus ex X being set st for a being end; end; and for expandable types with the following syntax: registration let x1 be 1; x2 be 2; : : : ; xn be n; sethood of 1 : : : m proof
thus ex X being set st for a being 1 : : : end; end; st (x1; x2; : : : ; xn; a) holds a in X; m
holds a in X; 2 2.1
Syntax definition let x1 be 1; x2 be 2; : : : ; xn be n; mode of x1; x2; : : : ; xn -> means :ident:
(x1; x2; : : : ; xn; it); existence; sethood wrt X(x1; x2; : : : ; xn) proof
thus for a being end; end; and in the case of expandable modes it is:
This property registers that each term of a type with the property registered is an element of some set. But the sets are hidden within the proofs of the correctness of the property (sets X in the above proofs) and cannot be used in other formulas and reasonings outside the proofs.
In this paper we propose an extension of the Mizar language to make declared universes visible outside the registrations and to use them for various purposes during verification process. We present the syntax of the extension, possible usage and profits of new functionality, its influence on the Mizar Mathematical Library [BBG+18] and briefly discuss possible negative consequences of the proposed solution.
To achieve our goal that is making universes of types visible and accessible in the library, not only locally in particular proofs, we propose a simple extension of the grammar of the Mizar language with a new word wrt followed by a proposed universe. In the cases of non-expandable modes the syntax is:
st (x1; x2; : : : ; xn; a) holds a in X(x1; x2; : : : ; xn); registration let x1 be 1; x2 be 2; : : : ; xn be n; sethood of 1 : : : m wrt X(x1; x2; : : : ; xn) proof
thus for a being 1 : : : m end; end;
holds a in X(x1; x2; : : : ; xn);
Correctness conditions generated by the system for proving the soundness of properties are presented in the above snaps as well. They ensure that all terms of types for which the sethood property is declared belong to the declared universes.
Examples of practical usages of those declarations taken from the Mizar Mathematical Library for both nonexpandable and expandable types are [INKK17]: registration sethood of Complex wrt COMPLEX proof thus for c being Complex holds c in COMPLEX; end; end; definition let V,A be set; mode NonatomicND of V,A -> Function means ex S being FinSequence st S IsNDRankSeq V,A & it in Union S; existence; sethood wrt Union FNDSC(V,A) proof thus for f being Function st ex S being FinSequence st S IsNDRankSeq V,A & f in Union S holds f in Union FNDSC(V,A); end; end;
It is worth to mention that wrt clause is not obligatory, authors can decided whether to make the universe visible or not. If wrt is not used for some property, no changes in the processing of the property will be observed. 2.2
Properties Two main modules of the Mizar verifier are: Analyzer responsible, among others, for type checking, identification of objects, and resolving disambiguations, and Checker responsible for verification of the logical correctness of proof steps.
At the stage of processing Fraenkel operators, Analyzer checks whether types of all variables bounded within the operators (using clause where) have the sethood property registered (if not, appropriate errors are reported). These functionality remains in our new approach of processing sethoodness. Sethoodness remains also inherited by sub-types and is propagated among all adjectives which expand to the adjective with the property declared explicitly, as well.
To see one of the most important profits of the new sethood property, what we claim that the better reusability of existing in the Mizar Mathematical Library theorems is, let us start from an example of using natural numbers in the Mizar system. Basically, there are two ways of using natural numbers in formulas: as variables of the type Nat, which is an abbreviation of the type natural number, or as variables of the type Element of NAT, where NAT is defined as the set of all natural numbers. By default in the Mizar system there is no automatic communication2 between these two types, but using the conditional registration mechanism Mizar allows to declare that each Element of NAT is a natural number as follows: registration cluster -> natural for Element of NAT; coherence; end; Having such a registration each Element of NAT is also identified as a Nat. On the other hand to allow the Mizar verifier to know that each natural number is an Element of NAT one has to explicitly refer to the appropriate theorem (or definition). Also theorems about Element of NAT are not directly accessible for terms of the type Nat.
New implementation of the sethood property establishes also the automatic communication from the type Nat to the type Element of NAT. For example, the following registration: registration sethood of Nat wrt NAT; end;
2By automatic communication we mean that the Mizar Analyzer and Checker can infer some facts without any explicit references to any definitions, theorems and schemas, but only “playing” with Mizar constructions like redefinitions, registrations, term reductions [Kor13], term identifications and properties [NB04] that are automatically processed by dedicated Mizar procedures. makes Checker to understand all Nats also as Elements of NAT. Then, all theorems about an Element of NAT will be applicable for terms of the type Nat, what will possibly result with less number of theorems stored in the Mizar Mathematical Library. Of course, a question: Why theorems involving variables of the type Element of NAT instead of Nat are kept in the MML? can arise. Reasons for that are various, e.g.: a) terms of the type Element of NAT are sub-terms of operations whose arguments must be elements of some sets, b) terms of the type Element of NAT are arguments of adjectives or types whose arguments must be elements of some sets, c) authors of Mizar works sometimes use Element of NAT simply “by chance”.
To achieve a good classification of types concerning their universes a bigger number of sethood registrations will be required in Mizar articles. Again, the example with numbers nicely illustrates the issue. Let us consider a chain of adjectives representing numbers: natural ! integer ! rational ! real ! complex already defined in the MML. In the old treatment of the sethood property, to know that all these types are included within an universe it was enough to register only one sethoodness for the biggest set, that is for complex numbers. The property was inherited by all adjectives which expand to complex numbers. In the new implementation of the sethood property such one registration for complex numbers will result with treatment all natural, integer, rational, real, and complex numbers as objects of the type Element of COMPLEX. To declare more precise universes for each mentioned type the following chain of sethood registrations is needed:
These registrations allow Checker to treat all discussed kinds of numbers as elements of the most appropriate sets, that is naturals as elements of N, integers as elements of Z, rationals as elements of Q, reals as elements of R, and finally complex numbers as elements of C. But, because the sethoodness is still inherited by sub-types, naturals will be treated not only as elements of N, but also as elements of Z, as elements of Q, as elements of R, and as elements of C. Consequently, integers, rationals, and reals will be treated as elements of universes declared in their sethood registrations, but also as elements of all their super-sets, what in some applications can be seen as undesirable. 3
In this paper we report about an extension of the Mizar system with a possibility of using universes of types presented in proofs of the sethood property of chosen types and adjectives to collect more types of terms which basic types have the sethood property registered. It may move work from the world of adjectives to the world of elements of appropriate universes.
This extension induces work for the Library Committee, who is responsible for the management, developing and revisions of the MML, concerning detection of cases where it is worth to introduce more sethoodness registrations in already stored Mizar documents, and in the case of approval, a refactoring of the MML [GS07] will be required while maintaining licensing its content [AKM+11].