(Swansea)

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,

respectively.

Board Room

Department of Computer Science