Digressions

6 Digressions

Les permutabilités, l'herbrandisation et la skolémisation syntaxiques sont apparemment inutiles à notre propos. En effet, nous nous intéressons principalement à la vérité, autrement dit la validité des formules. La notion sémantique d'herbrandisation ou de skolémisation réduit le problème de la validité à celui pour les formules existentielles, et nous pourrions nous satisfaire du théorème de Herbrand (théorème 28), dont la complétude de LK restreint aux formules existentielles découle immédiatement.

Pourquoi avons-nous donc redérivé l'herbrandisation et la skolémisation par des moyens syntaxiques ? La réponse est, pour mieux comprendre ce que cela signifie réellement, et parce que parfois, on ne peut pas faire autrement.

6.1 Logiques non classiques

Considérons par exemple le cas des logiques intuitionniste ou linéaire. Ces logiques, comme beaucoup d'autres, sont mieux comprises au travers de leurs systèmes de preuve. Les modèles de Kripke de la logique intuitionniste fournissent un moyen rapide de vérifier que certaines formules ne sont pas intuitionnistiquement valides, mais la sémantique la plus intéressante de la logique intuitionniste est l'interprétation de Brouwer-Heyting-Kolmogorov, ou de Curry-Howard : mais cette sémantique n'est que la théorie de la preuve de la logique, retraduite en notation functionnelle (en l-calcul).

La logique intuitionniste se présente sous la façon la plus simple en prenant le système de déduction naturelle de la logique classique du premier ordre, moins la règle :

(La règle (¬¬ I) peut être conservée, de toute façon elle est démontrable à partir des autres.)

Un système de séquents est obtenue en restreignant les séquents à n'avoir qu'une formule à droite, et en effectuant les ajustements nécessaires (cf. figure 4).

Figure 4: Le système LJ de Gentzen

