Journal & Issues

Volume 30 (2022): Issue 3 (October 2022)

Volume 30 (2022): Issue 2 (July 2022)

Volume 30 (2022): Issue 1 (April 2022)

Volume 29 (2021): Issue 4 (December 2021)

Volume 29 (2021): Issue 3 (October 2021)

Volume 29 (2021): Issue 2 (July 2021)

Volume 29 (2021): Issue 1 (April 2021)

Volume 28 (2020): Issue 4 (December 2020)

Volume 28 (2020): Issue 3 (October 2020)

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

Volume 28 (2020): Issue 1 (April 2020)

Volume 27 (2019): Issue 4 (December 2019)

Volume 27 (2019): Issue 3 (October 2019)

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

Volume 27 (2019): Issue 1 (April 2019)

Volume 26 (2018): Issue 4 (December 2018)

Volume 26 (2018): Issue 3 (October 2018)

Volume 26 (2018): Issue 2 (July 2018)

Volume 26 (2018): Issue 1 (April 2018)

Volume 25 (2017): Issue 4 (December 2017)

Volume 25 (2017): Issue 3 (October 2017)

Volume 25 (2017): Issue 2 (July 2017)

Volume 25 (2017): Issue 1 (March 2017)

Volume 24 (2016): Issue 4 (December 2016)

Volume 24 (2016): Issue 3 (September 2016)

Volume 24 (2016): Issue 2 (June 2016)

Volume 24 (2016): Issue 1 (March 2016)

Volume 23 (2015): Issue 4 (December 2015)

Volume 23 (2015): Issue 3 (September 2015)

Volume 23 (2015): Issue 2 (June 2015)

Volume 23 (2015): Issue 1 (March 2015)

Volume 22 (2014): Issue 4 (December 2014)

Volume 22 (2014): Issue 3 (September 2014)

Volume 22 (2014): Issue 2 (June 2014)
Special Issue: 25 years of the Mizar Mathematical Library

Volume 22 (2014): Issue 1 (March 2014)

Volume 21 (2013): Issue 4 (December 2013)

Volume 21 (2013): Issue 3 (October 2013)

Volume 21 (2013): Issue 2 (June 2013)

Volume 21 (2013): Issue 1 (January 2013)

Volume 20 (2012): Issue 4 (December 2012)

Volume 20 (2012): Issue 3 (September 2012)

Volume 20 (2012): Issue 2 (June 2012)

Volume 20 (2012): Issue 1 (January 2012)

Volume 19 (2011): Issue 4 (December 2011)

Volume 19 (2011): Issue 3 (September 2011)

Volume 19 (2011): Issue 2 (June 2011)

Volume 19 (2011): Issue 1 (March 2011)

Volume 18 (2010): Issue 4 (December 2010)

Volume 18 (2010): Issue 3 (September 2010)

Volume 18 (2010): Issue 2 (June 2010)

Volume 18 (2010): Issue 1 (March 2010)

Volume 17 (2009): Issue 4 (December 2009)

Volume 17 (2009): Issue 3 (September 2009)

Volume 17 (2009): Issue 2 (June 2009)

Volume 17 (2009): Issue 1 (March 2009)

Volume 16 (2008): Issue 4 (December 2008)

Volume 16 (2008): Issue 3 (September 2008)

Volume 16 (2008): Issue 2 (June 2008)

Volume 16 (2008): Issue 1 (March 2008)

Volume 15 (2007): Issue 4 (December 2007)

Volume 15 (2007): Issue 3 (September 2007)

Volume 15 (2007): Issue 2 (June 2007)

Volume 15 (2007): Issue 1 (March 2007)

Volume 14 (2006): Issue 4 (December 2006)

Volume 14 (2006): Issue 3 (September 2006)

Volume 14 (2006): Issue 2 (June 2006)

Volume 14 (2006): Issue 1 (March 2006)

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

Search

Volume 30 (2022): Issue 1 (April 2022)

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

Search

6 Articles
Open Access

Intuitionistic Propositional Calculus in the Extended Framework with Modal Operator. Part II

Published Online: 21 Dec 2022
Page range: 1 - 12

Abstract

Summary

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 H1-IQC 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].

Keywords

  • intuitionistic logic
  • deduction theorem
  • consequence operator

MSC

  • 03B20
  • 03F03
  • 68V20
Open Access

