Two new intuitionistic equivalents to Zarn’s Lemma are stated and proved.

Some aspects of the theory of Boolean algebras and distributive lattices–in particular, the Stone Representation Theorems and the properties of filters and ideals–are analyzed in a constructive setting.

The intersection of a linearly ordered set of total subrelations of a total relation with range 2 need not be total, constructively.

The topic of this article is the formal topology abstracted from the Zariski spectrum of a commutative ring. After recollecting the fundamental concepts of a basic open and a covering relation, we study some candidates for positivity. In particular, we present a coinductively generated positivity relation. We further show that, constructively, the formal Zariski topology cannot have enough points.

Should weak forms of the axiom of choice really be accepted within constructive mathematics? A critical view of the Brouwer-Heyting-Kolmogorov interpretation, accompanied by the intention to include nondeterministic algorithms, leads us to subscribe to Richman's appeal for dropping countable choice. As an alternative interpretation of intuitionistic logic, we propose to renew dialogue semantics.