Quatrième exposé : introduction à la logique catégorique

David A. Madore

23 novembre 1998

1 Motivations

La logique catégorique étudie à la fois l’aspect syntaxique et l’aspect sémantique de la logique. Dans l’étude de l’aspect sémantique, on cherche des catégories dont les objets et les flèches représentent les objets d’étude du système formel (typiquement, les ensembles). Dans l’étude de l’aspect syntaxique, les objets des catégories sont censées être des propositions et les flèches des démonstrations entre de ces propositions. En ce qui concerne l’étude de l’aspect sémantique, un type de catégories jouera un rôle essentiel, ce sont les topoi, originalement introduits par Grothendieck dans l’étude des topologies étale et plate des schémas. Les catégories utilisées dans la considération de la syntaxe ont moins été étudiées, et notamment celles qui servent pour le calcul des prédicats n’ont à ma connaissance pas été convenablement formalisées. On ne pourra donc donner ici qu’un aperçu assez sommaires de ces questions. Les topoi et les faisceaux sur les topologies de Grothendieck et de Lawvere-Tierney feront l’objet d’un exposé à part.

Il existe en logique catégorique un lien surprenant entre la syntaxe et la sémantique, c’est que les topoi sont des cas particuliers des catégories bicartésiennes closes utilisées dans l’étude de la syntaxe. Par ailleurs, lorsqu’on en écrit les objets et les flèches au moyen d’une notation appelée notation lambda, ces catégories bicartésiennes closes présentent une forte parenté avec le lambda-calcul typé. C’est cette ubiquité fondamentale qui constitue le début de ce qu’on appelle l’isomorphisme de Curry-Howard. Celle-ci n’est pas sans application pratique, puisque c’est elle qui sous-tend certains programmes informatiques de vérification formelle des démonstrations et de certification des programmes, comme le programme Coq développé par l’INRIA (dont la catégorie possède des propriétés supplémentaires admirables, comme celle d’admettre des constructions inductives positives arbitraires).

Sur le plan de la pure logique, la logique catégorique (des prédicats) est une logique très forte, qui contient strictement la logique du premier ordre, du second ordre, et même d’ordre n pour tout n : c’est une logique à types, dans laquelle on dispose du produit, coproduit et de l’exponentielle de deux types quelconques. C’est une logique naturellement intuitionniste (c’est-à-dire qu’elle ne vérifie pas le principe du tertium non datur ¬¬A ⇒ A), et on peut même décrire de façon naturelle dans les mêmes lignes des logiques plus faibles comme la logique linéaire, ou encore des logiques plus complexes comme la logique modale.

Sur le plan épistémologique, certains y voient une façon de libérer les mathématiques de la tyrannie du “paradis Cantorien”, la théorie des ensembles, à laquelle on reproche de trop se concentrer sur les codages particuliers des objets d’étude, plutôt que sur leurs propriétés. (Aus diesem Paradies, daß Cantor uns geschaffen, sollen wir endlich vertrieben werden.)

2 Catégories cartésiennes et cartésiennes closes

On veut considérer une catégorie dont les objets soient des propositions et les flèches A → B des démonstrations de B partant de A. On pourrait se contenter de considérer “brutalement” les telles démonstrations, et définir la composée de deux flèches A → B et B → C comme la démonstration de C à partir de A obtenue en mettant bout à bout les deux démonstrations. Un tel procédé n’a qu’un intérêt limité : par exemple, aucune flèche sauf les identités ne sera inversible, et aucun objet ne vérifie aucune propriété universelle intéressante.

Considérons le cas du ET logique : il est clair que proposer une démonstration de A∧B à partir de S c’est “la même chose” que proposer une démonstration de A à partir de S ainsi qu’une démonstration de B à partir de S. C’est-à-dire que non seulement on demande une règle de logique permettant de former une démonstration (u, v): S ⊢ A ∧ B à partir de u: S ⊢ A et v: S ⊢ B, mais on demande aussi d’identifier la démonstration u avec la démonstration composée de (u, v) par la démonstration triviale p_{1} : A ∧ B ⊢ A, et de même pour v. Et on demande encore que (u, v) soit la seule démonstration de A∧B à partir de S ayant cette propriété. Ce sont là des identifications raisonables entre démonstrations. Les ayant fait, on remarque alors que A ∧ B vérifie précisément la propriété universelle d’un produit de A et B : on a un isomorphisme naturel Hom(S, A∧B) ≅ Hom(S, A)×Hom(S, B).

Il en va de même du VRAI : une démonstration S ⊢ ⊤ n’apporte rien d’informatif, et on souhaite donc toutes les identifier. Lorsqu’on le fait, le ⊤ devient un objet universel dans la catégorie étudiée. Celle-ci admet donc des produits finis quelconques.

Ceci nous conduit à définir une catégorie cartésienne comme une catégorie admettant un objet terminal et des produits binaires (i.e. des produits finis quelconques). En fait, ceci n’est pas très satisfaisant. Plutôt que de supposer l’existence de ces produits, on préférera se les donner. Soit : Définition 2.1. On appelle catégorie cartésienne une catégorie C munie d’un foncteur ⊤: 1 → C (identifié à un objet de C) et d’un foncteur ∧: C^{2} → C qui définissent respectivement un objet universel (i.e. terminal) ⊤ de C et un produit A∧B pour tous objets A, B de C (pour être encore plus pédant, ce sont donc des adjoints à droite respectivement du foncteur trivial C → 1 et du foncteur diagonal C → C^{2}).

La propriété universelle de l’implication est plus subtile. Il faut la voir dans le théorème de déduction : il revient au même de se donner une démonstration A ∧ B ⊢ C qu’une démonstration A ⊢ B ⇒ C (si on veut démontrer B ⇒ C, on suppose que B est vrai et on démontre C). On recheche donc un isomorphisme naturel

Hom(A ∧ B, C) ≅ Hom(A, B ⇒ C)

Ou encore : l’objet B ⇒ C est un objet qui représente le foncteur A ↦ Hom(A∧B, C). (En particulier, une démonstration de B ⇒ C à partir de ⊤, i.e. de rien du tout, correspond naturellement à une démonstration de C à partir de B : c’est pourquoi B ⇒ C s’appelle souvent un objet “Hom interne”.) Cette propriété est une adjonction de foncteurs : le foncteur ⇒ est adjoint à droit du foncteur ∧ (par rapport à la deuxième variable, c’est-à-dire que B ⇒ est adjoint à droite de ∧B).

On est donc conduit à la définition suivante : Définition 2.2. On appelle catégorie cartésienne close une catégorie cartésienne C munie d’un foncteur ⇒: C^{2} → C adjoint à droite par rapport à la deuxième variable du foncteur ∧.

(Le terme “close” vient de ce que B ⇒ C peut être considéré comme un produit de copies de C indicées non pas par un certain ensemble mais par l’objet B.)

