# Volume 27 (2019): Issue 2 (July 2019)

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

#### On Roots of Polynomials over F[X]/ 〈p〉

Published Online: 20 Jul 2019
Page range: 93 - 100

#### Abstract

This is the first part of a four-article series containing a Mizar [3], [1], [2] formalization of Kronecker’s construction about roots of polynomials in field extensions, i.e. that for every field F and every polynomial pF [X]\F there exists a field extension E of F such that p has a root over E. The formalization follows Kronecker’s classical proof using F [X]/<p> as the desired field extension E [9], [4], [6].

In this first part we show that an irreducible polynomial pF [X]\F has a root over F [X]/<p>. Note, however, that this statement cannot be true in a rigid formal sense: We do not have F ⊆ [X]/ < p > as sets, so F is not a subfield of F [X]/<p>, and hence formally p is not even a polynomial over F [X]/ < p >. Consequently, we translate p along the canonical monomorphism ϕ: FF [X]/<p> and show that the translated polynomial ϕ(p) has a root over F [X]/<p>.

Because F is not a subfield of F [X]/<p> we construct in the second part the field (E \ ϕF )∪F for a given monomorphism ϕ : FE and show that this field both is isomorphic to F and includes F as a subfield. In the literature this part of the proof usually consists of saying that “one can identify F with its image ϕF in F [X]/<p> and therefore consider F as a subfield of F [X]/<p>”. Interestingly, to do so we need to assume that F ∩ E =∅, in particular Kronecker’s construction can be formalized for fields F with F \ F [X] =∅.

Surprisingly, as we show in the third part, this condition is not automatically true for arbitray fields F : With the exception of 𝕑2 we construct for every field F an isomorphic copy F of F with F′F′ [X] ∅. We also prove that for Mizar’s representations of 𝕑n, 𝕈 and 𝕉 we have 𝕑n ∩ 𝕑n[X] = ∅, 𝕈 ∩ 𝕈[X] = ∅and 𝕉 ∩ 𝕉[X] = ∅, respectively.

In the fourth part we finally define field extensions: E is a field extension of F i F is a subfield of E. Note, that in this case we have F ⊆ E as sets, and thus a polynomial p over F is also a polynomial over E. We then apply the construction of the second part to F [X]/<p> with the canonical monomorphism ϕ : FF [X]/<p>. Together with the first part this gives - for fields F with FF [X] = ∅ - a field extension E of F in which pF [X]\F has a root.

#### Keywords

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

• 12E05
• 12F05
• 68T99
• 03B35
Open Access

#### Isomorphisms from the Space of Multilinear Operators

Published Online: 20 Jul 2019
Page range: 101 - 106

#### Abstract

In this article, using the Mizar system [5], [2], the isomorphisms from the space of multilinear operators are discussed. In the first chapter, two isomorphisms are formalized. The former isomorphism shows the correspondence between the space of multilinear operators and the space of bilinear operators.

The latter shows the correspondence between the space of multilinear operators and the space of the composition of linear operators. In the last chapter, the above isomorphisms are extended to isometric mappings between the normed spaces. We referred to [6], [11], [9], [3], [10] in this formalization.

#### Keywords

• linear operators
• bilinear operators
• multilinear operators
• isomorphism of linear operator spaces

• 46-00
• 47A07
• 47A30
• 68T99
• 03B35
Open Access

#### Invertible Operators on Banach Spaces

Published Online: 20 Jul 2019
Page range: 107 - 115

#### Abstract

In this article, using the Mizar system [2], [1], we discuss invertible operators on Banach spaces. In the first chapter, we formalized the theorem that denotes any operators that are close enough to an invertible operator are also invertible by using the property of Neumann series.

In the second chapter, we formalized the continuity of an isomorphism that maps an invertible operator on Banach spaces to its inverse. These results are used in the proof of the implicit function theorem. We referred to [3], [10], [6], [7] in this formalization.

#### Keywords

• Banach space
• invertible operator
• Neumann series
• isomorphism of linear operator spaces

• 47A05
• 47J07
• 68T99
• 03B35
Open Access

#### Implicit Function Theorem. Part II

Published Online: 20 Jul 2019
Page range: 117 - 131

#### Abstract

