Théorie du premier ordre associée à une esquisse,
par Alain Molinier
(30 janvier 2019)
Prise de vue, séquençage et mise en page web : S. Dugowson
Cet exposé fait suite à celui fait au séminaire CLE le 14 novembre 2018 par Alain Molinier.
Le but de l'exposé : associer une théorie du 1er ordre à toute esquisse (et réciproquement)
Références
Voir aussi : Séminaire général de logique 1984
Pour la réciproque, on considérera l'exemple des théories algébriques : à toute théorie algébrique peut être associée une esquisse.
Question : retrouve-t-on la même théorie lorsqu'on considère la théorie du premier ordre associée à cette esquisse ?
Rappels sur les esquisses et sur les théories du premier ordre
Esquisses
Les esquisses sont des graphes à composition, avec la donnée de :
familles potentiellement monomorphes
familles potentiellement épimorphes
cônes projectif limites potentielles ( = cônes distingués)
cônes inductifs (co)limites potentielles ( = co-cônes distingués)
Théories du 1er ordre
Langage : sortes et variables, symboles fonctionnels et leurs profils, symboles relationnels et leurs profils,
Termes, construits par récurrence à partir des variables
Formules : formules atomiques, etc..
formules closes, axiomes
On part d'une esquisse, associons-lui une théorie du 1er ordre.
Aux objets on fait correspondre des sortes
Aux identités on associe des symboles fonctionnels
Symbole fonctionnel associé à une flèche
Traduction en axiomes des composées de flèches
Axiome associé à une famille monomorphe potentielle
Notion de familles monomorphe dans le cas de la catégorie des ensembles
Le produit est un cas particulier de famille monomorphe, et réciproquement, dans Ens, toute famille monomorphe est obtenue comme partie de produits.
Axiome associé à une famille monomorphe (de l'esquisse considérée)
Remarque : dans Ens, cas où l'ensemble d'indexation est vide.
Axiome associé à une famille épimorphe potentielle
Axiome associé à un "cône projectif limite potentielle" (= "cône distingué")
Remarque terminologique : A. Molinier parle de "cônes projectifs" pour désigner ce qu'ailleurs on appelle souvent des "cônes" (et à l'opposé, de "cônes inductifs" là où un autre usage parle de cocônes). Les "cônes projectifs potentiellement limites" (ou plutôt, puisqu'il le tourne ainsi : "cônes projectifs limites potentielles") s'identifient alors aux "cônes distingués", et les "cônes inductifs limites potentielles" aux "co-cônes distingués" (et on parle aussi de co-limites).
(N.D.S.D.)
Construction de la limite dans le cas de la catégorie des ensembles.
Construction de l'axiome associé à un "cône projectif potentiellement limite" de l'esquisse considérée
Remarque : cas (considéré dans la catégorie des ensembles) où la catégorie d'indexation est vide
Axiome associé à un "cône inductif limite potentielle" ( = "co-cône distingué")
I) Premier cas : J connexe et non réduit à 0 ou 1
Comment ça fonctionne dans le cas de la catégorie des ensembles ?
Zigzags
Axiome de la théorie associe à un "cône inductif limite potentielle" dans ce cas (J connexe ni 0 ni 1)
II) Deuxième cas : J est non connexe
Vous voulez que je l'écrive ?
non !
si !