Computational Content of Classical Logic Thierry Coquand
Thierry Coquand · Cambridge University Press eBooks · 1997
Introduction This course is an introduction to the research trying to connect the proof theory of classical logic and computer science. We omit important and standard topics, among them the connection between the computational interpretation of classical logic and the programming operator callcc. Instead, here we put the emphasis on actual mathematical examples. We analyse the following questions: what can be the meaning of a non-effective proof of an existential statement, a statement that claims the existence of a finite object that satisfies a decidable property? Is it clear that a non-effective proof has a meaning at all? Can we always say that this proof contains implicitly, if not explicitly, some effective witness? Is this witness unique? By putting the emphasis on actual mathematical examples, we follow Gentzen who founded natural deduction by analysing concrete mathematical examples, like Euclid's proof of the infinity of prime numbers. We present general methods that can be used to compute effectively such witnesses. The three methods we shall analyse are The negative translation. This is a quite natural translation of classical logic in intuitionistic logic, which is both simple and powerful. A game-theoretic interpretation of classical logic, which is a suggestive reformulation of Gentzen-Novikov's sequent calculus, and may be in some cases more convenient than negative translation. Use of formal topology. It consists of realising some conditions in a topological model. In some cases, it is possible then to realise these conditions effectively, while the “absolute” realisation of these conditions is impossible.