Running the classical pigeonhole principle in Agda
Martin Escardo & Paulo Oliva, May 2011. In collaboration with Ulrich
Berger & Monika Seisenberger. Transcribed to Agda 29 April - 3 May
2011 by Martin Escardo, based on other Agda modules produced in
previous years (for the selection monad J and continuation monad K, double-negation shift, classical choice etc., which are also included below).
This version 27th May 2011, 19:27 BST.
You can download all the agda files as a zip file.
The main Agda files (html-formated with hyperlinks to the other files, which allow navigation by clicking at any word) are
The classical axiom of countable choice (that is, choice formulated with the classical existential quantifier) is realized in K-AC-N using any of
- Slides of talk given at MFPS.
(See also InfinitePigeonLessEfficient.)
by performing a suitable choice in the wrapper module K-Shift.
with Berardi, Bezem and Coquand's functional,
with Berger-Oliva modified bar recursion,
- K-Shift-Selection with Escardo and Oliva's countable product of selection functions (download pdf),
The classical infinite pigeonhole principle says that any infinite
sequence of booleans has an infinite constant subsequence (this is the
We work with the negative translation or more generally Friedman's
A-translation, which amounts to prefixing "K R" (double negation
monad) in front of existential quantifiers, disjunctions, and atomic
formulas (equations of ground type), where R is an arbitrary
proposition (as a first approximation, think of the parameter R as
Starting with a proof that uses both excluded middle and classical
countable choice (i.e. choice formulated with the classical
existential quantifier), we eventually get to a theorem that avoids K
and considers a finite version of the pigeonhole principle. The point
is to illustrate how one can extract witnesses from proofs that use
classical logic and countable choice.
(We don't use the Agda libraries, and hence this set of Agda files is