Volume 26 (2018): Issue 1 (April 2018)

Using the Mizar system [1], [5], we start to show, that the Call-Option, the Put-Option and the Straddle (more generally defined as in the literature) are random variables ([4], p. 15), see (Def. 1) and (Def. 2). Next we construct and prove the simple random variables ([2], p. 14) in (Def. 8).

In the third section, we introduce the definition of arbitrage opportunity, see (Def. 12). Next we show, that this definition can be characterized in a different way (Lemma 1.3. in [4], p. 5), see (17). In our formalization for Lemma 1.3 we make the assumption that ϕ is a sequence of real numbers (there are only finitely many valued of interest, the values of ϕ in R^d). For the definition of almost sure with probability 1 see p. 6 in [2]. Last we introduce the risk-neutral probability (Definition 1.4, p. 6 in [4]), here see (Def. 16).

We give an example in real world: Suppose you have some assets like bonds (riskless assets). Then we can fix our price for these bonds with x for today and x · (1 + r) for tomorrow, r is the interest rate. So we simply assume, that in every possible market evolution of tomorrow we have a determinated value. Then every probability measure of Ω_fut1 is a risk-neutral measure, see (21). This example shows the existence of some risk-neutral measure. If you find more than one of them, you can determine – with an additional conidition to the probability measures – whether a market model is arbitrage free or not (see Theorem 1.6. in [4], p. 6.)

A short graph for (21):

Suppose we have a portfolio with many (in this example infinitely many) assets. For asset d we have the price π(d) for today, and the price π(d) (1 + r) for tomorrow with some interest rate r > 0.

Let G be a sequence of random variables on Ω_fut1, Borel sets. So you have many functions f_k : {1, 2, 3, 4}→ R with G(k) = f_k and f_k is a random variable of Ω_fut1, Borel sets. For every f_k we have f_k(w) = π(k)·(1+r) for w {1, 2, 3, 4}.

TodayTomorrowonly one scenario{w21={1,2}w22={3,4}for all d∈𝕅 holds π(d){fd(w)=G(d)(w)=π(d)⋅(1+r),w∈w21 or w∈w22,r>0 is the interest rate.$$\matrix{ {Today} & {Tomorrow} \cr {{\rm{only}}\,{\rm{one}}\,{\rm{scenario}}} & {\left\{ {\matrix{ {w_{21} = \left\{ {1,2} \right\}} \hfill \cr {w_{22} = \left\{ {3,4} \right\}} \hfill \cr } } \right.} \cr {{\rm{for}}\,{\rm{all}}\,d \in N\,{\rm{holds}}\,\pi \left( d \right)} & {\left\{ {\matrix{ {f_d \left( w \right) = G\left( d \right)\left( w \right) = \pi \left( d \right) \cdot \left( {1 + r} \right),} \hfill \cr {w \in w_{21} \,or\,w \in w_{22} ,} \hfill \cr {r > 0\,{\rm{is}}\,{\rm{the}}\,{\rm{interest}}\,{\rm{rate}}.} \hfill \cr } } \right.} \cr }$$

Here, every probability measure of Ω_fut1 is a risk-neutral measure.

We show that the set of all partial predicates over a set D together with the disjunction, conjunction, and negation operations, defined in accordance with the truth tables of S.C. Kleene’s strong logic of indeterminacy [17], forms a Kleene algebra. A Kleene algebra is a De Morgan algebra [3] (also called quasi-Boolean algebra) which satisfies the condition x ∧¬:x ⩽ y ∨¬ :y (sometimes called the normality axiom). We use the formalization of De Morgan algebras from [8].

The term “Kleene algebra” was introduced by A. Monteiro and D. Brignole in [3]. A similar notion of a “normal i-lattice” had been previously studied by J.A. Kalman [16]. More details about the origin of this notion and its relation to other notions can be found in [24, 4, 1, 2]. It should be noted that there is a different widely known class of algebras, also called Kleene algebras [22, 6], which generalize the algebra of regular expressions, however, the term “Kleene algebra” used in this paper does not refer to them.

Algebras of partial predicates naturally arise in computability theory in the study on partial recursive predicates. They were studied in connection with non-classical logics [17, 5, 18, 32, 29, 30]. A partial predicate also corresponds to the notion of a partial set [26] on a given domain, which represents a (partial) property which for any given element of this domain may hold, not hold, or neither hold nor not hold. The field of all partial sets on a given domain is an algebra with generalized operations of union, intersection, complement, and three constants (0, 1, n which is the fixed point of complement) which can be generalized to an equational class of algebras called DMF-algebras (De Morgan algebras with a single fixed point of involution) [25]. In [27] partial sets and DMF-algebras were considered as a basis for unification of set-theoretic and linguistic approaches to probability.

Partial predicates over classes of mathematical models of data were used for formalizing semantics of computer programs in the composition-nominative approach to program formalization [31, 28, 33, 15], for formalizing extensions of the Floyd-Hoare logic [7, 9] which allow reasoning about properties of programs in the case of partial pre- and postconditions [23, 20, 19, 21], for formalizing dynamical models with partial behaviors in the context of the mathematical systems theory [11, 13, 14, 12, 10].

Tim Makarios (with Isabelle/HOL¹) and John Harrison (with HOL-Light²) shown that “the Klein-Beltrami model of the hyperbolic plane satisfy all of Tarski’s axioms except his Euclidean axiom” [3], [4], [14], [5].

With the Mizar system [2], [7] we use some ideas are taken from Tim Makarios’ MSc thesis [13] for the formalization of some definitions (like the absolute) and lemmas necessary for the verification of the independence of the parallel postulate. This work can be also treated as further development of Tarski’s geometry in the formal setting [6]. Note that the model presented here, may also be called “Beltrami-Klein Model”, “Klein disk model”, and the “Cayley-Klein model” [1].

Tim Makarios (with Isabelle/HOL¹) and John Harrison (with HOL-Light²) have shown that “the Klein-Beltrami model of the hyperbolic plane satisfy all of Tarski’s axioms except his Euclidean axiom” [2, 3, 15, 4].

With the Mizar system [1], [10] we use some ideas are taken from Tim Makarios’ MSc thesis [12] for formalized some definitions (like the tangent) and lemmas necessary for the verification of the independence of the parallel postulate. This work can be also treated as a further development of Tarski’s geometry in the formal setting [9].

The goal of this article is to show Fubini’s theorem for non-negative or non-positive measurable functions [10], [2], [3], using the Mizar system [1], [9]. We formalized Fubini’s theorem in our previous article [5], but in that case we showed the Fubini’s theorem for measurable sets and it was not enough as the integral does not appear explicitly.

On the other hand, the theorems obtained in this paper are more general and it can be easily extended to a general integrable function. Furthermore, it also can be easy to extend to functional space L^p [12]. It should be mentioned also that Hölzl and Heller [11] have introduced the Lebesgue integration theory in Isabelle/HOL and have proved Fubini’s theorem there.

In the article we formalize some properties needed to prove that sequences of prime reciprocals are divergent. The aim is to show that the series exhibits log-log growth. We introduce some auxiliary notions as harmonic numbers, telescoping series, and prove some standard properties of logarithms and exponents absent in the Mizar Mathematical Library. At the end we proceed with square-free and square-containing parts of a natural number and reciprocals of corresponding products.

In this article, we define Diophantine sets using the Mizar formalism. We focus on selected properties of multivariate polynomials, i.e., functions of several variables to show finally that the class of Diophantine sets is closed with respect to the operations of union and intersection.

This article is the next in a series [1], [5] aiming to formalize the proof of Matiyasevich’s negative solution of Hilbert’s tenth problem.