Abstract
Classical logic and intuitionistic logic can be seen as irreconcilable enemies, as in the polemic between Hilbertand Brouwer in 1927. More positively, we can, like Gödel in the 1930s, use intuitionistic logic to better understand classical logic. First of all, classical logic can be seen as intuitionistic logic to which we add a classical axiom, such as the excluded third " P or ¬P ", which gives this lecture its title. More surprisingly : classical logic delves into intuitionistic logic via a translation by double negation. If P is a propositional formula, P is true in classical logic if and only if ¬ ¬P, " P is not false ", is provable in intuitionistic logic. Kolmogorov, Gödel, Gentzen and Kuroda extended this double-negative translation to formulas with quantifiers.
In 1990 , Murthy and Griffin brought these approaches to classical logic into line with the concept of continuation in programming languages. In a functional language, the continuation of an expression a is the calculation remaining to complete the program once a has been evaluated. This continuation can be seen as a function of the value of a towards the value of the complete program. A program can act on its continuations in two ways : either it is written in Continuation-Passing Style (CPS), where each expression receives its continuation as an additional argument ; or control operators are added to the programming language to reify continuations, such as the call/cc operator in the Scheme language. Murthy was the first to observe that CPS transformations, which put a program into CPS form, correspond, in Curry-Howard's sense, with double negation translations in logic. At the same time, Griffin observes that certain control operators admit types that correspond, in the Curry-Howard sense, with axioms of classical logic. Thus, the call/cc operator corresponds to Clavius' law, (¬P ⇒ P) ⇒ P, and Felleisen's C operator to the elimination of double negation, ¬¬P ⇒ P.
These fine results already make it possible to identify the computational content of classical demonstrations. However, an important aspect of classical logic is lost : the duality between conjunction and disjunction via negation, visible in de Morgan's law ¬ (P ∧ Q) ⇔ ¬P ∨ ¬Q and masterfully expressed in Gentzen's (1934) calculus of classical sequents. Which programming language corresponds by Curry-Howard to this classical sequence calculus ? Recent work by Parigot, Curien, Herbelin, Wadler and others provides some answers to this question.
