|
|
 |
|
Vendredi 9 Septembre
| Heure: |
10:30 - 12:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Les algèbres implicatives, d'après A. Miquel (1ère partie) |
| Description: |
Luc Pellissier Les structures implicatives sont des structures algèbriques extrèmement simples
généralisant à la fois les modèles dénotationnels du ?-calcul et les algèbres de
Heyting. Elles permettent donc d'interpréter à la fois les termes et les types,
qui se retrouvent ainsi identifiés.
Les structures implicatives sont donc une fondation naturelle pour le forcing
(où l'on interprète les formules dans des algèbres de Boole dans le cas
classique ou de Heyting dans le cas intuitionniste) et la réalisabilité (où
l'on interprète les formules par des ensembles de ?-termes). On verra qu'en
effet, une structure implicative munie d'un quotient adéquat engendre un tripos,
c'est-à-dire un modèle de la logique intitutionniste d'ordre supérieure
(imprédicative). |
|
|
