Computational Content of Classical Logic

The problem of extracting a witness from a non-constructive proof of a purely existential statement is one of the basic problems in proof theory. The negative translation, refined by H. Friedman, gives a solution for a large class of systems, but does not work for some natural systems, like ID1 or Peano arithmetic with induction restricted to purely existential statements, and some more sophisticated method (Dialectica interpretation, ordinal analysis) is needed. We have made the following contributions to these questions:

A suggestive game-theoretic interpretation of Gentzen's first consistency proof and a variation of Tait's sequent calculus. The process of cut-elimination was formulated as interaction of strategies, and a combinatorial lemma which expresses that this process terminates were proved.

(Together with S. Berardi and M. Bezem) A modified realizability interpretation of the system HAw with excluded middle and axiom of choices, with a (classical) proof of normalisation.

A general method, based on the use of topological model and formal topology, for interpreting in type theory objects whose existence rely usually on Zorn's lemma (prime ideals, non principal ultrafilters, valuation rings, ...) This method can be used also to interpret ``minimal bad sequence arguments''(Higman's lemma, Zantema's problem, ...) It can also be used to give new simple interpretations of logical systems in their intuitionistic version (like ID1 or Peano restricted to Sigma01-induction).

It has been argued (Weyl, Feferman) that excluded-middle may be justified over natural numbers, but that the ``openness'' of the notion of functions makes it less clear at the level of functions. Together with Erik Palmgren, we give a method to build constructively sheaf models that captures this intuition: these are models of the ``limited principle of omniscience'', while quantifications over functions is interpreted intuitionistically.

Last modified: Thu May 28 13:01:12 MET DST 1998