# Volume 24 (2016): Issue 4 (December 2016)

Journal Details
Format
Journal
eISSN
1898-9934
ISSN
1426-2630
First Published
09 Jun 2008
Publication timeframe
4 times per year
Languages
English

7 Articles
Open Access

#### Homography in ℝℙ

Published Online: 23 Feb 2017
Page range: 239 - 251

#### Abstract

The real projective plane has been formalized in Isabelle/HOL by Timothy Makarios [13] and in Coq by Nicolas Magaud, Julien Narboux and Pascal Schreck [12].

Some definitions on the real projective spaces were introduced early in the Mizar Mathematical Library by Wojciech Leonczuk [9], Krzysztof Prazmowski [10] and by Wojciech Skaba [18].

In this article, we check with the Mizar system [4], some properties on the determinants and the Grassmann-Plücker relation in rank 3 [2], [1], [7], [16], [17].

Then we show that the projective space induced (in the sense defined in [9]) by ℝ3 is a projective plane (in the sense defined in [10]).

Finally, in the real projective plane, we define the homography induced by a 3-by-3 invertible matrix and we show that the images of 3 collinear points are themselves collinear.

#### Keywords

• projectivity
• projective transformation
• projective collineation
• real projective plane
• Grassmann-Plücker relation

• 51N15
• 03B35
Open Access

#### The Basic Existence Theorem of Riemann-Stieltjes Integral

Published Online: 23 Feb 2017
Page range: 253 - 259

#### Abstract

In this article, the basic existence theorem of Riemann-Stieltjes integral is formalized. This theorem states that if f is a continuous function and ρ is a function of bounded variation in a closed interval of real line, f is Riemann-Stieltjes integrable with respect to ρ. In the first section, basic properties of real finite sequences are formalized as preliminaries. In the second section, we formalized the existence theorem of the Riemann-Stieltjes integral. These formalizations are based on [15], [12], [10], and [11].

#### Keywords

• Riemann-Stieltjes integral
• bounded variation
• continuous function

• 26A42
• 26A45
• 03B35
Open Access

#### On Subnomials

Published Online: 23 Feb 2017
Page range: 261 - 273

#### Abstract

While discussing the sum of consecutive powers as a result of division of two binomials W.W. Sawyer [12] observes

“It is a curious fact that most algebra textbooks give our ast result twice. It appears in two different chapters and usually there is no mention in either of these that it also occurs in the other. The first chapter, of course, is that on factors. The second is that on geometrical progressions. Geometrical progressions are involved in nearly all financial questions involving compound interest – mortgages, annuities, etc.”

It’s worth noticing that the first issue involves a simple arithmetical division of 99...9 by 9. While the above notion seems not have changed over the last 50 years, it reflects only a special case of a broader class of problems involving two variables. It seems strange, that while binomial formula is discussed and studied widely [7], [8], little research is done on its counterpart with all coefficients equal to one, which we will call here the subnomial. The study focuses on its basic properties and applies it to some simple problems usually proven by induction [6].

#### Keywords

• binomial formula
• geometrical progression
• polynomials

• 40-04
• 03B35
Open Access

#### Leibniz Series for π

Published Online: 23 Feb 2017
Page range: 275 - 280

#### Abstract

In this article we prove the Leibniz series for π which states that π4=n=0(1)n2n+1.$${\pi \over 4} = \sum\limits_{n = 0}^\infty {{{\left( { - 1} \right)^n } \over {2 \cdot n + 1}}.}$$

The formalization follows K. Knopp [8], [1] and [6]. Leibniz’s Series for Pi is item #26 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.

#### Keywords

• approximation
• Leibniz theorem
• Leibniz series

• 40G99
• 03B35
Open Access

#### The Axiomatization of Propositional Logic

Published Online: 23 Feb 2017
Page range: 281 - 290

#### Abstract

This article introduces propositional logic as a formal system ([14], [10], [11]). The formulae of the language are as follows φ ::= ⊥ | p | φφ. Other connectives are introduced as abbrevations. The notions of model and satisfaction in model are defined. The axioms are all the formulae of the following schemes

α ⇒ (βα),

(α ⇒ (βγ)) ⇒ ((αβ) ⇒ (αγ)),

β ⇒ ¬α) ⇒ ((¬βα) ⇒ β).

Modus ponens is the only derivation rule. The soundness theorem and the strong completeness theorem are proved. The proof of the completeness theorem is carried out by a counter-model existence method. In order to prove the completeness theorem, Lindenbaum’s Lemma is proved. Some most widely used tautologies are presented.

#### Keywords

• completeness
• formal system
• Lindenbaum’s lemma

• 03B05
• 03B35
Open Access

#### Algebraic Numbers

Published Online: 23 Feb 2017
Page range: 291 - 299

#### Abstract

This article provides definitions and examples upon an integral element of unital commutative rings. An algebraic number is also treated as consequence of a concept of “integral”. Definitions for an integral closure, an algebraic integer and a transcendental numbers [14], [1], [10] and [7] are included as well. As an application of an algebraic number, this article includes a formal proof of a ring extension of rational number field ℚ induced by substitution of an algebraic number to the polynomial ring of ℚ[x] turns to be a field.

#### Keywords

• algebraic number
• integral dependency

• 11R04
• 13B21
• 03B35
Open Access

#### Niven’s Theorem

Published Online: 23 Feb 2017
Page range: 301 - 308

#### Abstract

This article formalizes the proof of Niven’s theorem [12] which states that if x/π and sin(x) are both rational, then the sine takes values 0, ±1/2, and ±1. The main part of the formalization follows the informal proof presented at Pr∞fWiki (https://proofwiki.org/wiki/Niven’s_Theorem#Source_of_Name). For this proof, we have also formalized the rational and integral root theorems setting constraints on solutions of polynomial equations with integer coefficients [8, 9].

#### Keywords

• Niven’s theorem
• rational root theorem
• integral root theorem

• 97G60
• 12D10
• 03B35