Abstract
We define and investigate Heyting-valued interpretations for Constructive Zermelo–Frankel set theory (CZF). These interpretations provide models for CZF that are analogous to Boolean-valued models for ZF and to Heyting-valued models for IZF. Heyting-valued interpretations are defined here using set-generated frames and formal topologies. As applications of Heyting-valued interpretations, we present a relative consistency result and an independence proof.
| Original language | English |
|---|---|
| Pages (from-to) | 164-188 |
| Number of pages | 25 |
| Journal | Annals of Pure and Applied Logic |
| Volume | 137 |
| Issue number | 1-3 |
| DOIs | |
| Publication status | Published - Jan 2006 |
Keywords
- Constructive set theory
- Formal topology
- Pointfree topology
- Heyting algebra
- Frame
- Heyting-valued models