Peter LeFanu Lumsdaine: The zoo of realisability

Abstract

Compared to the relatively orderly garden of, say, sheaf models, realisability interpretations of logic — introduced by Kleene in 1945 to expose the computational content of first-order arithmetic — are, in several respects, a bit of a zoo. They can be presented via a variety of underlying approaches; they interpret an equally diverse range of formal systems; and they can host a wide variety of surprising phenomena, including counterexamples to many classical theorems — the reals can be countable! limit ordinals can be chain-complete! small categories can be complete!

I will give an introduction to and survey of realisability models, starting elementarily before moving to a modern categorical framework, and presenting a brief tour of the startling phenomena they can exhibit.