×

Trames et sémantiques catégoriques des systèmes de trames. (Screens and categorical semantics of systems of screens). (French) Zbl 0672.18001

Diagrammes 18, CL1-CL47 (1988).
On sait qu’une esquisse [voir Ch. Ehresmann, Bul. Inst. Politeh. Iaşi, New Ser. 14(18), No.1/2, 1-14 (1968; Zbl 0196.031)] est une présentation diagrammatique (ou catégorique, ou grapico- équationnelle) d’un genre de structures donné. Précisément, les modèles (ou réalisations) d’esquisses sont exactement les modèles de théories du premier ordre. Nous introduisons ici la notion de trame, plus générale que celle d’esquisse: une trame est encore une présentation diagrammatique d’un genre de structures donné, mais cette fois d’ordre supérieur. Nous prouvons cependant que la structure de trame, tout comme celle d’esquisse, est encore projectivement esquissable, i.e. est essentiellement algébrique.
On sait que les catégories cartésiennes fermées ou les topos (ou d’autres catégories munies d’une structure supplémentaire d’un certain genre) peuvent être considérées comme des modèles catégoriques convenables pour faire de la logique catégorique du premier ordre. Ce sont, en fait, des structures essentiellement algébriques, puisque modèles d’une esquisse projective particulière (qui est sur-esquisse de l’esquisse de catégorie), et les “propriétés logiques” de ces catégories sur-structurées particulières sont, en réalité, étroitement liées à la seule nature universelle (ou co-universelle) des constructions de types (i.e. d’objets) que le genre de sur-structure considéré permet.
Nous introduisons ici la notion de sémantique catégorique d’un système de trames donné: ce sont exactement les catégories munies de constructeurs de types universels et/ou co-universels, mais cette fois d’ordre supérieur. Ainsi, par exemple, les catégories où l’on peut faire de la logique d’ordre supérieur (par exemple du \(\lambda\)-calcul du deuxième ordre) sont exactement les sémantiques catégoriques d’un certain système de trames. Nous prouvons, surtout, que ce genre de catégories sur-structurées est encore projectivement esquissable, i.e. qu’il s’agit encore de structure essentiellement algèbriques (dont beaucoup s’évertuent à chercher, dans la pratique particulière, des “présentations équationnelles”... que les présentes considérations fournissent donc automatiquement).

MSC:

18C99 Categories and theories
18D99 Categorical structures
03G30 Categorical logic, topoi
18A10 Graphs, diagram schemes, precategories

Citations:

Zbl 0196.031
Full Text: EuDML