<abstract xmlns="http://www.w3.org/1999/xhtml">Formalization of a part of <xref ref-type="bibr" rid="j_forma-2016-0008_ref_011_w2aab2b8c11b1b7b1ab1ac11Aa">[11]</xref>. Unfortunately, not all is possible to be formalized. Namely, in the paper there is a mistake in the proof of Lemma 3. It states that there exists <italic>x</italic> ∈ <italic>M</italic>1 such that <italic>M</italic>1(<italic>x</italic>) > <italic>N</italic>1(<italic>x</italic>) and (∀<italic>y</italic> ∈ <italic>N</italic>1)<italic>x</italic> ⊀ <italic>y</italic>. It should be <italic>M</italic>1(<italic>x</italic>) ⩾ <italic>N</italic>1(<italic>x</italic>). Nevertheless we do not know whether <italic>x</italic> ∈ <italic>N</italic>1 or not and cannot prove the contradiction. In the article we referred to <xref ref-type="bibr" rid="j_forma-2016-0008_ref_008_w2aab2b8c11b1b7b1ab1ab8Aa">[8]</xref>, <xref ref-type="bibr" rid="j_forma-2016-0008_ref_009_w2aab2b8c11b1b7b1ab1ab9Aa">[9]</xref> and <xref ref-type="bibr" rid="j_forma-2016-0008_ref_010_w2aab2b8c11b1b7b1ab1ac10Aa">[10]</xref>.</abstract>

On Multiset Ordering

<abstract xmlns="http://www.w3.org/1999/xhtml">We formalize, in two different ways, that “the <italic>n</italic>-dimensional Euclidean metric space is a complete metric space” (version 1. with the results obtained in <xref ref-type="bibr" rid="j_forma-2016-0009_ref_013_w2aab2b8b5b1b7b1ab1ac13Aa">[13]</xref>, <xref ref-type="bibr" rid="j_forma-2016-0009_ref_026_w2aab2b8b5b1b7b1ab1ac26Aa">[26]</xref>, <xref ref-type="bibr" rid="j_forma-2016-0009_ref_025_w2aab2b8b5b1b7b1ab1ac25Aa">[25]</xref> and version 2., the results obtained in <xref ref-type="bibr" rid="j_forma-2016-0009_ref_013_w2aab2b8b5b1b7b1ab1ac13Aa">[13]</xref>, <xref ref-type="bibr" rid="j_forma-2016-0009_ref_014_w2aab2b8b5b1b7b1ab1ac14Aa">[14]</xref>, (<italic>registrations</italic>) <xref ref-type="bibr" rid="j_forma-2016-0009_ref_024_w2aab2b8b5b1b7b1ab1ac24Aa">[24]</xref>).With the Cantor’s theorem - in complete metric space (proof by Karol Pąk in <xref ref-type="bibr" rid="j_forma-2016-0009_ref_022_w2aab2b8b5b1b7b1ab1ac22Aa">[22]</xref>), we formalize “The Nested Intervals Theorem in 1-dimensional Euclidean metric space”.Pierre Cousin’s proof in 1892 <xref ref-type="bibr" rid="j_forma-2016-0009_ref_018_w2aab2b8b5b1b7b1ab1ac18Aa">[18]</xref> the lemma, published in 1895 <xref ref-type="bibr" rid="j_forma-2016-0009_ref_009_w2aab2b8b5b1b7b1ab1ab9Aa">[9]</xref> states that:
<disp-quote>“Soit, sur le plan YOX, une aire connexe <italic>S</italic> limitée par un contour fermé simple ou complexe; on suppose qu’à chaque point de <italic>S</italic> ou de son périmètre correspond un cercle, de rayon non nul, ayant ce point pour centre : il est alors toujours possible de subdiviser <italic>S</italic> en régions, en nombre fini et assez petites pour que chacune d’elles soit complétement intérieure au cercle correspondant à un point convenablement choisi dans <italic>S</italic> ou sur son périmètre.”</disp-quote>
(In the plane YOX let <italic>S</italic> be a connected area bounded by a closed contour, simple or complex; one supposes that at each point of <italic>S</italic> or its perimeter there is a circle, of non-zero radius, having this point as its centre; it is then always possible to subdivide <italic>S</italic> into regions, finite in number and sufficiently small for each one of them to be entirely inside a circle corresponding to a suitably chosen point in <italic>S</italic> or on its perimeter) <xref ref-type="bibr" rid="j_forma-2016-0009_ref_023_w2aab2b8b5b1b7b1ab1ac23Aa">[23]</xref>.Cousin’s Lemma, used in Henstock and Kurzweil integral <xref ref-type="bibr" rid="j_forma-2016-0009_ref_029_w2aab2b8b5b1b7b1ab1ac29Aa">[29]</xref> (generalized Riemann integral), state that: “for any gauge <italic>δ</italic>, there exists at least one <italic>δ</italic>-fine tagged partition”. In the last section, we formalize this theorem. We use the suggestions given to the Cousin’s Theorem p.11 in <xref ref-type="bibr" rid="j_forma-2016-0009_ref_005_w2aab2b8b5b1b7b1ab1ab5Aa">[5]</xref> and with notations: <xref ref-type="bibr" rid="j_forma-2016-0009_ref_004_w2aab2b8b5b1b7b1ab1ab4Aa">[4]</xref>, <xref ref-type="bibr" rid="j_forma-2016-0009_ref_029_w2aab2b8b5b1b7b1ab1ac29Aa">[29]</xref>, <xref ref-type="bibr" rid="j_forma-2016-0009_ref_019_w2aab2b8b5b1b7b1ab1ac19Aa">[19]</xref>, <xref ref-type="bibr" rid="j_forma-2016-0009_ref_028_w2aab2b8b5b1b7b1ab1ac28Aa">[28]</xref> and <xref ref-type="bibr" rid="j_forma-2016-0009_ref_012_w2aab2b8b5b1b7b1ab1ac12Aa">[12]</xref>.</abstract>

