Pour ce premier séminaire de Fédération,  nous accueillons Glynn Winskel (Collegium de Lyon, University of Cambridge).

Titre : « The True Concurrency of Herbrand’s Theorem »

Résumé : The brilliant French mathematician Jacques Herbrand died in 1931 in a mountaineering accident at the age of 23. Despite his youth he has two major theorems to his name. One is a foundational result in logic. Herbrand’s Theorem is perhaps the first example of information being extracted from a formula in predicate calculus from the bare fact of its provability. In its simplest form his theorem states that if an existential formula of predicate calculus is provable then so is a disjunction got by instantiating its body with finitely many witnesses. More generally, Herbrand showed how an arbitrary formula in the predicate calculus is provable only if a quantifier-free disjunctive formula is provable. Herbrand’s proof didn’t work directly off the composition of the original formula. Indeed, it seems to be folklore that there is a problem in giving a compositional proof of Herbrand’s Theorem. This is made precise by Kohlenbach who shows that one cannot hope directly to use collections of Herbrand witnesses for provable A and (A implies B) to give a collection for B. That leaves open the possibility of making some richer data compositional. In this talk I will sketch how it is useful to regard a classical proof as a distributed strategy. In this way we can obtain a compositional proof of Herbrand’s theorem. The `true concurrency’ in the title refers to the approach to distributed computation initiated by Carl Adam Petri; in modelling a proof as distributed computation we shall take careful account of the causal dependencies between events intrinsic to the proof. In effect, we exhibit the computational content of a classical proof as a distributed computation. (The talk is based on joint work with Aurore Alcolei and Pierre Clairambault at ENS Lyon, and Martin Hyland at the University of Cambridge.)