Formalized Mathematics    (ISSN 1898-9934 (Online), ISSN 1426-2630 (Print))
Volume 13, Number 1 (2005): pdf, ps, dvi.
  1. Ming Liang, Yuzhong Ding. Partial Sum of Some Series, Formalized Mathematics 13(1), pages 1-4, 2005. MML Identifier: SERIES_2
    Summary: Solving the partial sum of some often used series.
  2. Patrick Braselmann, Peter Koepke. Substitution in First-Order Formulas: Elementary Properties, Formalized Mathematics 13(1), pages 5-15, 2005. MML Identifier: SUBSTUT1
    Summary: This article is part of a series of Mizar articles which constitute a formal proof (of a basic version) of Kurt G{\"o}del's famous completeness theorem (K. G{\"o}del, ``Die Vollst{\"a}ndigkeit der Axiome des logischen Funktionenkalk{\"u}ls'', Monatshefte f\"ur Mathematik und Physik 37 (1930), 349-360). The completeness theorem provides the theoretical basis for a uniform formalization of mathematics as in the Mizar project. We formalize first-order logic up to the completeness theorem as in H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 1984, Springer Verlag New York Inc. The present article introduces the basic concepts of substitution of a variable for a variable in a first-order formula. The contents of this article correspond to Chapter III par. 8, Definition 8.1, 8.2 of Ebbinghaus, Flum, Thomas.
  3. Patrick Braselmann, Peter Koepke. Coincidence Lemma and Substitution Lemma, Formalized Mathematics 13(1), pages 17-26, 2005. MML Identifier: SUBLEMMA
    Summary: This article is part of a series of Mizar articles which constitute a formal proof (of a basic version) of Kurt G{\"o}del's famous completeness theorem (K. G{\"o}del, ``Die Vollst{\"a}ndigkeit der Axiome des logischen Funktionenkalk{\"u}ls'', Monatshefte f\"ur Mathematik und Physik 37 (1930), 349--360). The completeness theorem provides the theoretical basis for a uniform formalization of mathematics as in the Mizar project. We formalize first-order logic up to the completeness theorem as in H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 1984, Springer Verlag New York Inc. The present article establishes further concepts of substitution of a variable for a variable in a first-order formula. The main result is the substitution lemma. The contents of this article correspond to Chapter III par. 5, 5.1 Coincidence Lemma and Chapter III par. 8, 8.3 Substitution Lemma of Ebbinghaus, Flum, Thomas.
  4. Patrick Braselmann, Peter Koepke. Substitution in First-Order Formulas. Part II. The Construction of First-Order Formulas, Formalized Mathematics 13(1), pages 27-32, 2005. MML Identifier: SUBSTUT2
    Summary: This article is part of a series of Mizar articles which constitute a formal proof (of a basic version) of Kurt G{\"o}del's famous completeness theorem (K. G{\"o}del, ``Die Vollst{\"a}ndigkeit der Axiome des logischen Funktionenkalk{\"u}ls'', Monatshefte f\"ur Mathematik und Physik 37 (1930), 349-360). The completeness theorem provides the theoretical basis for a uniform formalization of mathematics as in the Mizar project. We formalize first-order logic up to the completeness theorem as in H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 1984, Springer Verlag New York Inc. The present article establishes that every substitution can be applied to every formula as in Chapter III par. 8, Definition 8.1, 8.2 of Ebbinghaus, Flum, Thomas. After that, it is observed that substitution doesn't change the number of quantifiers of a formula. Then further details about substitution and some results about the construction of formulas are proven.
  5. Patrick Braselmann, Peter Koepke. A Sequent Calculus for First-Order Logic, Formalized Mathematics 13(1), pages 33-39, 2005. MML Identifier: CALCUL_1
    Summary: This article is part of a series of Mizar articles which constitute a formal proof (of a basic version) of Kurt G{\"o}del's famous completeness theorem (K. G{\"o}del, ``Die Vollst{\"a}ndigkeit der Axiome des logischen Funktionenkalk{\"u}ls'', Monatshefte f\"ur Mathematik und Physik 37 (1930), 349--360). The completeness theorem provides the theoretical basis for a uniform formalization of mathematics as in the Mizar project. We formalize first-order logic up to the completeness theorem as in H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 1984, Springer Verlag New York Inc. The present article introduces a sequent calculus for first-order logic. The correctness of this calculus is shown and some important inferences are derived. The contents of this article correspond to Chapter IV of Ebbinghaus, Flum, Thomas.
  6. Patrick Braselmann, Peter Koepke. Consequences of the Sequent Calculus, Formalized Mathematics 13(1), pages 41-44, 2005. MML Identifier: CALCUL_2
    Summary: This article is part of a series of Mizar articles which constitute a formal proof (of a basic version) of Kurt G{\"{o}}del's famous completeness theorem (K. G{\"{o}}del, ``Die Vollst{\"{a}}ndigkeit der Axiome des logischen Funktionenkalk{\"{u}}ls'', Monatshefte f\"ur Mathematik und Physik 37 (1930), 349-360). The completeness theorem provides the theoretical basis for a uniform formalization of mathematics as in the Mizar project. We formalize first-order logic up to the completeness theorem as in H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 1984, Springer Verlag New York Inc. The first main result of the present article is that the derivablility of a sequent doesn't depend on the ordering of the antecedent. The second main result says: if a sequent is derivable, then the formulas in the antecendent only need to occur once.
  7. Patrick Braselmann, Peter Koepke. Equivalences of Inconsistency and Henkin Models, Formalized Mathematics 13(1), pages 45-48, 2005. MML Identifier: HENMODEL
    Summary: This article is part of a series of Mizar articles which constitute a formal proof (of a basic version) of Kurt G{\"{o}}del's famous completeness theorem (K. G{\"{o}}del, ``Die Vollst{\"{a}}ndigkeit der Axiome des logischen Funktionenkalk{\"{u}}ls'', Monatshefte f\"ur Mathematik und Physik 37 (1930), 349--360). The completeness theorem provides the theoretical basis for a uniform formalization of mathematics as in the Mizar project. We formalize first-order logic up to the completeness theorem as in H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 1984, Springer Verlag, New York Inc. The present article establishes some equivalences of inconsistency. It is proved that a countable union of consistent sets is consistent. Then the concept of a Henkin model is introduced. The contents of this article correspond to Chapter IV, par. 7 and Chapter V, par. 1 of Ebbinghaus, Flum, Thomas.
  8. Patrick Braselmann, Peter Koepke. G\"odel's Completeness Theorem, Formalized Mathematics 13(1), pages 49-53, 2005. MML Identifier: GOEDELCP
    Summary: This article is part of a series of Mizar articles which constitute a formal proof (of a basic version) of Kurt G{\"o}del's famous completeness theorem (K. G{\"o}del, ``Die Vollst{\"a}ndigkeit der Axiome des logischen Funktionenkalk{\"u}ls'', Monatshefte f\"ur Mathematik und Physik 37 (1930), 349--360). The completeness theorem provides the theoretical basis for a uniform formalization of mathematics as in the Mizar project. We formalize first-order logic up to the completeness theorem as in H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 1984, Springer Verlag New York Inc. The present article contains the proof of a simplified completeness theorem for a countable relational language without equality.
  9. Shunichi Kobayashi. Propositional Calculus for Boolean Valued Functions. Part VIII, Formalized Mathematics 13(1), pages 55-58, 2005. MML Identifier: BVFUNC26
    Summary: In this paper, we proved some elementary propositional calculus formulae for Boolean valued functions.
  10. Yasumasa Suzuki. H\"older's Inequality and Minkowski's Inequality, Formalized Mathematics 13(1), pages 59-61, 2005. MML Identifier: HOLDER_1
    Summary: In this article, H\"older's inequality and Minkowski's inequality are proved. These equalities are basic ones of functional analysis.
  11. Yasumasa Suzuki. The Banach Space $l^p$, Formalized Mathematics 13(1), pages 63-66, 2005. MML Identifier: LP_SPACE
    Summary: We introduce the arithmetic addition and multiplication in the set of $l^p$ real sequences and also introduce the norm. This set has the structure of the Banach space.
  12. Yasunari Shidama, Noboru Endou. Lebesgue Integral of Simple Valued Function, Formalized Mathematics 13(1), pages 67-71, 2005. MML Identifier: MESFUNC3
    Summary: In this article, the authors introduce Lebesgue integral of simple valued function.
  13. Artur Kornilowicz, Yasunari Shidama. Inverse Trigonometric Functions Arcsin and Arccos, Formalized Mathematics 13(1), pages 73-79, 2005. MML Identifier: SIN_COS6
    Summary: Notions of inverse sine and inverse cosine have been introduced. Their basic properties have been proved.
  14. Artur Kornilowicz. On Some Points of a Simple Closed Curve, Formalized Mathematics 13(1), pages 81-87, 2005. MML Identifier: JORDAN21
    Summary:
  15. Artur Kornilowicz, Adam Grabowski. On Some Points of a Simple Closed Curve. Part II, Formalized Mathematics 13(1), pages 89-91, 2005. MML Identifier: JORDAN22
    Summary: In the paper we formalize some lemmas needed by the proof of the Jordan Curve Theorem according to \cite{TAKE-NAKA}. We show basic properties of the upper and the lower approximations of a simple closed curve (as its compactness and connectedness) and some facts about special points of such approximations.
  16. Noboru Endou. Uniform Continuity of Functions on Normed Complex Linear Spaces, Formalized Mathematics 13(1), pages 93-98, 2005. MML Identifier: NCFCONT2
    Summary:
  17. Czeslaw Bylinski. Introduction to Real Linear Topological Spaces, Formalized Mathematics 13(1), pages 99-107, 2005. MML Identifier: RLTOPSP1
    Summary:
  18. Artur Kornilowicz, Yasunari Shidama. Some Properties of Rectangles on the Plane, Formalized Mathematics 13(1), pages 109-115, 2005. MML Identifier: TOPREALA
    Summary:
  19. Artur Kornilowicz, Yasunari Shidama. Some Properties of Circles on the Plane, Formalized Mathematics 13(1), pages 117-124, 2005. MML Identifier: TOPREALB
    Summary:
  20. Adam Naumowicz. On the Characterization of Collineations of the Segre Product of Strongly Connected Partial Linear Spaces, Formalized Mathematics 13(1), pages 125-131, 2005. MML Identifier: PENCIL_3
    Summary: In this paper we characterize the automorphisms (collineations) of the Segre product of partial linear spaces. In particular, we show that if all components of the product are strongly connected, then every collineation is determined by a set of isomorphisms between its components. The formalization follows the ideas presented in the {\em Journal of Geometry} paper \cite{ANKPJG} by Naumowicz and Pra\.zmowski.
  21. Adam Naumowicz. Spaces of Pencils, Grassmann Spaces, and Generalized Veronese Spaces, Formalized Mathematics 13(1), pages 133-138, 2005. MML Identifier: PENCIL_4
    Summary: In this paper we construct several examples of partial linear spaces. First, we define two algebraic structures, namely the spaces of $k$-pencils and Grassmann spaces for vector spaces over an arbitrary field. Then we introduce the notion of generalized Veronese spaces following the definition presented in the paper \cite{ANKPRM} by Naumowicz and Pra\.zmowski. For all spaces defined, we state the conditions under which they are not degenerated to a single line.
  22. Adam Grabowski. On the Boundary and Derivative of a Set, Formalized Mathematics 13(1), pages 139-146, 2005. MML Identifier: TOPGEN_1
    Summary: This is the first Mizar article in a series aiming at a complete formalization of the textbook ``General Topology'' by Engelking \cite{ENGEL:1}. We cover the first part of Section 1.3, by defining such notions as a derivative of a subset $A$ of a topological space (usually denoted by $A^{\rm d}$, but ${\rm Der~} A$ in our notation), the derivative and the boundary of families of subsets, points of accumulation and isolated points. We also introduce dense-in-itself, perfect and scattered topological spaces and formulate the notion of the density of a space. Some basic properties are given as well as selected exercises from \cite{ENGEL:1}.
  23. Christoph Schwarzweller. Construction of Gr\"obner Bases: Avoiding S-Polynomials -- Buchberger's First Criterium, Formalized Mathematics 13(1), pages 147-156, 2005. MML Identifier: GROEB_3
    Summary: We continue the formalization of Groebner bases following the book ``Groebner Bases -- A Computational Approach to Commutative Algebra'' by Becker and Weispfenning. Here we prove Buchberger's first criterium on avoiding S-polynomials: S-polynomials for polynomials with disjoint head terms need not be considered when constructing Groebner bases. In the course of formalizing this theorem we also introduced the splitting of a polynomial in an upper and a lower polynomial containing the greater resp. smaller terms of the original polynomial with respect to a given term order.
  24. Wenpai Chang, Hiroshi Yamazaki, Yatsuka Nakamura. A Theory of Matrices of Complex Elements, Formalized Mathematics 13(1), pages 157-162, 2005. MML Identifier: MATRIX_5
    Summary: A concept of ``Matrix of Complex'' is defined here. Addition, subtraction, scalar multiplication and product are introduced using correspondent definitions of ``Matrix of Field''. Many equations for such operations consist of a case of ``Matrix of Field''. A calculation method of product of matrices is shown using a finite sequence of Complex in the last theorem.
  25. Grzegorz Bancerek. On the Characteristic and Weight of a Topological Space, Formalized Mathematics 13(1), pages 163-169, 2005. MML Identifier: TOPGEN_2
    Summary: We continue Mizar formalization of General Topology according to the book \cite{ENGEL:1} by Engelking. In the article the formalization of Section 1.1 is completed. Namely, the paper includes the formalization of theorems on correspondence of the basis and basis in a point, definitions of the character of a point and a topological space, a neighborhood system, and the weight of a topological space. The formalization is tested with almost discrete topological spaces with infinity.
  26. Grzegorz Bancerek. On Constructing Topological Spaces and Sorgenfrey Line, Formalized Mathematics 13(1), pages 171-179, 2005. MML Identifier: TOPGEN_3
    Summary: We continue Mizar formalization of General Topology according to the book \cite{ENGEL:1} by Engelking. In the article the formalization of Section 1.2 is almost completed. Namely, we formalize theorems on introduction of topologies by bases, neighborhood systems, closed sets, closure operator, and interior operator. The Sorgenfrey line is defined by a basis. It is proved that the weight of it is continuum. Other techniques are used to demonstrate introduction of discrete and anti-discrete topologies.
  27. Artur Kornilowicz. On the Real Valued Functions, Formalized Mathematics 13(1), pages 181-187, 2005. MML Identifier: PARTFUN3
    Summary:
  28. Adam Grabowski, Markus Moschner. Formalization of Ortholattices via~Orthoposets, Formalized Mathematics 13(1), pages 189-197, 2005. MML Identifier: ROBBINS3
    Summary: There are two approaches to lattices used in the Mizar Mathematical Library: on the one hand, these structures are based on the set with two binary operations (with an equational characterization as in \cite{LATTICES.ABS}). On the other hand, we may look at them as at relational structures (posets -- see \cite{ORDERS_1.ABS}). As the main result of this article we can state that the Mizar formalization enables us to use both approaches simultaneously (Section 3). This is especially useful because most of lemmas on ortholattices in the literature are stated in the poset setting, so we cannot use equational theorem provers in a straightforward way. We give also short equational characterization of lattices via four axioms (as it was done in \cite{McCune:2005} with the help of the Otter prover). Some corresponding results about ortholattices are also formalized.