In this article, we formalize differentiability of implicit function theorem in the Mizar system [3], [1]. In the first half section, properties of Lipschitz continuous linear operators are discussed. Some norm properties of a direct sum decomposition of Lipschitz continuous linear operator are mentioned here.

In the last half section, differentiability of implicit function in implicit function theorem is formalized. The existence and uniqueness of implicit function in [6] is cited. We referred to [10], [11], and [2] in the formalization.

#### Keywords

• implicit function theorem
• Lipschitz continuity
• differentiability
• implicit function

• 26B10
• 47A05
• 47J07
• 53A07
• 03B35
Open Access

#### On Monomorphisms and Subfields

Published Online: 20 Jul 2019
Page range: 133 - 137

#### Abstract

This is the second part of a four-article series containing a Mizar [2], [1] formalization of Kronecker’s construction about roots of polynomials in field extensions, i.e. that for every field F and every polynomial pF [X]\F there exists a field extension E of F such that p has a root over E. The formalization follows Kronecker’s classical proof using F [X]/<p> as the desired field extension E [5], [3], [4].

In the first part we show that an irreducible polynomial pF [X]\F has a root over F [X]/<p>. Note, however, that this statement cannot be true in a rigid formal sense: We do not have F ⊆ [X]/ < p > as sets, so F is not a subfield of F [X]/<p>, and hence formally p is not even a polynomial over F [X]/ < p >. Consequently, we translate p along the canonical monomorphism ϕ : F → F [X]/<p> and show that the translated polynomial ϕ (p) has a root over F [X]/<p>.

Because F is not a subfield of F [X]/<p> we construct in this second part the field (E \ ϕF )∪F for a given monomorphism ϕ : F → E and show that this field both is isomorphic to F and includes F as a subfield. In the literature this part of the proof usually consists of saying that “one can identify F with its image ϕF in F [X]/<p> and therefore consider F as a subfield of F [X]/<p>”. Interestingly, to do so we need to assume that FE = ∅, in particular Kronecker’s construction can be formalized for fields F with FF [X] = ∅.

Surprisingly, as we show in the third part, this condition is not automatically true for arbitray fields F : With the exception of 𝕑2 we construct for every field F an isomorphic copy F′ of F with F′F′ [X] ∅. We also prove that for Mizar’s representations of 𝕑n, 𝕈 and 𝕉 we have 𝕑n ∩ 𝕑n[X] = ∅, 𝕈 ∩ 𝕈 [X] = ∅ and 𝕉 ∩ 𝕉 [X] = ∅, respectively.

In the fourth part we finally define field extensions: E is a field extension of F iff F is a subfield of E. Note, that in this case we have FE as sets, and thus a polynomial p over F is also a polynomial over E. We then apply the construction of the second part to F [X]/<p> with the canonical monomorphism ϕ : F → F [X]/<p>. Together with the first part this gives - for fields F with F ∩ F [X] = ∅ - a field extension E of F in which pF [X]\F has a root.

#### Keywords

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

#### MSC 2010

• 12E05
• 12F05
• 68T99
• 03B35
Open Access

Published Online: 20 Jul 2019
Page range: 139 - 152

#### Abstract

In [3] the existence of the Cantor normal form of ordinals was proven in the Mizar system [6]. In this article its uniqueness is proven and then used to formalize the natural sum of ordinals.

#### Keywords

• ordinal numbers
• Cantor normal form
• Hessenberg sum
• natural sum

#### MSC 2010

• 03E10
• 68T99
• 03B35
Open Access

Published Online: 20 Jul 2019
Page range: 153 - 179

#### Abstract

The previous articles [5] and [6] introduced formalizations of the step-by-step operations we use to construct finite graphs by hand. That implicitly showed that any finite graph can be constructed from the trivial edgeless graph K1 by applying a finite sequence of these basic operations. In this article that claim is proven explicitly with Mizar[4].

#### Keywords

• supergraph
• graph operations
• construction of finite graphs

• 05C76
• 68T99
• 03B35
Open Access

#### Partial Correctness of a Factorial Algorithm

Published Online: 20 Jul 2019
Page range: 181 - 187

#### Abstract

In this paper we present a formalization in the Mizar system [3],[1] of the partial correctness of the algorithm:

i := val.1 j := val.2 n := val.3 s := val.4 while (i <> n) i := i + j s := s * i return s

