Gaussian integer is one of basic algebraic integers. In this article we formalize some definitions about Gaussian integers [27]. We also formalize ring (called Gaussian integer ring), Z-module and Z-algebra generated by Gaussian integer mentioned above. Moreover, we formalize some definitions about Gaussian rational numbers and Gaussian rational number field. Then we prove that the Gaussian rational number field and a quotient field of the Gaussian integer ring are isomorphic.

Si considera il calcolo modale interpretato $ℳ{𝒞}^{\nu }$, che è basato su un sistema di tipi con infiniti livelli, contiene descrizioni, ed è dotato di una semantica di tipo generale - v. [2], o [3], o [4], o [5]. In modo semplice e naturale si introducono in $ℳ{𝒞}^{\nu }$ operatori vincolanti variabili, di tipo generale. Per teorie basate sul calcolo logico risultante $ℳ{𝒞}^{\nu }$ vale un teorema di completezza, che si dimostra in modo immediato sulla base dell'estensione del teorema parziale di completezza stabilito in [11], fatta...

An algebra $𝒜=(A,F)$ is subregular alias regular with respect to a unary term function $g$ if for each $\Theta ,\Phi \in \text{Con}𝒜$ we have $\Theta =\Phi$ whenever ${\left[g\left(a\right)\right]}_{\Theta }={\left[g\left(a\right)\right]}_{\Phi }$ for each $a\in A$. We borrow the concept of a deductive system from logic to modify it for subregular algebras. Using it we show that a subset $C\subseteq A$ is a class of some congruence on $\Theta$ containing $g\left(a\right)$ if and only if $C$ is this generalized deductive system. This method is efficient (needs a finite number of steps).

An R-algebra A is called an E(R)-algebra if the canonical homomorphism from A to the endomorphism algebra $En{d}_{R}A$ of the R-module ${}_{R}A$, taking any a ∈ A to the right multiplication $a_r\in En{d}_{R}A$ by a, is an isomorphism of algebras. In this case ${}_{R}A$ is called an E(R)-module. There is a proper class of examples constructed in [4]. E(R)-algebras arise naturally in various topics of algebra. So it is not surprising that they were investigated thoroughly in the last decades; see [3, 5, 7, 8, 10, 13, 14, 15, 18, 19]. Despite...

We study unbounded versions of effect algebras. We show a necessary and sufficient condition, when lattice operations of a such generalized effect algebra $P$ are inherited under its embeding as a proper ideal with a special property and closed under the effect sum into an effect algebra. Further we introduce conditions for a generalized homogeneous, prelattice or MV-effect effect algebras. We prove that every prelattice generalized effect algebra $P$ is a union of generalized MV-effect algebras and...

The notion of a construction of a fuzzy preference structures is introduced. The properties of a certain class of generated fuzzy implications are studied. The main topic in this paper is investigation of the construction of the monotone generator triplet $(p,i,j)$, which is the producer of fuzzy preference structures. Some properties of mentioned monotone generator triplet are investigated.

In this paper, some generating methods for principal topology are introduced by means of some logical operators such as uninorms and triangular norms and their properties are investigated. Defining a pre-order obtained from the closure operator, the properties of the pre-order are studied.

Fuzzy Mathematical Morphology aims to extend the binary morphological operators to grey-level images. In order to define the basic morphological operations fuzzy erosion, dilation, opening and closing, we introduce a general method based upon fuzzy implication and inclusion grade operators, including as particular case, other ones existing in related literature. In the definition of fuzzy erosion and dilation we use several fuzzy implications (Annexe A, Table of fuzzy implications), the paper includes...

Using the Mizar system [2], we formalized that homographies of the projective real plane (as defined in [5]), form a group. Then, we prove that, using the notations of Borsuk and Szmielew in [3] “Consider in space ℝℙ2 points P1, P2, P3, P4 of which three points are not collinear and points Q1,Q2,Q3,Q4 each three points of which are also not collinear. There exists one homography h of space ℝℙ2 such that h(Pi) = Qi for i = 1, 2, 3, 4.” (Existence Statement 52 and Existence Statement 53) [3]. Or,...

We translate the articles covering group theory already available in the Mizar Mathematical Library from multiplicative into additive notation. We adapt the works of Wojciech A. Trybulec [41, 42, 43] and Artur Korniłowicz [25]. In particular, these authors have defined the notions of group, abelian group, power of an element of a group, order of a group and order of an element, subgroup, coset of a subgroup, index of a subgroup, conjugation, normal subgroup, topological group, dense subset and basis...

This article is the second in a series formalizing some results in my joint work with Prof. Joanna Golinska-Pilarek ([9] and [10]) concerning a logic proposed by Prof. Andrzej Grzegorczyk ([11]). This part presents the syntax and axioms of Grzegorczyk’s Logic of Descriptions (LD) as originally proposed by him, as well as some theorems not depending on any semantic constructions. There are both some clear similarities and fundamental differences between LD and the non-Fregean logics introduced by...