<abstract xmlns="http://www.w3.org/1999/xhtml">

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

Department of Medical Molecular Informatics

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

<abstract xmlns="http://www.w3.org/1999/xhtml">

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

Compactness of Neural Networks

<abstract xmlns="http://www.w3.org/1999/xhtml">

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 <italic>X</italic>2 − 2, <italic>X</italic>3 − 1, <italic>X</italic>2 + <italic>X</italic> + 1 and <italic>X</italic>3 − 2 over <italic>Q</italic> 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 <italic>X</italic>3 − 2 does not split over <inline-formula>
<alternatives>
<inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2022-0003_eq_001.png"></inline-graphic>
<math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"><mrow><mi>𝒬</mi><mrow><mo>(</mo><mrow><mroot><mn>2</mn><mn>3</mn></mroot></mrow><mo>)</mo></mrow></mrow></math>
<tex-math>\mathcal{Q}\left( {\root 3 \of 2 } \right)</tex-math>
</alternatives>
</inline-formula>. Because <italic>X</italic>3 − 2 obviously has a root over <inline-formula>
<alternatives>
<inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2022-0003_eq_002.png"></inline-graphic>
<math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"><mrow><mi>𝒬</mi><mrow><mo>(</mo><mrow><mroot><mn>2</mn><mn>3</mn></mroot></mrow><mo>)</mo></mrow></mrow></math>
<tex-math>\mathcal{Q}\left( {\root 3 \of 2 } \right)</tex-math>
</alternatives>
</inline-formula> this shows that the field extension <inline-formula>
<alternatives>
<inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2022-0003_eq_003.png"></inline-graphic>
<math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"><mrow><mi>𝒬</mi><mrow><mo>(</mo><mrow><mroot><mn>2</mn><mn>3</mn></mroot></mrow><mo>)</mo></mrow></mrow></math>
<tex-math>\mathcal{Q}\left( {\root 3 \of 2 } \right)</tex-math>
</alternatives>
</inline-formula> is not normal over <italic>Q</italic> [3], [4], [5] and [7].
</abstract>

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

<abstract xmlns="http://www.w3.org/1999/xhtml">

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.
</abstract>

Absolutely Integrable Functions

<abstract xmlns="http://www.w3.org/1999/xhtml">

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 (<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.
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 <italic>ω</italic> (NAT), following the notion of Robert M. Solovay2. The following result links the universes <bold>U</bold>0 (FinSETS) and <bold>U</bold>1 (SETS):
<disp-formula>
<alternatives>
<graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2022-0005_eq_001.png"></graphic>
<math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="block"><mrow><mtext>Grothendieck</mtext><mi> </mi><mtext>Universe</mtext><mi> </mi><mi>ω</mi><mo>=</mo><mtext>Grothendieck</mtext><mi> </mi><mtext>Universe</mtext><mi> </mi><msub><mrow><mstyle fontweight="bold" fontstyle="normal"><mi>U</mi></mstyle></mrow><mn>0</mn></msub><mo>=</mo><msub><mrow><mstyle fontweight="bold" fontstyle="normal"><mi>U</mi></mstyle></mrow><mn>1</mn></msub></mrow></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.
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].
</abstract>

Non-Trivial Universes and Sequences of Universes

<abstract xmlns="http://www.w3.org/1999/xhtml">

This paper formalizes in Mizar [1], [2], that the isometric isomorphisms between spaces formed by an (<italic>n</italic> + 1)-dimensional multilinear map and an <italic>n</italic>-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 (<italic>n</italic> + 1)-dimensional multilinear map and an <italic>n</italic>-fold compositions. We referred to [4], [11], [8], [9] in this formalization.
</abstract>

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

AHEAD OF PRINT

Volume 31 (2023): Issue 1 (September 2023)

Volume 30 (2022): Issue 4 (December 2022)

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 (December 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 (January 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 (January 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 (January 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 (January 2007)

Volume 15 (2007): Issue 1 (January 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)

Formalized Mathematics

  Pioneering Journal in the field of formalized and mechanically checked mathematics. Excellent articles on latest research in formal methods and computer-checked mathematics. Full-length original research articles in English. Archival issues available at the journal's home page fm.mizar.org/.   To build a uniform and extensible computer-checked repository of mathematical knowledge.  Reconstruction of mathematics based on mechanization of mathematical reasoning.  To check a wide range of mathematical theorems using a computer in an automatic fashion.  General mathematics: especially topology, lattice theory, functional analysis.  Applications: computer-aided verification of software and hardware, computer-aided teaching of mathematics.   Why subscribe and read   Pioneering source of high quality research in formalized and mechanically checked mathematics.  The oldest journal in the field, a medium for the publication of research reporting pioneering findings of broad mathematical significance that are likely to advance the direction and thinking of the field.  Long-term experience in publishing original articles on mechanizing mathematics and various aspects of automated reasoning, since 1990.   Why submit   Fair and constructive peer review by international experts in the field (three referees are designated for the assessment of each manuscript) - double-blind review process.  New publishing technology: articles automatically translated from a formal language into English and automatically typeset, available in both forms - electronic and printed.  Articles abstracted by online indexing services and databases.   Rejection Rate   59% of submitted articles.  The rejection percentage is described in detail in the following paper, pp.239-240: dx.doi.org/10.1007/978-3-540-73086-6_20 Archiving  Sciendo archives the contents of this journal in Portico - digital long-term preservation service of scholarly books, journals and collections.  Plagiarism Policy  The editorial board is participating in a growing community of Similarity Check System's users in order to ensure that the content published is original and trustworthy. Similarity Check is a medium that allows for comprehensive manuscripts screening, aimed to eliminate plagiarism and provide a high standard and quality peer-review process. Back Issues fm.mizar.org/   Other Files  Addenda 2008Formalized Mathematics Bibliography File.Formalized Mathematics External Bibliography File.  "In years: 2016-2017, the English version of Formalized Mathematics was financed under agreements 548/P-DUN/2016 and 548/1/P-DUN/2016 with the funds from the Polish Minister of Science and Higher Education for the dissemination of science." 