Rencontre, Nov. 24, 2022

Cette rencontre se tiendra à Paris. plus précisément à l'amphithéâtre Pierre-Gilles de Gennes au rez-de-chaussée du bâtiment Condorcet, sur le campus des Grands Moulins, non loin de Sophie Germain, arrêt Bibliothèque F. Mitterrand (métro 14 ou RER C).

Un accueil sera proposé à partir de 10h.


10:00 – 10:30
10:30 – 11:30
13:30 – 14:30
Giulio Guerrieri (LIS, Aix-Marseille Université)

The semantics of the untyped (call-by-name) lambda-calculus is a well developed field built around the concept of solvable terms, which are elegantly characterized in many different ways. In particular, unsolvable terms provide a consistent notion of meaningless term. The semantics of the untyped call-by-value lambda-calculus (CbV) is instead still in its infancy, because of some inherent difficulties but also because CbV solvable terms are less studied and understood than in call-by-name. On the one hand, we show that a carefully crafted presentation of CbV allows us to recover many of the properties that solvability has in call-by-name, in particular qualitative and quantitative characterizations via multi types. On the other hand, we stress that, in CbV, solvability plays a different role: identifying unsolvable terms as meaningless induces an inconsistent theory.

This is joint work with Beniamino Accattoli, published at ICFP 2022

15:00 – 16:30
Hugo Herbelin (INRIA)

Completeness of first-order logic against Tarski semantics, that is Gödel's completeness theorem, has been abundantly studied in the context of classical and intuitionistic reverse mathematics in either second-order arithmetic or set theory, sometimes with inconsistent results (e.g. Krivine asserting it is fully constructive, Kreisel deriving Markov's principle, McCarty asserting it requires excluded-middle, Simpson asserting it is classically Weak Kőnig Lemma, Henkin that it is classically the Ultrafilter Theorem, etc.).

We will survey these results, sorting out the reasons for these apparently inconsistent results, eventually clarifying that completeness with respect to Tarski semantics over recursively enumerable theories intuitionistically requires:

  • a purely intuitionistic (unexpected) predicative form of the Weak Fan Theorem for dealing with the underlying logical structure and the negative connectives,
  • Markov's Principle for dealing with positive/additive falsity,
  • a form of Double Negation Shift for dealing with positive disjunction.

Interestingly, Markov's Principle and Double Negation Shift are weakly classical principles which preserve the witness and disjunction properties, and thus, are in this sense "valid" intuitionistic principles.