Toposes from Forcing for Intuitionistic ZF with Atoms

拓扑斯中的常域公理

The Constant Domain Axiom in Toposes

研究常域直觉主义逻辑在拓扑斯理论中的情况，核心方法是用特定对象取代常量预层，主要贡献是证明这些对象在任何拓扑斯中构成布尔预拓扑斯。

Implicative algebras: a new foundation for realizability and forcing

We introduce the notion of implicative algebra, a simple algebraic structure intended to factorize the model constructions underlying forcing and realizability (both in intuitionistic and classical logic). The salient feature of this structure is that its elements can be seen both as truth values and as (generalized) realizers, thus blurring the frontier between proofs and types. We show that each implicative algebra induces a (Set-based) tripos, using a construction that is reminiscent from the construction of a realizability tripos from a partial combinatory algebra. Relating this constructi…

The logic of sheaves, sheaf forcing and the independence of the Continuum Hypothesis

An introduction is given to the logic of sheaves of structures and to set theoretic forcing constructions based on this logic. Using these tools, it is presented an alternative proof of the independence of the Continuum Hypothesis; which simplifies and unifies the classical boolean and intuitionistic approaches, avoiding the difficulties linked to the categorical machinery of the topoi based approach.

Topological Forcing Semantics with Settling

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…

集合论的Krivine可实现性指南

A Guide to Krivine Realizability for Set Theory

本文介绍Krivine对传统可实现性方法的扩展，通过一类模型元素名称给出其可实现性理论的改进形式化，并探讨该方法与直觉主义可实现性、双重否定翻译及力迫理论的关联。