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

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

0 Articles
Open Access

#### Vieta’s Formula about the Sum of Roots of Polynomials

Published Online: 23 Sep 2017
Page range: 87 - 92

#### Abstract

In the article we formalized in the Mizar system [2] the Vieta formula about the sum of roots of a polynomial anxn + an−1xn−1 + ··· + a1x + a0 defined over an algebraically closed field. The formula says that x1+x2++xn1+xn=an1an$x_1 + x_2 + \cdots + x_{n - 1} + x_n = - {{a_{n - 1} } \over {a_n }}$ , where x1, x2,…, xn are (not necessarily distinct) roots of the polynomial [12]. In the article the sum is denoted by SumRoots.

#### Keywords

• roots of polynomials
• Vieta’s formula

• 12E05
• 03B35
Open Access

#### Basic Formal Properties of Triangular Norms and Conorms

Published Online: 23 Sep 2017
Page range: 93 - 100

#### Abstract

In the article we present in the Mizar system [1], [8] the catalogue of triangular norms and conorms, used especially in the theory of fuzzy sets [13]. The name triangular emphasizes the fact that in the framework of probabilistic metric spaces they generalize triangle inequality [2].

After defining corresponding Mizar mode using four attributes, we introduced the following t-norms:

minimum t-norm minnorm (Def. 6),

product t-norm prodnorm (Def. 8),

Łukasiewicz t-norm Lukasiewicz_norm (Def. 10),

drastic t-norm drastic_norm (Def. 11),

nilpotent minimum nilmin_norm (Def. 12),

Hamacher product Hamacher_norm (Def. 13),

and corresponding t-conorms:

maximum t-conorm maxnorm (Def. 7),

probabilistic sum probsum_conorm (Def. 9),

bounded sum BoundedSum_conorm (Def. 19),

drastic t-conorm drastic_conorm (Def. 14),

nilpotent maximum nilmax_conorm (Def. 18),

Hamacher t-conorm Hamacher_conorm (Def. 17).

Their basic properties and duality are shown; we also proved the predicate of the ordering of norms [10], [9]. It was proven formally that drastic-norm is the pointwise smallest t-norm and minnorm is the pointwise largest t-norm (maxnorm is the pointwise smallest t-conorm and drastic-conorm is the pointwise largest t-conorm).

This work is a continuation of the development of fuzzy sets in Mizar [6] started in [11] and [3]; it could be used to give a variety of more general operations on fuzzy sets. Our formalization is much closer to the set theory used within the Mizar Mathematical Library than the development of rough sets [4], the approach which was chosen allows however for merging both theories [5], [7].

#### Keywords

• fuzzy set
• triangular norm
• triangular conorm
• fuzzy logic

• 03E72
• 94D05
• 03B35
Open Access

#### Introduction to Stopping Time in Stochastic Finance Theory

Published Online: 23 Sep 2017
Page range: 101 - 105

#### Abstract

We start with the definition of stopping time according to [4], p.283. We prove, that different definitions for stopping time can coincide. We give examples of stopping time using constant-functions or functions defined with the operator max or min (defined in [6], pp.37–38). Finally we give an example with some given filtration. Stopping time is very important for stochastic finance. A stopping time is the moment, where a certain event occurs ([7], p.372) and can be used together with stochastic processes ([4], p.283). Look at the following example: we install a function ST: {1,2,3,4} → {0, 1, 2} ∪ {+∞}, we define:

a. ST(1)=1, ST(2)=1, ST(3)=2, ST(4)=2.

b. The set {0,1,2} consists of time points: 0=now,1=tomorrow,2=the day after tomorrow.

We can prove:

c. {w, where w is Element of Ω: ST.w=0}=∅ & {w, where w is Element of Ω: ST.w=1}={1,2} & {w, where w is Element of Ω: ST.w=2}={3,4} and

ST is a stopping time.

We use a function Filt as Filtration of {0,1,2}, Σ where Filt(0)=Ωnow, Filt(1)=Ωfut1 and Filt(2)=Ωfut2. From a., b. and c. we know that:

d. {w, where w is Element of Ω: ST.w=0} in Ωnow and

{w, where w is Element of Ω: ST.w=1} in Ωfut1 and

{w, where w is Element of Ω: ST.w=2} in Ωfut2.

The sets in d. are events, which occur at the time points 0(=now), 1(=tomorrow) or 2(=the day after tomorrow), see also [7], p.371. Suppose we have ST(1)=+∞, then this means that for 1 the corresponding event never occurs.

As an interpretation for our installed functions consider the given adapted stochastic process in the article [5].

ST(1)=1 means, that the given element 1 in {1,2,3,4} is stopped in 1 (=tomorrow). That tells us, that we have to look at the value f2(1) which is equal to 80. The same argumentation can be applied for the element 2 in {1,2,3,4}.

ST(3)=2 means, that the given element 3 in {1,2,3,4} is stopped in 2 (=the day after tomorrow). That tells us, that we have to look at the value f3(3) which is equal to 100.

ST(4)=2 means, that the given element 4 in {1,2,3,4} is stopped in 2 (=the day after tomorrow). That tells us, that we have to look at the value f3(4) which is equal to 120.