Et la sémantique de Kripke de la logique intuitionniste est donnée par un cadre (W,£), où £ est un ordre (comme pour S4), un domaine non vide D, une interprétation I des symboles de fonction et de prédicats (où I(P), pour chaque prédicat P d'arité m, est une fonction de D^m vers P W et non plus B), et où pour toute affectation r :

w,I,r |= A si et seulement si w'Î [A] I r pour tout w' ³ w, où A est un atome; (en S4, on aurait juste écrit wÎ [A] I r;)
w,I,r |= FÙF' si et seulement si w,I,r|=F et w,I,r|=F';
w,I,r |= FÚF' si et seulement si w,I,r |= F ou w,I,r |= F';
w,I,r |= ¬F si et seulement si pour tout w'³ w, non w',I,r |= F; (comparer avec S4 !)
w,I,r |= FÞF' si et seulement si pour tout w'³ w, si w',I,r |= F alors w',I,r |= F'; (comparer avec S4 !)
w,I,r |= " x · F si et seulement si pour tout w' ³ w, pour tout vÎ D, w',I,r[v/x] |= F;
w,I,r |= $ x · F si et seulement s'il existe vÎ D tel que w,I,r[v/x] |= F.

La preuve de complétude est plus compliquée que dans le cas classique, et se complique d'autant plus si l'on veut savoir si la contraction (la duplication en terme de tableaux) est éliminable ou non. En fait, la contraction n'est pas éliminable, et le mieux qu'on puisse faire sur LJest de la visser dans les règles d'où elle n'est pas éliminable (notamment, ÞL et "L).

De plus, en LK toutes les stratégies étaient également acceptables pour trouver une preuve, mais en LJ ce n'est pas le cas. On peut le remarquer sémantiquement : certaines règles ne sont pas inversibles, autrement dit, certaines ont la propriété que la conjonction de leurs prémisses n'est pas équivalente à leur conclusion. On peut le remarquer directement sur le système de preuve, car certaines règles ne permutent pas. Il y a en fait 11 impermutabilités dans LJ : "L/"R, "L/$L, $R/"R (comme dans le cas classique), ÞL/ÞR, ¬L/ÞR, ÞL/¬R, ¬L/¬R, ÞL/ÚL, ÚR/ÚL, ¬L/ÚL et $R/ÚL. (Exercice.)

On peut partiellement corriger certains de ces problèmes : cf. [Dyc92] pour divers systèmes dans le cas propositionnel, certains maximisant le nombre de règles inversibles, et un évitant totalement la contraction; cf. aussi [MMO93] pour le cas intuitionniste au premier ordre. Le lecteur qui aura lu les deux articles sera sans doute convaincu que l'approche syntaxique est plus simple que l'approche sémantique. (Cf. figure 5 pour ce dernier système; les séquents sont de la forme G ¾® D₁; D₂, où G, D₁ et D₂ sont des multi-ensembles de formules; un séquent G ¾® F₁, ..., F_m; Y₁, ..., Y_n se traduit en un séquent G, ¬ Y₁, ..., ¬ Y_n ¾® F₁ Ú ... Ú F_m de LJ, et est vérifié au monde w si et seulement si non w,I,r |= F pour au moins une formule F de G, ou w,I,r |= F_i pour un certain i, 1£ i£ m, ou il existe j, 1£ j£ n, et w'³ w tel que w',I,r |= Y_j.)

Figure 5: Le système de Miglioli, Moscato et Ornaghi

Le cas de la logique linéaire est encore plus frappant. Alors que l'on connait plusieurs sémantiques de la logique linéaire du premier ordre, aucune sémantique n'a été prouvée complète---du moins, aucune sémantique plus simple que le système de preuves. La plupart des résultats en logique linéaire (la cohérence, notamment) n'ont pu être déduits que par l'élimination des coupures et les propriétés des preuves par séquents sans coupure.

Du point de vue de la démonstration automatique, un système de séquents sans coupure fournit aussi directement une méthode de tableaux, et donc une méthode naturelle de recherche de preuve. (Mais en trouver une efficace, qui évite les répétitions durant la recherche, est beaucoup moins évident.)

6.2 Arithmétique

D'autre systèmes de preuve sont incomplets : le fait de chercher une preuve de F dans de tels systèmes n'est pas la même chose que de vérifier si F est valide. Nous serions tentés d'ajouter de nouvelles règles de preuve, dans ces conditions, pour obtenir un système de preuve complet, mais il y a des cas où c'est impossible. Ceci est une conséquence du théorème d'incomplétude de Gödel :

Théorème 33 [Gödel] Soit D un système de preuve, dans lequel on peut interpréter l'arithmétique de Peano du premier ordre PA₁, autrement dit il existe des formules Z(x) (``x égale zéro''), S(x,y) (``y est le successeur de x''), P(x,y,z) (``z=x+y''), T(x,y,z) (``z=xy''), E(x,y) (``x égale y''), L(x,y) (``x est inférieur ou égal à y'') dans le langage de D qui vérifient prouvablement tous les axiomes de PA₁.

Alors une des assertions suivantes doit être vraie :

D est incomplet, autrement dit il existe une formule F construite au moyen des connecteurs logiques, et des quantificateurs sur les formules Z, S, P, T, E, L ci-dessus, telle que F soit vraie dans le modèle standard N de l'arithmétique, mais n'est pas prouvable dans D;
ou D est incohérente, autrement dit toute formule est prouvable dans D;
ou D n'est pas effectif, autrement dit il n'existe aucun algorithme décidant si une formule est (textuellement) un axiome de D ou si une règle d'inférence est une règle de D;

ce qui laisse un choix assez restreint. Il est clair que l'on préfère usuellement que D soit incomplet mais effectif et (on l'espère) cohérent. (Pour une preuve de ce théorème, voir [Joh92] ou [Man77].)

À cause du théorème d'incomplétude de Gödel, il existe des systèmes de preuve, comme ceux qui décrivent l'arithmétique de Peano du premier ordre ou la théorie des ensembles de Zermelo-Frænkel (dans laquelle on peut construire les entiers), où on ne peut pas raisonner sémantiquement ! Certains énoncés valides n'ont en effet aucune preuve dans le système correspondant. Nous sommes alors forcés de raisonner syntaxiquement, autrement dit sur le système de preuve directement.

Gerhard Gentzen a inventé les systèmes de séquents justement pour cela, et dériver des preuves de cohérence pour l'arithmétique, ce qu'il est arrivé à faire en 1934. L'idée est que les théorèmes de PA₁ sont exactement ceux du système de séquents Z, qui est LK plus une infinité d'axiomes (tous les séquents atomiques clos qui sont propositionnellement dérivables des instances d'axiomes de PA₁ sauf les axiomes de récurrence), et plus une règle appelée l'w-règle qui exprime que l'on peut déduire " n · P(n) de P(0), P(1), etc., et où les preuves ont une profondeur finie (bornée). L'élimination des coupures fonctionne pour Z exactement comme pour LK, et nous pouvons donc dériver les propriétés usuelles à partir de l'élimination des coupures, la cohérence et la propriété de sous-formule. (La compacité échoue car l'w-règle est infinitaire. De plus, l'élimination des coupures échoue dans LK plus l'axiome de récurrence : elle ne fonctionne que dans Z.)

Mais l'élimination des coupures fournit davantage. La preuve du théorème d'élimination des coupures est une preuve de terminaison, qui montre que le processus de remontée des coupures termine. Par la correspondance de Curry-Howard entre preuves et programmes, ceci signifie qu'un certain langage dont les types sont des formules du premier ordre est normalisant. En fait, ce langage est fortement normalisant, ce qui veut dire que toutes les stratégies de remontée des coupures terminent. Ce langage est le système T de Gödel [GLT89], et est essentiellement un l-calcul étendu avec des constantes 0 (zéro), s (successeur), et un récurseur R qui obéit aux règles de calcul :

R f z 0 ® z

R f z (s n) ® f z n (R f z n)

avec les types appropriés. Plus clairement, pour chaque fonction définissable f, R f z est une fonction g définie par récursion primitive (en chaque type, même d'ordre supérieur) par g(0) = z et g(n+1) = f (z,n,g(n)).

Des extensions de cette correspondance entre systèmes de preuve et programmes ont mené Jean-Yves Girard à montrer que PA₂ (l'arithmétique de Peano du second ordre, avec l'axiome de récurrence complet " P · P(0) Þ (" n · P(n) Þ P(s(n))) Þ " n · P(n)), et même PA_w (l'arithmétique de Peano d'ordre supérieur, avec l'axiome de récurrence complet et tous les raisonnements à tous les ordres) sont cohérents, en interprétant l'élimination des coupures comme la règle de réduction fondamentale d'un langage de programmation, le l-calcul de Church restreint aux termes typables dans le système F de Girard (resp. F_w), et en montrant que tous les termes du langage sont fortement normalisants. Le système F est essentiellement la logique propositionnelle quantifiée (intuitionniste), mais elle capture toutes les particularités de PA₂ pour ce qui est de la typabilité.

Grâce à l'élimination des coupures, PA₁ possède une forme de théorème de Herbrand. Il s'agit de l'interprétation par absence de contre-exemple (``no-counterexample interpretation'' en anglais) de Georg Kreisel pour PA₁. Alors que le théorème de Herbrand dit essentiellement que " x· $ y· Y est prouvable dans LK si et seulement si l'on peut trouver des témoins pour y sous la forme de programmes si-alors-sinon finis dépendant de x qui retournent des termes, le résultat de Kreisel dit que " x· $ y· Y est prouvable dans PA₁ (ou Z) si et seulement si l'on peut trouver une fonction f prenant x en argument, définie par des programmes finis construits à l'aide de récursions primitives en n'importe quel type (celles permises par les récurseurs de Gödel), telle que " x · Y [f(x)/y] soit ``vraie'', au sens où il n'existe pas de valeur calculable pour x telle que Y [f(x)/y] soit fausse. (Ce qui est assez tordu, on est d'accord.) C'est-à-dire que PA₁ enrichit l'ensemble des programmes dont nous avons besoin comme témoins, en permettant une forme de récursion contrôlée, qui termine, et appelée récursion primitive. (Voir [Sho67], spécialement le chapitre 8. Voir aussi [Sch77].)

6.3 Logique d'ordre supérieur

PA₂ et PA_w sont axiomatisables en logique du premier ordre, mais sous forme de théories relativement compliquées. Si nous souhaitons raisonner en arithmétique, il vaut mieux abandonner le domaine de la logique du premier ordre, soit en édifiant un nouveau système de preuve conçu exclusivement pour l'arithmétique, soit en se plaçant dans un cadre encore plus général.

Un de ces cadres est la logique d'ordre supérieur, où l'on peut quantifier non seulement sur des individus, mais aussi sur des prédicats, des fonctions, des prédicats portant sur des prédicats, et ainsi de suite. La logique d'ordre supérieur est très expressive, et on peut par exemple formaliser PA_w, ainsi que l'analyse (la théorie de la droite réelle R) du second ordre et à l'ordre supérieur, ainsi que la plupart des autres théories mathématiques sans difficulté. Le prix à payer est que pratiquement toutes les belles propriétés que nous avions auparavant sont fausses en logique d'ordre supérieur : la compacité et la complétude sont fausses, la propriété de sous-formule aussi (à moins d'accepter une notion passablement inutilisable de sous-formule), bien que l'élimination des coupures fonctionne toujours. Pire encore, on ne peut même plus effectuer d'herbrandisation ou de skolémisation à l'avance, et la recherche de preuve est considérablement compliquée par rapport au premier ordre par le fait que presque tous les sous-problèmes que l'on rencontre (l'unification en particulier) deviennent indécidables. (Voir [Hue73, Hue75] pour les problèmes, des explications, des exemples et tous les détails.)

Bien que nous n'étudions pas les logiques d'ordre supérieur, il est intéressant de donner une description rapide de la syntaxe, des règles de preuve, et des sémantiques des logiques d'ordre supérieur, de sorte que les problèmes soient plus visibles.

6.3.1 Syntaxe

La formulation la plus simple de la logique d'ordre supérieur est due à Church, qui l'a fondée sur le l-calcul simplement typé, en ajoutant des constantes pour représenter les quantificateurs. Syntaxiquement en effet, nous pouvons utiliser l'opérateur lieur de variables l pour représenter toutes les opérations qui lient des variables, et considérer " x·F comme une abréviation de "(l x·F), où " est une constante qui prend une fonction f à valeurs booléennes en argument et retourne T si et seulement si f est la fonction constante T. Le besoin d'utiliser un calcul typé au lieu du l-calcul non typé provient du fait que le système sans les types est incohérent. Un tel système non typé a été inventé par Gottlob Frege dans les années 1890 pour formaliser les mathématiques; mais on peut y écrire une formule qui se contredit elle-même, le paradoxe de Russell, qui est essentiellement la même chose que le paradoxe du menteur. Définissons F comme étant la fonction :

l x· ¬ x(x)

et considérons F(F). Par b-réduction, F(F) est égal à ¬ F(F), d'où l'on déduit n'importe quelle formule.

Définissons en premier l'algèbre des types simples. Les types de base sont soit B (le type des formules) soit T (le type des termes). Nous pourrions aussi raffiner T en plusieurs types différents, et c'est à la base ce que les logiques à sortes font (cf. [SS89, Wal88]). Les types simples sont les éléments du plus petit ensemble contenant les types de base, et tel que si t et t' sont des types simples, alors t®t' est un type simple. Comme d'habitude, nous supposons que les flèches associent à droite, donc t®t'®t'' signifie t®(t'®t'').

Pour définir les expressions de la logique d'ordre supérieur, fixons une signature S, qui est un ensemble de constantes pour chaque type. Nous supposons en général qu'il existe au moins une constante de chaque type. De même, nous supposons qu'il existe une infinité de variables x_t de chaque type t. Nous omettrons les indices de types lorsqu'ils ne sont pas nécessaires. La syntaxe des expressions d'ordre supérieur e est alors définie en même temps que les jugements de typage e:t comme suit :

x_t est une expression de type t (nous notons x_t:t);
si c est une constante de type t, alors c est une expression de type t;
si e:t®t' et e':t, alors ee', l'application de e à e', est une expression de type t';
si e:t', alors l x_t· e, l'abstraction de e sur x, est une expression de type t®t'.

Finalement, nous supposons que S contient les constantes logiques Ù:B®B®B (conjonction), Ú:B®B®B (disjonction), Þ:B®B®B (implication), ¬:B®B (négation), "_t:(t®B)®B (quantification universelle sur les objets de type t, pour chaque t), et $_t:(t®B)®B (quantification existentielle sur les objets de type t, pour chaque t). Les variables libres, les substitutions sont définies comme en logique du premier ordre, en prenant soin de renommer les variables liées pour éviter les captures de noms de variables.

Remarquons que nous pouvons coder les termes et les formules de la logique du premier ordre dans ce cadre. Nous traduisons les fonctions n-aires f en constantes f de type T®...®T ®T (avec n flèches ®), et les symboles de prédicat n-aires P en constantes P de type T®...®T ®B (avec n flèches ® encore). Ainsi, une application f(t₁,...,t_n) est codée sous forme de l'application (... (ft₁)t₁... t_n). Si nous utilisons la convention que l'application associe à gauche, nous pouvons aussi l'écrire ft₁... t_n.

6.3.2 Sémantique standard

La sémantique standard est essentiellement ce à quoi on s'attend après avoir vu la définition, sachant ce qu'est la sémantique de la logique du premier ordre. Une interprétation standard est un ensemble non vide D_I muni d'une interprétation pour chaque constante, cette interprétation respectant le type de la constante. Plus précisément, nous définissons l'interprétation des types par :

[T]I=D_I, [B]I=B;
[t®t']I est l'espace de toutes les applications (fonctions totales) de [t]I vers [t']I.

Pour que l'interprétation I(c) respecte le type t de c, nous devons imposer la contrainte : I(c)Î[t]I, autrement dit les constantes de type T doivent représenter des valeurs de D_I, les constantes de type T®T doivent représenter des applications unaires de D_I vers D_I, et ainsi de suite.

Naturellement, nous imposons aussi la constrainte que toutes les constantes logiques Ù, Ú, Þ, ¬, ", $ aient le sens souhaité, et :

[ee']Ir=[e]Ir([e']Ir);
[l x_t· e]Ir est l'application envoyant chaque vÎ[t]I vers [e]I(r[v/x]).

Dans la sémantique standard, nous pouvons définir l'arithmétique par les axiomes de Peano de base, plus l'axiome de récurrence (qui peut maintenant s'écrire sous forme d'un axiome unique, grâce à la quantification à l'ordre supérieur) :

" P

T®B

P(0)Ù (" x

· P(x)Þ P(s(x)))Þ

" x

· P(x)

et nous obtenons ainsi l'arithmétique d'ordre supérieur. Nous pouvons montrer que N est un modèle de l'arithmétique d'ordre supérieur, et que c'est le seul à isomorphisme près.

Le problème principal de l'arithmétique d'ordre supérieur est que, à cause du théorème de Gödel, et parce que nous avons un modèle (N), tout système axiomatique cohérent et effectif doit être incomplet. (Le système ci-dessus est effectif au second ordre, quoique ce ne soit pas facile à voir, par exemple.) De plus, nous pouvons coder l'arithmétique directement en logique d'ordre supérieure sans introduire de nouveaux symboles comme s ou de nouveaux axiomes comme ceux ci-dessus, en représentant les entiers n comme des entiers de Church l f_T_®_T·l x_T· f(f(... f(x)...) (où f est appliquée n fois à x). De nouveau, à cause du théorème de Gödel, tout système axiomatique cohérent et effectif pour la logique d'ordre supérieur est incomplet.

6.3.3 Systèmes de preuve

Nous décrivons maintenant comment le système de séquents du premier ordre LK peut être étendu aux ordres supérieurs. Le système obtenu est cohérent, ainsi que Girard l'a montré, donc il doit être incomplet.

Nous définissons les règles de réduction comme étant celles du l-calcul :

(b) (l x· e)e'® e[e'/x]
(h) l x· ex ® e si xÏfv(e)

Ceci définit deux relations binaires (notées ® ci-desus), que nous noterons b et h respectivement. Soit l l'une des deux relations b ou bÈh. Nous appelons ¾®_l la plus petite relation contenant l et stable par application de contexte (c'est-à-dire telle que si e¾®_l e', alors eu¾®_leu', ue¾®_lu'e, et l x· e¾®_ll x· e'). Notons ¾®_l^* la clôture réflexive transitive de ¾®_l, et =_l sa clôture réflexive symétrique transitive. Remarquons que, si e=_le', alors trivialement e et e' doivent avoir les mêmes interprétations standard.

Le l-calcul simplement typé a la propriété remarquable que nous pouvons décider si e=_le' en normalisant d'abord e et e' (c'est-à-dire en les réduisant tant que c'est possible, jusqu'à obtenir une forme normale), et en comparant les formes normales textuellement. C'est parce que ce calcul est confluent et terminant; pour plus de détails sur le l-calculus, consulter [Bar84].

Nous pouvons étendre LK simplement en remplaçant les règles d'inférence des quantificateurs par les versions typées suivantes :

où t est de type t, et la règle :

qui signifie que nous pouvons toujours remplacer toute expression par une qui lui est l-équivalente. En pratique, on maintient toutes les formules en forme normale pour ¾®_l, et ceci règle le cas de la règle (l).

Mais ceci ne traite vraiment du cas de la règle (l) que si toutes les instances en sont connues à l'avance. Considérons en effet la règle $R : pour montrer G¾® $ x_t·F, D, nous devons deviner une expression t de type t telle que G¾® F[t/x],D soit prouvable. Nous verrons que, au premier ordre, nous n'avons pas à deviner ce terme, parce qu'une procédure spéciale d'unification nous la fournira. L'unification au premier ordre signifie trouver une substitution s telle que ts=t's, étant donnés deux termes t et t'. Aux ordres supérieurs, l'unification d'ordre supérieur (trouver des substitutions s envoyant chaque variable vers des expressions du même type telles que ts=_lt's, étant donnés deux termes t et t' du même type) ne suffit plus dans les systèmes de tableaux. Mais même à part ça, ce problème est indécidable dès que des symboles de fonction ou de prédicats sont autorisés (et pourvu que l'on ait deux constantes aussi).

Pour voir que le système de logique d'ordre supérieur ci-dessus présente de nombreuses autres difficultés, considérons l'exemple :

¬ $ F

T®T®B

" P

T®B

$ x

" y

· FxyÛ Py

qui exprime une forme faible du théorème de Cantor (il n'existe pas d'application surjective F de D vers P(D), où D est représenté par le type T, et l'ensemble des parties P(D) est représenté comme l'ensemble des fonctions caractéristiques de type T®B; la formule exprime la surjectivité en disant que pour tout sous-ensemble P de D, il existe un x tel que Fx=P).

Nous serions tentés de skolémiser, et donc d'essayer de réfuter :

F(cX)yÛ Xy

où X_T_®_B et y_T sont les deux variables (X représente P), F est une constante de Skolem de type T®T®B, et c est une fonction de Skolem unaire, de type (T®B)®T. Nous pouvons conclure en utilisant la substitution [l x_T·¬ (Fxx)/X,c(l x_T·¬ (Fxx))/y].

Mais le problème est que, bien que la skolémisation soit correcte pour la sémantique standard, elle est incorrecte pour le système de preuve. La skolémisation dépend en effet de l'axiome du choix :

" P

t®t'®B

(" x

$ y

· Pxy) Þ

($ f

t®t'

" x

· Px(fx))

qui est improuvable dans ce système, bien qu'il soit vrai dans la sémantique standard.

La solution usuelle est d'enrichir le système de preuve par une règle exprimant l'axiome du choix. Nous avons alors le problème inverse : tenter de prouver une formule en la skolémisant puis en cherchant à trouver une preuve de la formule sans quantificateur qui en résulte est une méthode incomplète. En fait, nous devons de temps en temps utiliser l'axiome du choix (ou skolémiser certains quantificateurs seulement) en plein milieu de la recherche d'une preuve. Ceci est dû au fait que le remplacement de variables par des expressions d'ordre supérieur peut complètement changer la forme de la formule. Par exemple :

" P

B®B

P($ x

·F(x))

En appliquant la substitution [l y· y/P], nous pouvons en déduire :

$ x

· F(x)

où le quantificateur existentiel apparaît positivement, mais en appliquant [¬/P], nous obtenons :

¬$ x

· F(x)

où la quantification existentielle apparaît négativement. Il n'y a aucun moyen de décider à l'avance comment skolémiser ce quantificateur existentiel.

Le fait de remplacer P par des expressions booléennes plus compliquées peut en fait instancier la formule P($ x_T·F(x)) pour en extraire n'importe quelle formule. C'est la raison pour laquelle nous disons que la propriété de la sous-formule n'est pas valide des preuves sans coupure (et pourquoi l'unification ne suffit pas dans les tableaux). L'élimination des coupures fonctionne, mais ne fournit qu'une aide minime pour automatiser la recherche de preuve, ici.

