Topological Forcing Semantics with Settling

TL;DR

This paper introduces a new topological forcing semantics with settling to analyze constructive set theories, demonstrating how properties of the underlying space influence the validity of set-theoretic principles and independence results.

Contribution

It develops a variant topological forcing model with a revised satisfaction relation, generalizing previous models from the reals to arbitrary spaces, to study independence and principle validity.

Findings

Exponentiation does not prove Dedekind reals form a set in CZF minus Subset Collection.

Certain topological properties imply stronger set-theoretic principles.

The model generalizes earlier real-based semantics to arbitrary topological spaces.

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.