##
Hybrid realizability for intuitionistic and classical choice

### Valentin Blot

In intuitionistic realizability like Kleene's or Kreisel's, the axiom
of choice is trivially realized. It is even provable in Martin-L\"of's
intuitionistic type theory. In classical logic, however, even the
weaker axiom of countable choice proves the existence of non-
computable functions. This logical strength comes at the price of a
complicated computational interpretation which involves strong
recursion schemes like bar recursion. We take the best from both worlds
and define a realizability model for arithmetic and the axiom of choice
which encompasses both intuitionistic and classical reasoning. In this
model two versions of the axiom of choice can co-exist in a single
proof: intuitionistic choice and classical countable choice. We
interpret intuitionistic choice efficiently, however its premise cannot
come from classical reasoning. Conversely, our version of classical
choice is valid in full classical logic, but it is restricted to the
countable case and its realizer involves bar recursion. Having both
versions allows us to obtain efficient extracted programs while keeping
the provability strength of classical logic.