rss_2.0Sciendo RSS Feed for Formalized Mathematicshttps://sciendo.com/journal/FORMAhttps://www.sciendo.comhttps://sciendo-parsed-data-feed.s3.eu-central-1.amazonaws.com/63a6d101b460d8681e7a3f14/cover-image.jpghttps://sciendo.com/journal/FORMA140216https://sciendo.com/article/10.2478/forma-2022-0020<abstract> <title style='display:none'>Summary</title> <p>In our previous work [7] we prove that the set of prime numbers is diophantine using the 26-variable polynomial proposed in [4]. In this paper, we focus on the reduction of the number of variables to 10 and it is the smallest variables number known today [5], [10]. Using the Mizar [3], [2] system, we formalize the first step in this direction by proving Theorem 1 [5] formulated as follows: Let <italic>k</italic> ∈ ℕ. Then <italic>k</italic> is prime if and only if there exists <italic>f, i, j, m, u</italic> ∈ ℕ⁺, <italic>r, s, t</italic> ∈ ℕ unknowns such that <disp-formula> <alternatives> <graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2022-0020_eq_001.png"/> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="block"><mml:mrow><mml:mtable columnalign="left"><mml:mtr columnalign="left"><mml:mtd columnalign="left"><mml:mrow><mml:mi>D</mml:mi><mml:mi>F</mml:mi><mml:mi>I</mml:mi><mml:mi> </mml:mi><mml:mtext>is</mml:mtext><mml:mi> </mml:mi><mml:mtext>square</mml:mtext><mml:mi> </mml:mi><mml:mi> </mml:mi><mml:mi> </mml:mi><mml:mo>∧</mml:mo><mml:mi> </mml:mi><mml:mrow><mml:mo>(</mml:mo><mml:mrow><mml:msup><mml:mrow><mml:mi>M</mml:mi></mml:mrow><mml:mn>2</mml:mn></mml:msup><mml:mo>-</mml:mo><mml:mn>1</mml:mn></mml:mrow><mml:mo>)</mml:mo></mml:mrow><mml:msup><mml:mrow><mml:mi>S</mml:mi></mml:mrow><mml:mn>2</mml:mn></mml:msup><mml:mo>+</mml:mo><mml:mn>1</mml:mn><mml:mi> </mml:mi><mml:mi> </mml:mi><mml:mtext>is</mml:mtext><mml:mi> </mml:mi><mml:mi> </mml:mi><mml:mtext>square</mml:mtext><mml:mi> </mml:mi><mml:mi> </mml:mi><mml:mo>∧</mml:mo></mml:mrow></mml:mtd></mml:mtr><mml:mtr columnalign="left"><mml:mtd columnalign="left"><mml:mrow><mml:mrow><mml:mo>(</mml:mo><mml:mrow><mml:msup><mml:mrow><mml:mrow><mml:mrow><mml:mo>(</mml:mo><mml:mrow><mml:mi>M</mml:mi><mml:mi>U</mml:mi></mml:mrow><mml:mo>)</mml:mo></mml:mrow></mml:mrow></mml:mrow><mml:mn>2</mml:mn></mml:msup><mml:mo>-</mml:mo><mml:mn>1</mml:mn></mml:mrow><mml:mo>)</mml:mo></mml:mrow><mml:msup><mml:mrow><mml:mi>T</mml:mi></mml:mrow><mml:mn>2</mml:mn></mml:msup><mml:mo>+</mml:mo><mml:mn>1</mml:mn><mml:mi> </mml:mi><mml:mi> </mml:mi><mml:mtext>is</mml:mtext><mml:mi> </mml:mi><mml:mi> </mml:mi><mml:mtext>square</mml:mtext><mml:mo>∧</mml:mo></mml:mrow></mml:mtd></mml:mtr><mml:mtr columnalign="left"><mml:mtd columnalign="left"><mml:mrow><mml:mrow><mml:mo>(</mml:mo><mml:mrow><mml:mn>4</mml:mn><mml:msup><mml:mrow><mml:mi>f</mml:mi></mml:mrow><mml:mn>2</mml:mn></mml:msup><mml:mo>-</mml:mo><mml:mn>1</mml:mn></mml:mrow><mml:mo>)</mml:mo></mml:mrow><mml:msup><mml:mrow><mml:mrow><mml:mrow><mml:mo>(</mml:mo><mml:mrow><mml:mi>r</mml:mi><mml:mo>-</mml:mo><mml:mi>m</mml:mi><mml:mi>S</mml:mi><mml:mi>T</mml:mi><mml:mi>U</mml:mi></mml:mrow><mml:mo>)</mml:mo></mml:mrow></mml:mrow></mml:mrow><mml:mn>2</mml:mn></mml:msup><mml:mo>+</mml:mo><mml:mn>4</mml:mn><mml:msup><mml:mrow><mml:mi>u</mml:mi></mml:mrow><mml:mn>2</mml:mn></mml:msup><mml:msup><mml:mrow><mml:mi>S</mml:mi></mml:mrow><mml:mn>2</mml:mn></mml:msup><mml:msup><mml:mrow><mml:mi>T</mml:mi></mml:mrow><mml:mn>2</mml:mn></mml:msup><mml:mo>&lt;</mml:mo><mml:mn>8</mml:mn><mml:mi>f</mml:mi><mml:mi>u</mml:mi><mml:mi>S</mml:mi><mml:mi>T</mml:mi><mml:mrow><mml:mo>(</mml:mo><mml:mrow><mml:mi>r</mml:mi><mml:mo>-</mml:mo><mml:mi>m</mml:mi><mml:mi>S</mml:mi><mml:mi>T</mml:mi><mml:mi>U</mml:mi></mml:mrow><mml:mo>)</mml:mo></mml:mrow></mml:mrow></mml:mtd></mml:mtr><mml:mtr columnalign="left"><mml:mtd columnalign="left"><mml:mrow><mml:mi>F</mml:mi><mml:mi>L</mml:mi><mml:mo>|</mml:mo><mml:mrow><mml:mo>(</mml:mo><mml:mrow><mml:mi>H</mml:mi><mml:mo>-</mml:mo><mml:mi>C</mml:mi></mml:mrow><mml:mo>)</mml:mo></mml:mrow><mml:mi>Z</mml:mi><mml:mo>+</mml:mo><mml:mi>F</mml:mi><mml:mrow><mml:mo>(</mml:mo><mml:mrow><mml:mi>f</mml:mi><mml:mo>+</mml:mo><mml:mn>1</mml:mn></mml:mrow><mml:mo>)</mml:mo></mml:mrow><mml:mi>Q</mml:mi><mml:mo>+</mml:mo><mml:mi>F</mml:mi><mml:mrow><mml:mo>(</mml:mo><mml:mrow><mml:mi>k</mml:mi><mml:mo>+</mml:mo><mml:mn>1</mml:mn></mml:mrow><mml:mo>)</mml:mo></mml:mrow><mml:mrow><mml:mo>(</mml:mo><mml:mrow><mml:mrow><mml:mo>(</mml:mo><mml:mrow><mml:msup><mml:mrow><mml:mi>W</mml:mi></mml:mrow><mml:mn>2</mml:mn></mml:msup><mml:mo>-</mml:mo><mml:mn>1</mml:mn></mml:mrow><mml:mo>)</mml:mo></mml:mrow><mml:mi>S</mml:mi><mml:mi>u</mml:mi><mml:mo>-</mml:mo><mml:msup><mml:mrow><mml:mi>W</mml:mi></mml:mrow><mml:mn>2</mml:mn></mml:msup><mml:msup><mml:mrow><mml:mi>u</mml:mi></mml:mrow><mml:mn>2</mml:mn></mml:msup><mml:mo>+</mml:mo><mml:mn>1</mml:mn></mml:mrow><mml:mo>)</mml:mo></mml:mrow></mml:mrow></mml:mtd></mml:mtr></mml:mtable></mml:mrow></mml:math> <tex-math>\matrix{ {DFI\,is\,square\,\,\,{\Lambda}\,\left( {{M^2} - 1} \right){S^2} + 1\,\,is\,\,square\,\,{\Lambda}} \hfill \cr {\left( {{{\left( {MU} \right)}^2} - 1} \right){T^2} + 1\,\,is\,\,square{\Lambda}} \hfill \cr {\left( {4{f^2} - 1} \right){{\left( {r - mSTU} \right)}^2} + 4{u^2}{S^2}{T^2} &lt; 8fuST\left( {r - mSTU} \right)} \hfill \cr {FL|\left( {H - C} \right)Z + F\left( {f + 1} \right)Q + F\left( {k + 1} \right)\left( {\left( {{W^2} - 1} \right)Su - {W^2}{u^2} + 1} \right)} \hfill \cr }</tex-math> </alternatives> </disp-formula> where auxiliary variables <italic>A − I, L, M, S − W, Q</italic> ∈ ℤ are simply abbreviations defined as follows <italic>W</italic> = 100<italic>fk</italic>(<italic>k</italic> + 1), <italic>U</italic> = 100<italic>u</italic>³<italic>W</italic> ³ + 1, <italic>M</italic> = 100<italic>mUW</italic> + 1, <italic>S</italic> = (<italic>M −</italic>1)<italic>s</italic>+<italic>k</italic>+1, <italic>T</italic> = (<italic>MU −</italic>1)<italic>t</italic>+<italic>W −k</italic>+1, <italic>Q</italic> = 2<italic>MW −W</italic> ²<italic>−</italic>1, <italic>L</italic> = (<italic>k</italic>+1)<italic>Q</italic>, <italic>A</italic> = <italic>M</italic>(<italic>U</italic> +1), <italic>B</italic> = <italic>W</italic> +1, <italic>C</italic> = <italic>r</italic> +<italic>W</italic> +1, <italic>D</italic> = (<italic>A</italic>² <italic>−</italic>1)<italic>C</italic>² +1, <italic>E</italic> = 2<italic>iC</italic>²<italic>LD</italic>, <italic>F</italic> = (<italic>A</italic>² <italic>−</italic>1)<italic>E</italic>² +1, <italic>G</italic> = <italic>A</italic>+<italic>F</italic> (<italic>F −A</italic>), <italic>H</italic> = <italic>B</italic>+2(<italic>j −</italic>1)<italic>C</italic>, <italic>I</italic> = (<italic>G</italic>² <italic>−</italic>1)<italic>H</italic>² +1. It is easily see that (0.1) uses 8 unknowns explicitly along with five implicit one for each diophantine relationship: is square, inequality, and divisibility. Together with <italic>k</italic> this gives a total of 14 variables. This work has been partially presented in [8].</p> </abstract>ARTICLEtruehttps://sciendo.com/article/10.2478/forma-2022-00202023-02-18T00:00:00.000+00:00https://sciendo.com/article/10.2478/forma-2022-0022<abstract> <title style='display:none'>Summary</title> <p>This is the second part of a two-part article formalizing existence and uniqueness of algebraic closures, using the Mizar [2], [1] formalism. Our proof follows Artin’s classical one as presented by Lang in [3]. In the first part we proved that for a given field <italic>F</italic> there exists a field extension <italic>E</italic> such that every non-constant polynomial <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>] has a root in <italic>E</italic>. Artin’s proof applies Kronecker’s construction to each polynomial <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>]<italic>\F</italic> simultaneously. To do so we needed the polynomial ring <italic>F</italic> [<italic>X</italic>₁, <italic>X</italic>₂, ...] with infinitely many variables, one for each polynomal <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>]<italic>\F</italic>. The desired field extension <italic>E</italic> then is <italic>F</italic> [<italic>X</italic>₁, <italic>X</italic>₂, …]<italic>\I</italic>, where <italic>I</italic> is a maximal ideal generated by all non-constant polynomials <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>]. Note, that to show that <italic>I</italic> is maximal Zorn’s lemma has to be applied.</p> <p>In this second part this construction is iterated giving an infinite sequence of fields, whose union establishes a field extension <italic>A</italic> of <italic>F</italic>, in which every non-constant polynomial <italic>p</italic> ∈ <italic>A</italic>[<italic>X</italic>] has a root. The field of algebraic elements of <italic>A</italic> then is an algebraic closure of <italic>F</italic>. To prove uniqueness of algebraic closures, e.g. that two algebraic closures of <italic>F</italic> are isomorphic over <italic>F</italic>, the technique of extending monomorphisms is applied: a monomorphism <italic>F</italic> → <italic>A</italic>, where <italic>A</italic> is an algebraic closure of <italic>F</italic> can be extended to a monomorphism <italic>E</italic> → <italic>A</italic>, where <italic>E</italic> is any algebraic extension of <italic>F</italic>. In case that <italic>E</italic> is algebraically closed this monomorphism is an isomorphism. Note that the existence of the extended monomorphism again relies on Zorn’s lemma.</p> </abstract>ARTICLEtruehttps://sciendo.com/article/10.2478/forma-2022-00222023-02-18T00:00:00.000+00:00https://sciendo.com/article/10.2478/forma-2022-0023<abstract> <title style='display:none'>Summary</title> <p>In this article, we formalize the theorems about orthogonal decomposition of Hilbert spaces, using the Mizar system [1], [2]. For any subspace <italic>S</italic> of a Hilbert space <italic>H</italic>, any vector can be represented by the sum of a vector in <italic>S</italic> and a vector orthogonal to <italic>S.</italic> The formalization of orthogonal complements of Hilbert spaces has been stored in the Mizar Mathematical Library [4]. We referred to [5] and [6] in the formalization.</p> </abstract>ARTICLEtruehttps://sciendo.com/article/10.2478/forma-2022-00232023-02-18T00:00:00.000+00:00https://sciendo.com/article/10.2478/forma-2022-0021<abstract> <title style='display:none'>Summary</title> <p>In this article we formalize in Mizar [1], [2] the final step of our attempt to formally construct a prime representing polynomial with 10 variables proposed by Yuri Matiyasevich in [4].</p> <p>The first part of the article includes many auxiliary lemmas related to multivariate polynomials. We start from the properties of monomials, among them their evaluation as well as the power function on polynomials to define the substitution for multivariate polynomials. For simplicity, we assume that a polynomial and substituted ones as <italic>i</italic>-th variable have the same number of variables. Then we study the number of variables that are used in given multivariate polynomials. By the used variable we mean a variable that is raised at least once to a non-zero power. We consider both adding unused variables and eliminating them.</p> <p>The second part of the paper deals with the construction of the polynomial proposed by Yuri Matiyasevich. First, we introduce a diophantine polynomial over 4 variables that has roots in integers if and only if indicated variable is the square of a natural number, and another two is the square of an odd natural number. We modify the polynomial by adding two variables in such a way that the root additionally requires the divisibility of these added variables. Then we modify again the polynomial by adding two variables to also guarantee the nonnegativity condition of one of these variables. Finally, we combine the prime diophantine representation proved in [7] with the obtained polynomial constructing a prime representing polynomial with 10 variables. This work has been partially presented in [8] with the obtained polynomial constructing a prime representing polynomial with 10 variables in Theorem (85).</p> </abstract>ARTICLEtruehttps://sciendo.com/article/10.2478/forma-2022-00212023-02-18T00:00:00.000+00:00https://sciendo.com/article/10.2478/forma-2022-0013<abstract> <title style='display:none'>Summary</title> <p>The main purpose of the article is to construct a sophisticated polynomial proposed by Matiyasevich and Robinson [5] that is often used to reduce the number of unknowns in diophantine representations, using the Mizar [1], [2] formalism. The polynomial <disp-formula> <alternatives> <graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2022-0013_eq_001.png"/> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="block"><mml:mrow><mml:msub><mml:mrow><mml:mi>J</mml:mi></mml:mrow><mml:mi>k</mml:mi></mml:msub><mml:mrow><mml:mo>(</mml:mo><mml:mrow><mml:msub><mml:mrow><mml:mi>a</mml:mi></mml:mrow><mml:mn>1</mml:mn></mml:msub><mml:mo>,</mml:mo><mml:mo>…</mml:mo><mml:mo>,</mml:mo><mml:msub><mml:mrow><mml:mi>a</mml:mi></mml:mrow><mml:mi>k</mml:mi></mml:msub><mml:mo>,</mml:mo><mml:mi>x</mml:mi></mml:mrow><mml:mo>)</mml:mo></mml:mrow><mml:mo>=</mml:mo><mml:munder><mml:mo>∏</mml:mo><mml:mrow><mml:msub><mml:mrow><mml:mi>ɛ</mml:mi></mml:mrow><mml:mn>1</mml:mn></mml:msub><mml:mo>,</mml:mo><mml:mo>…</mml:mo><mml:mo>,</mml:mo><mml:msub><mml:mrow><mml:mi>ɛ</mml:mi></mml:mrow><mml:mi>k</mml:mi></mml:msub><mml:mo>∈</mml:mo><mml:mrow><mml:mo>{</mml:mo> <mml:mrow><mml:mo>±</mml:mo><mml:mn>1</mml:mn></mml:mrow> <mml:mo>}</mml:mo></mml:mrow></mml:mrow></mml:munder><mml:mrow><mml:mrow><mml:mo>(</mml:mo><mml:mrow><mml:mi>x</mml:mi><mml:mo>+</mml:mo><mml:msub><mml:mrow><mml:mi>ɛ</mml:mi></mml:mrow><mml:mn>1</mml:mn></mml:msub><mml:msqrt><mml:mrow><mml:msub><mml:mrow><mml:mi>a</mml:mi></mml:mrow><mml:mn>1</mml:mn></mml:msub></mml:mrow></mml:msqrt><mml:mo>+</mml:mo><mml:msub><mml:mrow><mml:mi>ɛ</mml:mi></mml:mrow><mml:mn>2</mml:mn></mml:msub><mml:msqrt><mml:mrow><mml:msub><mml:mrow><mml:mi>a</mml:mi></mml:mrow><mml:mn>2</mml:mn></mml:msub></mml:mrow></mml:msqrt><mml:mi>W</mml:mi></mml:mrow><mml:mo>)</mml:mo></mml:mrow><mml:mo>+</mml:mo><mml:mo>…</mml:mo><mml:mo>+</mml:mo><mml:msub><mml:mrow><mml:mi>ɛ</mml:mi></mml:mrow><mml:mi>k</mml:mi></mml:msub><mml:msqrt><mml:mrow><mml:msub><mml:mrow><mml:mi>a</mml:mi></mml:mrow><mml:mi>k</mml:mi></mml:msub></mml:mrow></mml:msqrt><mml:msup><mml:mrow><mml:mi>W</mml:mi></mml:mrow><mml:mrow><mml:mi>k</mml:mi><mml:mo>-</mml:mo><mml:mn>1</mml:mn></mml:mrow></mml:msup></mml:mrow></mml:mrow></mml:math> <tex-math>{J_k}\left( {{a_1}, \ldots ,{a_k},x} \right) = \prod\limits_{{\varepsilon _1}, \ldots ,{\varepsilon _k} \in \left\{ { \pm 1} \right\}} {\left( {x + {\varepsilon _1}\sqrt {{a_1}} + {\varepsilon _2}\sqrt {{a_2}} W} \right) + \ldots + {\varepsilon _k}\sqrt {{a_k}} {W^{k - 1}}}</tex-math> </alternatives> </disp-formula> with <inline-formula> <alternatives> <inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2022-0013_eq_002.png"/> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"><mml:mrow><mml:mi>W</mml:mi><mml:mo>=</mml:mo><mml:msubsup><mml:mo>∑</mml:mo><mml:mrow><mml:mi>i</mml:mi><mml:mo>=</mml:mo><mml:mn>1</mml:mn></mml:mrow><mml:mi>k</mml:mi></mml:msubsup><mml:mrow><mml:msubsup><mml:mrow><mml:mi>x</mml:mi></mml:mrow> <mml:mi>i</mml:mi><mml:mn>2</mml:mn></mml:msubsup></mml:mrow></mml:mrow></mml:math> <tex-math>W = \sum\nolimits_{i = 1}^k {x_i^2} </tex-math> </alternatives> </inline-formula> has integer coefficients and <italic>J_k</italic>(<italic>a</italic>₁, . . ., <italic>a_k, x</italic>) = 0 for some <italic>a</italic>₁, . . ., <italic>a_k, x</italic> ∈ ℤ if and only if <italic>a</italic>₁, . . ., <italic>a_k</italic>are all squares. However although it is nontrivial to observe that this expression is a polynomial, i.e., eliminating similar elements in the product of all combinations of signs we obtain an expression where every square root will occur with an even power. This work has been partially presented in [7].</p> </abstract>ARTICLEtruehttps://sciendo.com/article/10.2478/forma-2022-00132022-12-30T00:00:00.000+00:00https://sciendo.com/article/10.2478/forma-2022-0017<abstract> <title style='display:none'>Summary</title> <p>In this paper problems 17, 18, 26, 27, 28, and 98 from [9] are formalized, using the Mizar formalism [8], [2], [3], [6].</p> </abstract>ARTICLEtruehttps://sciendo.com/article/10.2478/forma-2022-00172022-12-30T00:00:00.000+00:00https://sciendo.com/article/10.2478/forma-2022-0019<abstract> <title style='display:none'>Summary</title> <p>This paper reports on the formalization in Mizar system [1], [2] of ten selected problems from W. Sierpinski’s book “250 Problems in Elementary Number Theory” [7] (see [6] for details of this concrete dataset). This article is devoted mainly to arithmetic progressions: problems 52, 54, 55, 56, 60, 64, 70, 71, and 73 belong to the chapter “Arithmetic Progressions”, and problem 50 is from “Relatively Prime Numbers”.</p> </abstract>ARTICLEtruehttps://sciendo.com/article/10.2478/forma-2022-00192022-12-30T00:00:00.000+00:00https://sciendo.com/article/10.2478/forma-2022-0018<abstract> <title style='display:none'>Summary</title> <p>This paper reports on the formalization of ten selected problems from W. Sierpinski’s book “250 Problems in Elementary Number Theory” [5] using the Mizar system [4], [1], [2]. Problems 12, 13, 31, 32, 33, 35 and 40 belong to the chapter devoted to the divisibility of numbers, problem 47 concerns relatively prime numbers, whereas problems 76 and 79 are taken from the chapter on prime and composite numbers.</p> </abstract>ARTICLEtruehttps://sciendo.com/article/10.2478/forma-2022-00182022-12-30T00:00:00.000+00:00https://sciendo.com/article/10.2478/forma-2022-0016<abstract> <title style='display:none'>Summary</title> <p>We formalize in the Mizar system [3], [4] some basic properties on left module over a ring such as constructing a module via a ring of endomorphism of an abelian group and the set of all homomorphisms of modules form a module [1] along with Ch. 2 set. 1 of [2].</p> <p>The formalized items are shown in the below list with notations: <italic>M_ab</italic>for an Abelian group with a suffix “<italic>_ab</italic>” and <italic>M</italic> without a suffix is used for left modules over a ring.</p> <p>1. The endomorphism ring of an abelian group denoted by <bold>End</bold>(<italic>M_ab</italic>).</p> <p>2. A pair of an Abelian group <italic>M_ab</italic>and a ring homomorphism <inline-formula> <alternatives> <inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2022-0016_eq_001.png"/> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"><mml:mrow><mml:mi>R</mml:mi><mml:mover><mml:mo>→</mml:mo><mml:mi>ρ</mml:mi></mml:mover></mml:mrow></mml:math> <tex-math>R\mathop \to \limits^\rho</tex-math> </alternatives> </inline-formula> <bold>End</bold> (<italic>M_ab</italic>) determines a left <italic>R</italic>-module, formalized as a function <bold>AbGrLMod</bold>(<italic>M_ab, ρ</italic>) in the article.</p> <p>3. The set of all functions from <italic>M</italic> to <italic>N</italic> form <italic>R</italic>-module and denoted by <bold>Func_Mod</bold><italic>_R</italic>(<italic>M, N</italic>).</p> <p>4. The set <italic>R</italic>-module homomorphisms of <italic>M</italic> to <italic>N</italic>, denoted by <bold>Hom</bold><italic>_R</italic>(<italic>M, N</italic>), forms <italic>R</italic>-module.</p> <p>5. A formal proof of <bold>Hom</bold><italic>_R</italic>(¯<italic>R, M</italic>) ≅<italic>M</italic> is given, where the ¯<italic>R</italic> denotes the regular representation of <italic>R</italic>, i.e. we regard <italic>R</italic> itself as a left <italic>R</italic>-module.</p> <p>6. A formal proof of <bold>AbGrLMod</bold>(<italic>M</italic>′<italic>_ab, ρ</italic>′) ≅ <italic>M</italic> where <italic>M</italic>′<italic>_ab</italic>is an abelian group obtained by removing the scalar multiplication from <italic>M</italic>, and ρ′ is obtained by currying the scalar multiplication of <italic>M</italic>.</p> <p>The removal of the multiplication from <italic>M</italic> has been done by the forgettable functor defined as <bold>AbGr</bold> in the article.</p> </abstract>ARTICLEtruehttps://sciendo.com/article/10.2478/forma-2022-00162022-12-30T00:00:00.000+00:00https://sciendo.com/article/10.2478/forma-2022-0012<abstract> <title style='display:none'>Summary</title> <p>Previous Mizar articles [7, 6, 5] formalized the implicit and inverse function theorems for Frechet continuously differentiable maps on Banach spaces. In this paper, using the Mizar system [1], [2], we formalize these theorems on Euclidean spaces by specializing them. We referred to [4], [12], [10], [11] in this formalization.</p> </abstract>ARTICLEtruehttps://sciendo.com/article/10.2478/forma-2022-00122022-12-30T00:00:00.000+00:00https://sciendo.com/article/10.2478/forma-2022-0015<abstract> <title style='display:none'>Summary</title> <p>This is Erdős’s proof of the divergence of the sum of prime reciprocals, using the Mizar system [2], [3], as reported in “Proofs from THE BOOK” [1].</p> </abstract>ARTICLEtruehttps://sciendo.com/article/10.2478/forma-2022-00152022-12-30T00:00:00.000+00:00https://sciendo.com/article/10.2478/forma-2022-0014<abstract> <title style='display:none'>Summary</title> <p>This is the first part of a two-part article formalizing existence and uniqueness of algebraic closures using the Mizar system [1], [2]. Our proof follows Artin’s classical one as presented by Lang in [3]. In this first part we prove that for a given field <italic>F</italic> there exists a field extension <italic>E</italic> such that every non-constant polynomial <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>] has a root in <italic>E</italic>. Artin’s proof applies Kronecker’s construction to each polynomial <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>]<italic>\F</italic> simultaneously. To do so we need the polynomial ring <italic>F</italic> [<italic>X</italic>₁, <italic>X</italic>₂, ...] with infinitely many variables, one for each polynomal <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>]<italic>\F</italic> . The desired field extension <italic>E</italic> then is <italic>F</italic> [<italic>X</italic>₁, <italic>X</italic>₂, ...]<italic>\I</italic>, where <italic>I</italic> is a maximal ideal generated by all non-constant polynomials <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>]. Note, that to show that <italic>I</italic> is maximal Zorn’s lemma has to be applied.</p> <p>In the second part this construction is iterated giving an infinite sequence of fields, whose union establishes a field extension <italic>A</italic> of <italic>F</italic>, in which every non-constant polynomial <italic>p</italic> ∈ <italic>A</italic>[<italic>X</italic>] has a root. The field of algebraic elements of <italic>A</italic> then is an algebraic closure of <italic>F</italic> . To prove uniqueness of algebraic closures, e.g. that two algebraic closures of <italic>F</italic> are isomorphic over <italic>F</italic>, the technique of extending monomorphisms is applied: a monomorphism <italic>F</italic> → <italic>A</italic>, where <italic>A</italic> is an algebraic closure of <italic>F</italic> can be extended to a monomorphism <italic>E</italic> → <italic>A</italic>, where <italic>E</italic> is any algebraic extension of <italic>F</italic> . In case that <italic>E</italic> is algebraically closed this monomorphism is an isomorphism. Note that the existence of the extended monomorphism again relies on Zorn’s lemma.</p> </abstract>ARTICLEtruehttps://sciendo.com/article/10.2478/forma-2022-00142022-12-30T00:00:00.000+00:00https://sciendo.com/article/10.2478/forma-2022-0011<abstract> <title style='display:none'>Summary</title> <p>In this paper problems 11, 16, 19–24, 39, 44, 46, 74, 75, 77, 82, and 176 from [10] are formalized as described in [6], using the Mizar formalism [1], [2], [4]. Problems 11 and 16 from the book are formulated as several independent theorems. Problem 46 is formulated with a given example of required properties. Problem 77 is not formulated using triangles as in the book is.</p> </abstract>ARTICLEtruehttps://sciendo.com/article/10.2478/forma-2022-00112022-12-24T00:00:00.000+00:00https://sciendo.com/article/10.2478/forma-2022-0008<abstract> <title style='display:none'>Summary</title> <p>This paper, using the Mizar system [1], [2], provides useful tools for working with real linear spaces and real normed spaces. These include the identification of a real number set with a one-dimensional real normed space, the relationships between real linear spaces and real Euclidean spaces, the transformation from a real linear space to a real vector space, and the properties of basis and dimensions of real linear spaces. We referred to [6], [10], [8], [9] in this formalization.</p> </abstract>ARTICLEtruehttps://sciendo.com/article/10.2478/forma-2022-00082022-12-24T00:00:00.000+00:00https://sciendo.com/article/10.2478/forma-2022-0009<abstract> <title style='display:none'>Summary</title> <p>In this article vertex, edge and total colorings of graphs are formalized in the Mizar system [4] and [1], based on the formalization of graphs in [5].</p> </abstract>ARTICLEtruehttps://sciendo.com/article/10.2478/forma-2022-00092022-12-24T00:00:00.000+00:00https://sciendo.com/article/10.2478/forma-2022-0007<abstract> <title style='display:none'>Summary</title> <p>We formalize in Mizar [1], [2] the notion of characteristic subgroups using the definition found in Dummit and Foote [3], as subgroups invariant under automorphisms from its parent group. Along the way, we formalize notions of Automorphism and results concerning centralizers. Much of what we formalize may be found sprinkled throughout the literature, in particular Gorenstein [4] and Isaacs [5]. We show all our favorite subgroups turn out to be characteristic: the center, the derived subgroup, the commutator subgroup generated by characteristic subgroups, and the intersection of all subgroups satisfying a generic group property.</p> </abstract>ARTICLEtruehttps://sciendo.com/article/10.2478/forma-2022-00072022-12-24T00:00:00.000+00:00https://sciendo.com/article/10.2478/forma-2022-0010<abstract> <title style='display:none'>Summary</title> <p>In this study, using the Mizar system [1], [2], we reuse formalization e orts in fuzzy sets described in [5] and [6]. This time the centroid method which is one of the fuzzy inference processes is formulated [10]. It is the most popular of all defuzzied methods ([11], [13], [7]) – here, defuzzified crisp value is obtained from domain of membership function as weighted average [8]. Since the integral is used in centroid method, the integrability and bounded properties of membership functions are also mentioned to fill the formalization gaps present in the Mizar Mathematical Library, as in the case of another fuzzy operators [4]. In this paper, the properties of piecewise linear functions consisting of two straight lines are mainly described.</p> </abstract>ARTICLEtruehttps://sciendo.com/article/10.2478/forma-2022-00102022-12-24T00:00:00.000+00:00https://sciendo.com/article/10.2478/forma-2022-0001<abstract> <title style='display:none'>Summary</title> <p>This paper is a continuation of Inoué [5]. As already mentioned in the paper, a number of intuitionistic provable formulas are given with a Hilbert-style proof. For that, we make use of a family of intuitionistic deduction theorems, which are also presented in this paper by means of Mizar system [2], [1]. Our axiom system of intuitionistic propositional logic IPC is based on the propositional subsystem of H₁-<bold>IQC</bold> in Troelstra and van Dalen [6, p. 68]. We also owe Heyting [4] and van Dalen [7]. Our treatment of a set-theoretic intuitionistic deduction theorem is due to Agata Darmochwał’s Mizar article “Calculus of Quantifiers. Deduction Theorem” [3].</p> </abstract>ARTICLEtruehttps://sciendo.com/article/10.2478/forma-2022-00012022-12-21T00:00:00.000+00:00https://sciendo.com/article/10.2478/forma-2022-0005<abstract> <title style='display:none'>Summary</title> <p>Universe is a concept which is present from the beginning of the creation of the Mizar Mathematical Library (MML) in several forms (Universe, Universe_closure, UNIVERSE) [25], then later as the_universe_of, [33], and recently with the definition GrothendieckUniverse [26], [11], [11]. These definitions are useful in many articles [28, 33, 8, 35], [19, 32, 31, 15, 6], but also [34, 12, 20, 22, 21], [27, 2, 3, 23, 16, 7, 4, 5].</p> <p>In this paper, using the Mizar system [9] [10], we trivially show that Grothendieck’s definition of Universe as defined in [26], coincides with the original definition of Universe defined by Artin, Grothendieck, and Verdier (<italic>Chapitre 0 Univers et Appendice “Univers” (par N. Bourbaki) de l’Exposé I. “PREFAISCE-AUX”</italic>) [1], and how the different definitions of MML concerning universes are related. We also show that the definition of Universe introduced by Mac Lane ([18]) is compatible with the MML’s definition.</p> <p>Although a universe may be empty, we consider the properties of non-empty universes, completing the properties proved in [25].</p> <p>We introduce the notion of “trivial” and “non-trivial” Universes, depending on whether or not they contain the set <italic>ω</italic> (NAT), following the notion of Robert M. Solovay². The following result links the universes <bold>U</bold>₀ (FinSETS) and <bold>U</bold>₁ (SETS): <disp-formula> <alternatives> <graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2022-0005_eq_001.png"/> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="block"><mml:mrow><mml:mtext>Grothendieck</mml:mtext><mml:mi> </mml:mi><mml:mtext>Universe</mml:mtext><mml:mi> </mml:mi><mml:mi>ω</mml:mi><mml:mo>=</mml:mo><mml:mtext>Grothendieck</mml:mtext><mml:mi> </mml:mi><mml:mtext>Universe</mml:mtext><mml:mi> </mml:mi><mml:msub><mml:mrow><mml:mstyle fontweight="bold" fontstyle="normal"><mml:mi>U</mml:mi></mml:mstyle></mml:mrow><mml:mn>0</mml:mn></mml:msub><mml:mo>=</mml:mo><mml:msub><mml:mrow><mml:mstyle fontweight="bold" fontstyle="normal"><mml:mi>U</mml:mi></mml:mstyle></mml:mrow><mml:mn>1</mml:mn></mml:msub></mml:mrow></mml:math> <tex-math>{\rm{Grothendieck}}\,{\rm{Universe}}\,\omega = {\rm{Grothendieck}}\,{\rm{Universe}}\,{{\bf{U}}_0} = {{\bf{U}}_1}</tex-math> </alternatives> </disp-formula> Before turning to the last section, we establish some trivial propositions allowing the construction of sets outside the considered universe.</p> <p>The last section is devoted to the construction, in Tarski-Grothendieck, of a tower of universes indexed by the ordinal numbers (See 8. Examples, Grothendieck universe, ncatlab.org [24]).</p> <p>Grothendieck’s universe is referenced in current works: “Assuming the existence of a sufficient supply of (Grothendieck) univers”, Jacob Lurie in “Higher Topos Theory” [17], “Annexe B – Some results on Grothendieck universes”, Olivia Caramello and Riccardo Zanfa in “Relative topos theory via stacks” [13], “Remark 1.1.5 (quoting Michael Shulman [30])”, Emily Riehl in “Category theory in Context” [29], and more specifically “Strict Universes for Grothendieck Topoi” [14].</p> </abstract>ARTICLEtruehttps://sciendo.com/article/10.2478/forma-2022-00052022-12-21T00:00:00.000+00:00https://sciendo.com/article/10.2478/forma-2022-0004<abstract> <title style='display:none'>Summary</title> <p>The goal of this article is to clarify the relationship between Riemann’s improper integrals and Lebesgue integrals. In previous articles [6], [7], we treated Riemann’s improper integrals [1], [11] and [4] on arbitrary intervals. Therefore, in this article, we will continue to clarify the relationship between improper integrals and Lebesgue integrals [8], using the Mizar [3], [2] formalism.</p> </abstract>ARTICLEtruehttps://sciendo.com/article/10.2478/forma-2022-00042022-12-21T00:00:00.000+00:00en-us-1