6.3.4 Sémantique générale

Nous avons vu qu'il y avait au moins quatre variantes différentes de logiques d'ordre supérieur, selon que nous admettons la b-égalité ou la bh-égalité, et selon que nous admettons ou non l'axiome du choix. Ces logiques ont réellement des ensembles de théorèmes différents, bien que cela ne se voie pas à l'examen de la sémantique standard.

Pour montrer plus précisément ce qui arrive dans ces divers systèmes, Leon Henkin a proposé une sémantique plus générale des logiques d'ordre supérieur en 1950 (see [And86]). L'astuce est que les dénotations des types fonctionnels peuvent devenir trop gros : par exemple, si T est interprété par N, T®T doit être interprété par l'ensemble de toutes les fonctions de N vers N dans la sémantique standard. Mais on ne peut décrire qu'un sous-ensemble dénombrable de fonctions par des formules, et nous pouvons penser que c'est une cause raisonnable d'incomplétude.

Henkin a donc conçu une notion plus abstraite d'interprétation des types, de l'application et de l'abstraction. Une interprétation générale remplace l'ensemble non vide D_I par une famille D d'ensembles D_t indicés par les types t, munie d'un opérateur d'application@_t,t', ou @ en abrégé, de D_t®t'× D_t vers D_t'. Le couple (D,@) est une structure applicative si et seulement si toutes les expressions ont des interprétations, où l'interprétation est définie en modifiant la notion d'interprétation standard :

