http://hdl.handle.net/11320/6511 Mon, 01 Jun 2026 17:17:16 GMT 2026-06-01T17:17:16Z http://hdl.handle.net/11320/6555 Tytuł: The Matiyasevich Theorem. Preliminaries Autorzy: Pąk, Karol Abstrakt: 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. Sun, 01 Jan 2017 00:00:00 GMT http://hdl.handle.net/11320/6555 2017-01-01T00:00:00Z http://hdl.handle.net/11320/6554 Tytuł: Tarski Geometry Axioms. Part III Autorzy: Coghetto, Roland; Grabowski, Adam Abstrakt: 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). Sun, 01 Jan 2017 00:00:00 GMT http://hdl.handle.net/11320/6554 2017-01-01T00:00:00Z http://hdl.handle.net/11320/6551 Tytuł: Introduction to Stopping Time in Stochastic Finance Theory. Part II Autorzy: Jaeger, Peter Abstrakt: 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 (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 [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 τ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]. Sun, 01 Jan 2017 00:00:00 GMT http://hdl.handle.net/11320/6551 2017-01-01T00:00:00Z http://hdl.handle.net/11320/6552 Tytuł: Implicit Function Theorem. Part I Autorzy: Nakasho, Kazuhisa; Futa, Yuichi; Shidama, Yasunari Abstrakt: 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. Sun, 01 Jan 2017 00:00:00 GMT http://hdl.handle.net/11320/6552 2017-01-01T00:00:00Z