L’instruction fork et le principe d’induction en réalisabilité classique

Carte non disponible
Speaker Home page :
Speaker :
Speaker Affiliation :

()

Date/heure
Date(s) - 24/09/2015
11 h 00 min - 12 h 00 min

Catégories


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.

Webpage« >Webpage


Retour en haut 

Secured By miniOrange