[ee']Ir=@([e]Ir,[e']Ir);
[l x_t· e]Ir est un élément f de D_t®t', où e:t', tel que pour tout vÎ[t]I, @(f,v)=[e]I(r[v/x]).

Une structure applicative est donc une structure qui contienne suffisamment d'éléments pouvant être interprétés comme des fonctions de D_t vers D_t'.

Nous pouvons maintenant définir le concept de structure générale. Une structure générale est une structure applicative munie d'une valuation, qui est par définition une application u de D_B vers B qui interprète les éléments de D_B comme des booléens, et telle que u(@([¬]Ir,x)) soit la négation de u(x), u(@(@([Ù]Ir,x),y)) soit la conjonction de u(x) et u(y), et ainsi de suite. En effet les structures applicatives n'imposent pas que l'interprétation de D_B soit B.

Remarquer aussi que nous n'avons pas exigé que fÎ D_t®t' soit unique parmi tous les éléments représentant la fonction l x_t· e dans la définition des interprétations générales. Et en effet, il existe des structures applicatives non extensionnelles, autrement dit des structures applicatives dans lesquelles " x· fx=gx n'implique pas f=g, pour certains termes f et g où x n'est pas libre. En fait, l'h-égalité est le cas particulier où g est l y· fy (par (b), pour tout x, fx = (l y· fy)x, donc l'extensionnalité implique f = l y· fy dans ce cas), et il existe des structures applicatives où (h) n'est pas valide; en particulier, (h) n'est pas prouvable à partir de la b-égalité seule.

