Truth in Higher Types

Ulrich Berger


In recent years a new brach of proof theory, dubbed
"proof mining", has gained considerable popularity.
In proof mining one extracts computational content from proofs
in order to obtain formally verified, more efficient, or new
algorithms. Very often the proofs are formulated in
systems based on higher types and, most curiously,
"false" axioms. That the extracted programs are
nevertheless correct hinges on the fact that there
are models of higher types where these "false" axioms
are actually true.

In this talk we investigate systematically how the
truth of a statement involving higher type functionals
depends on the underlying model.

More precisely, given models X and Y of Goedel's system
T of primitive recursive functionals in higher types, it is our aim to
characterise those higher-type quantifier prefixes such that
for all prenex formulas A with that quantifier prefix the truth of
A in X implies the truth of A in Y.

We will concentrate on the following four models of system T: The
full set-theoretic model, the model of continuous
functionals of Kleene and Kreisel, the model of hereditarily
effective operations and the closed term model.
These models are of particular interest for proof mining, but
they are also significant form a foundational point of view,
since they correspond (roughly) to the classical, intuitionistic,
constructivistic and formalistic perception of higher types,

Thursday 15th February 2007, 14:00
Board Room
Department of Computer Science