http://hdl.handle.net/11320/5549 2026-06-01T17:24:24Z http://hdl.handle.net/11320/5564 Tytuł: Niven’s Theorem Autorzy: Korniłowicz, Artur; Naumowicz, Adam Abstrakt: 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]. 2016-01-01T00:00:00Z http://hdl.handle.net/11320/5562 Tytuł: The Axiomatization of Propositional Logic Autorzy: Giero, Mariusz Abstrakt: 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. 2016-01-01T00:00:00Z http://hdl.handle.net/11320/5563 Tytuł: Algebraic Numbers Autorzy: Watase, Yasushige Abstrakt: 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. 2016-01-01T00:00:00Z http://hdl.handle.net/11320/5561 Tytuł: Leibniz Series for π Autorzy: Pąk, Karol Abstrakt: In this article we prove the Leibniz series for π which states that π4=∑n=0∞(−1)n2⋅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/. 2016-01-01T00:00:00Z