Typed realizability for first-order classical analysis

TL;DR

This paper introduces a realizability framework for classical first-order logic using typed lambda-mu calculus, enabling direct proof interpretation and efficient program extraction without negative translation.

Contribution

It presents a novel realizability approach for classical logic that simplifies proof interpretation and program extraction, especially for arithmetic and choice axioms.

Findings

G"odel's system T realizes Peano axioms

Bar recursion realizes dependent choice under certain conditions

Efficient program extraction with simpler types using Friedman's trick

Abstract

We describe a realizability framework for classical first-order logic in which realizers live in (a model of) typed {\lambda}{\mu}-calculus. This allows a direct interpretation of classical proofs, avoiding the usual negative translation to intuitionistic logic. We prove that the usual terms of G\"odel's system T realize the axioms of Peano arithmetic, and that under some assumptions on the computational model, the bar recursion operator realizes the axiom of dependent choice. We also perform a proper analysis of relativization, which allows for less technical proofs of adequacy. Extraction of algorithms from proofs of {\Pi}02 formulas relies on a novel implementation of Friedman's trick exploiting the control possibilities of the language. This allows to have extracted programs with simpler types than in the case of negative translation followed by intuitionistic realizability.