Calcul des prédicats

En logique mathématique, le calcul des prédicats du premier ordre, logique du premier ordre, calcul des relations, logique quantificationnelle^{[réf. nécessaire]}, ou tout simplement calcul des prédicats, est un système formel utilisé pour raisonner et décrire des énoncés en mathématiques, informatique, intelligence artificielle, philosophie et linguistique. Il a été proposé par Gottlob Frege comme une formalisation du langage des mathématiques entre la fin du XIX^e siècle et le début du XX^e siècle. La logique du premier ordre comporte deux parties :

• la syntaxe définit le vocabulaire symbolique de base ainsi que les règles permettant de construire des énoncés ;
• la sémantique interprète ces énoncés comme exprimant des relations entre les éléments d'un domaine, également appelé modèle.

Sur le plan syntaxique, les langages du premier ordre opposent deux grandes classes linguistiques :

• les constituants servant à identifier ou nommer des éléments du domaine : variables, symboles de constantes, termes ;
• les constituants servant à exprimer des propriétés ou des relations entre ces éléments : prédicats et formules.

Un prédicat est une expression linguistique qui peut être reliée à un ou plusieurs éléments du domaine pour former une phrase. Par exemple, dans la phrase « Mars est une planète », l'expression « est une planète » est un prédicat qui est relié au nom (symbole de constante) « Mars » pour former une phrase. Et dans la phrase « Jupiter est plus grand que Mars », l'expression « est plus grand que » est un prédicat qui se relie aux deux noms, « Jupiter » et « Mars », pour former une phrase.

Lorsqu'un prédicat est lié à une expression, on dit qu'il exprime une propriété (telle que la propriété d'être une planète), et lorsqu'il est lié à deux ou plusieurs expressions, on dit qu'il exprime une relation (telle que la relation d'être plus grand). Ainsi on peut raisonner sur des énoncés comme « il existe un $x$ tel que pour tout $y$, $x$ est ami avec $y$ », ce qui est exprimé symboliquement par la formule :

$\exists x\forall y~\mathrm {amis} (x,y)$.

