Realizability algebras II : new models of ZF + DC

TL;DR

This paper introduces a novel method based on proof-program correspondence to construct models of ZF set theory, establishing the relative consistency of certain properties of the real numbers without using forcing.

Contribution

It presents a new approach to model construction in set theory, providing results previously unattainable through forcing techniques.

Findings

Proves the relative consistency of ZF + DC with specific properties of R.

Introduces a proof-program based method for set-theoretic model construction.

Demonstrates the existence of decreasing sequences of subsets of R with particular properties.

Abstract

Using the proof-program (Curry-Howard) correspondence, we give a new method to obtain models of ZF and relative consistency results in set theory. We show the relative consistency of ZF + DC + there exists a sequence of subsets of R the cardinals of which are strictly decreasing + other similar properties of R. These results seem not to have been previously obtained by forcing.