Remarquer finalement que les structures applicatives peuvent ne pas être assez riches pour satisfaire l'axiome du choix. Elles n'ont besoin que de contenir des fonctions représentant les l-abstractions, mais pas les fonctions de choix. En particulier l'axiome du choix n'est pas prouvable à partir du système de séquents d'ordre supérieur de la dernière section.

Les structures générales jouent essentiellement le même rôle pour le système de séquents d'ordre supérieur que les interprétations du premier ordre jouent pour LK. Nous pouvons alors redévelopper une forme de théorie de Herbrand. En particulier, une structure générale parfaitement acceptable est celle de toutes les classes d'équivalence de l-termes typés modulo la congruence engendrée par (b) et (h), où @ est l'application ordinaire du l-calculus et D_B est l'ensemble des booléens de Church par exemple. Cette interprétation syntaxique est tout à fait analogue à celle de Herbrand sur l'univers des termes clos en logique du premier ordre.

Il n'est pas très surprenant que le système de séquents d'ordre supérieur de la dernière section soit correct et complet pour la sémantique des structures générales. Bien sûr, nous perdons la possibilité d'axiomatiser N ou R par des logiques d'ordre supérieur en sémantique des structures générales, à cause du théorème de Gödel.

En particulier, il reste des formules valides improuvables. Un cas particulièrement frustrant, dû à Michael Kohlhase [Koh95], est :

