Degrees of incomputability, realizability and constructive reverse mathematics

TL;DR

The work develops a Lifschitz-like realizability for Weihrauch degrees by introducing a site-based (relative pca, $j$-operator) framework that yields ${\bf IZF}$-realizability. It first analyzes a broad spectrum of nonconstructive principles through Weihrauch degrees and then proves intricate separations among these degrees using a recursion-trick-based reduction-game methodology. Finally, it shows how these Weihrauch separations lift to concrete separations in ${\bf IZF}$, providing explicit realizability models such as ${\bf IZF}+{\sf LLPO}+\neg{\sf RDIV}+\neg{\sf BE}$ and related combinations. The results illuminate how computational content and discontinuity degrees of theorems interplay with constructive set theory, offering systematic AC-free models that separate core principles in constructive reverse mathematics. This framework yields both a conceptual bridge between computability theory and intuitionistic set theory and a toolbox for constructing AC-free realizability models with precise logical properties.

Abstract

There is a way of assigning a realizability notion to each degree of incomputability. In our setting, we make use of Weihrauch degrees (degrees of incomputability/discontinuity of partial multi-valued functions) to obtain Lifschitz-like relative realizability predicates. In this note, we present sample examples on how to lift some separation results on Weihrauch degrees to those over intuitionistic Zermelo-Fraenkel set theory ${\bf IZF}$.

Figures (2)

• Figure 1: Nonconstructive principles over a base intuitionistic system
• Figure 2: Nonconstructive principles as variants of weak König's lemma

Theorems & Definitions (107)

• Theorem 1.1
• Example 2.1
• Example 2.2
• Example 2.3
• Example 2.4
• Remark
• Example 2.5
• Example 2.6
• Definition 3.1
• Remark