Cousin’s Lemma

<abstract xmlns="http://www.w3.org/1999/xhtml">In <xref ref-type="bibr" rid="j_forma-2016-0010_ref_021_w2aab2b8b7b1b7b1ab1ac21Aa">[21]</xref>, Marco Riccardi formalized that ℝN-basis <italic>n</italic> is a basis (in the algebraic sense defined in <xref ref-type="bibr" rid="j_forma-2016-0010_ref_026_w2aab2b8b7b1b7b1ab1ac26Aa">[26]</xref>) of <inline-formula><alternatives><inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2016-0010_eq_001.png"></inline-graphic><math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"><mrow><msubsup><mi>ℰ</mi><mi>T</mi><mi>n</mi></msubsup></mrow></math><tex-math>${\cal E}_T^n $</tex-math></alternatives></inline-formula> and in <xref ref-type="bibr" rid="j_forma-2016-0010_ref_020_w2aab2b8b7b1b7b1ab1ac20Aa">[20]</xref> he has formalized that <inline-formula><alternatives><inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2016-0010_eq_001.png"></inline-graphic><math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"><mrow><msubsup><mi>ℰ</mi><mi>T</mi><mi>n</mi></msubsup></mrow></math><tex-math>${\cal E}_T^n $</tex-math></alternatives></inline-formula> is second-countable, we build (in the topological sense defined in <xref ref-type="bibr" rid="j_forma-2016-0010_ref_023_w2aab2b8b7b1b7b1ab1ac23Aa">[23]</xref>) a denumerable base of <inline-formula><alternatives><inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2016-0010_eq_001.png"></inline-graphic><math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"><mrow><msubsup><mi>ℰ</mi><mi>T</mi><mi>n</mi></msubsup></mrow></math><tex-math>${\cal E}_T^n $</tex-math></alternatives></inline-formula>.Then we introduce the <italic>n</italic>-dimensional intervals (interval in <italic>n</italic>-dimensional Euclidean space, <italic>pavé (borné) de</italic> ℝ<italic>n</italic><xref ref-type="bibr" rid="j_forma-2016-0010_ref_016_w2aab2b8b7b1b7b1ab1ac16Aa">[16]</xref>, <italic>semi-intervalle (borné) de</italic> ℝ<italic>n</italic><xref ref-type="bibr" rid="j_forma-2016-0010_ref_022_w2aab2b8b7b1b7b1ab1ac22Aa">[22]</xref>).We conclude with the definition of Chebyshev distance <xref ref-type="bibr" rid="j_forma-2016-0010_ref_011_w2aab2b8b7b1b7b1ab1ac11Aa">[11]</xref>.</abstract>

