Sequential algorithms and the computational content of classical proofs

TL;DR

This paper establishes a framework linking sequential algorithms with classical logic through Kreisel's no-counterexample interpretation, providing a computational perspective on classical proofs, especially in analysis.

Contribution

It introduces a novel correspondence between sequential algorithms and classical reasoning, enabling a computational interpretation of classical proofs and the rule of dependent choice.

Findings

Develops a dynamic process model for realizers of the no-counterexample interpretation

Provides a computational interpretation of the rule of dependent choice

Offers insights into the computational content of classical analysis proofs

Abstract

We develop a correspondence between the theory of sequential algorithms and classical reasoning, via Kreisel's no-counterexample interpretation. Our framework views realizers of the no-counterexample interpretation as dynamic processes which interact with an oracle, and allows these processes to be modelled at any given level of abstraction. We discuss general constructions on algorithms which represent specific patterns which often appear in classical reasoning, and in particular, we develop a computational interpretation of the rule of dependent choice which is phrased purely on the level of algorithms, giving us a clearer insight into the computational meaning of proofs in classical analysis.