Independence Results around Constructive ZF

TL;DR

This paper demonstrates through Kripke models that certain constructive set theories like CZF cannot prove the Power Set axiom, and similar results hold when Subset Collection is replaced by Exponentiation.

Contribution

It provides independence results for CZF regarding Power Set and Subset Collection using Kripke models, clarifying the limitations of these theories.

Findings

CZF does not prove Power Set

CZF with Exponentiation replacing Subset Collection does not prove Subset Collection

Kripke models are effective for independence proofs in constructive set theories

Abstract

Using Kripke models, it is shown that CZF does not prove Power Set, and that CZF with Subset Collection substituted by Exponentiation does not prove Subset Collection.