Chebyshev Distance

<abstract xmlns="http://www.w3.org/1999/xhtml">Rough sets, developed by Zdzisław Pawlak <xref ref-type="bibr" rid="j_forma-2016-0011_ref_012_w2aab2b8b3b1b7b1ab1ac12Aa">[12]</xref>, are an important tool to describe the state of incomplete or partially unknown information. In this article, which is essentially the continuation of <xref ref-type="bibr" rid="j_forma-2016-0011_ref_008_w2aab2b8b3b1b7b1ab1ab8Aa">[8]</xref>, we try to give the characterization of approximation operators in terms of ordinary properties of underlying relations (some of them, as serial and mediate relations, were not available in the Mizar Mathematical Library <xref ref-type="bibr" rid="j_forma-2016-0011_ref_011_w2aab2b8b3b1b7b1ab1ac11Aa">[11]</xref>). Here we drop the classical equivalence- and tolerance-based models of rough sets trying to formalize some parts of <xref ref-type="bibr" rid="j_forma-2016-0011_ref_018_w2aab2b8b3b1b7b1ab1ac18Aa">[18]</xref>.The main aim of this Mizar article is to provide a formal counterpart for the rest of the paper of William Zhu <xref ref-type="bibr" rid="j_forma-2016-0011_ref_018_w2aab2b8b3b1b7b1ab1ac18Aa">[18]</xref>. In order to do this, we recall also Theorem 3 from Y.Y. Yao’s paper <xref ref-type="bibr" rid="j_forma-2016-0011_ref_017_w2aab2b8b3b1b7b1ab1ac17Aa">[17]</xref>. The first part of our formalization (covering first seven pages) is contained in <xref ref-type="bibr" rid="j_forma-2016-0011_ref_008_w2aab2b8b3b1b7b1ab1ab8Aa">[8]</xref>. Now we start from page 5003, sec. 3.4. <xref ref-type="bibr" rid="j_forma-2016-0011_ref_018_w2aab2b8b3b1b7b1ab1ac18Aa">[18]</xref>. We formalized almost all numbered items (definitions, propositions, theorems, and corollaries), with the exception of Proposition 7, where we stated our theorem only in terms of singletons. We provided more thorough discussion of the property <italic>positive alliance</italic> and its connection with seriality and reflexivity (and also transitivity). Examples were not covered as a rule as we tried to construct a more general mechanism of finding appropriate models for approximation spaces in Mizar providing more automatization than it is now <xref ref-type="bibr" rid="j_forma-2016-0011_ref_010_w2aab2b8b3b1b7b1ab1ac10Aa">[10]</xref>.Of course, we can see some more general applications of some registrations of clusters, essentially not dealing with the notion of an approximation: the notions of an alliance binary relation were not defined in the Mizar Mathematical Library before, and we should think about other properties which are also absent but needed in the context of rough approximations <xref ref-type="bibr" rid="j_forma-2016-0011_ref_009_w2aab2b8b3b1b7b1ab1ab9Aa">[9]</xref>, <xref ref-type="bibr" rid="j_forma-2016-0011_ref_005_w2aab2b8b3b1b7b1ab1ab5Aa">[5]</xref>. Via theory merging, using mechanisms described in <xref ref-type="bibr" rid="j_forma-2016-0011_ref_006_w2aab2b8b3b1b7b1ab1ab6Aa">[6]</xref> and <xref ref-type="bibr" rid="j_forma-2016-0011_ref_007_w2aab2b8b3b1b7b1ab1ab7Aa">[7]</xref>, such elementary constructions can be extended to other frameworks.</abstract>

Binary Relations-based Rough Sets – an Automated Approach

