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

#### Search

Open Access

#### Automatization of Ternary Boolean Algebras

Page range: 153 - 159

#### Abstract

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.

#### Keywords

- ternary Boolean algebra
- single axiom system
- lattice

#### MSC

- 68V20
- 06B05
- 06B75

Open Access

#### Duality Notions in Real Projective Plane

Page range: 161 - 173

#### Abstract

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 [...]^{2}”).

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

#### Keywords

- Principle of Duality
- duality
- real projective plane
- converse theorem

#### MSC

- 51A05
- 51N15
- 68V20

Open Access

#### Finite Dimensional Real Normed Spaces are Proper Metric Spaces

Page range: 175 - 184

#### Abstract

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.

#### Keywords

- real vector space
- topological space
- normed spaces
- L1-norm
- maximum norm
- linear isometry
- proper metric space

#### MSC

- 15A04
- 40A05
- 46A50
- 68V20

Open Access

#### Relationship between the Riemann and Lebesgue Integrals

Page range: 185 - 199

#### Abstract

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.

#### Keywords

- Riemann integrals
- Lebesgue integrals

#### MSC

- 26A42
- 68V20

#### Abstract

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.

#### Keywords

- Improper integrals

#### MSC

- 26A42
- 68V20

#### Abstract

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 (^{2}+((^{2}+(2 · ^{3}·(2·^{2}+1−^{2})^{2}+ (^{2} + (^{3} · (^{2} + 1 − ^{2})^{2} + (^{2} − (^{2} −′ 1) · ^{2} − 1)^{2} + (16 · (^{2} − 1) · ^{2} · ^{2} · ^{2} + 1 − ^{2})^{2} + (((^{2} · (^{2} − ^{2} − 1) · (^{2} + 1 − (^{2})^{2} + (^{2} − (^{2} −′ 1) · ^{2} − 1)^{2} + (^{2} + (^{2} + (^{2} − 1) − ^{2} + (^{2} − 1) − ^{2} + (^{2} − 1) − ^{2} and we prove that that for any positive integer

#### Keywords

- prime number
- polynomial reduction
- diophantine equation

#### MSC

- 11D45
- 68V20

#### Abstract

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

#### Keywords

- field extensions
- quadratic polynomials
- quadratic extensions

#### MSC

- 12F05
- 68V20

Open Access

#### The 3-Fold Product Space of Real Normed Spaces and its Properties

Page range: 241 - 248

#### Abstract

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.

#### Keywords

- 3-fold product spaces
- linear spaces
- normed spaces

#### MSC

- 46B15
- 46B20
- 68V20

#### Abstract

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

#### Keywords

- graph union
- graph sum

#### MSC

- 05C76
- 68V20

#### Abstract

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.

#### Keywords

- improper integral

#### MSC

- 26A42
- 68V20