computing the factorial of given natural number n, where variables i, n, s are located as values of a V-valued Function, loc, as: loc/.1 = i, loc/.3 = n and loc/.4 = s, and the constant 1 is located in the location loc/.2 = j (set V represents simple names of considered nominative data [16]).

This work continues a formal verification of algorithms written in terms of simple-named complex-valued nominative data [6],[8],[14],[10],[11],[12]. The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data [9]. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic [2],[4] with partial pre- and post-conditions [13],[15],[7],[5].

#### Keywords

• factorial
• nominative data
• program verification

• 68Q60
• 68T37
• 03B70
• 03B35
Open Access

#### Partial Correctness of a Power Algorithm

Published Online: 20 Jul 2019
Page range: 189 - 195

#### Abstract

This work continues a formal verification of algorithms written in terms of simple-named complex-valued nominative data [6],[8],[15],[11],[12],[13]. In this paper we present a formalization in the Mizar system [3],[1] of the partial correctness of the algorithm:

i := val.1 j := val.2 b := val.3 n := val.4 s := val.5 while (i <> n) i := i + j s := s * b return s

computing the natural n power of given complex number b, where variables i, b, n, s are located as values of a V-valued Function, loc, as: loc/.1 = i, loc/.3 = b, loc/.4 = n and loc/.5 = s, and the constant 1 is located in the location loc/.2 = j (set V represents simple names of considered nominative data [17]).

The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data [9]. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic [2],[4] with partial pre- and post-conditions [14],[16],[7],[5].

#### Keywords

• power
• nominative data
• program verification

• 68Q60
• 68T37
• 03B70
• 03B35
Open Access

#### Diophantine Sets. Part II

Published Online: 20 Jul 2019
Page range: 197 - 208

#### Abstract

The article is the next in a series aiming to formalize the MDPR-theorem using the Mizar proof assistant [3], [6], [4]. We analyze four equations from the Diophantine standpoint that are crucial in the bounded quantifier theorem, that is used in one of the approaches to solve the problem.

Based on our previous work [1], we prove that the value of a given binomial coefficient and factorial can be determined by its arguments in a Diophantine way. Then we prove that two products

z=i=1x(1+iy),z=i=1x(y+1-j),(0.1)$$z = \prod\limits_{i = 1}^x {\left( {1 + i \cdot y} \right),\,\,\,\,\,\,\,\,} z = \prod\limits_{i = 1}^x {\left( {y + 1 - j} \right),\,\,\,\,\,\,(0.1)}$$

where y > x are Diophantine.

The formalization follows [10], Z. Adamowicz, P. Zbierski [2] as well as M. Davis [5].

#### Keywords

• Hilbert’s 10th problem
• Diophantine relations

• 11D45
• 68T99
• 03B35
Open Access

#### Formalization of the MRDP Theorem in the Mizar System

Published Online: 20 Jul 2019
Page range: 209 - 221

#### Abstract

In our approach, we work with the Pell’s Equation defined in [2]. We analyzed this equation in the general case to show its solvability as well as the cardinality and shape of all possible solutions. Then we focus on a special case of the equation, which has the form x2 (a2 − 1)y2 = 1 [8] and its solutions considered as two sequences {xi(a)}i=0,{yi(a)}i=0$\left\{ {{x_i}(a)} \right\}_{i = 0}^\infty ,\left\{ {{y_i}(a)} \right\}_{i = 0}^\infty$. We showed in [1] that the n-th element of these sequences can be obtained from lists of several basic Diophantine relations as linear equations, finite products, congruences and inequalities, or more precisely that the equation x = yi(a) is Diophantine. Following the post-Matiyasevich results we show that the equality determined by the value of the power function y = xz is Diophantine, and analogously property in cases of the binomial coe cient, factorial and several product [9].

In this article, we combine analyzed so far Diophantine relation using conjunctions, alternatives as well as substitution to prove the bounded quantifier theorem. Based on this theorem we prove MDPR-theorem that every recursively enumerable set is Diophantine, where recursively enumerable sets have been defined by the Martin Davis normal form.

The formalization by means of Mizar system [5], [7], [4] follows [10], Z. Adamowicz, P. Zbierski [3] as well as M. Davis [6].

#### Keywords

• Hilbert’s 10th problem
• Diophantine relations

• 11D45
• 68T99
• 03B35