<abstract xmlns="http://www.w3.org/1999/xhtml">In our earlier article <xref ref-type="bibr" rid="j_forma-2016-0012_ref_012_w2aab2b8b1b1b7b1ab1ac12Aa">[12]</xref>, the first part of axioms of geometry proposed by Alfred Tarski <xref ref-type="bibr" rid="j_forma-2016-0012_ref_014_w2aab2b8b1b1b7b1ab1ac14Aa">[14]</xref> was formally introduced by means of Mizar proof assistant <xref ref-type="bibr" rid="j_forma-2016-0012_ref_009_w2aab2b8b1b1b7b1ab1ab9Aa">[9]</xref>. We defined a structure <monospace>TarskiPlane</monospace> with the following predicates:
<list list-type="bullet"><list-item>of betweenness <monospace>between</monospace> (a ternary relation),</list-item><list-item>of congruence of segments <monospace>equiv</monospace> (quarternary relation),</list-item></list>
which satisfy the following properties:
<list list-type="bullet"><list-item>congruence symmetry (A1),</list-item><list-item>congruence equivalence relation (A2),</list-item><list-item>congruence identity (A3),</list-item><list-item>segment construction (A4),</list-item><list-item>SAS (A5),</list-item><list-item>betweenness identity (A6),</list-item><list-item>Pasch (A7).</list-item></list>
Also a simple model, which satisfies these axioms, was previously constructed, and described in <xref ref-type="bibr" rid="j_forma-2016-0012_ref_006_w2aab2b8b1b1b7b1ab1ab6Aa">[6]</xref>. In this paper, we deal with four remaining axioms, namely:
<list list-type="bullet"><list-item>the lower dimension axiom (A8),</list-item><list-item>the upper dimension axiom (A9),</list-item><list-item>the Euclid axiom (A10),</list-item><list-item>the continuity axiom (A11).</list-item></list>
They were introduced in the form of Mizar attributes. Additionally, the relation of congruence of triangles <monospace>cong</monospace> is introduced via congruence of sides (SSS).In order to show that the structure which satisfies all eleven Tarski’s axioms really exists, we provided a proof of the registration of a cluster that the Euclidean plane, or rather a natural <xref ref-type="bibr" rid="j_forma-2016-0012_ref_005_w2aab2b8b1b1b7b1ab1ab5Aa">[5]</xref> extension of ordinary metric structure <monospace>Euclid 2</monospace> satisfies all these attributes.Although the tradition of the mechanization of Tarski’s geometry in Mizar is not as long as in Coq <xref ref-type="bibr" rid="j_forma-2016-0012_ref_011_w2aab2b8b1b1b7b1ab1ac11Aa">[11]</xref>, first approaches to this topic were done in Mizar in 1990 <xref ref-type="bibr" rid="j_forma-2016-0012_ref_016_w2aab2b8b1b1b7b1ab1ac16Aa">[16]</xref> (even if this article started formal Hilbert axiomatization of geometry, and parallel development was rather unlikely at that time <xref ref-type="bibr" rid="j_forma-2016-0012_ref_008_w2aab2b8b1b1b7b1ab1ab8Aa">[8]</xref>). Connection with another proof assistant should be mentioned – we had some doubts about the proof of the Euclid’s axiom and inspection of the proof taken from Archive of Formal Proofs of Isabelle <xref ref-type="bibr" rid="j_forma-2016-0012_ref_010_w2aab2b8b1b1b7b1ab1ac10Aa">[10]</xref> clarified things a bit. Our development allows for the future faithful mechanization of <xref ref-type="bibr" rid="j_forma-2016-0012_ref_013_w2aab2b8b1b1b7b1ab1ac13Aa">[13]</xref> and opens the possibility of automatically generated Prover9 proofs which was useful in the case of lattice theory <xref ref-type="bibr" rid="j_forma-2016-0012_ref_007_w2aab2b8b1b1b7b1ab1ab7Aa">[7]</xref>.</abstract>

Rue de la Brasserie 5, 7100 La Louvière,

Institute of Informatics, University of Białystok, Ciołkowskiego 1M, 15-245 Białystok,

Tarski Geometry Axioms – Part II

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 (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 (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 (June 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." 