La théorie du Calcul des Constructions pur se ramène essentiellement à celle du système Fω par effacement des dépendances en les preuves dans les types (cf chapitre sur l’extraction).
Tous deux correspondent à une logique très faible, puisqu’en interprétant Prop de manière booléenne, toute formule admet un modèle fini. En revanche, tous deux correspondent à un langage de fonctions très riche puisqu’ils contiennent toutes les fonctions prouvablement totales dans l’arithmétique d’ordre supérieur.
Le CC admet un modèle booléen, dans lequel Prop est interprété par l’ensemble a deux élément B={ true, false}. L’imprédicativité se résume alors à une quantification finie sur B. Les types de Type sont construits récursivement à partir de B et le produit fonctionnel. Dans le cas d’un produit A → T avec A une proposition et T un type, l’interprétation est celle1. L’interprétation s’applique à tous les jugements qui ne sont pas des jugements de preuve (on note X, P, Q et T, U pour les objets et types du niveau Type et x, t, u et A, B pour les objets et types2 du niveau Prop).
|
La règle de conversion est validée par le modèle et on a ⊢ t:A qui implique [[A]]= true, d’où la cohérence du CC puisque [[∀ A:Prop.A]]= false.
Le modèle est localement fini et [[A]]= true est décidable puisque les quantifications ne portent que sur des espaces fonctionnels engendrés à partir de B qui est fini et d’un nombre fini de construction par produit. En particulier la cohérence de CC est prouvable dans l’arithmétique.
Dans ce modèle, tous les entiers (dans le type ∀ A. (A → A) → (A → A)) sont identifiés. On ne peut donc prouver 0 ≠ 1. Les axiomes de Peano ne sont donc pas dérivables, en accord avec l’existence d’une preuve de cohérence dans l’arithmétique.
Question ouverte: complétion de Fω (et plus généralement de CC
dans son modèle booléen standard) vis à vis du modèle booléen. Quels
axiomes ajouter pour obtenir ([[A]]= true) → ⊢ A
(candidats: ∀ A:Prop. A= True ∨ A= False
(complétude propositionnelle) et ∀ f,g:(∀
x:T.U). (∀ u:T. f u =Uu g u) → f=g
(extensionnalité)) ?
Remarque 1: l’indiscernabilité des preuves (« proof-irrelevance »), la
complétude propositionnelle et le tiers-exclu sont tous les trois
validés par le modèle booléen..
Remarque 2: on peut typiquement représenter false en théorie des ensembles par l’ensemble vide ∅ et true par un ensemble singleton (typiquement l’ensemble {∅} dont l’unique élément est l’ensemble vide); en ce cas, [[∀ X:T. B]]ρ s’exprime comme ∩V∈[[T]] [[B]]ρ,X:=V.
Il existe une variante du modèle booléen qui préserve le contenu calculatoire des preuves. Ce modèle, non exprimable dans l’arithmétique, permet par exemple de montrer la non prouvabilité de l’induction de Peano [Geu01, SG95]. La différence par rapport au modèle booléen à preuve unique est que les propositions vraies sont interprétées par l’ensemble Λ de tous les λ-termes purs. L’interprétation est donc la suivante:
|
et on montre que ⊢ t:A implique [[t]] ∈ [[A]].
Le CC admet aussi un modèle par réalisabilité qui respecte le contenu intensionnel des fonctions (et des preuves). Un tel type de modèle permet de prouver la normalisation forte de CC et Fω, donc la cohérence de l’arithmétique d’ordre supérieur et, a fortiori, de l’arithmétique. En particulier, le modèle par réalisabilité montre la cohérence de CC + (0≠ n+1) + injectivité du successeur + induction, c’est-à-dire de CC + les axiomes de Peano.
Tous les programmes prouvablement terminant dans l’arithmétique d’ordre supérieur sont dérivables dans Fω et donc dans le CC [Gir72].
Schématiquement, le modèle par réalisabilité interprète les propositions comme des ensembles de λ-termes clos par β-expansion avec la propriété que t∈ [[A→ B]] ssi tu ∈ [[B]] pour tout u ∈ [[A]] (propriété dite de réductibilité). L’interprétation des types de Type est alors la même que pour le modèle booléen standard du CC : le produit du CC est interprété comme le produit ensembliste à ceci près que le domaine de base, Prop, est maintenant un ensemble de parties de λ-termes.
Les systèmes U- et U (dus à J.-Y. Girard [Gir72]) sont en fait des extensions du système Fω. Alors que la couche Type de Fω correspond à un λ-calcul simplement typé bati sur la constante Prop, la couche Type des systèmes U- et U correspond à un λ-calcul polymorphe (le système F) incluant Prop comme type de base.
Le système Type:Type (énoncé par P. Martin-Löf) est le système où Prop et Type sont confondus et où tous les produits sont permis. En particulier, Type:Type est un objet terminal de la catégorie des PTS : tout PTS se plonge dans Type:Type.
Ces trois systèmes sont incohérents. Une des manières de dériver une incohérence est de construire dans U- (et donc aussi dans les 2 autres systèmes) un type Univ:Type et une injection3 i:∀ A:Type.(A→ A→ Prop)→ (A→ Prop)→ Univ.
En spécialisant i à Univ, on peut plonger dans Univ toute relation R:Univ→ Univ→ Prop définie sur un domaine D:Univ→ Prop. Par ce fait, on peut dériver le paradoxe de Burali-Forti (cf Girard [Gir72, Coq86]), le paradoxe de Reynolds-Coquand (cf Coquand [Coq94b]), ou plus généralement encoder la théorie naïve des ensembles de Cantor et en particulier le paradoxe de Russell (cf Miquel [Miq01]).
Le Calcul des Constructions avec univers CCω étend le CC avec une hiérarchie dénombrable d’univers Type1:Type2:Type3... (on identifie alors le niveau Type de CC avec Type1). Les produits sur cette hiérarchie sont prédicatifs : si T:Typei et U(X):Typej alors Π X:T. U(X):Typemax(i,j). La sorte Prop reste imprédicative : si T:Typei et U(X):Prop alors Π X:T. U(X):Prop.
De plus, CCω introduit une relation de sous-typage vérifiant Prop ⊂ Type1 ⊂ Type2 ⊂ Type3... Concrètement, la relation de conversion est remplacée par une relation de sous-typage définie par
Typei ⊂ Typej ssi i≤ j |
Prop ⊂ Typei |
Π X:T. U(X) ⊂ Π X:T′. U′(X) ssi T =βT′ et U(X) ⊂ U(X′) |
T ⊂ T′ ssi T =βT′ sinon |
La règle de conversion est remplacée en conséquence par
|
CCω correspond à la partie sans inductifs et sans Set du Calcul des Constructions Inductives4.
Dans CCω, on peut définir l’ensemble des entiers naturels au niveau Type2
|
puis on peut définir le prédicat caractéristique des entiers naturels par
IsNat := λ n:Nat.∀ P:Nat→ Prop. P(0)→(∀ m:Nat. P(m)→ P(s(m)))→ P(n) |
On peut alors prouver que 0≠ s(n) et que s est injectif sur tout entier de IsNat, ce qui donne l’arithmétique de Peano.
Ainsi, CC avec juste un niveau supplémentaire de Type contient l’arithmétique5.
En utilisant un codage des ensembles sous forme de graphe pointé, Miquel [Miq01] a pu plonger la théorie des ensembles de Zermelo (qui est beaucoup plus faible que ZF) dans CCω avec trois niveaux6 de Type.
Nous allons faire une analyse de la force logique de CCω en termes ensemblistes, c’est-à-dire en termes de profondeur d’imbrication des ensembles que l’on peut construire dans ECC 7.
On vient de voir que Type2 contient l’ensemble des entiers naturels (ω) ce qui correspond en théorie des ensembles à un ensemble de profondeur ω. Par ailleurs, la construction de chaque Typei+1 permet au plus d’itèrer ω fois le produit fonctionnel à partir de Typei. Les fonctions étant représentées en théorie des ensembles par des relations, une fonction de type A → B correspond en théorie des ensembles à une partie de l’ensemble produit A × B et plus généralement, une fonction de type Π x:A. B(x) est une partie de A × ∪x∈ A B(x). Ainsi, l’ensemble de fonctions Π x:A. B(x) se construit en ajoutant un niveau d’imbrication au maximum des niveaux de A et des B(x). Les types de Typei+1 ont donc un nombre fini de niveaux d’imbrication en plus du niveau d’imbrication de Typei. En passant à la limite, le type Typei+1 lui-même a donc ω niveaux d’imbrication en plus que Typei. On arrive de la sorte à établir que Typei contient des ensembles de niveaux d’imbrication ensemblistes ω.i. En passant à la limite une nouvelle fois, on établit que ECC doit contenir des ensembles de niveau d’imbrication au moins ω2.
Par ailleurs, P.-A. Melliès et B. Werner [MW98] ont exhibé un modèle de cette cardinalité montrant que la force ordinale de ECC était bien ω2 (itération ω2 des parties).
On considère le Calcul des Constructions Inductives avec Set et Prop.
Dans le cas où Set est imprédicatif, il n’existe pas de modèle complet du CCI. Les deux approximations les plus proches sont
Dans le cas d’un Set prédicatif, il n’existe pas non plus explicitement de modèle, mais il est communément admis que le modèle booléen avec Set interprété comme Type0 fonctionne.
L’axiome K de Streicher énonce que toute preuve de la réflexivité de l’égalité peut être remplacée dans tout contexte par la preuve canonique de réflexivité
∀ A:Set.∀ a:A.∀ p:(a=a).∀ P:a=a→ Prop. P(refl_equal(a))−>P(x) |
Cet énoncé est équivalent à l’existence d’une unique preuve de réflexivité de l’égalité
∀ A:Set.∀ a:A.∀ p:(a=a),p=refl_equal(a) |
Il existe plusieurs autres formulations équivalentes à l’axiome K. L’une d’elle est particulièrement intéressante en pratique: elle exprime que deux objets dans des types dépendants sont égaux dès lors qu’ils sont dans la même instance dépendante
∀ A:Set.∀ B:A→Set.∀ a:A.∀ b,b′:B(a). (a,b)=(a,b′) → b=b′ |
Notons que l’axiome K est dérivable si l’égalité sur A est décidable (ce qui est le cas en particulier en admettant la logique classique). Notons par ailleurs que l’axiome K est une conséquence directe de l’indiscernabilité des preuves, indépendamment alors de la logique classique.
L’indiscernabilité des preuves s’exprime par
∀ A:Prop.∀ p,q:A.p=q |
Indépendant dans CC : non prouvable (pas de preuve close), validé par le modèle booléen. Incohérent dans CCI en remplaçant Prop par Set (car 0≠1 dans Set).
La logique classique peut être exprimée par exemple par le tiers-exclu.
∀ A:Prop. A∨ ¬ A |
Indépendant dans CC et ECC : non prouvable (pas de preuve close), validé par le modèle booléen.
Incohérent dans CCI si la disjonction est dans Set : de part la dérivabilité de l’axiome du choix (somme forte/élimination dépendante) et de true ≠ false dans Set, on peut injecter Prop dans bool (une « rétraction »), puis encoder le système U- et dériver l’absurde.
Remarque: ∀ A:Set. A∨ ¬ A est supposé cohérent. Ce qui permet vraiment de montrer une incohérence, c’est que la disjonction soit dans Set.
Dans CCI, la logique classique entraîne l’indiscernabilité des preuves (la preuve nécessite l’élimination dépendante des inductifs de Prop et l’imprédicativité, cf Barbanera et Berardi [BB96]).
La complétude propositionnelle (∀ A:Prop.A=True ∨ A=False) est équivalente dans CC à la conjonction de la logique classique et de l’extensionnalité propositionnelle (∀ A,B:Prop.(A↔ B)→ A=B).
Dans CCI, l’extensionnalité propositionnelle entraîne l’indiscernabilité des preuves (la preuve nécessite l’élimination dépendante des inductifs de Prop).
L’axiome du choix (forme fonctionnelle) est dérivable si l’existentielle (notée alors comme un Σ-type) est dans Set ou dans Type :
(∀ x:X.Σ y:Y. P(x,y))→ Σ f:X→ Y.∀ x:X. P(x,fx) |
Si l’existentielle est dans Prop et Y dans Set, l’axiome est incohérent en présence de la logique classique dans Prop, car alors, on peut injecter Prop dans bool et encoder le système U-.
∀ X:Type. ∀ A:Set. (∀ x:X.∃ a:A. P(x,y))→ ∃ f:X→ A.∀ x:X. P(x,fx) |
En fait, une forme beaucoup plus faible de l’axiome du choix (bien que plus compliquée à exprimer), à savoir l’axiome de description suffit à obtenir cette contradiction.
Remarque: Si Y est dans Type, du fait du sous-typage Set ⊂ Type, la contradiction avec la logique classique persiste.
Contrairement à ce que son nom suggère, l’axiome de choix unique ne choisit pas. Ce qu’exprime l’axiome du choix unique, c’est que toute relation fonctionnelle peut être « réifiée » en une fonction :
(∀ a:A.∃ ! b:B. P(a,b))→ ∃ f:A→ B.∀ a:A. P(a,fa) . |
Si l’existentielle est dans Set ou Type, l’axiome est dérivable. Dans Prop (et avec B dans Set ou Type), il entraîne l’existence d’une rétraction de Prop vers bool:Set. Ainsi, l’axiome est incohérent avec la logique classique dans Prop pour le CCI avec Set imprédicatif (car alors on peut simuler le système U-). Si Set est prédicatif, il reste cohérent avec la logique classique (la rétraction s’interprète comme un oracle qui décide la validité de toute proposition).
On peut aussi s’intéresser aux interactions avec la logique classique calculatoire, c’est-à-dire basée sur une réalisation par l’opérateur call-cc de Scheme ou SML ou l’opérateur µ de Parigot. Une telle interprétation calculatoire de la logique classique est incompatible avec l’axiome de description même avec Set prédicatif [Her05].
Le principe de description indéfinie affirme l’existence a priori d’un témoin canonique dans tout prédicat non vide sur un domaine non vide. On peut l’exprimer en Coq par la proposition
A non vide → Σ x:A. (∃ x:A. P(x)) → P(x) . |
Ce principe est équivalent à se donner, pour tout A non vide, un opérateur є:(A→ Prop)→ A tel que ∃ x:A. P(x) → P(є(P)) (opérateur є de Hilbert).
De manière évidente, le principe de description indéfinie entraîne l’axiome du choix.
Le principe de description indéfinie (dans sa version constructive) exprime que si une proposition est prouvablement habitée, alors il existe un terme qui dénote un habitant de cette proposition. Ce principe peut être exprimé dans le CCI par la formule
∃ x:A. P(x) → Σ x:A. P(x) . |
Notons que le principe de description indéfinie est dérivable si A est dénombrable et P décidable. En effet, on peut alors construire un programme qui teste successivement si chacun des éléments de A, dans l’ordre, vérifie P. Ce programme est calculable par décidabilité de P et terminant par existence d’un habitant dans P. On en déduit le principe de description (cf theories/Logic/ConstructiveEpsilon.v).
Le principe de description définie restreint le principe de description indéfinie au cas des prédicats habités par un objet unique. Le témoin a priori de la non vacuité du prédicat ne vérifie le prédicat que si ce terme est prouvablement unique. Le principe de description définie peut être exprimé dans le CCI par la formule
A non vide → Σ x:A. (∃ ! x:A. P(x)) → P(x) . |
Ce principe est équivalent à se donner, pour tout A non vide, un opérateur ι:(A→ Prop)→ A tel que ∃ ! x:A. P(x) → P(ι(P)) (opérateur ι de Church).
Ce schéma n’entraîne pas l’axiome du choix mais il entraîne l’axiome du choix unique.
Dans sa version constructive, le principe de description définie ne présuppose pas l’existence a priori de témoins : le témoin d’un prédicat n’aura une dénotation que si le prédicat est effectivement habité de manière unique. Ce principe s’exprime dans le CCI par la formule
∃ ! x:A. P(x) → Σ x:A. P(x) . |
Tout comme le principe de description indéfinie dans sa version constructive, la description définie est dérivable dans sa version constructive si A est dénombrable et P décidable.
L’axiome du choix sous sa forme relationnelle s’exprime par
|
L’axiome du choix relationnel + l’axiome de choix unique est équivalent à l’axiome du choix fonctionnel.
Dans les conflits entre logique classique, axiome du choix et imprédicativité de Set, c’est la composante « choix unique » qui pose problème. En effet, cette dernière, en présence de la logique classique, peuple le monde des fonctions d’objets non calculables, ce qui est incompatible avec la vision du monde requise par l’imprédicativité, vision pour laquelle seules existent les fonctions qui sont calculables.
Ainsi, l’axiome du choix (avec sa réelle capacité à ordonner les domaines non dénombrables) n’a semble-t-il rien d’incompatible avec logique classique et imprédicativité si l’on se restreint à sa formulation relationnelle.
L’extensionnalité des prédicats + l’axiome du choix (même sous une forme relationnelle qui n’implique pas l’axiome de description) entraîne la logique classique !! C’est à l’origine un résultat de Diaconescu pour la théorie des ensembles qui a été adapté à la théorie des types par Lacas et Werner [Dia75, LW99].
L’extensionnalité des fonctions exprime pour deux types A et B (ou plus généralement pour un produit fonctionnel ∀ x:A.B(x)) que deux fonctions ayant le même graphe d’entrées-sorties sont égales
∀ f,g:(∀ x:A.B(x)). (∀ x:A. f(x)=g(x))→ f=g |
Typiquement, l’extensionnalité fonctionnelle implique que l’addition sur les entiers définie par récurrence sur son premier argument est égale à l’addition définie par récurrence sur son second argument. L’extensionnalité n’est pas prouvable (elle n’est pas validée par le modèle de réalisabilité qui est intentionnel; par ailleurs, une inspection des formes normales possibles d’une éventuelle preuve devraient permettre d’affirmer l’absence d’une telle preuve).
Un modèle ensembliste validerait l’extensionnalité fonctionnelle. Donner un modèle ensembliste du Calcul des Constructions Inductives avec Set prédicatif est faisable à la condition de retirer la règle de sous-typage Prop ⊂ Type.
En présence de Prop ⊂ Type, il est vraisemblable que le modèle ensembliste fonctionne mais il reste des obstacles techniques. Une question ouverte reste donc la compatibilité de l’extensionnalité fonctionnelle avec le sous-typage Prop ⊂ Type.
Sans condition de garde, on peut directement dériver l’absurde:
Fixpoint Paradox (u:unit) : False := Paradox u.
Sans condition de positivité, on peut facilement dériver l’absurde:
Inductive A : Prop := intro : (A->False)->A. Definition Paradox : False := (fun (H:A->False) => H (intro H)).
Sans restriction de l’élimination forte sur un inductif large, on pourrait encapsuler le type des propositions (un type large) comme une proposition (un petit type) et le redécapsuler à volonté sans perte d’information.
Inductive prop : Prop := down : Prop -> prop. Definition up (p:prop) : Prop := let (A) := p in A. Theorem iso : forall A:Prop, up (down A) = A. Proof. reflexivity. Qed.
La quantification imprédicative dans Type du système U- deviendrait ainsi simulable dans le CCI par une simple quantification imprédicative dans Prop, rendant possible la dérivation d’un paradoxe dans le CCI.
La positivité large n’est pas suffisante pour garantir l’absence de paradoxe. De fait, autoriser le type non strictement positif suivant
Inductive T : Type := I : ((T->Prop)->Prop)->T.
conduit à un paradoxe. L’idée (extraite de Coquand–Paulin-Mohring [CPM90]) est la suivante: Tout objet de type A peut s’interpréter comme un ensemble singleton de type A→Prop en posant sA(t) = λ x:A. x=t. Pour A étant T→ Prop, on en déduit l’existence d’un plongement φ(P) = I (sT→Prop(t)) de T→Prop vers T. Ce plongement est injectif par injectivité de I. On pose alors
|
Par injectivité de φ, on montre que P0(φ(P0)) est équivalent à ¬ P0(φ(P0)). Contradiction.