Topological Forcing Semantics with Settling

Abstract

It was realized early on that topologies can model constructive systems, as the open sets form a Heyting algebra. After the development of forcing, in the form of Boolean-valued models, it became clear that, just as over ZF any Boolean-valued model also satisfies ZF, so do Heyting-valued models satisfy IZF, which stands for Intuitionistic ZF, the most direct constructive re-working of the ZF axioms. In this paper, we return to topologies, and introduce a variant model, along with a correspondingly revised forcing or satisfaction relation. The purpose is to prove independence results related to weakenings of the Power Set axiom. The original motivation is earlier work, based on the set of reals, which shows that Exponentiation, in the context of CZF minus Subset Collection, does not suffice to prove that the Dedekind reals form a set. The current semantics is the generalization of that model from R to an arbitrary topological space. It is investigated which set-theoretic principles hold in such models in general. In addition, natural properties of the underlying topological space are shown to imply the validity of stronger such principles.