rss_2.0Formalized Mathematics FeedSciendo RSS Feed for Formalized Mathematics Mathematics Feed Extensions<abstract> <title style='display:none'>Summary</title> <p>In this article we continue the formalization of field theory in Mizar. We introduce simple extensions: an extension <italic>E</italic> of <italic>F</italic> is simple if <italic>E</italic> is generated over <italic>F</italic> by a single element of <italic>E</italic>, that is <italic>E</italic> = <italic>F</italic> (<italic>a</italic>) for some <italic>a</italic> ∈ <italic>E</italic>. First, we prove that a finite extension <italic>E</italic> of <italic>F</italic> is simple if and only if there are only finitely many intermediate fields between <italic>E</italic> and <italic>F</italic> [<xref ref-type="bibr" rid="j_forma-2023-0023_ref_007">7</xref>]. Second, we show that finite extensions of a field <italic>F</italic> with characteristic 0 are always simple [<xref ref-type="bibr" rid="j_forma-2023-0023_ref_001">1</xref>]. For this we had to prove, that irreducible polynomials over <italic>F</italic> have single roots only, which required extending results on divisibility and gcds of polynomials [<xref ref-type="bibr" rid="j_forma-2023-0023_ref_014">14</xref>], [<xref ref-type="bibr" rid="j_forma-2023-0023_ref_013">13</xref>] and formal derivation of polynomials [<xref ref-type="bibr" rid="j_forma-2023-0023_ref_015">15</xref>].</p> </abstract>ARTICLEtrue Geometry Axioms. Part V – Half-planes and Planes<abstract> <title style='display:none'>Summary</title> <p>In the article, we continue the formalization of the work devoted to Tarski’s geometry – the book “Metamathematische Methoden in der Geometrie” by W. Schwabhäuser, W. Szmielew, and A. Tarski. We use the Mizar system to formalize Chapter 9 of this book. We deal with half-planes and planes proving their properties as well as the theory of intersecting lines.</p> </abstract>ARTICLEtrue Piecewise Linear Functions Composed by Absolute Value Function<abstract> <title style='display:none'>Summary</title> <p>We continue the formal development of the application of piecewise linear functions and centroids in the area of fuzzy set theory. The corresponding piecewise linear functions are symmetrical and composed by absolute function. In this paper we prove that the membership functions of isosceles triangle type and isosceles trapezoid type can be constructed by functions of this type.</p> </abstract>ARTICLEtrue of Continuous Functions of Two Variables<abstract> <title style='display:none'>Summary</title> <p>We extend the formalization of the integral theory of one-variable functions for Riemann and Lebesgue integrals, showing that the Lebesgue integral of a continuous function of two variables coincides with the Riemann iterated integral of a projective function.</p> </abstract>ARTICLEtrue Number Theory Problems. Part XII – Primes in Arithmetic Progression<abstract> <title style='display:none'>Summary</title> <p>In this paper another twelve problems from W. Sierpiński’s book “250 Problems in Elementary Number Theory” are formalized, using the Mizar formalism, namely: 42, 43, 51, 51a, 57, 59, 72, 135, 136, and 153–155. Significant amount of the work is devoted to arithmetic progressions.</p> </abstract>ARTICLEtrue of Orderings<abstract> <title style='display:none'>Summary</title> <p>In this article we extend the algebraic theory of ordered fields [<xref ref-type="bibr" rid="j_forma-2023-0027_ref_006">6</xref>], [<xref ref-type="bibr" rid="j_forma-2023-0027_ref_008">8</xref>] in Mizar. We introduce extensions of orderings: if <italic>E</italic> is a field extension of <italic>F</italic>, then an ordering <italic>P</italic> of <italic>F</italic> extends to <italic>E</italic>, if there exists an ordering <italic>O</italic> of <italic>E</italic> containing <italic>P</italic>. We first prove some necessary and su cient conditions for <italic>P</italic> being extendable to <italic>E</italic>, in particular that <italic>P</italic> extends to <italic>E</italic> if and only if the set <inline-formula> <alternatives> <inline-graphic xmlns:xlink="" xlink:href="graphic/j_forma-2023-0027_ieq_001.png"/> <mml:math xmlns:mml=""><mml:mrow><mml:mi>Q</mml:mi><mml:mi>S</mml:mi><mml:mi> </mml:mi><mml:mi> </mml:mi><mml:mi>E</mml:mi><mml:mo>:</mml:mo><mml:mo>=</mml:mo><mml:mrow><mml:mo>{</mml:mo> <mml:mrow><mml:mo>∑</mml:mo> <mml:mrow><mml:mi>a</mml:mi><mml:mo>*</mml:mo><mml:msup><mml:mrow><mml:mi>b</mml:mi></mml:mrow><mml:mn>2</mml:mn></mml:msup><mml:mo>|</mml:mo><mml:mi>a</mml:mi><mml:mo>∈</mml:mo><mml:mi>P</mml:mi><mml:mo>,</mml:mo><mml:mi> </mml:mi><mml:mi> </mml:mi><mml:mi>b</mml:mi><mml:mo>∈</mml:mo><mml:mi>E</mml:mi></mml:mrow></mml:mrow> <mml:mo>}</mml:mo></mml:mrow></mml:mrow></mml:math> <tex-math>QS\,\,E: = \left\{ {\sum {a*{b^2}|a \in P,\,\,b \in E} } \right\}</tex-math> </alternatives> </inline-formula> is a preordering of <italic>E</italic> – or equivalently if and only if −1 <italic>/</italic> ∉ <italic>QS E</italic>. Then we show for non-square <italic>a</italic> ∈ <italic>F</italic> that <italic>P</italic> extends to <inline-formula> <alternatives> <inline-graphic xmlns:xlink="" xlink:href="graphic/j_forma-2023-0027_ieq_002.png"/> <mml:math xmlns:mml=""><mml:mrow><mml:mi>F</mml:mi><mml:mrow><mml:mo>(</mml:mo><mml:mrow><mml:msqrt><mml:mi>a</mml:mi></mml:msqrt></mml:mrow><mml:mo>)</mml:mo></mml:mrow></mml:mrow></mml:math> <tex-math>F\left( {\sqrt a } \right)</tex-math> </alternatives> </inline-formula> if and only if <italic>P</italic> and finally that every ordering <italic>P</italic> of <italic>F</italic> extends to <italic>E</italic> if the degree of <italic>E</italic> over <italic>F</italic> is odd.</p> </abstract>ARTICLEtrue Measure Space and Integration<abstract> <title style='display:none'>Summary</title> <p>This paper introduces multidimensional measure spaces and the integration of functions on these spaces in Mizar. Integrals on the multidimensional Cartesian product measure space are defined and appropriate formal apparatus to deal with this notion is provided as well.</p> </abstract>ARTICLEtrue of Game Theoretic and Tree Theoretic Approaches to Conway Numbers<abstract> <title style='display:none'>Summary</title> <p>In this article, we develop our formalised concept of Conway numbers as outlined in [<xref ref-type="bibr" rid="j_forma-2023-0019_ref_009">9</xref>]. We focus mainly pre-order properties, birthday arithmetic contained in the Chapter 1, <italic>Properties of Order and Equality</italic> of John Conway’s seminal book. We also propose a method for the selection of class representatives respecting the relation defined by the pre-ordering in order to facilitate combining the results obtained for the original and tree-theoretic definitions of Conway numbers.</p> </abstract>ARTICLEtrue Number Theory Problems. Part XI<abstract> <title style='display:none'>Summary</title> <p>In this paper we present the Mizar formalization of the 36th problem from W. Sierpiński’s book “250 Problems in Elementary Number Theory” [<xref ref-type="bibr" rid="j_forma-2023-0021_ref_010">10</xref>].</p> </abstract>ARTICLEtrue Ring of Conway Numbers in Mizar<abstract> <title style='display:none'>Summary</title> <p>Conway’s introduction to algebraic operations on surreal numbers with a rather simple definition. However, he combines recursion with Conway’s induction on surreal numbers, more formally he combines transfinite induction-recursion with the properties of proper classes, which is diffcult to introduce formally.</p> <p>This article represents a further step in our ongoing e orts to investigate the possibilities offered by Mizar with Tarski-Grothendieck set theory [<xref ref-type="bibr" rid="j_forma-2023-0020_ref_004">4</xref>] to introduce the algebraic structure of Conway numbers and to prove their ring character.</p> </abstract>ARTICLEtrue Numbers – Formal Introduction<abstract> <title style='display:none'>Summary</title> <p>Surreal numbers, a fascinating mathematical concept introduced by John Conway, have attracted considerable interest due to their unique properties. In this article, we formalize the basic concept of surreal numbers close to the original Conway’s convention in the field of combinatorial game theory. We define surreal numbers with the pre-order in the Mizar system which satisfy the following condition: <italic>x</italic> ⩽ <italic>y</italic> iff <italic>L<sub>x</sub></italic> ≪ {<italic>y</italic>} <italic>Λ</italic> {<italic>x</italic>} ≪ <italic>R<sub>y</sub></italic>.</p> </abstract>ARTICLEtrue Number Theory Problems. Part X – Diophantine Equations<abstract> <title style='display:none'>Summary</title> <p>This paper continues the formalization of problems defined in the book “250 Problems in Elementary Number Theory” by Wacław Sierpiński.</p> </abstract>ARTICLEtrue Fuzzy Negations and Laws of Contraposition. Lattice of Fuzzy Negations<abstract> <title style='display:none'>Summary</title> <p>This the next article in the series formalizing the book of Baczyński and Jayaram “Fuzzy Implications”. We define the laws of contraposition connected with various fuzzy negations, and in order to make the cluster registration mechanism fully working, we construct some more non-classical examples of fuzzy implications. Finally, as the testbed of the reuse of lattice-theoretical approach, we introduce the lattice of fuzzy negations and show its basic properties.</p> </abstract>ARTICLEtrue Number Theory Problems. Part IX<abstract> <title style='display:none'>Summary</title> <p>This paper continues the formalization of chosen problems defined in the book “250 Problems in Elementary Number Theory” by Wacław Sierpiński.</p> </abstract>ARTICLEtrue Principle for Rings and Abelian Groups<abstract> <title style='display:none'>Summary</title> <p>The article concerns about formalizing a certain lemma on embedding of algebraic structures in the Mizar system, claiming that if a ring <italic>A</italic> is embedded in a ring <italic>B</italic> then there exists a ring <italic>C</italic> which is isomorphic to <italic>B</italic> and includes <italic>A</italic> as a subring. This construction applies to algebraic structures such as Abelian groups and rings.</p> </abstract>ARTICLEtrue Extensions<abstract> <title style='display:none'>Summary</title> <p>In this article we continue the formalization of field theory in Mizar [<xref ref-type="bibr" rid="j_forma-2023-0011_ref_001">1</xref>], [<xref ref-type="bibr" rid="j_forma-2023-0011_ref_002">2</xref>], [<xref ref-type="bibr" rid="j_forma-2023-0011_ref_004">4</xref>], [<xref ref-type="bibr" rid="j_forma-2023-0011_ref_003">3</xref>]. We introduce normal extensions: an (algebraic) extension <italic>E</italic> of <italic>F</italic> is normal if every polynomial of <italic>F</italic> that has a root in <italic>E</italic> already splits in <italic>E</italic>. We proved characterizations (for finite extensions) by minimal polynomials [<xref ref-type="bibr" rid="j_forma-2023-0011_ref_007">7</xref>], splitting fields, and fixing monomorphisms [<xref ref-type="bibr" rid="j_forma-2023-0011_ref_006">6</xref>], [<xref ref-type="bibr" rid="j_forma-2023-0011_ref_005">5</xref>]. This required extending results from [<xref ref-type="bibr" rid="j_forma-2023-0011_ref_011">11</xref>] and [<xref ref-type="bibr" rid="j_forma-2023-0011_ref_012">12</xref>], in particular that <italic>F</italic>[<italic>T</italic>] = {<italic>p</italic>(<italic>a</italic><sub>1</sub>, . . . <italic>a<sub>n</sub></italic>) | <italic>p</italic> ∈ <italic>F</italic>[<italic>X</italic>], <italic>a<sub>i</sub></italic> ∈ <italic>T</italic>} and <italic>F</italic>(<italic>T</italic>) = <italic>F</italic>[<italic>T</italic>] for finite algebraic <italic>T</italic> ⊆ <italic>E</italic>. We also provided the counterexample that 𝒬(∛2) is not normal over 𝒬 (compare [<xref ref-type="bibr" rid="j_forma-2023-0011_ref_013">13</xref>]).</p> </abstract>ARTICLEtrue and Integration<abstract> <title style='display:none'>Summary</title> <p>In this paper, we introduce indefinite integrals [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_008">8</xref>] (antiderivatives) and proof integration by substitution in the Mizar system [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_002">2</xref>], [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_003">3</xref>]. In our previous article [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_015">15</xref>], we have introduced an indefinite-like integral, but it is inadequate because it must be an integral over the whole set of real numbers and in some sense it causes some duplication in the Mizar Mathematical Library [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_013">13</xref>]. For this reason, to define the antiderivative for a function, we use the derivative of an arbitrary interval as defined recently in [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_007">7</xref>]. Furthermore, antiderivatives are also used to modify the integration by substitution and integration by parts.</p> <p>In the first section, we summarize the basic theorems on continuity and derivativity (for interesting survey of formalizations of real analysis in another proof-assistants like ACL2 [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_012">12</xref>], Isabelle/HOL [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_011">11</xref>], Coq [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_004">4</xref>], see [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_005">5</xref>]). In the second section, we generalize some theorems that were noticed during the formalization process. In the last section, we define the antiderivatives and formalize the integration by substitution and the integration by parts. We referred to [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_001">1</xref>] and [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_006">6</xref>] in our development.</p> </abstract>ARTICLEtrue Direct Products and the Universal Property of Direct Product Groups<abstract> <title style='display:none'>Abstract</title> <p>This is a “quality of life” article concerning product groups, using the Mizar system [2], [4]. Like a Sonata, this article consists of three movements.</p> <p>The first act, the slowest of the three, builds the infrastructure necessary for the rest of the article. We prove group homomorphisms map arbitrary finite products to arbitrary finite products, introduce a notion of “group yielding” families, as well as families of homomorphisms. We close the first act with defining the inclusion morphism of a subgroup into its parent group, and the projection morphism of a product group onto one of its factors.</p> <p>The second act introduces the universal property of products and its consequences as found in, e.g., Kurosh [7]. Specifically, for the product of an arbitrary family of groups, we prove the center of a product group is the product of centers. More exciting, we prove for a product of a finite family groups, the commutator subgroup of the product is the product of commutator subgroups, but this is because in general: the direct sum of commutator subgroups is the subgroup of the commutator subgroup of the product group, and the commutator subgroup of the product is a subgroup of the product of derived subgroups. We conclude this act by proving a few theorems concerning the image and kernel of morphisms between product groups, as found in Hungerford [5], as well as quotients of product groups.</p> <p>The third act introduces the notion of an internal direct product. Isaacs [6] points out (paraphrasing with Mizar terminology) that the internal direct product is a predicate but the external direct product is a [Mizar] functor. To our delight, we find the bulk of the “recognition theorem” (as stated by Dummit and Foote [3], Aschbacher [1], and Robinson [11]) are already formalized in the heroic work of Nakasho, Okazaki, Yamazaki, and Shimada [9], [8]. We generalize the notion of an internal product to a set of subgroups, proving it is equivalent to the internal product of a family of subgroups [10].</p> </abstract>ARTICLEtrue Number Theory Problems. Part VIII<abstract><title style='display:none'>Abstract</title> <p>In this paper problems 25, 86, 88, 105, 111, 137–142, and 184–185 from [12] are formalized, using the Mizar formalism [3], [1], [4]. This is a continuation of the work from [5], [6], and [2] as suggested in [8]. The automatization of selected lemmas from [11] proven in this paper as proposed in [9] could be an interesting future work.</p> </abstract>ARTICLEtrue Regular Graphs<abstract><title style='display:none'>Abstract</title> <p>In this article regular graphs, both directed and undirected, are formalized in the Mizar system [7], [2], based on the formalization of graphs as described in [10]. The handshaking lemma is also proven.</p> </abstract>ARTICLEtrue