Séminaire, 10 mars 2016
Le matin, nous serons a priori en salle B1 (4ème étage). L'après-midi, nous serons en amphi B (3è étage).
Programme
- 10:30 – 12:00
-
Laurent Regnier (Univ. Aix-Marseille)
Realisability was originally designed by Kleene in order to build models of intuitionistic arithmetic (Heyting Arithmetic) as a kind of synthesis between Gödel's Dialectica interpretation and Brouwer-Heyting-Kolmogorov interpretation. Indeed the basic idea is to extend the notion of justifications of mathematical statements from (formal) proofs to programs thus defining the notion of a formula justified (proved) by a program.
Kleene used (indices of) recursive functions for his programs, but rapidly realisability was adapted to other formalisms, mostly based on lambda-calculus. Also realisability was soon seen to be also extendable to classical theories, but not as a primitive notion since one has to use a Gödel's like not-not-translations to transfer the semantics from intuitionnistic to classical logic.
It is thus not a small achievement that Krivine at the end of the nineties could define a direct notion of realisability for classical logic. In a first step the semantics was defined for higher order arithmetic, then further extended to full set theory by finding realisers for each axioms of ZF. Interestingly enough these realisers are all very simple programs, but the one for the extensionality axiom which implements a real algorithm (essentialy a while loop).
The so-called classical realisability thus allows to define new semantics for arithmetic, analysis and now set theory in which the truth value of a formula is the set of its realisers. Krivine has shown that this construction can be seen as an extension of Cohen's forcing, but with some very new properties (eg, contrarily to forcing, ordinals are not preserved between the base model and the realisability model) that are almost all yet to be discovered and understood...
- 14:00 – 15:00
-
Julien Melleray (Univ. Lyon 1)
Abstract: A common theme in mathematics is to try and find complete invariants for various classification problems (typically, one tries to understand isomorphism between some mathematical structures). One would then like to know whether the invariants used are as simple as possible; namely, one would like to know the precise complexity of the classification problem under consideration. There are many ways to address this type of question; I will try to motivate and explain the point of view of Borel complexity, focusing on classification problems induced by a group action, hoping to give an idea of the overall picture and of some open problems. The talk will be introductory and the speaker will aim at making it as self-contained as possible.
- 15:30 – 16:30
-
Pierre Simon (Univ. Lyon 1)
Je présenterai les structures NIP : structures dans lesquelles les
familles d'ensembles définissables sont de VC-dimension finie.
J'expliquerai ensuite en quoi elles sont liées à des résultats de
régularité pour des familles particulières de graphes.