On rappelle certaines identités valables dans toute catégorie cartésienne close : (A ∧ B) ∧ C ≅ A ∧ (B ∧ C) (naturellement en A, B et C, et de plus cet objet représente un produit triple), A ∧ B ≅ B ∧ A (naturellement en A et B), A ∧ ⊤ ≅ A (naturellement en A), A ⇒ ⊤ ≅ ⊤ (naturellement en A), ⊤ ⇒ A ≅ A (naturellement en A), A ⇒ B ∧C ≅ (A ⇒ B)∧(A ⇒ C) (naturellement en A, B, C), A∧B ⇒ C ≅ A ⇒ B ⇒ C (isomorphisme de curryfication/décurryfication, naturel en A, B, C).

On rappelle que d’un ensemble partiellement ordonné on peut faire une catégorie en décrétant qu’il y a une unique flèche A → B si et seulement si A ≤ B. Dans ce cas, un objet terminal est précisément la même chose qu’un plus grand élément. Le produit binaire A∧B est la même chose que l’inf de l’ensemble {A, B} (i.e. le produit est représentable si et seulement si l’inf existe, et dans ce cas ils coïncident). Un ensemble partiellement ordonné est donc une catégorie cartésienne si et seulement si il a un plus grand élément et que toute partie à deux éléments (donc toute partie finie) admet une borne inférieure. Dans ces conditions, B ⇒ C est alors (s’il existe) la borne supérieure des A tels que inf(A, B) ≤ C.

Parmi les catégories cartésiennes closes, on en signalera une particulièrement importante : c’est celle qui se déduit de l’ensemble partiellement ordonné {0, 1} : elle a deux objets, 1 = ⊤ et 0 = ⊥ avec pour seule flèche hormis les identités une flèche 0 → 1. On la notera 2. Les tables des opérations ∧ et ⇒ sont les tables habituelles.

3 Foncteurs logiques et constructions coüniverselles

La définition d’un morphisme entre catégories cartésiennes ou cartésiennes closes ne fait aucun doute, c’est un foncteur qui préserve les opérations définies sur la catégorie : Définition 3.1. Soient C et D des catégories cartésiennes (resp. cartésiennes closes). On appelle foncteur logique (strict) un foncteur F: C → D qui commute aux foncteurs ⊤ et ∧ (resp. ⊤, ∧ et ⇒). Avec ces morphismes, les catégories cartésiennes (resp. cartésiennes closes) forment une catégorie notée Cart (resp. CartC).

La raison du mot “strict” est que, pour faire les choses vraiment correctement, il vaudrait mieux se contenter de demander que le foncteur commute aux connecteurs à isomorphisme près, c’est-à-dire se donner un foncteur F: C → D ainsi que des isomorphismes naturels F (⊤) ≅ ⊤, F (A∧B) ≅ F (A)∧F (B), et éventuellement F (A ⇒ B) ≅ F (A) ⇒ F (B), la composition étant alors donnée de façon relativement claire. Dans ce cas, on est obligé de considérer aussi les morphismes entre tels foncteurs (transformations naturelles), et on obtient finalement une 2-catégorie des catégories cartésiennes (resp. des catégories cartésiennes closes), notée ℭ𝔞𝔯𝔱 (resp. ℭ𝔞𝔯𝔱ℭ). La catégorie définie ci-dessus en est une strictification (note : je ne sais pas du tout ce que c’est mais je suis sûr que ça doit être ça). En l’occurrence, on n’a pas besoin de s’encombrer de tels détails car la strictification marche très bien dans le contexte présent.

L’idée intuitive est qu’un foncteur logique apporte éventuellement de nouvelles propositions à la catégorie cartésienne close, éventuellement de nouvelles démonstrations (axiomes), donc éventuellement des identifications nouvelles entre les propositions, mais que tout ce qui était vrai dans C reste vrai dans D. On dit encore que la catégorie D (avec le foncteur F) est un modèle de la catégorie C. Lorsque la catégorie D est 2, on parlera d’un choix binaire de valeurs de vérité (on notera que lorsque F (A) = 1 et qu’on a une flèche A → B dans C alors on a aussi F (B) = 1).

Si un foncteur logique apporte de nouvelles propositions et de nouveaux axiomes, on peut s’attendre à ce que l’objet initial de la catégorie Cart ou CartC ne possède aucun axiome et ne possède que les propositions qui sont nécessaires. C’est effectivement le cas. D’ailleurs, cet objet initial est bien peu intéressant puisqu’il n’a qu’un objet, à savoir ⊤, et une seule flèche, l’identité sur ⊤. Nettement plus intéressantes sont les catégories obtenues en rajoutant librement des variables propositionnelles, que nous décrivons maintenant. Définition 3.2. Soit n ∈ ℕ. On note Cart(P_{1}, …, P_{n}) (resp. CartC(P_{1}, …, P_{n})) la catégorie dont les objets sont les catégories cartésiennes (resp. cartésiennes closes) munies de n objets P_{1}, …, P_{n}, et dont les flèches sont les morphismes logiques entre telles catégories qui préservent P_{1}, …, P_{n}.

L’objet initial de Cart(P_{1}, …, P_{n}) (resp. CartC(P_{1}, …, P_{n})) est la catégorie cartésienne (resp. cartésienne close) librement engendrée par les variables propositionnelles P_{1}, …, P_{n}, sans aucune relation entre elles, i.e. sans aucun axiome les liant. Théorème 3.3. La catégorie Cart(P_{1}, …, P_{n}) (resp. CartC(P_{1}, …, P_{n})) admet un objet initial noté cart[P_{1}, …, P_{n}] (resp. cartC[P_{1}, …, P_{n}]). On l’appelle catégorie cartésienne (resp. cartésienne close) librement engendrée par les variables propositionnelles P_{1}, …, P_{n}.

(La démonstration est formelle ou bien découle de théorèmes archi-généraux, et que personne n’a jamais énoncé, sur la libre génération des structures. On invite le lecteur à s’en convaincre en répétant un nombre suffisant de fois les mots magiques “Sétrive Yahl”.)

Pour faire les choses vraiment correctement, il faudrait plutôt considérer un objet 2-initial de la catégorie ℭ𝔞𝔯𝔱(P_{1}, …, P_{n}) (resp. ℭ𝔞𝔯𝔱ℭ(P_{1}, …, P_{n})). Il faut cependant noter qu’en faisant ça on perd la notion précise d’égalité entre objets et on ne garde vraiment qu’une existence ou non d’isomorphismes.

