# Volume 25 (2017): Issue 4 (December 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

#### Formally Real Fields

Published Online: 28 Mar 2018
Page range: 249 - 259

#### Abstract

We extend the algebraic theory of ordered fields [7, 6] in Mizar [1, 2, 3]: we show that every preordering can be extended into an ordering, i.e. that formally real and ordered fields coincide.We further prove some characterizations of formally real fields, in particular the one by Artin and Schreier using sums of squares . In the second part of the article we define absolute values and the square root function .

#### Keywords

• formally real fields
• ordered fields
• abstract value
• square roots

• 12J15 03B35

#### MML

• identifier: REALALG2
• version: 8.1.06 5.45.1311
Open Access

#### Introduction to Stopping Time in Stochastic Finance Theory. Part II

Published Online: 28 Mar 2018
Page range: 261 - 268

#### Abstract

We start proceeding with the stopping time theory in discrete time with the help of the Mizar system , . We prove, that the expression for two stopping times k1 and k2 not always implies a stopping time (k1 + k2) (see Theorem 6 in this paper). If you want to get a stopping time, you have to cut the function e.g. (k1 + k2) ⋂ T (see [2, p. 283 Remark 6.14]). Next we introduce the stopping time in continuous time. We are focused on the intervals [0, r] where r ∈ ℝ. We prove, that for I = [0, r] or I = [0,+∞[ the set {A ⋂ I : A ∈ Borel-Sets} is a σ-algebra of I (see Definition 6 in this paper, and more general given in [3, p.12 1.8e]). The interval I can be considered as a timeline from now to some point in the future. This set is necessary to define our next lemma. We prove the existence of the σ-algebra of the τ -past, where τ is a stopping time (see Definition 11 in this paper and [6, p.187, Definition 9.19]). If τ1 and τ2 are stopping times with τ1 is smaller or equal than τ2 we can prove, that the σ-algebra of the τ1-past is a subset of the σ-algebra of the τ2-past (see Theorem 9 in this paper and [6, p.187 Lemma 9.21]). Suppose, that you want to use Lemma 9.21 with some events, that never occur, see as a comparison the paper  and the example for ST(1)={+∞} in the Summary. We don’t have the element +1 in our above-mentioned time intervals [0, r[ and [0,+1[. This is only possible if we construct a new σ-algebra on ℝ {−∞,+∞}. This construction is similar to the Borel-Sets and we call this σ-algebra extended Borel sets (see Definition 13 in this paper and [3, p. 21]). It can be proved, that {+∞} is an Element of extended Borel sets (see Theorem 21 in this paper). Now we use the interval [0,+∞] as a basis. We construct a σ-algebra on [0,+∞] similar to the book ([3, p. 12 18e]), see Definition 18 in this paper, and call it extended Borel subsets. We prove for stopping times with this given σ-algebra, that for τ1 and τ2 are stopping times with τ1 is smaller or equal than τ2 we have the σ-algebra of the τ1-past is a subset of the σ-algebra of the τ2-past, see Theorem 25 in this paper. It is obvious, that {+∞} 2 extended Borel subsets. In general, Lemma 9.21 is important for the proof of the Optional Sampling Theorem, see 10.11 Proof of (i) in [6, p. 203].

#### Keywords

• stopping time
• stochastic process

• 60G40 03B35

#### MML

• identifier: FINANCE5
• version: 8.1.06 5.45.1311
Open Access

#### Implicit Function Theorem. Part I

Published Online: 28 Mar 2018
Page range: 269 - 281

#### Abstract

In this article, we formalize in Mizar ,  the existence and uniqueness part of the implicit function theorem. In the first section, some composition properties of Lipschitz continuous linear function are discussed. In the second section, a definition of closed ball and theorems of several properties of open and closed sets in Banach space are described. In the last section, we formalized the existence and uniqueness of continuous implicit function in Banach space using Banach fixed point theorem. We referred to , , and  in this formalization.

#### Keywords

• implicit function theorem
• Banach fixed point theorem
• Lipschitz continuity

#### MSC 2010

• 26B10 53A07 03B35

#### MML

• identifier: NDIFF 8
• version: 8.1.06 5.45.1311
Open Access

#### Introduction to Diophantine Approximation. Part II

Published Online: 28 Mar 2018
Page range: 283 - 288

#### Abstract

In the article we present in the Mizar system ,  the formalized proofs for Hurwitz’ theorem [4, 1891] and Minkowski’s theorem . Both theorems are well explained as a basic result of the theory of Diophantine approximations appeared in , . A formal proof of Dirichlet’s theorem, namely an inequation |θ−y/x| ≤ 1/x2 has infinitely many integer solutions (x, y) where θ is an irrational number, was given in . A finer approximation is given by Hurwitz’ theorem: |θ− y/x|≤ 1/√5x2. Minkowski’s theorem concerns an inequation of a product of non-homogeneous binary linear forms such that |a1x + b1y + c1| · |a2x + b2y + c2| ≤ ∆/4 where ∆ = |a1b2 − a2b1| ≠ 0, has at least one integer solution.

#### Keywords

• Diophantine approximation
• rational approximation
• Dirichlet
• Hurwitz
• Minkowski

#### MSC 2010

• 11J20 11J25 03B35

#### MML

• identifier: DIOPHAN2
• version: 8.1.06 5.45.1311
Open Access

#### Tarski Geometry Axioms. Part III

Published Online: 28 Mar 2018
Page range: 289 - 313

#### Abstract

In the article, we continue the formalization of the work devoted to Tarski’s geometry - the book “Metamathematische Methoden in der Geometrie” by W. Schwabhäuser, W. Szmielew, and A. Tarski. After we prepared some introductory formal framework in our two previous Mizar articles, we focus on the regular translation of underlying items faithfully following the abovementioned book (our encoding covers first seven chapters). Our development utilizes also other formalization efforts of the same topic, e.g. Isabelle/HOL by Makarios, Metamath or even proof objects obtained directly from Prover9. In addition, using the native Mizar constructions (cluster registrations) the propositions (“Satz”) are reformulated under weaker conditions, i.e. by using fewer axioms or by proposing an alternative version that uses just another axioms (ex. Satz 2.1 or Satz 2.2).

#### Keywords

• Tarski’s geometry axioms
• foundations of geometry
• Euclidean plane

#### MSC 2010

• 51A05 51M04 03B35

#### MML

• identifier: GTARSKI3
• version: 8.1.06 5.45.1311
Open Access

#### The Matiyasevich Theorem. Preliminaries

Published Online: 28 Mar 2018
Page range: 315 - 322

#### Abstract

In this article, we prove selected properties of Pell’s equation that are essential to finally prove the Diophantine property of two equations. These equations are explored in the proof of Matiyasevich’s negative solution of Hilbert’s tenth problem.

#### Keywords

• Pell’s equation
• Diophantine equation
• Hilbert’s 10th problem

• 11D45 03B35

#### MML

• identifier: HILB10 1
• version: 8.1.06 5.45.1311