Partenaires

logo Sphere
CNRS
Logo Université Paris-Diderot Logo Université Paris1-Panthéon-Sorbonne


Rechercher

Sur ce site

Sur le Web du CNRS


Accueil > Colloques, journées d’étude, conférences > The singularity of forcing

The singularity of forcing


Wednesday May 29, 2019


Study Day
Room Dali, 240A, Building Condorcet, level 2,
University Paris Diderot*



PROGRAM

  • 9:00–10:30 Mirna Dzamonja (IHPST)
    Le forcing et la logique du premier ordre
  • 10:45–12:15 Boban Velickovic (IMJ-PRG)
    The dogmas of set theory
  • 14:00–15:30 Luc Pellissier (IRIF)
    Du calcul pour compléter le forcing
  • 15:45–17:15 Guilhem Jaber (LS2N)
    Un tour d’horizon du forcing en théorie des types
  • 17:30–19:00 Jean-Michel Salanskis (IRePh)
    Le forcing dans tous ses états



ABSTRACTS

  • 9:00–10:30 Mirna Dzamonja (IHPST)
    Le forcing et la logique du premier ordre
    Pour comprendre en quoi le forcing est spécial par rapport d’autres dérivés de l’indépendance, si en effet il l’est, il convient de se rappeler un autre objet, tout aussi spécial et en relation proche avec le forcing. Il s’agit de la logique classique du premier ordre. Malgré le travail profond et productif dans le domaine de la logique abstrait, la logique du premier ordre reste la seule d’avoir toutes les propriétés qui font d’elle un outil indispensable pour les applications de logique en mathématiques : la complétude, la compacité et la propriété de Löwenheim-Skolem. En effet, elle est la maximale avec ces propriétés (Lindström). Sa sémantique et sa syntaxe sont parfaitement reliées. Si, par exemple, la logique du deuxième ordre est très expressive et assez catégorique, elle n’est pas un outil mathématique, car il lui manque des propriétés convenables, comme la compacité.
    Le forcing est une technique pour démontrer l’indépendance en s’appuyant sur la logique du premier ordre. Il obéit au théorème du forcing, ce qui donne une traduction entre la sémantique du départ et celle de l’extension par forcing. Il préserve la relation entre la syntaxe et la sémantique. Cela fait de forcing un outil mathématique, ce qui le distingue d’autres outils d’indépendance. Il n’est pas le plus général, mais il a de la flexibilité qui le rend utile.
  • 10:45–12:15 am, Boban Velickovic (IMJ-PRG)
    The dogmas of set theory
    Set theory plays a dual role in mathematics. On one hand it is used as the foundations for all of mathematics and on the other it is a subject in its own right with its problems and techniques.
    From the foundational point of view the key questions are how to cope with the incompleteness phenomenon in mathematics and how to justify the consistency or even ’truth’ of strong theories.
    Over the years some beliefs have emerged that technical notions and tools, such as large cardinal axioms and the method of forcing, can provide answers to these foundational problems.
    We examine the resulting dogmas and try to formulate precise mathematical statements about them.
  • 2:00–2:30 Luc Pellissier (IRIF)
    Du calcul pour compléter le forcing
    La présentation catégorique du forcing possède des extensions naturelles, dans lesquelles l’ensemble des conditions de forcing sont remplacées par des structures plus générales.
    Suivant des résultats autour de la réalisabilité classique, nous verrons que ces structures doivent laisser une place au calcul au sein des preuves.
  • 3:45–5:15 Guilhem Jaber (LS2N)
    Un tour d’horizon du forcing en théorie des types
    Dans cet exposé, nous nous intéresserons au forcing vu comme une traduction syntaxique de preuves, suivant en cela les travaux de Krivine et Miquel.
    Nous nous placerons dans le cadre de la théorie des types dépendants de Martin-Löf, et plus précisément dans le Calcul des Constructions introduit par Coquand comme cadre logique à l’assistant de preuves Coq. Nous verrons comment le forcing vu comme traduction permet d’étendre Coq avec de nouveaux principes de raisonnements, tout en conservant ses propriétés essentielles : correction, canonicité et décidabilité de la vérification des preuves.
    De plus, suivant la correspondance preuves/programmes de Curry-Howard, nous présenteront le contenu calculatoire du forcing dans ce cadre, qui correspond à une version monotone de la monade de lecture (‘reader monad’).
    Nous considérerons d’abord la traduction de forcing venant de la reformulation du forcing dans les modèles de (pré)-faisceaux. Cependant, cette traduction souffre de problèmes de cohérences, dus au fait que la théorie des types considérées est intensionnelle. En décomposant cette traduction en utilisant le ‘call-by-push-value’ de Levy, nous verrons que cette traduction est en appel par valeur, mais qu’il existe une autre traduction, plus mystérieuse, en appel par nom, qui ne souffre pas de ces problèmes de cohérence.
    Nous nous intéresserons de plus aux liens entre ces traductions de forcing définies pour la théorie des types et les définitions sémantiques usuelles du forcing en théorie des ensembles.
  • 5:30–7:00 Jean-Michel Salanskis (IRePh)
    Le forcing dans tous ses états
    Il peut sembler raisonnable, dans la réception du travail pionnier de Cohen, de comprendre le forcing comme une technique assurant une sorte de médiation ou de transition entre le régime constructif et le régime “corrélatif” de la théorie des ensembles.
    Cette interprétation philosophique garde-t-elle sa valeur lorsqu’on prend en considération d’autres versions du forcing, comme celle qui s’installe dans le langage de la théorie des modèles, autrefois proposée par Robinson, celle qui se tient dans le cadre des théories constructives, exposée par Beeson, ou celle qui se situe dans le contexte catégorique, plus spécialement dans celui des topos ?
    On voudrait essayer de répondre à une telle question, tout en s’efforçant de dégager, peut-être, d’autres éléments philosophiques caractéristiques de la technique ou du dispositif du forcing.



ORGANISATION
Thomas Tulinski (ENS Lyon, SPHERE)






University Paris Diderot – CNRS
Laboratoire SPHERE - UMR 7219
Building Condorcet, 4, rue Elsa Morante
75013 Paris


Access map


Metro line 14 & RER C / Stop : Bibliothèque François Mitterrand
Metro line 6 / Station : Quai de la Gare
Bus 62 & 89 / Stop:Bibliothèque rue Mann
Bus 64 / Stop : Tolbiac-Bibliothèque François Mitterrand
Bus 325 / Stop : Watt