On peut non seulement fabriquer des catégories cartésiennes (resp. cartésiennes closes) librement générées à partir de variables propositionnelles, mais aussi rajouter librement des variables propositionnelles, ou bien des axiomes à une catégorie cartésienne (resp. cartésienne close) existant. Théorème 3.4. Soit C une catégorie cartésienne (resp. cartésienne close), n, k ∈ ℕ, et Q_{1}, …, Q_{k} des objets de C. On note Cart(C, P_{1}, …, P_{n}, x_{1} : Q_{1}, …, x_{k} : Q_{k}) (resp. CartC(…)) la catégorie dont les objets sont les foncteurs logiques F: C → D, la catégorie D étant munie d’objets P_{1}, …, P_{n} et de flèches x_{1}, …, x_{k}, avec x_{i}: ⊤ → F (Q_{i}), les morphismes étant les foncteurs logiques D → D′ qui préservent toutes ces données. Alors cette catégorie a un objet initial, noté C[P_{1}, …, P_{n}, x_{1} : Q_{1}, …, x_{k} : Q_{k}].

Bien sûr, on peut rajouter librement un axiome x: A → B puisque cela revient exactement à rajouter x: ⊤ → A ⇒ B, en vertu du théorème de déduction. Par ailleurs, il est trivial ( ?) que les objets de C[x_{1} : Q_{1}, …, x_{k} : Q_{k}] sont les mêmes que les objets de C.

On a le résultat important suivant : Théorème 3.5 (complétude fonctionnelle). Soit C une catégorie cartésienne (resp. cartésienne close), et A un type de C. Soit f′ une flèche B → C de la catégorie C[x : A]. Alors il existe une unique flèche f: A ∧ B → C (ou, ce qui revient au même, dans le cas cartésien clos, B → A ⇒ C) de C telle que f′ = f(x), avec l’abus de notation évident.

(C’est intuitivement évident : postuler un nouvel axiome x qui affirme A permet de démontrer précisément les choses qu’on sait montrer à partir de A.)

Ainsi, la catégorie C[x : A] peut se construire très facilement comme catégorie coslice sur A, c’est-à-dire comme catégorie des flèches A → B dans C. Cette observation peut d’ailleurs, retrospectivement, servir à démontrer le théorème (3.4), auquel cas le théorème de complétude fonctionnelle est trivial.

(En fait, les catégories Cart et CartC admettent tous les coproduits finis. C’est clair... si on le veut vraiment.)

4 Notations des flèches et lambda-calcul

Plaçons-nous dans une catégorie cartésienne close C. Les objets de C seront appelés les types, et une flèche f: A_{1} ∧ ⋯ ∧ A_{n} → B sera appelé un terme de type B (à variables libres de types A_{1}, …, A_{n}). On remarque qu’on peut toujours rajouter des variables libres à un type, en composant par des flèches canoniques A → ⊤. Par ailleurs, on notera par des lettres comme x, y, z, … les termes identiques A → A de type A ayant une variable libre dans A.

Si g est un terme de type B ⇒ C et f un terme de type B (ayant certaines variables libres non précisées), soit g: Y → B ⇒ C et f: X → B, on peut construire un terme g^{∗}: Y × B → C et en composant en déduire un terme Y × X → C, donc de type C ayant les variables libres de f et g réunies, qu’on note gf et qu’on appelle application de g à f.

Attention : l’application n’est pas associative : lorsqu’on écrit hgf, c’est (hg)f qu’on entend et non pas h(gf). Au passage, signalons que quand on écrira A ⇒ B ⇒ C c’est A ⇒ (B ⇒ C) qu’on entend et non pas (A ⇒ B) ⇒ C.

En appliquant le théorème de déduction dans l’autre sens, on peut au contraire retirer des variables libres : si f: X ∧ A → B est un terme de type B ayant au moins une variable libre de type A (plus éventuellement d’autres non précisées), et qu’on a noté par x le terme identique de type A, on note λ[x : A].f le terme X → A ⇒ B de type A ⇒ B n’ayant plus la variable x de libre, obtenu par application du théorème de déduction. Cette opération lambda s’appelle l’abstraction (de la variable x).

Prenons un exemple très simple : si A est un type, alors x peut désigner le terme identique A → A (de type A ayant x comme variable libre de type A), et alors λ[x : A].x désigne un terme de type A ⇒ A sans variable libre (i.e. une flèche ⊤ → A ⇒ A), qu’on appelle abusivement l’identité sur A.

Un peu plus compliqué : si f est un terme de type A ⇒ B, alors λ[x : A].fx est précisément égal à f. En effet, fx désigne le terme de type B à variable libre x de type A obtenu par application du théorème de déduction dans un sens à partir de f, et λ[x : A].fx applique le théorème de déduction dans l’autre sens, donc on retombe sur f.

