Guillaume Geoffroy
I2M, Aix-Marseille Université
/user/guillaume.geoffroy/
Date(s) : 24/09/2015 iCal
11 h 00 min - 12 h 00 min
Je commencerai par quelques rappels sur les modèles de réalisabilité classique de l’arithmétique d’ordre 2, puis je montrerai le lien entre l’instruction « fork » (qui exécute deux sous-programmes en parallèle) et le principe d’induction :
Dans un modèle de réalisabilité, tous les axiomes de l’arithmétique de Peano d’ordre 2 sont réalisés, sauf éventuellement le principe d’induction. Autrement dit, un modèle de réalisabilité peut contenir à la fois des entiers naturels, qui vérifient le principe d’induction, et d’autres éléments « non entiers », qui ne le vérifient pas.
Le but est de montrer que le principe d’induction dans le modèle de réalisabilité (c’est-à-dire l’énoncé « tous les éléments du modèle de réalisabiilité sont des entiers naturels ») est équivalent, dans un sens à préciser, à la présence de l’instruction « fork ». On peut par ailleurs montrer (mais ce n’est pas l’objet de l’exposé) que l’instruction « fork » est présente si et seulement si le modèle de réalisabilité est en fait un modèle de forcing.
Catégories