Classical consequences of continuous choice principles from intuitionistic analysis

TL;DR

This paper explores how certain intuitionistic proofs imply classical consequences under specific conditions, emphasizing the role of uniformity and realizability in the logical relationship between systems.

Contribution

It establishes that proofs of certain statements in weak intuitionistic systems guarantee the provability of their sequential forms in weak classical systems, highlighting the importance of uniformity.

Findings

Proofs in weak intuitionistic systems imply sequential forms in weak classical systems.

Uniformity of proofs is crucial for transferring results between systems.

Realizability techniques are used to establish these logical connections.

Abstract

The sequential form of a statement $\forall\xi(B(\xi) \rightarrow \exists\zeta A(\xi,\zeta))$ is the statement $\forall\xi(\forall n B(\xi_n) \rightarrow \exists\zeta \forall n A(\xi_n,\zeta_n))$. There are many classically true statements of the first form whose proofs lack uniformity and therefore the corresponding sequential form is not provable in weak classical systems. The main culprit for this lack of uniformity is of course the law of excluded middle. Continuing along the lines of previous work by Hirst and Mummert, we show that if a statement of the first form satisfying certain syntactic requirements is provable in some weak intuitionistic system, then the proof is necessarily sufficiently uniform that the corresponding sequential form is provable in a corresponding weak classical system. Our results depend on Kleene's realizability with functions and the Lifschitz variant thereof.