Volume 25 (2017): Issue 4 (December 2017)

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 [4]. In the second part of the article we define absolute values and the square root function [5].

We start proceeding with the stopping time theory in discrete time with the help of the Mizar system [1], [4]. We prove, that the expression for two stopping times k1 and k2 not always implies a stopping time (k₁ + k₂) (see Theorem 6 in this paper). If you want to get a stopping time, you have to cut the function e.g. (k₁ + k₂) ⋂ 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 τ₁ and τ₂ are stopping times with τ₁ is smaller or equal than τ₂ we can prove, that the σ-algebra of the τ₁-past is a subset of the σ-algebra of the τ₂-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 [5] 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 τ₁ and τ₂ are stopping times with τ₁ is smaller or equal than τ₂ we have the σ-algebra of the τ₁-past is a subset of the σ-algebra of the τ₂-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].

In this article, we formalize in Mizar [1], [3] 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 [7], [8], and [2] in this formalization.

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

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

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.