Compactness of Neural Networks

Published Online: 21 Dec 2022
Page range: 13 - 21

Abstract

Summary

In this article, Feed-forward Neural Network is formalized in the Mizar system [1], [2]. First, the multilayer perceptron [6], [7], [8] is formalized using functional sequences. Next, we show that a set of functions generated by these neural networks satisfies equicontinuousness and equiboundedness property [10], [5]. At last, we formalized the compactness of the function set of these neural networks by using the Ascoli-Arzela’s theorem according to [4] and [3].

Keywords

  • neural network
  • compactness
  • Ascoli-Arzela’s theorem
  • equicontinuousness of continuous functions
  • equiboundedness of continuous functions

MSC

  • 46B50
  • 68T05
  • 68V20
Open Access

Splitting Fields for the Rational Polynomials X2−2, X2+X+1, X3−1, and X3−2

Published Online: 21 Dec 2022
Page range: 23 - 30

Abstract

Summary

In [11] the existence (and uniqueness) of splitting fields has been formalized. In this article we apply this result by providing splitting fields for the polynomials X2 − 2, X3 − 1, X2 + X + 1 and X3 − 2 over Q using the Mizar [2], [1] formalism. We also compute the degrees and bases for these splitting fields, which requires some additional registrations to adopt types properly.

The main result, however, is that the polynomial X3 − 2 does not split over 𝒬(23) \mathcal{Q}\left( {\root 3 \of 2 } \right) . Because X3 − 2 obviously has a root over 𝒬(23) \mathcal{Q}\left( {\root 3 \of 2 } \right) this shows that the field extension 𝒬(23) \mathcal{Q}\left( {\root 3 \of 2 } \right) is not normal over Q [3], [4], [5] and [7].

Keywords

  • splitting fields
  • rational polynomials

MSC

  • 12F05
  • 68V20
Open Access

Absolutely Integrable Functions

Published Online: 21 Dec 2022
Page range: 31 - 52

Abstract

Summary

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.

Keywords

  • absolutely integrable
  • improper integral

MSC

  • 26A42
  • 68V20
Open Access

Non-Trivial Universes and Sequences of Universes

Published Online: 21 Dec 2022
Page range: 53 - 66

Abstract

Summary

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].

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 (Chapitre 0 Univers et Appendice “Univers” (par N. Bourbaki) de l’Exposé I. “PREFAISCE-AUX”) [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.

Although a universe may be empty, we consider the properties of non-empty universes, completing the properties proved in [25].

We introduce the notion of “trivial” and “non-trivial” Universes, depending on whether or not they contain the set ω (NAT), following the notion of Robert M. Solovay2. The following result links the universes U0 (FinSETS) and U1 (SETS): GrothendieckUniverseω=GrothendieckUniverseU0=U1 {\rm{Grothendieck}}\,{\rm{Universe}}\,\omega = {\rm{Grothendieck}}\,{\rm{Universe}}\,{{\bf{U}}_0} = {{\bf{U}}_1} Before turning to the last section, we establish some trivial propositions allowing the construction of sets outside the considered universe.

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]).

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].

Keywords

  • Tarski-Grothendieck set theory
  • Grothendieck universe
  • universe hierarchy

MSC

  • 03E70
  • 68V20
Open Access

Isomorphism between Spaces of Multilinear Maps and Nested Compositions over Real Normed Vector Spaces

Published Online: 21 Dec 2022
Page range: 67 - 77

Abstract

Summary

This paper formalizes in Mizar [1], [2], that the isometric isomorphisms between spaces formed by an (n + 1)-dimensional multilinear map and an n-fold composition of linear maps on real normed spaces. This result is used to describe the space of nth-order derivatives of the Frechet derivative as a multilinear space. In Section 1, we discuss the spaces of 1-dimensional multilinear maps and 0-fold compositions as a preparation, and in Section 2, we extend the discussion to the spaces of (n + 1)-dimensional multilinear map and an n-fold compositions. We referred to [4], [11], [8], [9] in this formalization.

Keywords

  • Banach space
  • composition function
  • multilinear function

MSC

  • 15A69
  • 47A07
  • 68V20
6 Articles
Open Access

Intuitionistic Propositional Calculus in the Extended Framework with Modal Operator. Part II

Published Online: 21 Dec 2022
Page range: 1 - 12

Abstract

Summary

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 H1-IQC 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].

