On some peculiar aspects of the constructive theory of point-free spaces

TL;DR

This paper explores independence results in the constructive theory of point-free spaces, focusing on the relationship between topos-valid and predicative theories, and examines the consistency of Troelstra's uniformity principle within constructive frameworks.

Contribution

It provides new independence results and analyzes the consistency of Troelstra's uniformity principle in constructive set and type theories.

Findings

Certain consequences of Troelstra's uniformity principle are consistent with constructive set theory.

Independence results highlight differences between topos-valid and predicative theories.

The paper clarifies the logical boundaries of constructive point-free space theories.

Abstract

This paper presents several independence results concerning the topos-valid and the intuitionistic (generalized) predicative theories of locales. In particular, certain consequences of the consistency of a general form of Troelstra's uniformity principle with constructive set theory and type theory are examined.