Il convient de noter cependant que la logique du premier ordre ne contient aucune relation spécifique (comme telle relation d'ordre, d'inclusion ou d'égalité) ; en fait, il ne s'agit que d'étudier la façon dont on doit parler et raisonner avec les expressions du langage mathématique.

Les traits caractéristiques de la logique du premier ordre sont :

• l'utilisation de variables comme $x$, $y$, etc. pour dénoter des éléments du domaine d'interprétation ;
• l'utilisation de prédicats (ou relations) sur les éléments ;
• l'utilisation d'opérations logiques (et, ou, implique, etc.) ;
• l'utilisation de quantifications, par exemple, l'une universelle (« Quel que soit », « pour tout » noté ∀) et l'autre existentielle (« il existe au moins un… tel que », noté ∃).

Le calcul des prédicats du premier ordre égalitaire adjoint au calcul des prédicats un symbole de relation, l'égalité, dont l'interprétation est l'affirmation que deux éléments sont les mêmes, et qui est axiomatisée en conséquence. Suivant le contexte, on peut parler simplement de calcul des prédicats pour le calcul des prédicats égalitaire.

On parle de logique du premier ordre par opposition aux logiques d'ordre supérieur, où l'on peut aussi appliquer les quantificateurs et les prédicats aux prédicats ou aux fonctions, en plus des variables. En outre, cet article ne traite que de la logique du premier ordre classique, mais on notera qu'il existe aussi une logique du premier ordre intuitionniste.

Introduction

Alors que la logique propositionnelle traite des propositions déclaratives simples, la logique du premier ordre couvre en plus les prédicats et la quantification.

Un prédicat prend en entrée une ou plusieurs entités du domaine du discours et en sortie, il est soit Vrai, soit Faux. Considérons les deux phrases « Socrate est un philosophe » et « Platon est un philosophe ». En logique propositionnelle, ces phrases sont considérées comme non liées et peuvent être désignées, par exemple, par des variables telles que p et q. Le prédicat « est un philosophe » apparaît dans les deux phrases, dont la structure commune est « a est un philosophe ». La variable a est instanciée en tant que « Socrate » dans la première phrase, et est instanciée en tant que « Platon » dans la deuxième phrase. Alors que la logique du premier ordre permet l'utilisation de prédicats, tels que « est un philosophe » dans cet exemple, la logique propositionnelle ne le permet pas.

Les relations entre les prédicats peuvent être énoncées à l'aide de connecteurs logiques. Considérons, par exemple, la formule du premier ordre « si a est un philosophe, alors a est un savant ». Cette formule est un énoncé conditionnel dont l'hypothèse est « a est un philosophe » et la conclusion « a est un savant ». La vérité de cette formule dépend de l'objet désigné par a, et des interprétations des prédicats « est un philosophe » et « est un savant ».

Les quantificateurs peuvent être appliqués aux variables d'une formule. La variable a de la formule précédente peut être quantifiée universellement, par exemple avec la phrase du premier ordre « Pour tout a, si a est un philosophe, alors a est un savant ». Le quantificateur universel « pour chaque » dans cette phrase exprime l'idée que l'affirmation « si a est un philosophe, alors a est un savant » est valable pour tous les choix de a.

La négation de la phrase « Pour tout a, si a est un philosophe, alors a est un savant » est logiquement équivalente à la phrase « Il existe a tel que a est un philosophe et a n'est pas un savant ». Le quantificateur existentiel « il existe » exprime l'idée que l'affirmation « a est un philosophe et a n'est pas un savant » est valable pour un certain choix de a.

Les prédicats « est un philosophe » et « est un savant » prennent chacun une seule variable. En général, les prédicats peuvent prendre plusieurs variables. Dans la phrase du premier ordre « Socrate est le professeur de Platon », le prédicat « est le professeur de » prend deux variables.

Histoire

Emmanuel Kant croyait à tort que la logique de son temps, celle d’Aristote, était une science complète et définitivement achevée (préface de la seconde édition de la critique de la raison pure, 1787). Les logiciens du XIX^e siècle se sont rendu compte que la théorie d’Aristote ne dit rien ou presque sur la logique des relations. Gottlob Frege et beaucoup d'autres ont comblé cette lacune en définissant le calcul des prédicats au premier ordre.

Kurt Gödel a démontré en 1929 (dans sa thèse de doctorat) que le calcul des prédicats est complet, au sens où on peut donner un nombre fini de principes (axiomes logiques, schémas d'axiomes logiques et règles de déduction) qui suffisent pour déduire de façon mécanique toutes les lois logiques (voir le théorème de complétude de Gödel). Il y a équivalence entre la présentation sémantique et la présentation syntaxique du calcul des prédicats. Tout énoncé universellement valide (c'est-à-dire vrai dans tout modèle du langage utilisé) est un théorème (c'est-à-dire qu'il peut être déduit d'un calcul, un système de règles logiques et d'axiomes, de façon équivalente un système à la Hilbert, la déduction naturelle, ou le calcul des séquents), et réciproquement. La logique du premier ordre est donc achevée au sens où le problème de la correction logique des démonstrations y est résolu. Elle continue cependant à faire l’objet d’importantes recherches : théorie des modèles, théorie de la démonstration, mécanisation du raisonnement…

Syntaxe

Exemple d'une formule de la logique du premier ordre. Le schéma montre les quantificateurs, les occurrences des symboles de fonctions et des symboles de prédicats.

Contrairement à un langage naturel, comme le français, la logique du premier ordre est un langage formel. Cette section donne une brève présentation de la syntaxe du langage formel du calcul des prédicats. Pour cela, on a besoin d'un alphabet, c'est-à-dire un ensemble de symboles utilisées pour écrire les énoncés (ou formules). On se donne un ensemble des symboles appelés variables, toujours infini : $x$, $y$, $z$, etc.

Signature

On se donne une signature, c'est-à-dire :

• un ensemble de symboles de fonctions : $f$, $g$, $h$, etc. ;
• un ensemble de symboles de prédicats : $P$, $Q$, $R$, etc.

Chaque symbole de fonction et chaque symbole de prédicat a une arité : il s'agit du nombre d'arguments ou d'objets auxquels il est appliqué. Par exemple, le prédicat $B$ pour « est bleu(e) » a une arité égale à 1 (on dit qu'il est unaire ou monadique), tandis que le prédicat $amis$ pour « être amis » a une arité de deux (on dit qu'il est binaire ou dyadique). Il peut y avoir des symboles de fonction ou de prédicat d'arité 0. Un symbole de fonction d'arité 0 s'appelle une constante. Les constantes se notent généralement $a$, $b$, $c$, etc.

Exemples

• Si l'on veut parler de personnes, Bob est un symbole de constante, mère(.) est un symbole de fonction d'arité 1, amis(., .) est un symbole de prédicats d'arité 2.
• Si l'on veut parler d'entiers naturels, « 0, 1 » sont des symboles de constantes. Les symboles + et × sont des symboles de fonctions d'arité 2. Les symboles = et ≤ sont des symboles de prédicats d'arité 2.

Termes

Les termes sont définis par induction :

• un symbole de variable est un terme ;
• un symbole de constante est un terme ;
• si $f$ est un symbole de fonctions d'arité n, et que t₁, …, t_n sont des termes alors $f(t_{1},\dots ,t_{n})$ est un terme.

Exemples

• Bob, mère(Bob), mère(mère(Bob)), mère(x) sont des termes
• 0 + 1, x + 3 × y × y sont des termes.

Formule

Les formules du calcul des prédicats du premier ordre sont définies par induction :

• $P(t_{1},\dots ,t_{n})$ si $P$ un symbole de prédicat d'arité n et t₁, …, t_n sont des termes
• ¬e si e est une formule ;
• (e₁∧e₂) si e₁ et e₂ sont des formules ;
• (e₁∨e₂) si e₁ et e₂ sont des formules ;
• (e₁→e₂) si e₁ et e₂ sont des formules ;
• $\forall x\;e$ si e est une formule ;
• $\exists x\;e$ si e est une formule.

Une formule de la forme $P(t_{1},\dots ,t_{n})$ s'appelle un atome ou une formule atomique. Les symboles $\lnot$ (non), $\land$ (et), $\lor$ (ou) et $\to$ (implique), qui sont des connecteurs que possède aussi le calcul des propositions. Les symboles $\forall$ (quel que soit) et $\exists$ (il existe), appelés quantificateurs. On pourrait se contenter d'un seul quantificateur $\forall$ et de deux connecteurs logiques $\lnot$ et $\land$ en définissant les autres connecteurs et quantificateur à partir de ceux-ci. Par exemple $\exists x\;P(x)$ est défini comme $\lnot (\forall x\;\lnot P(x))$. Les symboles de parenthèses « ) » et « ( » sont comparables aux symboles de ponctuations dans une langue naturelle. On appelle énoncé une formule dont toutes les variables sont liées par un quantificateur (donc qui n'a pas de variable libre).

Exemples

Exemple 1

Si on se donne pour constantes les deux symboles 0 et 1, pour symboles de fonctions binaires + et ., et pour symboles de prédicats binaires les symboles = et <, alors le langage utilisé peut être interprété comme étant celui de l'arithmétique. x et y désignant des variables, x + 1 est un terme, 0 + 1 + 1 est un terme clos, x < y + 1 est une formule, 0 + 1 + 1 < 0 + 1 + 1 +1 est une formule close.

Exemple 2

Si on se donne un ensemble de variables quelconque, une constante notée « e », un symbole de fonction binaire noté « * », un symbole de fonction unaire notée « ^-1 », un symbole de relation binaire « = », alors le langage utilisé peut être interprété comme étant celui de la théorie des groupes. Si x et y désignent des variables, x * y est un terme, e * e est un terme clos, x = y * y est une formule, e = e * e^-1 et (e^-1 * e)^-1 = (e^-1)^-1 sont des formules closes.

Prédicats, formules closes, formules polies, variables libres, variables liées

Lorsqu’une variable $x$ appartient à une sous-formule précédée d’un quantificateur, $\forall x$ ou $\exists x$, elle est dite liée par ce quantificateur. Si une variable n’est liée par aucun quantificateur, elle est libre.

La distinction entre variable libre et variable liée est importante. Une variable liée ne possède pas d'identité propre et peut être remplacée par n'importe quel autre nom de variable qui n'apparaît pas dans la formule. Ainsi, $\exists x(x<y)$ est identique à $\exists z(z<y)$ mais pas à $\exists x(x<z)$ et encore moins à $\exists y(y<y)$.

Une formule close est une formule dont toutes les variables sont liées. Un prédicat est une formule qui contient une ou plusieurs variables libres. On peut considérer les prédicats comme des concepts. Ainsi, $\forall x\exists y(x<y)$ est une formule close du langage de l'arithmétique. $\forall x(x<z)$ est un prédicat portant sur la variable z.

Une formule est dite polie lorsque d'une part aucune variable n'y a à la fois d'occurrences libres et d'occurrences liées et que d'autre part aucune variable liée n'est soumise à plus d'une mutification (on dit qu'un signe est mutificateur lorsqu'il permet de confirmer l'hypothèse d'une variable liée).

Sémantique

Voici un modèle pour la logique du premier ordre. Le domaine a trois éléments : un bonhomme de neige, un oiseau et une cerise. Le modèle permet d'interpréter un prédicat binaire $\mathrm {aime}$ : le bonhomme de neige aime l'oiseau, l'oiseau aime tout le monde (y compris lui-même) et la cerise n'aime personne.

La théorie de la vérité des formules du calcul des prédicats a été appelée par Tarski sa sémantique^{[réf. nécessaire]}.

Une interprétation d'un langage du premier ordre dans un domaine d'interprétation, appelé aussi modèle du langage, décrit les valeurs prises par les constituants du premier ordre (variables, symboles de constantes, termes) et les relations associées aux prédicats. Chaque énoncé se voit attribuer une valeur de vérité. L'étude des interprétations des langages formels est appelée sémantique formelle ou théorie des modèles. Ce qui suit est une description de la sémantique standard ou tarskienne pour la logique du premier ordre. Il existe d'autres types de sémantique, notamment la sémantique des jeux, qui ne sont pas détaillés dans cet article.

Modèle

Un modèle M d'un langage du premier ordre est une structure : c'est un ensemble d'éléments (appelé domaine) dans lequel on donne un sens aux symboles du langage. Généralement, si le langage possède un prédicat binaire pour le symbole d'égalité « = », alors son interprétation dans la structure est l'égalité.

Conditions de vérité

Un modèle donne une valeur de vérité (vrai ou faux) à toute formule close du langage. Les conditions de vérité sont définies par induction structurelle sur les formules. Par exemple, dans le modèle ci-contre :

• $\exists x\forall y~\mathrm {aime} (x,y)$ est vraie dans le modèle M car il existe un élément (l'oiseau) qui aime tout le monde ;
• $\exists x\forall y~\lnot \mathrm {aime} (x,y)$ est vraie dans le modèle M car il existe un élément (la cerise) qui n'aime personne.

Formule satisfaisable

Une formule est satisfaisable s'il existe un modèle M qui la rend vraie. Par exemple $\exists x\forall y~\mathrm {aime} (x,y)$ est satisfaisable.

Formule valide

On dit qu'une formule F du langage est une formule valide si cette formule est vraie dans tout modèle du langage, ce qu'on note $\vDash F$. Par exemple, la formule $\exists x\forall y~\mathrm {aime} (x,y)\to \forall y\exists x~\mathrm {aime} (x,y)$ est une formule valide. Dans un modèle M, si $\exists x\forall y~\mathrm {aime} (x,y)$ est vraie alors, il existe un élément $x$ dans le domaine qui aime tout le monde. Mais alors tout le monde est aimé et donc la formule $\forall y\exists x~\mathrm {aime} (x,y)$ est vraie dans le modèle M. L'implication étant vraie dans tout modèle M, la formule est valide.

Par contre, la formule $\forall y\exists x~\mathrm {aime} (x,y)\to \exists x\forall y~\mathrm {aime} (x,y)$ n'est pas valide. En effet, dans un modèle avec deux éléments {a, b} et où $\mathrm {aime}$ est interprété par a n'aime que a et b n'aime que b, la formule $\forall y\exists x\;~\mathrm {aime} (x,y)$ est vraie alors que $\exists x\forall y\;~\mathrm {aime} (x,y)$ est fausse. L'implication est donc fausse dans le modèle et la formule n'est pas valide.

Conséquence sémantique

On dit que F est conséquence sémantique d'une théorie T si, tout modèle qui satisfait toutes les formules de T satisfait aussi F.

Système de déduction

Dans le calcul des prédicats, on peut également déduire des formules au moyen de déductions relevant d'un calcul. Une déduction consiste à partir d’hypothèses, ou d'axiomes, à progresser par étapes logiques jusqu'à une conclusion selon des règles prédéfinies. Il existe plusieurs présentations possibles de ces axiomes et de ces règles :

• la déduction naturelle. Les principes logiques y sont présentés d’une façon aussi proche que possible des raisonnements naturels. Elle consiste en une liste de treize règles. Elles pourraient être réduites à un plus petit nombre, mais l'évidence des principes serait moins naturelle ;
• le calcul des séquents ;
• la résolution ;
• les axiomes logiques. Plusieurs systèmes d’axiomes équivalents peuvent être proposés. Cette approche, adoptée par presque tous les logiciens depuis les Principia Mathematica de Whitehead et Russell, a une grande importance à la fois métamathématique et historique. L'un des systèmes d'axiomes le plus court est constitué du triplet suivant :

  Les axiomes du calcul des propositions

  $f\to (g\to f)$

  $(f\to (g\to h))\to ((f\to g)\to (f\to h))$

  $(\lnot f\to g)\to ((\lnot f\to \lnot g)\to f)$

  les axiomes relatifs au quantificateur $\forall$

  $\forall x(f\to g(x))\to (f\to \forall xg(x))$ où x n'est pas libre dans f

  $\forall xf(x)\to f(a)$ où x n'a pas d'occurrence libre dans une partie bien formée de f de la forme $\forall a,h$ (ceci pour éviter une substitution embarrassante si par exemple, f(x) est de la forme $\exists a,a<x$).

  La règle du modus ponens

  si on a prouvé $f\to g$ et $f$, alors on a prouvé $g$

  La règle de généralisation

  si on a prouvé $f(x)$, alors on a prouvé $\forall xf(x)$ (puisque le x de la première preuve joue un rôle arbitraire).

Mais si la recherche de systèmes d'axiomes minimaux met en évidence les principes élémentaires sur lesquels peuvent s'appuyer tous les raisonnements, elle ne montre pas le caractère d’évidence naturelle des principes logiques plus généraux :

• la logique du dialogue apporte également un autre éclairage sur la nature des lois logiques ;
• voir aussi correspondance de Curry-Howard.

Quelle que soit la présentation abordée, les axiomes et règles peuvent être codés de façon qu'une machine puisse vérifier la validité ou non d'une déduction conduisant à une formule F. Si la déduction est correcte, la formule F est appelé théorème. On dit aussi qu'elle est prouvable, ce qu'on note $\vdash F$.

Propriétés

Complétude

Le théorème de complétude dit que F est valide est équivalent à F est prouvable. Mieux, on parle de complétude forte : si F est conséquence sémantique d'une théorie T alors F est prouvable à partir de T.

Indécidabilité

Tous les systèmes logiques ne sont pas décidables, autrement dit bien qu'ils soient parfaitement définis, il n'existe pas toujours un algorithme pour dire si une formule est oui ou non un théorème. D'ailleurs historiquement la théorie de la calculabilité s'est construite pour démontrer précisément leur indécidabilité. Avant de développer ces résultats, voici résumé ce qu'on sait sur la décidabilité et l'indécidabilité des systèmes logiques.

• Calcul propositionnel : décidable et complet. Pour la décidabilité, il y a donc une procédure effective pour décider si une formule du calcul propositionnel est satisfaisable, c'est-à-dire que l'on peut affecter aux variables propositionnelles des valeurs de vérité qui la rendent vraie, mais le problème, nommé problème SAT, est NP-complet, c'est-à-dire que tous les algorithmes déterministes connus de recherche d'une solution sont en temps exponentiel par rapport au nombre de variables (voir l'article Problème SAT).
• Calcul des prédicats du premier ordre monadique, c'est-à-dire réduit aux relations unaires et sans fonctions : décidable et complet, par réduction au calcul propositionnel.
• Calcul des prédicats du premier ordre : réductible au calcul des prédicats dyadique, soit avec au plus des prédicats binaires (comme il en est en théorie des ensembles n'ayant que l'appartenance et l'égalité comme symboles primitifs) : semi-décidable et complet.
• Calcul des prédicats de deuxième ordre : [quid sur sa décidabilité], et théorème de complétude partiel sur une sous-classe de formules^{[réf. souhaitée]}.
• Calcul des prédicats d'ordre supérieur :

Le calcul des prédicats est semi-décidable, dans le sens où une machine peut énumérer les théorèmes les uns après les autres. Mais, contrairement au calcul des propositions, il n'est pas en général décidable dans le sens où il n'existe pas de moyen « mécanique » qui, si on se donne une formule F, permette de décider si F est un théorème ou non. La semi-décidabilité ne permet pas de conclure : la confrontation de F avec la liste des théorèmes se terminera si F est effectivement un théorème, mais dans l'attente de la terminaison, a priori on ne sait pas si le calcul des théorèmes n'a pas été mené assez loin pour identifier F comme théorème ou si ce calcul ne se terminera pas parce que F n'est pas un théorème.

Cela dépend cependant du langage utilisé, en particulier du choix des symboles primitifs (la signature). Le calcul des prédicats égalitaire monadique (n'ayant que des symboles de prédicats unaires et pas de symbole de fonction) est décidable. Le calcul des prédicats égalitaire pour un langage comportant au moins un symbole de prédicat binaire est indécidable (algorithmiquement).

Des fragments syntaxiques sont décidables comme la logique monadique du premier ordre ou la classe de Bernays-Schönfinkel.

Compacité

Voir théorème de compacité.

Expressivité

Une application intéressante du théorème de compacité est qu'il n'existe pas de formules qui exprime « le domaine est infini ».

Théorème de Löwenheim-Skolem

Voir théorème de Löwenheim-Skolem.

Incomplétude

En un sens différent, les théories « raisonnables » qui permettent de formaliser suffisamment l'arithmétique intuitive, comme l'arithmétique de Peano, ou la théorie des ensembles ne sont pas complètes : il existe un énoncé non démontrable dont la négation est également non démontrable (voir théorèmes d'incomplétude de Gödel).

Fragments décidables

Le problème de satisfiabilité d'une formule de la logique du premier ordre est indécidable. Mais en se restreignant à certaines classes de formules, le problème de satisfiabilité devient décidable. Le tableau suivant énumère quelques fragments décidables.

Fragments
Fragment monadique et symboles de fonction d'arité 1
Fragment à deux variables seulement
Classe de Bernays-Schönfinkel, Classe $\exists ^{*}\forall ^{*}$ sans symboles de fonction et égalité
Classe $\exists ^{*}\forall ^{2}\exists ^{*}$ sans symboles de fonction
Classe $\exists ^{*}\forall \exists ^{*}$ avec symboles de fonction
Classe $\exists ^{*}$ avec symboles de fonction et égalité
Fragment monadique avec symboles de fonction d'arité et égalité
Classe $\exists ^{*}\forall \exists ^{*}$ avec symboles de fonction d'arité un, et égalité

Variantes

Le calcul des propositions est un fragment syntaxique de la logique du premier ordre où il n'y a pas de variables et où tous les prédicats sont d'arité 0^{[réf. nécessaire]}.

La logique modale propositionnelle et la logique de description sont des fragments syntaxiques de la logique du premier ordre^{[réf. nécessaire]}. D'ailleurs, toute formule du premier ordre qui est invariante par bisimulation est équivalente à une formule de la logique modale : c'est le théorème de Van Benthem^{[réf. nécessaire]}. La logique du premier ordre a aussi été étendu à la logique modale du premier ordre^{[réf. nécessaire]}. La logique de la dépendance (dependence logic) est une généralisation de la logique du premier ordre où les dépendances entre variables sont explicitement décrites dans le langage^{[réf. nécessaire]}.

Notes et références

Annexes

Articles connexes

• Calcul des propositions
• Théorie des modèles
• Skolémisation
• Langage formel mathématique
• Théorème de Lindström
• Langage informatique Prolog
• Déduction naturelle
• Signature (logique)
• Structure (logique mathématique)
• Théorème d'interpolation de Craig
• Théorème de Trakhtenbrot

Bibliographie

• Stephen Kleene, Logique mathématique, Armand Colin, 1971 ou Gabay 1987 (ISBN 2-87647-005-5)
• R. David, K. Nour et C. Raffalli, Introduction à la logique. Théorie de la démonstration. Cours et exercices corrigés, Dunod, 2001 (ISBN 2-10-006796-6)
• Pierre Lebarbenchon, Sophie Pinchinat, François Schwarzentruber, Logique : fondements et applications. Dunod 2022 (ISBN 978-2100821587)