Keywords

  • intuitionistic logic
  • deduction theorem
  • consequence operator

MSC

  • 03B20
  • 03F03
  • 68V20
Open Access

Compactness of Neural Networks

Published Online: 21 Dec 2022
Page range: 13 - 21

Abstract

Summary

In this article, Feed-forward Neural Network is formalized in the Mizar system [1], [2]. First, the multilayer perceptron [6], [7], [8] is formalized using functional sequences. Next, we show that a set of functions generated by these neural networks satisfies equicontinuousness and equiboundedness property [10], [5]. At last, we formalized the compactness of the function set of these neural networks by using the Ascoli-Arzela’s theorem according to [4] and [3].

Keywords

  • neural network
  • compactness
  • Ascoli-Arzela’s theorem
  • equicontinuousness of continuous functions
  • equiboundedness of continuous functions

MSC

  • 46B50
  • 68T05
  • 68V20
Open Access

Splitting Fields for the Rational Polynomials X2−2, X2+X+1, X3−1, and X3−2

Published Online: 21 Dec 2022
Page range: 23 - 30

Abstract

Summary

In [11] the existence (and uniqueness) of splitting fields has been formalized. In this article we apply this result by providing splitting fields for the polynomials X2 − 2, X3 − 1, X2 + X + 1 and X3 − 2 over Q using the Mizar [2], [1] formalism. We also compute the degrees and bases for these splitting fields, which requires some additional registrations to adopt types properly.

The main result, however, is that the polynomial X3 − 2 does not split over 𝒬(23) \mathcal{Q}\left( {\root 3 \of 2 } \right) . Because X3 − 2 obviously has a root over 𝒬(23) \mathcal{Q}\left( {\root 3 \of 2 } \right) this shows that the field extension 𝒬(23) \mathcal{Q}\left( {\root 3 \of 2 } \right) is not normal over Q [3], [4], [5] and [7].

Keywords

  • splitting fields
  • rational polynomials

MSC

  • 12F05
  • 68V20
Open Access

Absolutely Integrable Functions

Published Online: 21 Dec 2022
Page range: 31 - 52

Abstract

Summary

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.

Keywords

  • absolutely integrable
  • improper integral

MSC

  • 26A42
  • 68V20
Open Access

Non-Trivial Universes and Sequences of Universes

Published Online: 21 Dec 2022
Page range: 53 - 66

Abstract

Summary

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].

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 (Chapitre 0 Univers et Appendice “Univers” (par N. Bourbaki) de l’Exposé I. “PREFAISCE-AUX”) [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.

Although a universe may be empty, we consider the properties of non-empty universes, completing the properties proved in [25].

We introduce the notion of “trivial” and “non-trivial” Universes, depending on whether or not they contain the set ω (NAT), following the notion of Robert M. Solovay2. The following result links the universes U0 (FinSETS) and U1 (SETS): GrothendieckUniverseω=GrothendieckUniverseU0=U1 {\rm{Grothendieck}}\,{\rm{Universe}}\,\omega = {\rm{Grothendieck}}\,{\rm{Universe}}\,{{\bf{U}}_0} = {{\bf{U}}_1} Before turning to the last section, we establish some trivial propositions allowing the construction of sets outside the considered universe.

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]).

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].

Keywords

  • Tarski-Grothendieck set theory
  • Grothendieck universe
  • universe hierarchy

MSC

  • 03E70
  • 68V20
Open Access

Isomorphism between Spaces of Multilinear Maps and Nested Compositions over Real Normed Vector Spaces

Published Online: 21 Dec 2022
Page range: 67 - 77

Abstract

Summary

This paper formalizes in Mizar [1], [2], that the isometric isomorphisms between spaces formed by an (n + 1)-dimensional multilinear map and an n-fold composition of linear maps on real normed spaces. This result is used to describe the space of nth-order derivatives of the Frechet derivative as a multilinear space. In Section 1, we discuss the spaces of 1-dimensional multilinear maps and 0-fold compositions as a preparation, and in Section 2, we extend the discussion to the spaces of (n + 1)-dimensional multilinear map and an n-fold compositions. We referred to [4], [11], [8], [9] in this formalization.

Keywords

  • Banach space
  • composition function
  • multilinear function

MSC

  • 15A69
  • 47A07
  • 68V20

Plan your remote conference with Sciendo