Volume 19 (2011): Issue 2 (January 2011)

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

Partial Differentiation, Differentiation and Continuity on n-Dimensional Real Normed Linear Spaces

Published Online: 18 Jul 2011
Page range: 65 - 68

Abstract

In this article, we aim to prove the characterization of differentiation by means of partial differentiation for vector-valued functions on n-dimensional real normed linear spaces (refer to [15] and [16]).

Open Access

Differentiable Functions into Real Normed Spaces

Published Online: 18 Jul 2011
Page range: 69 - 72

Abstract

In this article, we formalize the differentiability of functions from the set of real numbers into a normed vector space [14].

Open Access

Conway's Games and Some of their Basic Properties

Published Online: 18 Jul 2011
Page range: 73 - 81

Abstract

We formulate a few basic concepts of J. H. Conway's theory of games based on his book [6]. This is a first step towards formalizing Conway's theory of numbers into Mizar, which is an approach to proving the existence of a FIELD (i.e., a proper class that satisfies the axioms of a real-closed field) that includes the reals and ordinals, thus providing a uniform, independent and simple approach to these two constructions that does not go via the rational numbers and hence does for example not need the notion of a quotient field.

In this first article on Conway's games, we provide a definition of games, their birthdays (or ranks), their trees (a notion which is not in Conway's book, but is useful as a tool), their negates and their signs, together with some elementary properties of these notions. If one is interested only in Conway's numbers, it would have been easier to define them directly, but going via the notion of a game is a more general approach in the sense that a number is a special instance of a game and that there is a rich theory of games that are not numbers.

The main obstacle in formulating these topics in Mizar is that all definitions are highly recursive, which is not entirely simple to translate into the Mizar language. For example, according to Conway's definition, a game is an object consisting of left and right options which are themselves games, and this is by definition the only way to construct a game. This cannot directly be translated into Mizar, but a theorem is included in the article which proves that our definition is equivalent to Conway's.

Open Access

Veblen Hierarchy

Published Online: 18 Jul 2011
Page range: 83 - 92

Abstract

The Veblen hierarchy is an extension of the construction of epsilon numbers (fixpoints of the exponential map: ωε = ε). It is a collection φα of the Veblen Functions where φ0(β) = ωβ and φ1(β) = εβ. The sequence of fixpoints of φ1 function form φ2, etc. For a limit non empty ordinal λ the function φλ is the sequence of common fixpoints of all functions φα where α < λ.

The Mizar formalization of the concept cannot be done directly as the Veblen functions are classes (not (small) sets). It is done with use of universal sets (Tarski classes). Namely, we define the Veblen functions in a given universal set and φα(β) as a value of Veblen function from the smallest universal set including α and β.

Open Access

Sorting by Exchanging

Published Online: 18 Jul 2011
Page range: 93 - 102

Abstract

We show that exchanging of pairs in an array which are in incorrect order leads to sorted array. It justifies correctness of Bubble Sort, Insertion Sort, and Quicksort.

Open Access

Linear Transformations of Euclidean Topological Spaces

Published Online: 18 Jul 2011
Page range: 103 - 108

Abstract

We introduce linear transformations of Euclidean topological spaces given by a transformation matrix. Next, we prove selected properties and basic arithmetic operations on these linear transformations. Finally, we show that a linear transformation given by an invertible matrix is a homeomorphism.

Open Access

Linear Transformations of Euclidean Topological Spaces. Part II

Published Online: 18 Jul 2011
Page range: 109 - 112

Abstract

We prove a number of theorems concerning various notions used in the theory of continuity of barycentric coordinates.

Open Access

The Axiomatization of Propositional Linear Time Temporal Logic

Published Online: 18 Jul 2011
Page range: 113 - 119

Abstract

The article introduces propositional linear time temporal logic as a formal system. Axioms and rules of derivation are defined. Soundness Theorem and Deduction Theorem are proved [9].

Open Access

Banach Algebra of Bounded Complex-Valued Functionals

Published Online: 18 Jul 2011
Page range: 121 - 126

Abstract

In this article, we describe some basic properties of the Banach algebra which is constructed from all bounded complex-valued functionals.