In the real world, these functions can be used for questions like: when does the share price exceed a certain limit? (see [7], p.372).

#### Keywords

• stopping time
• stochastic process

• 60G40
• 03B35
Open Access

#### Pascal’s Theorem in Real Projective Plane

Published Online: 23 Sep 2017
Page range: 107 - 119

#### Abstract

In this article we check, with the Mizar system [2], Pascal’s theorem in the real projective plane (in projective geometry Pascal’s theorem is also known as the Hexagrammum Mysticum Theorem)1. Pappus’ theorem is a special case of a degenerate conic of two lines.

For proving Pascal’s theorem, we use the techniques developed in the section “Projective Proofs of Pappus’ Theorem” in the chapter “Pappus’ Theorem: Nine proofs and three variations” [11]. We also follow some ideas from Harrison’s work. With HOL Light, he has the proof of Pascal’s theorem2. For a lemma, we use PROVER93 and OTT2MIZ by Josef Urban4 [12, 6, 7]. We note, that we don’t use Skolem/Herbrand functions (see “Skolemization” in [1]).

#### Keywords

• Pascal’s theorem
• real projective plane
• Grassman-Plücker relation

• 51E15
• 51N15
• 03B35
Open Access

#### About Quotient Orders and Ordering Sequences

Published Online: 23 Sep 2017
Page range: 121 - 139

#### Abstract

In preparation for the formalization in Mizar [4] of lotteries as given in [14], this article closes some gaps in the Mizar Mathematical Library (MML) regarding relational structures. The quotient order is introduced by the equivalence relation identifying two elements x, y of a preorder as equivalent if xy and yx. This concept is known (see e.g. chapter 5 of [19]) and was first introduced into the MML in [13] and that work is incorporated here. Furthermore given a set A, partition D of A and a finite-support function f : A → ℝ, a function Σf : D → ℝ, Σf (X)= ∑xXf(x) can be defined as some kind of natural “restriction” from f to D. The first main result of this article can then be formulated as: xAf(x)=XDΣf(X)(=XDxXf(x))$$\sum\limits_{x \in A} {f(x)} = \sum\limits_{X \in D} {\Sigma _f (X)\left( { = \sum\limits_{X \in D} {\sum\limits_{x \in X} {f(x)} } } \right)}$$

After that (weakly) ascending/descending finite sequences (based on [3]) are introduced, in analogous notation to their infinite counterparts introduced in [18] and [13].

The second main result is that any finite subset of any transitive connected relational structure can be sorted as a ascending or descending finite sequence, thus generalizing the results from [16], where finite sequence of real numbers were sorted.

The third main result of the article is that any weakly ascending/weakly descending finite sequence on elements of a preorder induces a weakly ascending/weakly descending finite sequence on the projection of these elements into the quotient order. Furthermore, weakly ascending finite sequences can be interpreted as directed walks in a directed graph, when the set of edges is described by ordered pairs of vertices, which is quite common (see e.g. [10]).

Additionally, some auxiliary theorems are provided, e.g. two schemes to find the smallest or the largest element in a finite subset of a connected transitive relational structure with a given property and a lemma I found rather useful: Given two finite one-to-one sequences s, t on a set X, such that rng t ⊆ rng s, and a function f : X → ℝ such that f is zero for every x ∈ rng s \ rng t, we have ∑ f o s = ∑ f o t.

#### Keywords

• quotient order
• ordered finite sequences

• 06A05
• 03B35
Open Access

#### Basel Problem – Preliminaries

Published Online: 23 Sep 2017
Page range: 141 - 147

#### Abstract

In the article we formalize in the Mizar system [4] preliminary facts needed to prove the Basel problem [7, 1]. Facts that are independent from the notion of structure are included here.

#### Keywords

• Basel problem

• 11M06
• 03B35
Open Access

#### Basel Problem

Published Online: 23 Sep 2017
Page range: 149 - 155

#### Abstract

A rigorous elementary proof of the Basel problem [6, 1] n=11n2=π26$$\sum\nolimits_{n = 1}^\infty {{1 \over {n^2 }} = {{\pi ^2 } \over 6}}$$ is formalized in the Mizar system [3]. This theorem is item #14 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.

#### Keywords

• Basel problem

• 11M06
• 03B35
Open Access

#### Dual Lattice of ℤ-module Lattice

Published Online: 23 Sep 2017
Page range: 157 - 169

#### Abstract

In this article, we formalize in Mizar [5] the definition of dual lattice and their properties. We formally prove that a set of all dual vectors in a rational lattice has the construction of a lattice. We show that a dual basis can be calculated by elements of an inverse of the Gram Matrix. We also formalize a summation of inner products and their properties. Lattice of ℤ-module is necessary for lattice problems, LLL(Lenstra, Lenstra and Lovász) base reduction algorithm and cryptographic systems with lattice [20], [10] and [19].

#### Keywords

• ℤ-lattice
• dual lattice of ℤ-lattice
• dual basis of ℤ-lattice

• 15A03
• 15A09
• 03B35