¬ cbÚ c(¬¬ b)

qui est improuvable dans notre système de séquents, ou dans le premier système de tableaux de Kohlhase, qui est intensionnel (autrement dit, non extensionnel). La raison en est que la seule façon de le prouver est de montrer que b=¬¬ b. Malheureusement, nous pouvons prouver b Û ¬¬ b, et bien que nous puissions penser que l'équivalence logique et l'égalité devrait être les mêmes objets de type B, les structures générales permettent le contraire. (Choisir D_B contenant plus de deux éléments.)

On peut le réparer en considérant les modèles généraux, qui sont des structures générales dans lesquelles D_B est contraint à être exactement B, et u à être l'identité. Au système de preuve, nous ajoutons les axiomes suivants d'extensionnalité booléenne (qui était donc improuvable à partir des autres) :

" F

" G

· (FÛ G)Û F= G

où = est l'égalité définissable de la logique d'ordre supérieur, à savoir F= G égale " P· P(F)Þ P(G). (Il s'agit de l'égalité de Leibniz, qui dit que deux objets sont égaux si et seulement s'ils ont les mêmes propriétés.) Le système de preuve qui en résulte est alors correct et complet pour les modèles généraux (mais pas pour les modèles standard, bien sûr).

Nous terminons ici notre étude des notions et chausses-trappes fondamentales de la logique d'ordre supérieur. Pour plus de détails, consulter [And86], un bon livre sur la logique et les preuves consacré pour une bonne part à un système minimal décrivant la logique d'ordre supérieur (avec la règle h, mais sans l'axiome du choix). Il existe des méthodes de preuve automatique pour les logiques d'ordre supérieur : la résolution d'ordre supérieur de Huet [Hue73] et les tableaux d'ordre supérieur de Kohlhase [Koh95] en sont deux. Ces méthodes ont toutes besoin d'une forme d'unification modulo la théorie de la b (resp. bh) conversion entre l-termes typés. La procédure d'unification d'ordre supérieur de Huet est la référence [Hue75], et est en général efficace en pratique. On consultera aussi [SG89] pour une présentation complètement détaillée. On peut étendre une forme de théorie de Herbrand aux ordres supérieurs, comme montré par Miller [Mil87].