Miscellaneous Graph Preliminaries. Part I

Summary This article contains many auxiliary theorems which were missing in the Mizar Mathematical Library to the best of the author’s knowledge. Most of them regard graph theory as formalized in the GLIB series and are needed in upcoming articles.

Enhancement of properties in Mizar

A “property” in the Mizar proof-assistant is a construction that can be used to register chosen features of predicates (e.g., “reflexivity”, “symmetry”), operations (e.g., “involutiveness”, “commutativity”) and types (e.g., “sethoodness”) declared at the definition stage. The current implementation of Mizar allows using properties for notions with a specific number of visible arguments (e.g., reflexivity for a predicate with two visible arguments and involutiveness for an operation with just one visible argument). In this paper we investigate a more general approach to overcome these limitations. We propose an extension of the Mizar language and a corresponding enhancement of the Mizar proof-checker which allow declaring properties of notions of arbitrary arity with respect to explicitly indicated arguments. Moreover, we introduce a new property—the “fixedpoint-free” property of unary operations—meaning that the result of applying the operation to its argument always differs from the argument. Results of tests conducted on the Mizar Mathematical Library are presented.

A Case Study of Transporting Urysohn’s Lemma from Topology via Open Sets into Topology via Neighborhoods

Summary Józef Białas and Yatsuka Nakamura has completely formalized a proof of Urysohn’s lemma in the article [4], in the context of a topological space defined via open sets. In the Mizar Mathematical Library (MML), the topological space is defined in this way by Beata Padlewska and Agata Darmochwał in the article [18]. In [7] the topological space is defined via neighborhoods. It is well known that these definitions are equivalent [5, 6]. In the definitions, an abstract structure (i.e. the article [17, STRUCT 0] and its descendants, all of them directly or indirectly using Mizar structures [3]) have been used (see [10], [9]). The first topological definition is based on the Mizar structure TopStruct and the topological space defined via neighborhoods with the Mizar structure: FMT Space Str. To emphasize the notion of a neighborhood, we rename FMT TopSpace (topology from neighbourhoods) to NTopSpace (a neighborhood topological space). Using Mizar [2], we transport the Urysohn’s lemma from TopSpace to NTop-Space. In some cases, Mizar allows certain techniques for transporting proofs, definitions or theorems. Generally speaking, there is no such automatic translating. In Coq, Isabelle/HOL or homotopy type theory transport is also studied, sometimes with a more systematic aim [14], [21], [11], [12], [8], [19]. In [1], two co-existing Isabelle libraries: Isabelle/HOL and Isabelle/Mizar, have been aligned in a single foundation in the Isabelle logical framework. In the MML, they have been used since the beginning: reconsider, registration, cluster, others were later implemented [13]: identify. In some proofs, it is possible to define particular functors between different structures, mainly useful when results are already obtained in a given structure. This technique is used, for example, in [15] to define two functors MXR2MXF and MXF2MXF between Matrix of REAL and Matrix of F-Real and to transport the definition of the addition from one structure to the other: [...] A + B -> Matrix of REAL equals MXF2MXR ((MXR2MXF A) + (MXR2MXF B)) [...]. In this paper, first we align the necessary topological concepts. For the formalization, we were inspired by the works of Claude Wagschal [20]. It allows us to transport more naturally the Urysohn’s lemma ([4, URYSOHN3:20]) to the topological space defined via neighborhoods. Nakasho and Shidama have developed a solution to explore the notions introduced in various ways https://mimosa-project.github.io/mmlreference/current/ [16]. The definitions can be directly linked in the HTML version of the Mizar library (example: Urysohn’s lemma http://mizar.org/version/current/html/urysohn3.html#T20).

Grothendieck Universes

