Volume 22 (2014): Issue 3 (September 2014)

In this article, we formalize some basic facts of Z-module. In the first section, we discuss the rank of submodule of Z-module and its properties. Especially, we formally prove that the rank of any Z-module is equal to or more than that of its submodules, and vice versa, and that there exists a submodule with any given rank that satisfies the above condition. In the next section, we mention basic facts of linear transformations between two Z-modules. In this section, we define homomorphism between two Z-modules and deal with kernel and image of homomorphism. In the last section, we formally prove some basic facts about linearly independent subsets and linear combinations. These formalizations are based on [9](p.191-242), [23](p.117-172) and [2](p.17-35).

We consider special events of Borel sets with the aim to prove, that the set of the irrational numbers is an event of the Borel sets. The set of the natural numbers, the set of the integer numbers and the set of the rational numbers are countable, so we can use the literature [10] (pp. 78-81) as a basis for the similar construction of the proof. Next we prove, that different sets can construct the Borel sets [16] (pp. 9-10). Literature [16] (pp. 9-10) and [11] (pp. 11-12) gives an overview, that there exists some other sets for this construction. Last we define special functions as random variables for stochastic finance in discrete time. The relevant functions are implemented in the article [15], see [9] (p. 4). The aim is to construct events and random variables, which can easily be used with a probability measure. See as an example theorems (10) and (14) in [20]. Then the formalization is more similar to the presentation used in the book [9]. As a background, further literatures is [3] (pp. 9-12), [13] (pp. 17-20), and [8] (pp.32-35).

The article focuses on simple identities found for binomials, their divisibility, and basic inequalities. A general formula allowing factorization of the sum of like powers is introduced and used to prove elementary theorems for natural numbers.

Formulas for short multiplication are sometimes referred in English or French as remarkable identities. The same formulas could be found in works concerning polynomial factorization, where there exists no single term for various identities. Their usability is not questionable, and they have been successfully utilized since for ages. For example, in his books published in 1731 (p. 385), Edward Hatton [3] wrote: “Note, that the differences of any two like powers of two quantities, will always be divided by the difference of the quantities without any remainer...”.

Despite of its conceptual simplicity, the problem of factorization of sums/differences of two like powers could still be analyzed [7], giving new and possibly interesting results [6].

In this article, we formalize topological properties of real normed spaces. In the first part, open and closed, density, separability and sequence and its convergence are discussed. Then we argue properties of real normed subspace. Then we discuss linear functions between real normed speces. Several kinds of subspaces induced by linear functions such as kernel, image and inverse image are considered here. The fact that Lipschitz continuity operators preserve convergence of sequences is also refered here. Then we argue the condition when real normed subspaces become Banach’s spaces. We also formalize quotient vector space. In the last session, we argue the properties of the closure of real normed space. These formalizations are based on [19](p.3-41), [2] and [34](p.3-67).

We introduce algorithmic logic - an algebraic approach according to [25]. It is done in three stages: propositional calculus, quantifier calculus with equality, and finally proper algorithmic logic. For each stage appropriate signature and theory are defined. Propositional calculus and quantifier calculus with equality are explored according to [24]. A language is introduced with language signature including free variables, substitution, and equality. Algorithmic logic requires a bialgebra structure which is an extension of language signature and program algebra. While-if algebra of generator set and algebraic signature is bialgebra with appropriate properties and is used as basic type of algebraic logic.

Almost Distributive Lattices (ADL) are structures defined by Swamy and Rao [14] as a common abstraction of some generalizations of the Boolean algebra. In our paper, we deal with a certain further generalization of ADLs, namely the Generalized Almost Distributive Lattices (GADL). Our main aim was to give the formal counterpart of this structure and we succeeded formalizing all items from the Section 3 of Rao et al.’s paper [13]. Essentially among GADLs we can find structures which are neither V-commutative nor Λ-commutative (resp., Λ-commutative); consequently not all forms of absorption identities hold.

We characterized some necessary and sufficient conditions for commutativity and distributivity, we also defined the class of GADLs with zero element. We tried to use as much attributes and cluster registrations as possible, hence many identities are expressed in terms of adjectives; also some generalizations of wellknown notions from lattice theory [11] formalized within the Mizar Mathematical Library were proposed. Finally, some important examples from Rao’s paper were introduced. We construct the example of GADL which is not an ADL. Mechanization of proofs in this specific area could be a good starting point towards further generalization of lattice theory [10] with the help of automated theorem provers [8].

In [11], the definitions of forward difference, backward difference, and central difference as difference operations for functions on R were formalized. However, the definitions of forward difference, backward difference, and central difference for functions on vector spaces over F have not been formalized. In cryptology, these definitions are very important in evaluating the security of cryptographic systems [3], [10]. Differential cryptanalysis [4] that undertakes a general purpose attack against block ciphers [13] can be formalized using these definitions. In this article, we formalize the definitions of forward difference, backward difference, and central difference for functions on vector spaces over F. Moreover, we formalize some facts about these definitions.