The extensional realizability model of continuous functionals and three weakly non-constructive classical theorems

TL;DR

This paper examines which classical analysis theorems are realizable within the extensional continuous functionals model, revealing specific theorems that are or are not realizable in this framework.

Contribution

It identifies the realizability status of three classical analysis statements within the extensional continuous functionals model based on Kleene's second model K2.

Findings

Riemann Permutation Theorem is not realizable in the model.

Partially Cauchy sequences being Cauchy is not realizable.

Product of two anti-Specker spaces is realizable.

Abstract

We investigate wether three statements in analysis, that can be proved classically, are realizable in the realizability model of extensional continuous functionals induced by Kleene's second model $K_2$. We prove that a formulation of the Riemann Permutation Theorem as well as the statement that all partially Cauchy sequences are Cauchy cannot be realized in this model, while the statement that the product of two anti-Specker spaces is anti-Specker can be realized.