On vérifiera ainsi par exemple que les termes k_{A,B} = λ[x : A].λ[y : B].x et s_{A,B,C} = λ[x : A ⇒ B ⇒ C].λ[y : A ⇒ B].λ[z : A].xz(yz) sont des termes clos (i.e. sans variables libres) de types respectifs A ⇒ B ⇒ A et (A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C.

Par ailleurs, si u et v sont des termes de types respectifs A et B on note (u, v) le terme évident de type A ∧ B (dont les variables libres sont celles de u et celles de v). On se permettra aussi, un peu abusivement, des notations telles que λ[(u, v) : A ∧ B]. · · ·, pour désigner la chose évidente : l’opération qui consiste à passer de A ∧ B ⇒ X à A ⇒ B ⇒ X s’appelle la curryfication. On note enfin ⋆ le terme unique de type ⊤ (et qui a toutes les variables libres qu’on voudra bien lui prêter).

Il faut préciser que dans l’écriture d’un terme λ, on omet parfois abusivement l’indication du type de la variable abstraite. Par exemple, on dira que λx.x est un terme de type A ⇒ A (A étant un type non précisé), que λx.λy.x (aussi noté λxy.x) est un terme de type A ⇒ B ⇒ A, et que λxyz.xy(xz) est un terme de type (A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C. Les informaticiens connaissent des algorithmes (algorithmiquement complexes) permettant d’effectuer la résolution des types : on pourra par exemple utiliser le langage caml à cet effet.

Il faut dire à ce stade-là que la catégorie cartésienne close maternelle pour toutes ces opérations est la catégorie cartC[P_{1}, …, P_{n}] librement construite sur n types sans aucune information sur eux. Bien sûr, un terme de cette catégorie détermine un terme sur n’importe quelle catégorie cartésienne close munie de n types, d’après la propriété coüniverselle de cartC[P_{1}, …, P_{n}]. En fait, tout terme de cartC[P_{1}, …, P_{n}] peut être écrit avec les opérations que nous avons définies. Pour cette raison, on les appelle les termes du lambda-calcul libre sur les n types P_{1}, …, P_{n}.

Considérons maintenant les termes suivants :

\begin{aligned}i = λx.x & : A ⇒ A \\ k = λxy.x & : A ⇒ B ⇒ A \\ s = λxyz.xz(yz) & : (A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C \\ ⋆ & : ⊤ \\ π_{1} = λ(x, y).x & : A ∧ B ⇒ A \\ π_{2} = λ(x, y).y & : A ∧ B ⇒ B \\ p = λxy.(x, y) & : A ⇒ B ⇒ A ∧ B \end{aligned}

On les appelle axiomes de Hilbert. Ils possèdent la propriété remarquable que tout terme écrit avec les opérations que nous avons énumérées peut se réécrire avec la simple opération d’application à partir des axiomes de Hilbert et des variables libres ou axiomes de la catégorie.

Pour montrer ce résultat, commençons par considérer un terme λx.f. On peut supposer que f est déjà écrit comme application d’axiomes de Hilbert. Soit f = uv l’application la plus extérieure. Alors on a λx.f = s(λx.u)(λx.v) comme on le vérifie facilement. Reste donc le cas où f est soit une variable soit un axiome. Si f = x alors λx.x = i. Sinon, ou en fait dès que x n’apparaît pas dans f, on a λx.f = kf. En ce qui concerne un terme du type λ(x, y).f, il suffit de l’écrire λz.f′, où f′ est obtenu en remplaçant x dans f par π_{1}z et y par π_{2}z. Enfin, un terme (x, y) s’écrit pxy. Ceci termine la démonstration.

Ainsi, une démonstration peut se faire soit en utilisant les règles du calcul propositionnel et sans aucun axiome que ceux de la catégorie, soit en utilisant les axiomes de Hilbert et pour seule règle la règle d’application, c’est-à-dire le modus ponens.

Prenons un exemple. La commutativité du ∧ est un terme de type A ∧ B ⇒ B ∧ A, qui s’écrit c = λ(x, y).(y, x). Autrement dit, la démonstration avec les règles du calcul propositionnel s’écrit “par le théorème de déduction, on peut supposer A ∧ B et on doit montrer B ∧A; puisqu’on a A∧B, on a A d’une part (appelons x ce résultat), et B d’autre part (appelons y ce résultat) ; on a alors montré B et montré A, donc on a montré B ∧ A (c’est (y, x)), ce qui conclut la démonstration”. Pour réécrire cette démonstration au moyen des axiomes de Hilbert, on l’écrit c = λz.p(π_{2}z)(π_{1}z), et il reste à éliminer l’abstraction : on a c = s(λz.p(π_{2}z))(λz.π_{1}z), soit c = s(s(λz.p)(λz.π_{2}z))π_{1}, soit encore c = s(s(kp)π_{2})π_{1}. Voici une vérification de ce fait en utilisant le langage caml :

      pleiades david ~ $ ocaml
             Objective Caml version 1.07
      # let k = fun x -> fun y -> x;;
      val k : 'a -> 'b -> 'a = <fun>

      # let s = fun x -> fun y -> fun z -> x z (y z);;
      val s : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c = <fun>
      # let pi1 = fun (x,y) -> x;;
      val pi1 : 'a * 'b -> 'a = <fun>
      # let pi2 = fun (x,y) -> y;;
      val pi2 : 'a * 'b -> 'b = <fun>
      # let p = fun x -> fun y -> x,y;;
      val p : 'a -> 'b -> 'a * 'b = <fun>
      # s(s(k p)pi2)pi1;;
      - : '_a * '_b -> '_b * '_a = <fun>

Ici, si on veut écrire les étapes de la démonstration formelle, ce sont les suivantes :

1  s  (A ∧ B ⇒ A ⇒ B ∧ A) ⇒ (A ∧ B ⇒ A) ⇒ A ∧ B ⇒ B ∧ A  axiome
2  s  (A ∧ B ⇒ B ⇒ A ⇒ B ∧ A) ⇒ (A ∧ B ⇒ B) ⇒ A ∧ B ⇒ A ⇒ B ∧ A  axiome
3  k  (B ⇒ A ⇒ B ∧ A) ⇒ A ∧ B ⇒ B ⇒ A ⇒ B ∧ A  axiome
4  p  B ⇒ A ⇒ B ∧ A  axiome
5  kp  A ∧ B ⇒ B ⇒ A ⇒ B ∧ A  modus ponens 3/4
6  s(kp)  (A ∧ B ⇒ B) ⇒ A ∧ B ⇒ A ⇒ B ∧ A  modus ponens 2/5
7  π_{2}  A ∧ B ⇒ B  axiome
8  s(kp)π_{2}  A ∧ B ⇒ A ⇒ B ∧ A  modus ponens 6/7
9  s(s(kp)π_{2})  (A ∧ B ⇒ A) ⇒ A ∧ B ⇒ B ∧ A  modus ponens 1/8
10  π_{1}  A ∧ B ⇒ A  axiome
11 s(s(kp)π_{2})π_{1}  A ∧ B ⇒ B ∧ A  modus ponens 9/10

On notera au passage que les axiomes de Hilbert permettent, du moins en théorie, d’imaginer un langage de programmation entièrement dépourvu de variables.

Remarque culturelle : On sait construire une catégorie cartésienne close ayant exactement deux types, ⊤ et U, avec ⊤ ≅ U̸, et U ∧ U = U = U ⇒ U. Cette catégorie permet de définir le lambda-calcul non typé. Le lambda-calcul non typé, à la différence du lambda-calcul librement typé que nous avons introduit, n’est pas décidable.

5 Catégories bicartésiennes closes

Jusqu’ici, on s’est intéressé exclusivement aux connecteurs logiques ⇒, ∧ et ⊤. Pour obtenir la logique intutionniste, il faut rajouter encore les connecteurs ∨ et ⊥, dont les propriétés sont duales de ∧ et ⊤, c’est-à-dire qu’ils vérifient des propriétés coüniverselles : Hom(A∨B, C) ≅ Hom(A, C)×Hom(B, C) (naturellement en A, B, C) et Hom(⊥, A) ≅ {•} (naturellement en A). On pose donc : Définition 5.1. On appelle catégorie bicartésienne close une catégorie cartésienne close C munie d’un foncteur ⊥: 1 → C (identifié à un objet de C) et d’un foncteur ∨: C^{2} → C qui définissent respectivement un objet initial ⊥ de C et un coproduit A∨B pour tous objets A, B de C (pour être encore plus pédant, ce sont donc des adjoints à gauche respectivement du foncteur trivial C → 1 et du foncteur diagonal C → C^{2}).

Les résultats exposés sur les catégories cartésiennes closes restent valables, mutatis mutandis pour les catégories bicartésiennes closes. Il faut noter que l’ajout libre de nouveaux types dépend de si on considère la catégorie comme cartésienne, cartésienne close, ou bicartésienne close : les catégories cart[P_{1}, …, P_{n}], cartC[P_{1}, …, P_{n}] et biCartC[P_{1}, …, P_{n}] ne sont pas équivalentes. En revanche, l’ajout libre de nouveaux axiomes n’en dépend pas : si C est bicartésienne close, alors la catégorie C[x_{1} : Q_{1}, …, x_{k} : Q_{k}] ne dépend pas du fait que la catégorie C soit considérée comme cartésienne, cartésienne close ou cocartésienne close (c’est de toute façon la catégorie coslice sur Q_{1} ∧ ⋯ ∧ Q_{k}).

On a des isomorphismes dans toute catégorie bicartésienne close, naturels en toutes les variables, entre (A ⇒ C) ∧ (B ⇒ C) et A ∨ B ⇒ C, entre ⊥ ⇒ A et ⊤, entre A ∧ (B ∨ C) et (A ∧ B) ∨ (A ∧ C), et entre A ∧ ⊥ et ⊥. Par exemple pour le dernier : une flèche A ∧ ⊥ → S correspond à une flèche ⊥ → A ⇒ S par théorème de déduction, et il n’y en a qu’une par définition du ⊥, donc A ∧ ⊥ est aussi terminal, donc isomorphe à ⊥. Dans cette démonstration, l’existence de ⇒ (l’adjonction) est essentielle, et ce résultat n’est pas valable dans une catégorie bicartésienne quelconque.

On se gardera du reste des analogies trompeuses : on a bien des flèches naturelles et canoniques A∨(B ∧C) → (A∨B)∧(A∨C) et A∨⊤ → ⊤, et même des flèches dans l’autre sens (encore naturelles mais nettement moins canoniques :-), mais ces flèches ne sont pas des isomorphismes en général. Il suffit pour s’en convaincre de regarder la catégorie des ensembles (qui est bien bicartésienne close, le ∧ étant le produit, le ∨ l’union disjointe, le ⊤ le singleton, le ⊥ l’ensemble vide, et le ⇒ l’ensemble des fonctions).

Les notations du lambda-calcul s’étendent encore aux catégories bicartésiennes closes, par exemple avec les notations suivantes. Si x est un terme de type A, on notera x^{←} (ou x^{←B} s’il est nécessaire de préciser) le terme de type A ∨ B qui s’en déduit, et de même pour x^{→}. Pour définir un terme de type A ∨ B ⇒ C, on note λ[x : A|y : B].(f|g), où f et g sont tous deux des termes de type C, ayant x et y respectivement comme variable libre de type A ou B respectivement. Enfin, pour définir un terme de type ⊥ ⇒ A, on écrit tout simplement λ[].().

Les axiomes de Hilbert se complètent en rajoutant

\begin{aligned}ω_{1} = λx.x^{←} & : A ⇒ A ∨ B \\ ω_{2} = λy.y^{→} & : B ⇒ A ∨ B \\ q = λxy.λ[u : A|v : B].(xu|yv) & : (A ⇒ C) ⇒ (B ⇒ C) ⇒ A ∨ B ⇒ C \\ F = λ[].() & : ⊥ ⇒ A \end{aligned}

L’introduction du OU, et surtout du FAUX, dans la catégorie, a des conséquences assez fondamentales. À commencer par celle-ci : Proposition 5.2. Dans une catégorie bicartésienne close, pour tout objet A, s’il existe une flèche A → ⊥, alors c’est un isomorphisme (et donc A est un objet initial, et donc cette flèche est unique).

Démonstration. Soit A →^{f} ⊥ cette flèche. La composée ⊥ → A →^{f} ⊥ est l’identité car il n’y a qu’une flèche ⊥ → ⊥ (puisque ⊥ est terminal). Il s’agit de montrer que la composée dans l’autre sens est aussi l’identité. Considérons le diagramme commutatif

A ⟶^{f} ⊥ ⟶ A
(1_{A},f)↓  ∥  ↑π_{1}
A ∧ ⊥ ⟶^{π_{2}} ⊥ ⟶ A ∧ ⊥

Le carré de droite est commutatif par définition de (1_{A}, f), et le carré de gauche est commutatif car il n’y a qu’une flèche qui part de ⊥. On a déjà montré que A ∧ ⊥ est isomorphe à ⊥, donc terminal, donc la composée des deux flèches de la ligne du bas est l’identité. Ainsi, la composée des deux flèches de la ligne du haut (celle qui nous intéresse) est la composée de la flèche de gauche et de la flèche de droite. Or par définition de (1_{A}, f), c’est précisément 1_{A}. Ceci démontre le résultat.

De manière intuitive, et quelque peu informelle, ce résultat s’énonce en disant qu’il n’y a qu’une façon d’établir ⊥, c’est de dire une connerie.

On note ¬A l’objet A ⇒ ⊥ (bien entendu, le ¬ est un foncteur). Une flèche X → ¬A correspond à une flèche X ∧ A → ⊥, et on a vu qu’il y en a au plus une : il y a au plus une façon de montrer une négation.

En particulier, si on appelle catégorie booléienne une catégorie bicartésienne close dans laquelle la flèche canonique A → ¬¬A (définie par λ[x : A].λ[y : A ⇒ ⊥].yx) est un isomorphisme, on voit que dans une catégorie booléienne tous les ensembles Hom ont au plus un élément, i.e. que la catégorie est en fait un ensemble préordonné. Celui-ci est alors équivalent à un ensemble partiellement ordonné (en quotientant par la relation d’équivalence associée au préordre), et un tel ensemble partiellement ordonné (i.e. un ensemble partiellement ordonné qui en tant que catégorie est une catégorie booléienne) est appelé une algèbre de Boole.

Dans l’étude de la logique catégorique, on est plus intéressé par les algèbres de Heyting : une algèbre de Heyting est un ensemble partiellement ordonné qui en tant que catégorie est une catégorie bicartésienne close. De manière équivalente, c’est un treillis distributif dans lequel pour tous éléments B et C l’ensemble des A tels que A ∧ B ≤ C admet une borne supérieure, notée B ⇒ C.

Remarque : Si dans une catégorie bicartésienne close C il existe un objet A tel que A ≅ ¬A, alors on a une flèche A → A ⇒ ⊥, d’où A ∧ A → ⊥, et en composant avec la diagonale A → A∧A on en déduit une flèche A → ⊥. Or on a vu que ceci implique A ≅ ⊥, et donc ¬A ≅ ⊤. Mais alors on a un isomorphisme ⊥ ≅ ⊤, et il est facile de voir que tous les objets sont isomorphes, i.e. que la catégorie est (équivalente à) 1. Une telle catégorie est dite inconsistante. Dans le cas contraire, elle est dite consistante.

6 Passage au calcul des prédicats

Tout d’abord, un mot d’avertissement. Le calcul des prédicats en logique catégorique est un terrain bien moins balisé que le calcul propositionnel. Il n’y a pas d’étude bien approfondie (à ma connaissance) du lambda-calcul qui s’y rattache. Les auteurs se dégonflent et se place dans les topoi pour étudier le problème, ce qui est une solution peu élégante (les topoi sont les catégories adaptées à la sémantique, mais conviennent mal pour faire de la syntaxe). Ce qui suit est donc à prendre avec des précautions.

Comme on l’a déjà signalé dans l’exposé de rappels, il existe plusieurs sortes de calculs des prédicats. En logique du premier ordre, toutes les variables sont de la même espèce. En logique du second ordre, on a des variables d’individus et des variables de prédicats, sur lesquelles on peut aussi quantifier. Autrement dit, on a (au moins) deux types de variables, disons U pour les variables d’individus et Ω^{U^{k}} pour les variables de prédicats, cette notation servant à suggérer qu’elles se comportent comme des fonctions de U^{k} vers Ω = Ω^{U^{0}} (le type des prédicats à 0 variables, ou encore des valeurs de vérité). Par ailleurs, on a introduit en logique du second ordre l’axiome de compréhension, qui permet de construire des termes de prédicats (de type Ω^{U^{k}}) à partir de n’importe quelle formule dans laquelle les seules variables libres sont des variables d’individus. On a choisi de noter les utilisations de l’axiome de compréhension avec la notation lambda, qui est à rapprocher de la notation lambda introduite plus haut dans cet exposé.

Le calcul des prédicats catégorique, ou calcul des types, pousse ces idées plus loin. On se permet d’étudier des termes de toute une multitude de types, ces types eux-mêmes formant une catégorie bicartésienne close (ou moins si on le souhaite, mais pourquoi se priver des bonnes choses). On possède donc pour les former tout l’arsenal de notations du lambda-calcul qu’on a déjà vues. Mais on utilisera des notations plus mathématiques pour la formation des types, notant 1 le type terminal, 0 le type initial, × le produit de deux types, + leur somme, et avec un exposant le hom interne (exponentielle de deux types).

À côté de cela, on a sur certains types eux-mêmes des structures supplémentaires. Par exemple, dans l’étude de l’arithmétique, si on considère un type N pour les naturels, on le supposera muni d’un terme (clos) 0 de type N et d’un terme (clos) s de type N^{N} (la fonction successeur). Un type particulièrement important est le type Ω des valeurs de vérité, ou, plus précisément, des propositions (prédicats sans variable, les autres types de prédicats s’en déduisant par les mécanismes normaux de construction des types). C’est sur ce type, i.e. sur les termes de ce type, que s’appliquent les conjoncteurs ∧, ∨, etc, que nous avons rencontrés. Plus précisément, ⇒, ∧ et ∨ sont des termes de type Ω^{Ω×Ω}, ⊤ et ⊥ des termes de type Ω.

Mais si les termes de type Ω doivent correspondre aux propositions, alors les démonstrations sont des termes dont le type est lui-même un terme de type Ω. Autrement dit, on a non seulement une structure de catégorie bicartésienne close sur les types, mais aussi sur les propositions, i.e. sur le type Ω. On a deux catégories bicartésiennes closes en jeu : la catégorie “externe”, structurale, et la catégorie “interne”, le type Ω muni de sa structure. Au niveau externe, produits et autres opérations universelles seront notées par leurs notations mathématiques (×, +, 1, etc.), tandis qu’au niveau interne, ils seront notés par les symboles logiques (∧, ∨, ⊤, etc.).

Comment fait-on pour mettre sur un objet d’une catégorie bicartésienne close une structure de catégorie bicartésienne close ? C’est une façon générale de faire en théorie des catégories : on suppose que pour tout type X l’ensemble Ω(X) = Hom(X, Ω) des termes de type Ω ayant variables libres dans X est muni d’une structure de catégorie bicartésienne close, et que ces structures sont compatibles les unes aux autres par changement de X. Rigoureusement : Définition 6.1. Soit C une catégorie bicartésienne close, et Ω un type (objet) de C. Une structure de catégorie bicartésienne close interne sur l’objet Ω est la donnée d’une structure de catégorie bicartésienne close sur chacun des ensembles Ω(X) = Hom(X, Ω) (X un type de C), ainsi que pour toute flèche ϕ: X′ → X d’un foncteur logique (strict) Ω(X) → Ω(X′) qui sur les objets coïncide avec la flèche de composition (qui envoie f: X → Ω sur fϕ: X′ → Ω). Ceci se dit encore de la façon suivante : on a un foncteur de la catégorie C vers la catégorie BiCartC (des catégories bicartésiennes closes) dont le foncteur objet (i.e. la composée du foncteur en question avec le foncteur de BiCartC vers la catégorie des ensembles qui à une catégorie bicartésienne close associe l’ensemble de ses objets) est représentable par un objet Ω de C.

On remarquera qu’on n’exige pas la représentabilité du foncteur flèche, mais seulement du foncteur objet. Ceci est raisonable car on ne s’intéresse jamais à toutes les démonstrations (de n’importe quoi à partir de n’importe quoi). Cependant, il peut être judicieux de demander aussi la représentabilité du foncteur démonstrations de source donnée, i.e. exiger que pour tout X et tout p ∈ Ω(X) le foncteur qui à X′ → X fait correspondre l’ensemble des flèches de source (l’image dans Ω(X′) de) p, soit représentable par un objet de C (au-dessus de X bien sûr). Notamment lorsque p est en fait l’objet ⊤ (au-dessus de X = 1 disons), c’est ce qu’on a de plus près du “type des propositions qui sont vraies”.

D’autre part, le fait que Ω soit représentable (sur les objets) implique, d’après le lemme de Yoneda, que les morphismes ∧: Ω × Ω → Ω et compagnie sont aussi représentables. Il est donc justifié de les considérer comme des termes de type Ω^{Ω×Ω} etc.

Il faut noter qu’une démonstration, i.e. une flèche dans la catégorie interne Ω, a deux types de prémisses (dépendances, suppositions, hypothèses, variables libres, comme on voudra) : l’objet X de C au-dessus duquel elle est définie, et sa source dans Ω(X). Il se peut du reste fort bien que la source en question soit définie plus globalement que la démonstration elle-même (par exemple, on verra que ∃(x : X).⊤, qui est une proposition sans variable libre, n’a pas de démonstration sans variable libre (si X est un type sur lequel on n’a aucune donnée) mais qu’il a une démonstration (à savoir (x, ⋆)) ayant une variable libre x de type X).

7 Quantificateurs

Étant donnés un type A et un prédicat p, terme de type Ω ayant variables libres de type A × X (le X servant à représenter d’autres variables libres éventuelles du prédicat), on cherche à donner un sens à ∀(t : A).p et ∃(t : A).p, qui doivent être des termes de type X → Ω (autrement dit, la quantifiation doit retirer la variable libre t de type A et ne pas toucher aux autres).

Commençons par la quantification universelle. Si on a une démonstration δ d’un terme de type ∀(t : A).p, et qu’on a un terme u de type A, il est sensé d’appliquer la démonstration “au cas particulier t = u”, pour obtenir une démonstration de p_{u} (p dans lequel on a substitué u à t, ce qui s’écrit encore (λ[t : A].p)u si on préfère). On notera tout simplement δu la démonstration ainsi construite. Réciproquement, si on cherche à construire une démonstration de ∀(t : A).p, on procède en supposant donné un t et en démontrant alors p. Autrement dit, donnée une démonstration δ de p (avec la variable libre t), on construit une démonstration notée λ[t : A].δ de ∀(t : A).p. Il faut bien noter l’analogie entre l’abstraction lambda de type “fantaisie” (supposons que j’aie une démonstration t d’une assertion A) et l’abstraction de type “instantiation” (supposons que t soit une variable de type A). La différence étant une différence de niveau : dans le second cas A est un type, i.e. un objet de la catégorie externe C tandis que dans le premier cas A est une proposition, i.e. un terme de type la catégorie interne Ω. De plus, dans le cas où A est un type, non seulement δ pourra dépendre de t mais son type lui-même (qui est un terme p de type Ω) en dépendra en général.

On peut maintenant formuler précisément la propriété universelle de ∀(t : A).p. Soit p: X × A → Ω un terme de type Ω ayant X × A pour type des variables libres, la variable libre de type A étant notée t. Alors ∀(t : A).p est un terme de type X → Ω (de type Ω ayant X pour type des variables libres) muni d’un morphisme ϖ: (∀(t : A).p) → p dans la catégorie Ω(X × A) (ici, ∀(t : A).p, objet de la catégorie Ω(X), est étendu à Ω(X × A) de la façon connue), qui vérifie la propriété universelle suivante. Si q: X → Ω est un terme de type Ω ayant X mais pas A pour type des variables libres, et qu’on se donne une flèche δ: q → p dans la catégorie Ω(X × A) (même commentaire que ci-dessus), alors il existe une unique flèche λ[t : A].δ: q → ∀(t : A).p dans la catégorie Ω(X) dont la composée avec ϖ donne δ, i.e. telle que ϖ ∘ (λ[t : A].δ) = δ.

Cette propriété universelle, ici détaillée lourdement, peut s’énoncer d’une multitude de façons différentes. Par exemple, on peut dire que ϖ: ∀(t : A).p → p est la flèche terminale de type q → p avec q un terme de type Ω qui ne dépend pas de A. C’est-à-dire que démontrer p à partir d’hypothèses q ne faisant pas invervenir t, c’est “la même chose” que démontrer p à partir de ces hypothèses q. Ou encore Hom_{Ω(X×A)}(q, p) ≅ Hom_{Ω(X)}(q, ∀(t : A).p) pour tout objet q de Ω(X). On peut encore dire que le foncteur qui à p (objet de Ω(X × A)) associe ∀(t : A).p (objet de Ω(X)) est adjoint à droite du foncteur qui à q (objet de Ω(X) associe q transporté à Ω(X × A). On peut encore transformer cette assertion en quelque chose de totalement incompréhensible avec des fibrations de catégories ou même (si on veut jouer avec les 2-catégories) des champs dans tous les sens. Il n’en demeure pas moins qu’elle est complètement évidente, et que ∀(t : A).p est un produit catégorique de p indicé par A.

La propriété du ∃ et duale, elle est coüniverselle au lieu d’être universelle. C’est-à-dire que tandis que ∀(t : A).p est la plus faible assertion indépendante de t et qui démontre p, l’assertion ∃(t : A).p est la plus forte assertion indépendante de t que p démontre, et on a Hom_{Ω(X×A)}(p, q) ≅ Hom_{Ω(X)}(∃(t : A).p, q). En ce qui concerne les notations, si x est un terme de type A et δ une démonstration de p_{x} (p dans lequel on a substitué x pour t, i.e. (λ[t : A].p)x), alors on note (x, δ) la démonstration de ∃(t : A).p qui en découle. Et d’autre part, si δ est une démonstration de q, proposition indépendante de t, à partir de p dépendant de t de type A, on notera (t?δ) la démonstration de q à partir de ∃(t : A).p obtenue par la propriété universelle (il faut lire : on a supposé qu’il existait un terme de type A vérifiant p, appelons-le t).

Bien entendu, si C est une catégorie bicartésienne close et Ω un type de C muni d’une structure de catégorie bicartésienne close, il n’est pas dit d’avance que toutes les quantifications existent (i.e. soient représentables) dans Ω. Lorsque c’est le cas, on dira que Ω est une catégorie bicartésienne close complète interne. Plus précisément, il faut non pas postuler l’existence de telles quantifications mais bien les choisir. Autrement dit : Définition 7.1. Une CBCCCBCCCI (catégorie bicartésienne close à catégorie bicartésienne close complète interne) est une catégorie bicartésienne close C munie d’un objet Ω et d’une structure de catégorie bicartésienne close sur Ω ainsi que de foncteurs internes ∀ et ∃ qui vérifient les propriétés universelles précisées ci-dessus. Un foncteur logique F: C → C′ entre CBCCCBCCCI est un foncteur qui préserve toutes les données sur les catégories C et Ω, i.e. c’est un foncteur logique sur C qui vérifie F (Ω) = Ω′, et dont les applications induites Ω(X) → Ω′(F (X)) sont munies d’une structure de foncteur logique de façon naturelle en X. On note CBCCCBCCCI la catégorie des CBCCCBCCCI avec pour flèches les foncteurs logiques.

Un exemple de CBCCCBCCCI est la catégorie des ensembles avec pour Ω la catégorie interne 2 = {0, 1}.

De même que Cart, CartC et BiCartC, la catégorie CBCCCBCCCI admet toutes sortes de constructions coüniverselles. Elle admet un objet initial, noté cbcccbccci, qui a déjà une structure fort compliquée, et on a de plus la possibilité d’ajouter librement des types, des termes d’un type ou des démonstrations d’une proposition. Ces derniers ajouts se font avec des constructions coslice externe et coslice interne respectivement. (Ce qui est remarquable, c’est que le fait d’ajouter librement un terme p au type Ω ne perturbe pas sa nature de catégorie bicartésienne close complète interne.)

8 Récapitulation des notations et exemples

Ayant introduit tout un tas de notations non standard et pénibles, nous insistons sur la lourdeur en les récapitulant et en en donnant des exemples.

– (Élimination du ⇒, ou application, ou modus ponens.) Si v est une démonstration de P ⇒ Q et u une démonstration de P, alors vu est une démonstration de Q.

– (Introduction du ⇒, ou abstraction, ou fantaisie, ou “théorème de déduction”.) Si δ est une démonstration de Q qui fait intervenir une hypothèse ξ démonstration de P, alors λ[ξ : P].δ est une démonstration de P ⇒ Q.

– (Élimination du ∧.) Lorsqu’on démontre R à partir d’une hypothèse de type P ∧ Q, qui a été abstraite, on peut écrire cette hypothèse (u, v) et considérer u comme une démonstration de P et v comme une démonstration de Q. La démonstration finale s’écrit alors λ[(u, v) : P ∧ Q]. · · ·.^{1}

– (Introduction du ∧.) Si u est une démonstration de P et v une démonstration de Q, alors (u, v) est une démonstration de P ∧ Q.

– (Élimination du ⊤ : il n’y en a pas, le ⊤ ne s’élimine pas.)

– (Introduction du ⊤.) ⋆ est une démonstration de ⊤.

– (Élimination du ∨, ou division en cas.) Lorsqu’on démontre R à partir d’une hypothèse de type P ∨ Q, on peut écrire cette hypothèse u : P |v : Q et fournir une démonstration f de R à partir de u démonstration de P et une démonstration g de R à partir de v démonstration de Q, auquel cas la démonstration finale s’écrit λ[u : P |v : Q].(f|g).

– (Introduction du ∨.) Si u est une démonstration de P alors u^{→Q} est une démonstration de P ∨Q. Si v est une démonstration de Q alors v^{P ←} est une démonstration de P ∨Q.

– (Élimination du ⊥.) λ[].()^{P} est une démonstration de ⊥ ⇒ P.

– (Introduction du ⊥ : il n’y en a pas, le ⊥ ne s’introduit pas.)

– (Élimination du ∀, ou spécialisation.) Si δ est une démonstration de ∀(t : A).P alors δa est une démonstration de P_{a} = (λ[t : A].P)a pour tout terme a de type A.

– (Introduction du ∀, ou généralisation.) Si δ est une démonstration de P qui fait intervenir une variable t de type A, alors λ[t : A].δ est une démonstration de ∀(t : A).P. Ceci suppose qu’aucune des hypothèses de δ ne fait intervenir t.

– (Élimination du ∃, ou choix d’un témoin.) Si δ est une démonstration de Q (ne faisant pas intervenir t) à partir d’une hypothèse affirmant ∃(t : A).P, alors (t?δ) est une démonstration de Q à partir d’une hypothèse affirmant P.

– (Introduction du ∃.) Si a est un terme de type A et δ une démonstration de P_{a} = (λ[t : A].P)a, alors (a, δ) est une démonstration de ∃[t : A].P.

Comme premier exemple, nous démontrons

∀(p : Ω^{U×V}).(∃(x : U).∀(y : V).p(x, y) ⇒ ∀(y : V).∃(x : U).p(x, y))

Pour cela, donnons-nous un p de Ω^{U×V}. Si δ est une hypothèse qui affirme que ∀(y : V).p(x, y), où x est un terme de type U, et que y est un terme de type V, alors (x, δy) est une démonstration de ∃(x : U).p(x, y), donc λ[y : V].(x, δy) est une démonstration de ∀(y : V).∃(x : U).p(x, y). Comme x n’est plus libre dans cette assertion, on peut éliminer ∃ et dire que (x?λ[y : V].(x, δy)) est une démonstration de la même chose mais à partir de δ hypothèse qui affirme ∃(x : U).∀(y : V).p(x, y) cette fois. Et finalement, la démonstration voulue est

1Certes, cette règle n’est pas géniale. Il y aurait de meilleures façons de procéder. Mais c’est de peu d’importance somme toute.

λ[p : Ω^{U×V}].λ[δ : ∃(x : U).∀(y : V).p(x, y)].(x?λ[y : V].(x, δy))

Nous montrons maintenant le fait que l’égalité est symétrique. Pour cela il faut d’abord définir l’égalité. Cela se fait en introduisant la notation a = b (où a et b sont deux termes d’un même type U quelconque) comme signifiant ∀(p : Ω^{U}).(pa ⇒ pb). Attention : Cette égalité interne entre termes n’a pas de raison de coïncider avec l’égalité externe (égalité entre flèches de la catégorie). En fait, cela n’a pas vraiment de sens, puisque a = b est un élément de Ω tel que nous l’avons défini, pour l’égalité interne.

On veut donc montrer que

∀(a : U).∀(b : U).((∀(p : Ω^{U}).(pa ⇒ pb)) ⇒ (∀(q : Ω^{U}).(qb ⇒ qa)))

Soient donc a de type U, b de type U et δ une hypothèse affirmant que ∀(p : Ω^{U}).(pa ⇒ pb). Considérons λ[x : U].∀(q : Ω^{U}).(px ⇒ pa). C’est un terme de type Ω^{U}. On peut donc considérer δ(λ[x : U].∀(q : Ω^{U}).(qx ⇒ qa)), qui est une démonstration de (∀(q : Ω^{U}).(qa ⇒ qa)) ⇒ (∀(q : Ω^{U}).(qb ⇒ qa)). Or on peut trouver facilement une démonstration de ∀(q : Ω^{U}).(qa ⇒ qa). Par exemple, λ[q : Ω^{U}].λ[ξ : qa].ξ en est une. Finalement, la démonstration recherchée est

\begin{matrix}λ[a : U].λ[b : U].λ[δ : ∀(p : Ω^{U}).(pa ⇒ pb)]. \\ (δ(λ[x : U].∀(q : Ω^{U}).(qx ⇒ qa))(λ[q : Ω^{U}].λ[ξ : qa].ξ)) \end{matrix}

Voici la chose écrite en Coq.

      Welcome to Coq V6.2.2 (September 1998)
      No .coqrc or .coqrc.6.2.2 found. Skipping rcfile loading.
      Coq < Parameter U:Type.
      U is assumed
      Coq < Theorem symmetry :
      Coq < (a,b:U)(((p:U->Prop)((p a)->(p b)))->
      Coq < ((q:U->Prop)((q b)->(q a)))).
      1 subgoal
        ============================
         (a,b:U)((p:U->Prop)(p a)->(p b))->(q:U->Prop)(q b)->(q a)

symmetry < Intro a; Intro b; Intro delta.
1 subgoal
a : U
b : U
delta : (p:U->Prop)(p a)->(p b)
============================
 (q:U->Prop)(q b)->(q a)
symmetry < Cut (q:U->Prop)(q a)->(q a).
2 subgoals
a : U
b : U
delta : (p:U->Prop)(p a)->(p b)
============================
 ((q:U->Prop)(q a)->(q a))->(q:U->Prop)(q b)->(q a)
subgoal 2 is:
(q:U->Prop)(q a)->(q a)
symmetry < Exact (delta ([x:U](q:U->Prop)(q x)->(q a))).
1 subgoal
a : U
b : U
delta : (p:U->Prop)(p a)->(p b)
============================
 (q:U->Prop)(q a)->(q a)
symmetry < Intro q; Intro xi.
1 subgoal
a : U
b : U
delta : (p:U->Prop)(p a)->(p b)
q : U->Prop
xi : (q a)
============================

   (q a)
symmetry < Exact xi.
Subtree proved!
symmetry < Qed.
(Intro a; Intro b; Intro delta).
Cut (q:U->Prop)(q a)->(q a).
Exact (delta [x:U](q:U->Prop)(q x)->(q a)).
(Intro q; Intro xi).
Exact xi.
symmetry is defined
Coq < Print symmetry.
symmetry =
[a,b:U]
 [delta:(p:U->Prop)(p a)->(p b)]
  (delta [x:U](q:U->Prop)(q x)->(q a) [q:U->Prop][xi:(q a)]xi)
     : (a,b:U)((p:U->Prop)(p a)->(p b))->(q:U->Prop)(q b)->(q a)

Coq < Quit.

Accessoirement, la réflexivité et la transitivité de l’égalité sont beaucoup plus faciles.