Oskar Becker
Leave a reply
Category Archives: Logique
Philosophy and logic in central Europe from Bolzano to Tarski
Probability theory and the undefinability of truth
Logica universalis : towards a general theory of logic
CCC : cartesian closed category (catégories cartésiennes fermées)
Une catégorie est dite
cartésienne
si elle possède un objet terminal et si tout couple d’objets possède un produit.
https://fr.m.wikipedia.org/wiki/Catégorie_cartésienne
https://fr.m.wikipedia.org/wiki/Produit_(catégorie)
Rappel : objet terminal comme produit sont deux exemples de limites d’un diagramme
Un objet terminal (c’est à dire tel qu’il existe une flèche unique dirigée de tout objet de la catégorie vers cet objet terminal) est limité du diagramme vide (“goutte de néant qui manque à la mer”), un produit de deux objets est la limite du diagramme formé par ces deux objets uniquement (sans flèches)
Une catégorie cartésienne est dite fermée si elle est aussi munie de l’exponentiation, si pour tout couple d’objets Z et Y il existe un objet exponentielle ZY
https://fr.m.wikipedia.org/wiki/Objet_exponentiel
La page en anglais sur les CCC est nettement meilleure:
https://en.m.wikipedia.org/wiki/Cartesian_closed_category
Une exponentielle est définie aussi comme limite d’un diagramme:
On comprend plus facilement si l’on regarde ce qui se passe dans le cas de la catégorie des ensembles (qui est un topos, donc possède toutes les limites finies, donc est une CCC):
Si Z et Y sont des ensembles, objets du topos Ens, alors :
ZY est l’ensemble des applications (des flèches, des fonctions) de Y vers Z
ZY = {f | f: Y——-> Z}
La flèche (la fonction, dans le cas des ensembles) eval :
eval : ZY × Y ——–> Z
est la fonction évaluation qui envoie un couple (f, y) sur la valeur de f au point y qui est f(y) et appartient par définition à Z
Et l’application
λg : X ——> ZY
(Notation venant du λ-calcul, voir https://fr.m.wikipedia.org/wiki/Lambda-calcul)
est telle que:
λg(x)(y) = g(x,y)
C’est ce qu’on appelle en programmation la forme curryfiée de g
https://fr.m.wikipedia.org/wiki/Curryfication
A noter qu’une adjonction apparaît, dans le cas d’une CCC (munie d’exponentielle pout tout couple d’objets) : le foncteur qui envoie Z sur ZY est adjoint à droite du foncteur qui envoie A sur A × Y
Et cette adjonction est caractérisée par la bijection naturelle entre les ensembles de flèches :
Plan de travail sur les topoi et les n-topoi
Notes on topos theory
Ces notes passent en revue divers aspects des topoi, notamment les deux sortes de définitions (elementary topoi et Grothendieck topoi) et abordent les aspects logiques liant logique et topologie.
http://rin.io/swashbuckling-topoi/
Et il y a des tas de liens dans le corps du texte, notamment un cours d’introduction:
http://www.fuw.edu.pl/~kostecki/ittt.pdf
une introduction informelle de Leinster:
http://arxiv.org/pdf/1012.5647.pdf
et un article d’Awodey sur les connections entre géométrie, algèbre et logique : “Type theory and homotopy”:
Approche covariante : “a topos for algebraic quantum theory” (Spitters, Heunen, Landsman)
La nature duale de la théorie des topoi: géométrique et logique
Je rappelle l’existence de cet article “Locales and toposes as spaces”:
http://www.cs.bham.ac.uk/~sjv/LocTopSpaces.pdf
dont j’avais parlé ici:
https://mathesisuniversalis2.wordpress.com/2015/04/08/topoi-de-grothendieck-2-la-double-origine-geometrique-et-logique-de-la-theorie-des-topoi/
double nature qui correspond aux deux créateurs de la théorie des topoi : Grothendieck (pour la géométrie algébrique, qui n’est rien d’autre que la continuation des travaux de Descartes) et William Lawvere (pour la logique).
Et le fait que Lawvere ait donné cette année un cours spécial sur Grothendieck et la conception moderne de l’espace est hautement significatif :
http://ct2015.web.ua.pt/abstracts/lawvere_b.pdf
La mathématique est le domaine de l’unification comme l’indique d’ailleurs Lawvere lui même à propos de la création de la théorie des catégories par Mac Lane et Eilenberg (page 3 de l’interview suivante):
Henosophia Τοποσοφια οντοποσοφια μαθεσις uni√ersalis ενοσοφια 