Lorenzen and Constructive Mathematics

The goal of this paper is to present a short survey of some of Lorenzen’s contributions to constructive mathematics, and its influence on recent developments in mathematical logic and constructive algebra. We also present some work in measure theory which uses these contributions in an essential way.

A univalent formalization of the p-adic numbers

The goal of this paper is to report on a formalization of the p-adic numbers in the setting of the second author's univalent foundations program. This formalization, which has been verified in the Coq proof assistant, provides an approach to the p-adic numbers in constructive algebra and analysis.

Some relations and subsets generated by principal consistent subset of semigroup with apartness

The investigation is in the Constructive algebra in the sense of E. Bishop, F. Richman, W. Ruitenburg, D. van Dalen and A. S. Troelstra. Algebraic structures with apartness the first were defined and studied by A. Heyting. After that, some authors studied algebraic structures in constructive mathematics as for example: D. van Dalen, E. Bishop, P. T. Johnstone, A. Heyting, R. Mines, J. C. Mulvey, F. Richman, D. A. Romano, W. Ruitenburg and A. Troelstra. This paper is one of articles in their the author tries to investigate semugroups with apartnesses. Relation q on S is a coequality relation on S if it is consistent, symmetric and cotran-sitive; coequality relation is generalization of apatness. The main subject of this consideration are characterizations of some coequality relations on semigroup S with apartness by means od special ideals J(a) = {x E S : a# SxS}, principal consistent subsets C(a) = {x E S : x# SaS} (a E S) of S and by filled product of relations on S. Let S = (S, =, 1) be a semigroup with apartness. As preliminaries we will introduce some special notions, notations and results in set theory, commutative ring theory and semigroup theory in constructive mathematics and we will give proofs of several general theorems in semigroup theory. In the next section we will introduce relation s on S by (x, y) E s iff y E C(x) and we will describe internal filfulments c(s U s?1) and c(s ? s?1) and their classes A(a) = ?An(a) and K(a) = ?Kn(a) respectively. We will give the proof that the set K(a) is maximal strongly extensional consistent ideal of S for every a in S. Before that, we will analyze semigroup S with relation q = c(s U s?1 ) in two special cases: (i) the relation q is a band coequality relation on S : (ii) q is left zero band coequality relation on S. Beside that, we will introduce several compatible equality and coequality relations on S by sets A(a), An(a), K(a) and Kn(a).