Oberseminar "Mathematische Logik" - Prof. Dr. Helmut Schwichtenberg

We work in a constructive extension of classical logic, where in addition to the classical existential quantifier (not -- forall -- not) we have a constructive one which requires an example. In this setting we sketch a theory of computable functionals (TCF) which extends Heyting's arithmetic in all simple types. TCF includes Kreisel's (modified) realizability predicates and has invariance axioms stating that ''to assert is to realize'' (Feferman 1978) for realizability-free formulas. Using these TCF proves a soundness theorem: the term extracted from a realizability-free proof of A is a realizer of A. We conclude with some examples in constructive analysis implemented in the Minlog proof assistant.