Prise de vue et montage : S. Dugowson

The notion of classifying topos

Introduction to categorical and topos‐theoretic semantics: the notion of geometric theory, syntactic categories, construction of classifying toposes for geometric theories via syntactic sites, universal models and representability, theories classified by a presheaf topos and their quotients.

Introduction

Logique du 1er ordre

Langage du premier ordre (signatures, termes, formules atomiques...)

Connecteurs logiques et quantificateurs

Théories géométriques

Remarques

notation des séquents

Le vrai, le faux

Théories : les algébriques, les cartésiennes, les régulières et les "cohérentes".

Note du webmaster : je comprends bien que la dénomination "théorie cohérente" s'accorde avec celle de "faisceau cohérent" en géométrie algébrique (remarque de Laurent Lafforgue), il n'empêche que dans un contexte logique cela sonne tout de même bizarrement, surtout pour les théories qui se retrouvent "incohérentes". On ne peut que s'incliner devant l'usage, mais je prends sur moi de signaler la chose en mettant pour cette fois des guillemets à "cohérent".

Démontrabilité (+ retour sur les différents fragments de la logique du 1er ordre)

Interprétation

Sigma-structures (et morphismes entre elles)

Modèles

Foncteur T-mod, théorème de Joyal-Reyes (1977) & topos classifiants.

Morleyisation, ou pourquoi l'hypothèse "géométrique" n'est pas si contraignante

Topos "à 2 valeurs"

A propos des démonstrations de complétude

Construction du topos classifiant

Construction de la catégorie syntaxique

Construction de la topologie de Grothendieck syntaxique

Remarque sur les topos classifiants

Construction du modèle universel

Puissance de la non-canonicité : l'intérêt de varier les logiques

puisque la construction précédente fonctionne aussi pour les autres fragments de la logique géométrique...

... cela peut donner diverses constructions du topos classifiant d'une même théorie

Exemples

propriétés de compacité pour les théories "cohérentes"

(revoir les explications données hier sur le foncteur : site -> topos obtenu en composant Yoneda avec la faisceautisation).

Exemple 2, en logique cartésienne

(panne sèche, changement de bobine :)