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 !

Chemin réciproque : on part maintenant d'une théorie (algébrique = équationnelle)...

Discussion : Camell Kachour, Christian Lair, Anatole Khélif, ...

Table des matières détaillée