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

The main aim of this article is to introduce formally ternary Boolean algebras (TBAs) in terms of an abstract ternary operation, and to show their connection with the ordinary notion of a Boolean algebra, already present in the Mizar Mathematical Library [2]. Essentially, the core of this Mizar [1] formalization is based on the paper of A.A. Grau “Ternary Boolean Algebras” [7]. The main result is the single axiom for this class of lattices [12]. This is the continuation of the articles devoted to various equivalent axiomatizations of Boolean algebras: following Huntington [8] in terms of the binary sum and the complementation useful in the formalization of the Robbins problem [5], in terms of Sheffer stroke [9]. The classical definition ([6], [3]) can be found in [15] and its formalization is described in [4].

Similarly as in the case of recent formalizations of WA-lattices [14] and quasilattices [10], some of the results were proven in the Mizar system with the help of Prover9 [13], [11] proof assistant, so proofs are quite lengthy. They can be subject for subsequent revisions to make them more compact.

In this article, we check with the Mizar system [1], [2], the converse of Desargues’ theorem and the converse of Pappus’ theorem of the real projective plane. It is well known that in the projective plane, the notions of points and lines are dual [11], [9], [15], [8]. Some results (analytical, synthetic, combinatorial) of projective geometry are already present in some libraries Lean/Hott [5], Isabelle/Hol [3], Coq [13], [14], [4], Agda [6], . . . .

Proofs of dual statements by proof assistants have already been proposed, using an axiomatic method (for example see in [13] - the section on duality: “[...] For every theorem we prove, we can easily derive its dual using our function swap [...]²”).

In our formalisation, we use an analytical rather than a synthetic approach using the definitions of Leończuk and Prażmowski of the projective plane [12]. Our motivation is to show that it is possible by developing dual definitions to find proofs of dual theorems in a few lines of code.

In the first part, rather technical, we introduce definitions that allow us to construct the duality between the points of the real projective plane and the lines associated to this projective plane. In the second part, we give a natural definition of line concurrency and prove that this definition is dual to the definition of alignment. Finally, we apply these results to find, in a few lines, the dual properties and theorems of those defined in the article [12] (transitive, Vebleian, at_least_3rank, Fanoian, Desarguesian, 2-dimensional).

We hope that this methodology will allow us to continued more quickly the proof started in [7] that the Beltrami-Klein plane is a model satisfying the axioms of the hyperbolic plane (in the sense of Tarski geometry [10]).

In this article, we formalize in Mizar [1], [2] the topological properties of finite-dimensional real normed spaces. In the first section, we formalize the Bolzano-Weierstrass theorem, which states that a bounded sequence of points in an n-dimensional Euclidean space has a certain subsequence that converges to a point. As a corollary, it is also shown the equivalence between a subset of an n-dimensional Euclidean space being compact and being closed and bounded.

In the next section, we formalize the definitions of L1-norm (Manhattan Norm) and maximum norm and show their topological equivalence in n-dimensional Euclidean spaces and finite-dimensional real linear spaces. In the last section, we formalize the linear isometries and their topological properties. Namely, it is shown that a linear isometry between real normed spaces preserves properties such as continuity, the convergence of a sequence, openness, closeness, and compactness of subsets. Finally, it is shown that finite-dimensional real normed spaces are proper metric spaces. We referred to [5], [9], and [7] in the formalization.

The goal of this article is to clarify the relationship between Riemann and Lebesgue integrals. In previous article [5], we constructed a one-dimensional Lebesgue measure. The one-dimensional Lebesgue measure provides a measure of any intervals, which can be used to prove the well-known relationship [6] between the Riemann and Lebesgue integrals [1]. We also proved the relationship between the integral of a given measure and that of its complete measure. As the result of this work, the Lebesgue integral of a bounded real valued function in the Mizar system [2], [3] can be calculated by the Riemann integral.

In this article, we deal with Riemann’s improper integral [1], using the Mizar system [2], [3]. Improper integrals with finite values are discussed in [5] by Yamazaki et al., but in general, improper integrals do not assume that they are finite. Therefore, we have formalized general improper integrals that does not limit the integral value to a finite value. In addition, each theorem in [5] assumes that the domain of integrand includes a closed interval, but since the improper integral should be discusses based on the half-open interval, we also corrected it.

The main purpose of formalization is to prove that the set of prime numbers is diophantine, i.e., is representable by a polynomial formula. We formalize this problem, using the Mizar system [1], [2], in two independent ways, proving the existence of a polynomial without formulating it explicitly as well as with its indication.

First, we reuse nearly all the techniques invented to prove the MRDP-theorem [11]. Applying a trick with Mizar schemes that go beyond first-order logic we give a short sophisticated proof for the existence of such a polynomial but without formulating it explicitly. Then we formulate the polynomial proposed in [6] that has 26 variables in the Mizar language as follows (w·z+h+j−q)²+((g·k+g+k)·(h+j)+h−z)²+(2 · k³·(2·k+2)·(n + 1)²+1−f²)²+ (p + q + z + 2 · n − e)² + (e³ · (e + 2) · (a + 1)² + 1 − o²)² + (x² − (a² −′ 1) · y² − 1)² + (16 · (a² − 1) · r² · y² · y² + 1 − u²)² + (((a + u² · (u² − a))² − 1) · (n + 4 · d · y)² + 1 − (x + c · u)²)² + (m² − (a² −′ 1) · l² − 1)² + (k + i · (a − 1) − l)² + (n + l + v − y)² + (p + l · (a − n − 1) + b · (2 · a · (n + 1) − (n + 1)² − 1) − m)² + (q + y · (a − p − 1) + s · (2 · a · (p + 1) − (p + 1)² − 1) − x)² + (z + p · l · (a − p) + t · (2 · a · p − p² − 1) − p · m)² and we prove that that for any positive integer k so that k + 1 is prime it is necessary and sufficient that there exist other natural variables a-z for which the polynomial equals zero. 26 variables is not the best known result in relation to the set of prime numbers, since any diophantine equation over ℕ can be reduced to one in 13 unknowns [8] or even less [5], [13]. The best currently known result for all prime numbers, where the polynomial is explicitly constructed is 10 [7] or even 7 in the case of Fermat as well as Mersenne prime number [4]. We are currently focusing our formalization efforts in this direction.

In this article we further develop field theory [6], [7], [12] in Mizar [1], [2], [3]: we deal with quadratic polynomials and quadratic extensions [5], [4]. First we introduce quadratic polynomials, their discriminants and prove the midnight formula. Then we show that - in case the discriminant of p being non square - adjoining a root of p’s discriminant results in a splitting field of p. Finally we prove that these are the only field extensions of degree 2, e.g. that an extension E of F is quadratic if and only if there is a non square Element a ∈ F such that E and ( Fa F\sqrt a ) are isomorphic over F.

In this article, we formalize in Mizar [1], [2] the 3-fold product space of real normed spaces for usefulness in application fields such as engineering, although the formalization of the 2-fold product space of real normed spaces has been stored in the Mizar Mathematical Library [3].

First, we prove some theorems about the 3-variable function and 3-fold Cartesian product for preparation. Then we formalize the definition of 3-fold product space of real linear spaces. Finally, we formulate the definition of 3-fold product space of real normed spaces. We referred to [7] and [6] in the formalization.

In this article the sum (or disjoint union) of graphs is formalized in the Mizar system [4], [1], based on the formalization of graphs in [9].

In this article, using the Mizar system [2], [3], we deal with Riemann’s improper integral on infinite interval [1]. As with [4], we referred to [6], which discusses improper integrals of finite values.