Summary The foundation of the Mizar Mathematical Library [2], is first-order Tarski-Grothendieck set theory. However, the foundation explicitly refers only to Tarski’s Axiom A, which states that for every set X there is a Tarski universe U such that X ∈ U. In this article, we prove, using the Mizar [3] formalism, that the Grothendieck name is justified. We show the relationship between Tarski and Grothendieck universe. First we prove in Theorem (17) that every Grothendieck universe satisfies Tarski’s Axiom A. Then in Theorem (18) we prove that every Grothendieck universe that contains a given set X, even the least (with respect to inclusion) denoted by GrothendieckUniverseX, has as a subset the least (with respect to inclusion) Tarski universe that contains X, denoted by the Tarski-ClassX. Since Tarski universes, as opposed to Grothendieck universes [5], might not be transitive (called epsilon-transitive in the Mizar Mathematical Library [1]) we focused our attention to demonstrate that Tarski-Class X ⊊ GrothendieckUniverse X for some X. Then we show in Theorem (19) that Tarski-ClassX where X is the singleton of any infinite set is a proper subset of GrothendieckUniverseX. Finally we show that Tarski-Class X = GrothendieckUniverse X holds under the assumption that X is a transitive set. The formalisation is an extension of the formalisation used in [4].

On Fuzzy Negations Generated by Fuzzy Implications

SummaryWe continue in the Mizar system [2] the formalization of fuzzy implications according to the book of Baczyński and Jayaram “Fuzzy Implications” [1]. In this article we define fuzzy negations and show their connections with previously defined fuzzy implications [4] and [5] and triangular norms and conorms [6]. This can be seen as a step towards building a formal framework of fuzzy connectives [10]. We introduce formally Sugeno negation, boundary negations and show how these operators are pointwise ordered. This work is a continuation of the development of fuzzy sets [12], [3] in Mizar [7] started in [11] and partially described in [8]. This submission can be treated also as a part of a formal comparison of fuzzy and rough approaches to incomplete or uncertain information within the Mizar Mathematical Library [9].

Miscellaneous Graph Preliminaries

SummaryThis article contains many auxiliary theorems which were missing in the Mizar Mathematical Library [2] to the best of the author’s knowledge. Most of them regard graph theory as formalized in the GLIB series (cf. [8]) and most of them are preliminaries needed in [7] or other forthcoming articles.

Cross-Ratio in Real Vector Space

Summary Using Mizar [1], in the context of a real vector space, we introduce the concept of affine ratio of three aligned points (see [5]). It is also equivalent to the notion of “Mesure algèbrique”1, to the opposite of the notion of Teilverhältnis2 or to the opposite of the ordered length-ratio [9]. In the second part, we introduce the classic notion of “cross-ratio” of 4 points aligned in a real vector space. Finally, we show that if the real vector space is the real line, the notion corresponds to the classical notion3 [9]: The cross-ratio of a quadruple of distinct points on the real line with coordinates x1, x2, x3, x4 is given by: $$({x_1},{x_2};{x_3},{x_4}) = {{{x_3} - {x_1}} \over {{x_3} - {x_2}}}.{{{x_4} - {x_2}} \over {{x_4} - {x_1}}}$$ In the Mizar Mathematical Library, the vector spaces were first defined by Kusak, Leonczuk and Muzalewski in the article [6], while the actual real vector space was defined by Trybulec [10] and the complex vector space was defined by Endou [4]. Nakasho and Shidama have developed a solution to explore the notions introduced by different authors4 [7]. The definitions can be directly linked in the HTMLized version of the Mizar library5. The study of the cross-ratio will continue within the framework of the Klein- Beltrami model [2], [3]. For a generalized cross-ratio, see Papadopoulos [8].

Binary Representation of Natural Numbers

Summary Binary representation of integers [5], [3] and arithmetic operations on them have already been introduced in Mizar Mathematical Library [8, 7, 6, 4]. However, these articles formalize the notion of integers as mapped into a certain length tuple of boolean values. In this article we formalize, by means of Mizar system [2], [1], the binary representation of natural numbers which maps ℕ into bitstreams.

Arithmetic Operations on Short Finite Sequences

Summary In contrast to other proving systems Mizar Mathematical Library, considered as one of the largest formal mathematical libraries [4], is maintained as a single base of theorems, which allows the users to benefit from earlier formalized items [3], [2]. This eventually leads to a development of certain branches of articles using common notation and ideas. Such formalism for finite sequences has been developed since 1989 [1] and further developed despite of the controversy over indexing which excludes zero [6], also for some advanced and new mathematics [5]. The article aims to add some new machinery for dealing with finite sequences, especially those of short length.