# Volume 28 (2020): Issue 2 (July 2020)

Journal Details
Format
Journal
eISSN
1898-9934
ISSN
1426-2630
First Published
09 Jun 2008
Publication timeframe
4 times per year
Languages
English

0 Articles
Open Access

#### Renamings and a Condition-free Formalization of Kronecker’s Construction

Published Online: 09 Jan 2021
Page range: 129 - 135

#### Abstract

In , ,  we presented a formalization of Kronecker’s construction of a field extension E for a field F in which a given polynomial p ∈ F [X]\F has a root , , . A drawback of our formalization was that it works only for polynomial-disjoint fields, that is for fields F with FF [X] = ∅. The main purpose of Kronecker’s construction is that by induction one gets a field extension of F in which p splits into linear factors. For our formalization this means that the constructed field extension E again has to be polynomial-disjoint.

In this article, by means of Mizar system , , we first analyze whether our formalization can be extended that way. Using the field of polynomials over F with degree smaller than the degree of p to construct the field extension E does not work: In this case E is polynomial-disjoint if and only if p is linear. Using F [X]/<p> one can show that for F = ℚ and F = ℤn the constructed field extension E is again polynomial-disjoint, so that in particular algebraic number fields can be handled.

For the general case we then introduce renamings of sets X as injective functions f with dom(f) = X and rng(f) ∩ (XZ) = ∅ for an arbitrary set Z. This, finally, allows to construct a field extension E of an arbitrary field F in which a given polynomial pF [X]\F splits into linear factors. Note, however, that to prove the existence of renamings we had to rely on the axiom of choice.

#### Keywords

• roots of polynomials
• field extensions
• Kronecker’s construction

• 12E05
• 12F05
• 68V20
Open Access

#### Refined Finiteness and Degree Properties in Graphs

Published Online: 09 Jan 2021
Page range: 137 - 154

#### Abstract

In this article the finiteness of graphs is refined and the minimal and maximal degree of graphs are formalized in the Mizar system , based on the formalization of graphs in .

#### Keywords

• graph theory
• vertex degree
• maximum degree
• minimum degree

• 68V20
• 05C07
Open Access

#### About Graph Unions and Intersections

Published Online: 09 Jan 2021
Page range: 155 - 171

#### Abstract

In this article the union and intersection of a set of graphs are formalized in the Mizar system , based on the formalization of graphs in .

#### Keywords

• graph theory
• graph union
• graph intersection

• 68V20
• 05C76
Open Access

#### Unification of Graphs and Relations in Mizar

Published Online: 09 Jan 2021
Page range: 173 - 186

#### Abstract

A (di)graph without parallel edges can simply be represented by a binary relation of the vertices and on the other hand, any binary relation can be expressed as such a graph. In this article, this correspondence is formalized in the Mizar system , based on the formalization of graphs in  and relations in , . Notably, a new definition of createGraph will be given, taking only a non empty set V and a binary relation EV × V to create a (di)graph without parallel edges, which will provide to be very useful in future articles.

#### Keywords

• graph theory
• binary relation

• 05C62
• 68V20
Open Access

#### Partial Correctness of a Fibonacci Algorithm

Published Online: 09 Jan 2021
Page range: 187 - 196

#### Abstract

In this paper we introduce some notions to facilitate formulating and proving properties of iterative algorithms encoded in nominative data language  in the Mizar system , . It is tested on verification of the partial correctness of an algorithm computing n-th Fibonacci number:

i := 0

s := 0

b := 1

c := 0

while (i <> n)

c := s

s := b

b := c + s

i := i + 1

return s

This paper continues verification of algorithms , ,  written in terms of simple-named complex-valued nominative data , , , , , . The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data . Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic ,  with partial pre- and post-conditions , , , .

#### Keywords

• nominative data
• program verification
• Fibonacci sequence

• 68Q60
• 03B70
• 03B35
Open Access

#### Multiplication-Related Classes of Complex Numbers

Published Online: 09 Jan 2021
Page range: 197 - 210

#### Abstract

The use of registrations is useful in shortening Mizar proofs , , both in terms of formalization time and article space. The proposed system of classes for complex numbers aims to facilitate proofs involving basic arithmetical operations and order checking. It seems likely that the use of self-explanatory adjectives could also improve legibility of these proofs, which would be an important achievement . Additionally, some potentially useful definitions, following those defined for real numbers, are introduced.

#### Keywords

• complex numbers
• multiplication
• order

• 40-04
• 68V20
Open Access

#### Grothendieck Universes

Published Online: 09 Jan 2021
Page range: 211 - 215

#### Abstract

The foundation of the Mizar Mathematical Library , 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 XU. In this article, we prove, using the Mizar  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 , might not be transitive (called epsilon-transitive in the Mizar Mathematical Library ) 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 .

#### Keywords

• Tarski-Grothendieck set theory
• Tarski’s Axiom A
• Grothendieck universe

• 03E70
• 68V20
Open Access

#### Formalization of Quasilattices

Published Online: 09 Jan 2021
Page range: 217 - 225

#### Abstract

The main aim of this article is to introduce formally one of the generalizations of lattices, namely quasilattices, which can be obtained from the axiomatization of the former class by certain weakening of ordinary absorption laws. We show propositions QLT-1 to QLT-7 from , presenting also some short variants of corresponding axiom systems. Some of the results were proven in the Mizar ,  system with the help of Prover9  proof assistant.

#### Keywords

• lattice theory
• quasilattice
• absorption law

• 68V20
• 06B05
• 06B75