Déduction naturelle
Source: Wikipédia sous licence CC-BY-SA 3.0.
La liste des auteurs de cet article est disponible ici.

La déduction naturelle est une façon d'exposer les principes de la logique du premier ordre pour les rendre aussi proches que possible des façons naturelles de raisonner

Les origines de la déduction naturelle

L’histoire des théories de la déduction a suivi un cheminement curieux. De nombreux logiciens dont Bertrand Russell et Alfred North Whitehead avec leurs Principia Mathematica ont développé la logique (La logique (du grec logikê, dérivé de logos (λόγος), terme inventé par Xénocrate signifiant à la fois raison, langage, et raisonnement) est dans...) sous une forme axiomatique. Les lois logiques sont déduites à partir d’axiomes logiques, d’une façon qui ressemble à la méthode euclidienne, au moins aux yeux de ceux qui faisaient ces déductions. Cette méthode pouvait sembler relativement naturelle tant qu’on choisissait comme axiomes des lois dont la vérité logique était évidente. Mais le souci de formuler des systèmes d’axiomes aussi réduits que possible a conduit parfois à des formalismes où l’on déduit des vérités logiques évidentes à partir d’autres qui ne le sont pas. Les méthodes des logiciens permettaient de justifier tous les raisonnements dont la validité était reconnue mais elles étaient très éloignées de l’idéal d’évidence naturelle que l’on attend de la logique.

La notion de naturel est employé par les logiciens principalement en deux sens (SENS (Strategies for Engineered Negligible Senescence) est un projet scientifique qui a pour but l'extension radicale de l'espérance de vie humaine. Par une évolution...). S’il s’agit comme ci-dessus d’évidence naturelle, ou de concepts apparentés comme la déduction naturelle (La déduction naturelle est une façon d'exposer les principes de la logique du premier ordre pour les rendre aussi proches que possible des façons naturelles de raisonner), on veut insister sur leur caractère universel et nécessaire pour tout (Le tout compris comme ensemble de ce qui existe est souvent interprété comme le monde ou l'univers.) être rationnel. On peut vivre sans jamais savoir que 2+2 = 4 mais on ne peut pas être rationnel sans reconnaître que 2+2 = 4 est nécessaire, dès qu’on nous a appris à le dire. Le second sens de la notion de naturel intervient dans la distinction entre les langues naturelles et les langues formelles, ou artificielles. Les premières sont les langues qui nous sont familières, elles ont été façonnées par des siècles de culture (La définition que donne l'UNESCO de la culture est la suivante [1] :). Les secondes sont inventées par les logiciens pour développer des théories et pour donner des preuves.

Gerhard Gentzen est le premier à avoir développé des formalismes qui redonnent à la logique le caractère d’un cheminement naturel. La principale idée de départ de Gentzen était simple : pas d’axiomes logiques, que des règles de déduction et autant qu’il en faut pour reproduire toutes les formes élémentaires et naturelles de raisonnement. Pour réaliser cette idée, Gentzen a développé un formalisme où les déductions ne sont pas des suites de phrases mais des arbres, faits de colonnes de phrases qui se rejoignent jusqu’à la conclusion. Cette méthode est très suggestive pour l’intuition et elle a conduit Gentzen à faire de belles découvertes mais elle nuit à l’idée originale qui était de reproduire les formes naturelles de raisonnement. Fitch a modifié la méthode de Gentzen en renonçant aux déductions arborescentes. Les déductions de Fitch ne sont cependant pas de simples suites de phrases. Pour donner à une déduction un caractère naturel il faut faire apparaître des relations de dépendance entre les phrases. Au lieu d’une forme arborescente la méthode de Fitch se sert seulement de barres verticales. Une assertion (Dans la langue française, le mot assertion (n,f) représente une vérité absolue : il définit une proposition reconnue comme vraie. -> voir Wiktionary) dépend des phrases qui sont au dessus d’elle sauf de celles qui sont décalées sur la droite par ces barres. Cette règle simple permet de faire des déductions à la fois formelles et naturelles. Dans cette encyclopédie, nous ne noterons pas les barres, mais seulement les décalages. Une phrase dépendra de toutes les hypothèses qui sont au dessus d’elle sauf de celles qui sont décalées vers la droite. Les hypothèses sont des axiomes ou des hypothèses provisoires. Elles seront indiquées avec la mention (hyp) ou (axiome).

Dag Prawitz a démontré un théorème (Un théorème est une proposition qui peut être mathématiquement démontrée, c'est-à-dire une assertion qui peut être établie comme vraie au travers...) d'élimination des coupures en déduction naturelle.

Les règles de déduction pour les opérateurs booléens fondamentaux

Les règles exposées dans ce paragraphe sont celles de la déduction naturelle pour le calcul des propositions (Le calcul des propositions ou calcul propositionnel, dont le fondateur fut le logicien allemand Frege, version moderne de la logique stoïcienne, est une théorie logique qui définit les lois formelles du raisonnement. La notion de proposition...). Elles permettent d’enchaîner logiquement les phrases, c’est-à-dire d'introduire de nouvelles phrases comme conséquences logiques de ce qui a été dit auparavant. À chacun des opérateurs logiques fondamentaux sont associées deux règles de déduction. L'une des règles est une règle d'introduction : elle explique comment prouver une proposition possédant l'opérateur (Le mot opérateur est employé dans les domaines :). L'autre règle est une règle d'élimination : elle explique comment utiliser une proposition possédant l'opérateur pour poursuivre le raisonnement.

Introduction et élimination sont nécessaires pour pouvoir démonter et remonter des formules. La recherche (La recherche scientifique désigne en premier lieu l’ensemble des actions entreprises en vue de produire et de développer les connaissances scientifiques....) d’une déduction logique consiste justement à analyser les prémisses, c’est-à-dire à les démonter, et à réassembler les morceaux pour faire des formules que l’on peut enchainer logiquement jusqu’à la conclusion. On croit parfois qu’il est très difficile de faire des preuves mathématiques, mais dans son principe, ce n’est pas très différent d’un jeu de construction avec des cubes.

Les règles relatives à l'implication

La règle d'introduction de l'implication ou règle de l'abandon d'une hypothèse provisoire énonce que, pour prouver une implication "si P alors Q", il suffit de procéder de la façon suivante : on pose P comme hypothèse provisoire, on fait alors des déductions à partir de toutes les phrases antérieures plus P en vue (La vue est le sens qui permet d'observer et d'analyser l'environnement par la réception et l'interprétation des rayonnements lumineux.) d’atteindre Q. Une fois Q atteint, on peut alors en déduire "si P alors Q". Insistons sur un point : Q est démontrée sous l’hypothèse P mais "si P alors Q", elle, ne dépend que des prémisses antérieures. Si on utilise la méthode de Fitch, on peut introduire n’importe quand dans une déduction une hypothèse provisoire. Il suffit de la décaler vers la droite par rapport aux autres prémisses. Tout ce qui est déduit sous une hypothèse provisoire doit être sous elle ou sur sa droite mais jamais sur sa gauche. La règle d'introduction permet de conclure qu'on a prouvé "si P alors Q" sans l'hypothèse P. On peut décaler "si P alors Q" sur la gauche par rapport à P, mais pas par rapport aux autres prémisses utilisées dans la démonstration (En mathématiques, une démonstration permet d'établir une proposition à partir de propositions initiales, ou précédemment démontrées à partir de propositions initiales, en s'appuyant sur un ensemble de...) de Q. On notera :

1\quad \quad P (hypothèse provisoire)
2\quad \quad Q (propriété déduite de 1)
3\quad P \to Q (introduction de l'implication entre les deux lignes 1 et 2)

La règle d'élimination de l'implication, ou règle du détachement ou du modus ponens énonce que, des deux phrases "P" et "si P alors Q" on peut déduire "Q". Elle permet de passer (Le genre Passer a été créé par le zoologiste français Mathurin Jacques Brisson (1723-1806) en 1760.) de conditions déjà connues, P, à des conditions nouvelles, Q, pourvu qu’il y ait une loi qui l’autorise, "si P alors Q", ce qui sera noté :

1\quad P
2\quad P \to Q
3\quad Q (élimination de l'implication entre les lignes 1 et 2)

Montrons par exemple qu’avec ces deux règles on peut déduire "si P alors R" à partir des deux phrases "si P alors Q" et "si Q alors R" :

1\quad P \to Q (hypothèse)
2\quad Q \to R (hypothèse)
3\quad \quad P (hypothèse provisoire)
4\quad\quad Q (modus ponens sur 3 et 1)
5\quad\quad R (modus ponens sur 4 et 2)
6\quad P \to R(règle d'introduction de l'implication entre 3 et 5, abandon de l’hypothèse provisoire P).

Les règles relatives à la conjonction

Pour la conjonction, les règles sont très simples.

La règle d'introduction de la conjonction énonce que, à partir des deux phrases A et B on peut déduire la phrase (A et B).

1\quad A
2\quad B
3\quad A \land B (introduction de la conjonction entre 1 et 2)

La règle d'élimination de la conjonction énonce que, à partir de la phrase (A et B), on peut déduire les deux phrases A et B prises séparément.

1\quad A \land B
2\quad A (élimination de la conjonction 1)
3\quad B (élimination de la conjonction 1)

Ces règles permettent d'assembler ou au contraire de séparer des assertions qui sont toutes considérées comme vraies. C’est la forme logique de la capacité de la raison à analyser le monde (Le mot monde peut désigner :), c’est-à-dire à étudier ses parties séparément, et à le synthétiser, c’est-à-dire à rassembler les élements d’une étude en un tout. C’est pourquoi ces règles sont également appelées les règles de l'analyse et de la synthèse.

Les règles relatives à la disjonction

Les deux règles de déduction pour la disjonction sont les suivantes.

La règle d'introduction de la disjonction ou règle de l'affaiblissement d'une thèse (Une thèse (du nom grec thesis, se traduisant par « action de poser ») est l'affirmation ou la prise de position d'un locuteur, à l'égard du sujet ou du thème qu'il...) énonce que, à partir de la phrase P on peut déduire la phrase (P ou Q) aussi bien que la phrase (Q ou P), quelle que soit la phrase Q. Cette règle peut sembler peu intéressante mais elle est en vérité très importante. Parfois il est avantageux de déduire (P ou Q) après avoir prouvé P, car on peut savoir par ailleurs que (P ou Q) a d'autres conséquences.

1 \quad P
2 \quad P \lor Q (introduction de la disjonction à partir de 1)

et de même

1 \quad Q
2 \quad P \lor Q (introduction de la disjonction à partir de 1)

La règle d'élimination de la disjonction ou règle de la disjonction des hypothèses ou règle de la distinction des cas, stipule (En botanique, les stipules sont des pièces foliaires, au nombre de deux, en forme de feuilles réduites située de part et d'autre du pétiole, à sa base, au point d'insertion sur la tige.) que, si on a prouvé (P ou Q) et qu'on a également prouvé (si P alors R) ainsi que (si Q alors R), alors on a prouvé R. Cette règle sert quand on examine plusieurs cas possibles qui conduisent à la même conclusion.

1 \quad P\lor Q
2 \quad\quad P (hypothèse provisoire)
3 \quad\quad R (propriété déduite de 2)
4 \quad P \to R (introduction de l'implication entre 2 et 3)
5 \quad\quad Q (hypothèse provisoire)
6 \quad\quad R (propriété déduite de 5)
7 \quad Q \to R (introduction de l'implication entre 5 et 6)
8 \quad R (élimination de la disjonction entre 1, 4, 7)

Les règles relatives à la négation

La règle d'introduction de la négation énonce que, si on démontre une contradiction (Une contradiction existe lorsque deux affirmations, idées, ou actions s'excluent mutuellement.) à partir d’une hypothèse P alors celle-ci est nécessairement fausse et donc sa négation est vraie. Ainsi, si dans une déduction sous l’hypothèse provisoire P, on a trouvé une contradiction (Q et non Q), notée également \bot, alors on peut déduire nonP à partir de toutes les prémisses antérieures sauf P. Avec la méthode de Fitch, on décale donc (non P) sur la gauche par rapport à P, ce qui se représente comme suit :

1 \quad\quad P
2 \quad\quad \bot
3 \quad \lnot P (introduction de la négation entre 1 et 2)

La règle d'élimination de la négation ou règle de la suppression de la double-négation ou raisonnement par absurde énonce que, de (non nonP) on peut déduire P. Il s'agit bien du raisonnement par l'absurde car dans, un tel raisonnement, pour prouver P, on suppose (non P) et l'on cherche à obtenir une contradiction. Si tel est le cas, on a prouvé (non non P) d'après la règle d'introduction de la négation, et c'est bien la règle de suppression de la double-négation qui permet de conclure à P :

1\quad \lnot\lnot P
2 \quad P (élimination de la double négation 1)

ou bien

1\quad\quad \lnot P (hypothèse provisoire [raisonnement par l'absurde])
2\quad\quad \bot
3\quad \lnot \lnot P (introduction de la négation entre 1 et 2)
4\quad P (élimination de la double négation 3)

Quand on considère que toute phrase est nécessairement ou bien vraie ou bien fausse, la validité de cette dernière règle est évidente. Elle est caractéristique de la logique classique, qui est présentée ici et est utilisée par la grande majorité des scientifiques. Elle est parfois contestée à cause d’un problème important, celui des preuves d’existence par l’absurde. Il arrive que l’on puisse prouver qu’un problème a une solution sans être capable de la trouver. Pour cela il suffit de prouver que l’absence de solution conduit à une contradiction. Le raisonnement par l’absurde permet alors de conclure qu’il n’est pas vrai que le problème n’a pas de solution : non non (le problème a une solution). En logique classique, on supprime la double négation pour en conclure que le problème a une solution. Cependant, la démarche ainsi suivie ne fournit aucun procédé constructif de la solution cherchée. Cette objection fut soulevée par certains mathématiciens et logiciens, dont Brouwer, qui contestèrent cette méthode et s'opposèrent à Hilbert qui la défendait. Les mathématiciens constructivistes ou intuitionnistes estiment qu’une preuve d’existence n’a pas de sens si elle ne fournit pas également un procédé constructif de l'objet (De manière générale, le mot objet (du latin objectum, 1361) désigne une entité définie dans un espace à trois dimensions, qui a une fonction précise, et qui peut être désigné par...) en question. Aussi ces derniers rejettent-ils la règle de suppression de la double négation pour lui substituer la règle suivante : de P et (non P), on peut déduire une contradiction, et de cette contradiction n'importe quelle proposition Q.

1 \quad P
2 \quad \lnot P
3 \quad \bot
4 \quad Q (élimination de la négation 2 en logique intuitionniste)

Dans les exemples, nous utiliserons cette deuxième règle d'élimination lorsqu'il est possible de se passer de la règle d'élimination de la double négation

On peut introduire d’autres règles pour les autres opérateurs booléens, notamment l’opérateur d’équivalence, mais ce n’est pas nécessaire, parce que ces opérateurs peuvent être définis à partir des précédents et que leurs règles de déduction peuvent être alors déduites à partir des règles précédentes. (P équivaut à Q) est défini par ( (si P alors Q) et (si Q alors P) ) .

Exemples

Nous donnons ci-dessous quelques exemples d'utilisation de la déduction naturelle. Dans la première partie, nous n'utiliserons pas la règle d'élimination de la double négation. Dans la deuxième partie, nous utiliserons cette règle. Les formules déduites dans cette deuxième partie ne sont pas reconnues valides par les mathématiciens intuitionnistes. Nous utiliserons les symboles suivants : \to pour si ... alors ..., \lor pour ou, \land pour et, \lnot pour non. Le symbole \bot désigne une contradiction, c'est-à-dire une proposition fausse.

Exemples n'utilisant pas l'élimination de la double négation

Exemple 1 : (\lnot A \land \lnot B) \to \lnot(A \lor B)

01\quad\quad \lnot A \land \lnot B (hypothèse provisoire)
02\quad\quad \lnot A (élimination de la conjonction 01)
03\quad\quad \lnot B (élimination de la conjonction 01)
04\quad\quad\quad A \lor B (hypothèse provisoire)
05\quad\quad\quad\quad A (hypothèse provisoire)
06\quad\quad\quad\quad \botcontradiction entre 02 et 05
07\quad\quad\quad A \to \bot (introduction de l'implication entre 05 et 06)
08\quad\quad\quad\quad B (hypothèse provisoire)
09\quad\quad\quad\quad \bot contradiction entre 03 et 08
10\quad\quad\quad B \to \bot (introduction de l'implication entre 08 et 09)
11\quad\quad\quad \bot (élimination de la disjonction entre 04, 07, 10)
12\quad\quad \lnot (A \lor B) (introduction de la négation entre 04 et 11)
13\quad (\lnot A \land \lnot B) \to \lnot(A \lor B) (introduction de l'implication entre 01 et 12 et fin de la déduction)

On montre que la réciproque (La réciproque est une relation d'implication.) \lnot(A \lor B) \to (\lnot A \land \lnot B) est également valide. On montre également que (\lnot A \lor \lnot B) \to \lnot(A \land B), mais pour la réciproque de cette dernière propriété, on utilise l'élimination de la double négation.

Exemple 2 : A \to \lnot\lnot A

01\quad\quad A (hypothèse provisoire)
02\quad\quad\quad \lnot A (hypothèse provisoire)
03\quad\quad\quad \bot (élimination de la négation entre 01 et 02)
04\quad\quad \lnot\lnot A (introduction de la négation entre 02 et 03)
05\quad A \to \lnot\lnot A (introduction de l'implication entre 01 et 04, fin de la déduction)

La réciproque \lnot\lnot A \to A découle directement de l'élimination de la double négation et est rejetée par les intuitionnistes. Mais curieusement, il n'en est pas de même de \lnot\lnot\lnot A \to \lnot A qui se prouve sans cette hypothèse, et qui, elle, est acceptée par les intuitionnistes.

Exemple 3 : \lnot\lnot\lnot A \to \lnot A

01\quad\quad \lnot\lnot\lnot A (hypothèse provisoire)
02\quad\quad\quad A (hypothèse provisoire)
03\quad\quad\quad A \to \lnot\lnot A (théorème de l'exemple 2)
04\quad\quad\quad \lnot\lnot A (élimination de l'implication ou modus ponens entre 02 et 03)
05\quad\quad\quad \bot (élimination de la négation entre 01 et 04)
06\quad\quad \lnot A (introduction de la négation entre 02 et 05)
07\quad \lnot\lnot\lnot A \to \lnot A (introduction de l'implication entre 01 et 06, fin de la déduction)

Exemples utilisant l'élimination de la double négation

Les exemples qui suivent utilisent l'élimination de la double négation. On peut montrer que cette utilisation est nécessaire. Ils ne sont donc pas acceptés en logique intuitionniste.

Exemple 4 : \lnot(A \land B) \to (\lnot A \lor \lnot B)

01 \quad\quad \lnot(A \land B) (hypothèse provisoire [raisonnement par l'absurde])
02 \quad\quad\quad \lnot(\lnot A \lor \lnot B) (hypothèse provisoire)
03 \quad\quad\quad \lnot(\lnot A \lor \lnot B) \to (\lnot\lnot A \land \lnot\lnot B) (théorème, réciproque de l'exemple 1)
04 \quad\quad\quad \lnot\lnot A \land \lnot\lnot B (élimination de l'implication ou modus ponens entre 02 et 03)
05 \quad\quad\quad A \land B (élimination de la double négation dans 04)
06 \quad\quad\quad \bot (élimination de la négation entre 01 et 05)
07 \quad\quad \lnot\lnot(\lnot A \lor \lnot B) (introduction de la négation entre 02 et 06)
08 \quad\quad \lnot A \lor \lnot B (élimination de la double négation dans 07)
09 \quad \lnot(A \land B) \to (\lnot A \lor \lnot B) (introduction de l'implication entre 01 et 08)

Exemple 5 : si (A \to B) \to (\lnot B \to \lnot A) ne nécessite pas l'élimination de la double négation, celle-ci est nécessaire pour prouver la réciproque (\lnot B \to \lnot A) \to (A \to B).

Exemple 6 : de même la demonstration de la validité du tiers exclu A \lor \lnot A utilise l'élimination de la double négation. En supposant que \lnot(A \lor \lnot A), on en déduit \lnot A \land \lnot\lnot A (réciproque de l'exemple 1), d'où une contradiction et la validité de \lnot\lnot(A \lor \lnot A).

Si les intuitionnistes rejettent le tiers exclu, ils acceptent par contre le principe de non contradiction : \lnot(A \land \lnot A). En effet, la supposition A \land \lnot A est une contradiction. On a donc \lnot(A \land \lnot A) par introduction de la négation.

Exemple 7 connu sous le nom de loi de Peirce : ((A \to B) \to A) \to A. Curieusement, bien que ne contenant pas de négation, la déduction de cette loi nécessite l'élimination de la double négation, par exemple par l'intermédiaire de l'utilisation du tiers exclu. On suppose que l'on a ((A \to B) \to A). D'après le tiers exclu, ou bien on a (A \to B) et le modus ponens entraîne qu'on a A. Ou bien on a \lnot(A \to B), c'est-à-dire A \land \lnot B et donc on a bien A.

Les règles de déduction pour les quantificateurs

L’usage des noms de variable (En mathématiques et en logique, une variable est représentée par un symbole. Elle est utilisée pour marquer un rôle dans une formule, un prédicat ou un algorithme. En statistiques, une variable peut aussi...) dans les théories du premier ordre

Les règles de déduction pour les opérateurs universels et existentiels gouvernent l’usage des noms de variable. Cet usage (L’usage est l'action de se servir de quelque chose.) donne à une théorie (Le mot théorie vient du mot grec theorein, qui signifie « contempler, observer, examiner ». Dans le langage courant, une théorie est une idée ou une connaissance spéculative, souvent basée...) la puissance (Le mot puissance est employé dans plusieurs domaines avec une signification particulière :) de la généralité, c’est-à-dire la possibilité de connaître non chaque invividu pris isolément mais tous les individus d’un même genre, en une seule phrase.

Les règles d’usage des variables précisent à quelles conditions on peut introduire des noms de variable et ce qu’on peut alors dire à leur sujet. Ces règles sont naturelles mais il y a quelques difficultés techniques à propos des notions de terme, d’occurrence libre ou liée d’une variable, de substitution d’un terme aux occurrences d’une variable et de substitution d’une variable aux occurrences d’un terme.

Pour qu’une théorie puisse utiliser la logique du premier ordre il faut avoir défini un domaine d’objets et il faut que les prédicats attribués par la théorie à ses objets ne soient pas eux-mêmes des objets de la théorie.

La signification d’un nom de variable d’objet, c’est de représenter un objet quelconque de la théorie : soit x un nombre (La notion de nombre en linguistique est traitée à l’article « Nombre grammatical ».). Souvent on introduit un nom de variable dans des prémisses qui déterminent des conditions générales sur cet objet. x est un objet quelconque de la théorie pourvu seulement qu’il satisfasse à ces conditions : soit x un nombre premier (Un nombre premier est un entier naturel qui admet exactement deux diviseurs distincts entiers et positifs (qui sont alors 1 et lui-même). Cette...) ... Une théorie contient en général des noms pour ses objets. La théorie des nombres entiers contient par exemple des noms pour tous les nombres : 0, 1, 2, ..., -1, -2, ...

Les termes peuvent être simples ou composés. Ce sont les noms d’objet, les noms de variable d’objet, et toutes les expressions composées que l’on peut former à partir d’eux en appliquant les opérateurs d’objets de la théorie. Par exemple, 1, x, x+1et (x+x)+1 sont des termes de la théorie des nombres.

Rappelons d’abord la très importante distinction entre les variables liées par un opérateur et les autres, les variables libres. Les occurrences d’un nom de variable dans une phrase sont tous les endroits où ce nom apparait. Une occurrence peut être libre ou liée. Quand un opérateur existentiel ou universel en x est appliqué à une phrase complexe, toutes les occurrences de x deviennent liées par cet opérateur. Toutes les occurrences qui ne sont pas ainsi liées sont libres.

Si une phrase contient plusieurs opérateurs existentiels et universels, il est souhaitable que ces opérateurs portent tous sur des noms de variable différents. Cette règle n’est pas indispensable. Elle n’est pas respectée lorsque l’on met le calcul des prédicats (Le calcul des prédicats du premier ordre, ou calcul des relations, ou logique du premier ordre, ou tout simplement calcul des prédicats est une formalisation du langage des mathématiques proposée par les logiciens du début du...) sous la forme d’une algèbre (L'algèbre, mot d'origine arabe al-jabr (الجبر), est la branche des mathématiques qui étudie, d'une façon...) cylindrique (une algèbre cylindrique est une algèbre de Boole complétée par des lois particulières aux opérateurs universels et existentiels). Mais elle est toujours respectée en pratique parce qu’elle permet d’éviter des confusions.

Une phrase est obtenue à partir d’une autre par substitution d’un terme t aux occurrences d’une variable x lorsque toutes les occurrences libres de x ont été remplacées par t. Par exemple, (le père de x est humain et le père de x est honnête) est obtenu par substitution du terme le père de x à la variable y dans la formule (y est humain et y est honnête).

Ces préliminaires permettent de formuler les règles de déduction pour les opérateurs universels et existentiels.

Les règles relatives au quantificateur universel

La règle d'introduction du quantificateur universel ou règle de généralisation (La généralisation est un procédé qui consiste à abstraire un ensemble de concepts ou d'objets en négligeant les...) énonce que, de P(x) on peut déduire (pour tout x,P(x)) pourvu que le nom de variable x n’apparaisse jamais dans les hypothèses dont P(x) dépend.

1 \quad P(x)
2 \quad \forall x \; P(x) (introduction de quel que soit, où x n'est pas libre dans les prémisses de P)

Très souvent on introduit des variables dans des hypothèses provisoires. On raisonne ensuite sur elles comme si elles étaient des objets. On peut alors en déduire des lois générales, parce que ce qu’on a déduit est vrai pour tous les objets qui vérifient les mêmes hypothèses. Ce sont les règles d’abandon d’une hypothèse provisoire et de généralisation qui permettent de conclure.

La règle d'élimination du quantificateur universel ou règle de singularisation énonce que, à partir d’une phrase de la forme (pour tout x) P(x) , on peut déduire P(t), pour n’importe quel terme t dont les variables ne sont pas liées dans P(x). P(x) désigne une phrase quelconque qui contient x comme variable libre, P(t) désigne la phrase obtenue à partir de P(x) en y substituant t à toutes les occurrences libres de x. La règle de singularisation consiste simplement à appliquer une loi universelle à un cas singulier.

1 \quad \forall x \; P(x)
2 \quad P(t) (élimination de quel que soit)

Les règles relatives au quantificateur existentiel

La règle d'introduction du quantificateur existentiel, ou règle des preuves directes de l’existence, énonce que, à partir de la phrase P(t), on peut déduire il existe un x tel que P(x) pour toute variable x qui n’apparait pas dans P(t) et pour tout terme t dont les noms de variables ne sont pas liés dans P(x).

P(t) désigne une phrase quelconque qui contient au moins une fois le terme t. P(x) est obtenue à partir de P(t) en substituant x à t à une ou plusieurs de ses occurrences. Dans cette règle il n’est pas nécessaire de substituer x à toutes les occurrences de t.

1 \quad P(t)
2 \quad \exists x  \; P(x) (introduction de il existe)

La règle d'élimination du quantificateur existentiel ou règle des conséquences de l’existence permet, à partir d'une proposition (il existe x, P(x)), d'introduire une nouvelle hypothèse provisoire P(y) où y est un nom de variable qui n’a jamais été utilisé auparavant et où P(y) est obtenu à partir de P(x) en substituant y à toutes les occurrences de x. On peut alors raisonner sous cette hypothèse. La règle des conséquences de l’existence permet alors de conclure de la façon suivante : de la phrase (il existe un x tel que P(x)) on peut déduire R lorsque R a été déduit sous l’unique hypothèse provisoire supplémentaire P(y) et que y n’apparait ni dans les prémisses antérieures à P(y) ni dans R. y est une sorte d’être hypothétique. Il ne fait que servir d’intermédiaire dans une déduction mais il n’apparait ni dans ses prémisses, ni dans sa conclusion.

1 \quad \exists x \; P(x) (hypothèse)
2 \quad\quad P(y) (y variable nouvelle)
3 \quad\quad R (déduction à partir de 2, ne faisant pas intervenir y)
4 \quad R (élimination de il existe dans 1 et 3)

Exemples

Exemple 1 (\exists x \; \lnot A(x)) \to (\lnot \forall x \; A(x))

1 \quad\quad \exists x \; \lnot A(x)(hypothèse provisoire)
2 \quad\quad\quad \forall x \; A(x)(hypothèse provisoire)
3 \quad\quad\quad\quad \lnot A(y) (y variable nouvelle à partir de 1)
4 \quad\quad\quad\quad A(y)(élimination de quel que soit dans 2)
5 \quad\quad\quad\quad \bot(élimination de la négation 3, 4)
6 \quad\quad\quad \bot(élimination de il existe entre 1 et 5)
7 \quad\quad \lnot (\forall x \; A(x))(introduction de la négation entre 2 et 6)
8 \quad(\exists x \; \lnot A(x)) \to (\lnot \forall x \; A(x))(introduction de l'implication 1, 7)

Exemple 2 : on a également \lnot (\forall x \; A(x)) \to \exists x (\lnot A(x)), mais la preuve nécessite une élimination de la double négation, et ce théorème de la logique classique n'est pas accepté en logique intuitionniste.

Comment vérifier la correction d’un raisonnement ?

A ces douze règles, ou quatorze, si on compte que la règle d'éliminination de la conjonction est en fait une double règle, et de même pour la règle d'introduction de la disjonction, il faut en ajouter une quinzième, très simple, la règle de répétition : on peut toujours répéter une thèse antérieure, sauf si elle dépend d’une hypothèse qui a été abandonnée. On peut donc répéter toutes les thèses tant qu’on ne les décale pas sur la gauche. Cette règle est nécessaire quand on veut répéter une prémisse dans une conclusion ou quand on a besoin (Les besoins se situent au niveau de l'interaction entre l'individu et l'environnement. Il est souvent fait un classement des besoins humains en trois grandes catégories : les besoins primaires, les besoins secondaires et les besoins...) d’une thèse antérieure dans le corps d’une déduction sous hypothèse provisoire pour appliquer une règle.

La liste des quinze règles précédentes est complète au sens où elle suffit pour faire toutes les déductions correctes. Kurt Gödel a prouvé, (Théorème de complétude) pour un système logique différent, mais équivalent à celui qui vient d’être présenté, qu’il suffit pour formaliser toutes les déductions correctes du Calcul des prédicats du premier ordre.

Les déductions correctes sont d’abord toutes celles qui respectent rigoureusement ces règles fondamentales. Toutes les phrases doivent être ou bien des axiomes, ou bien des hypothèses provisoires, ou bien des conséquences des phrases qui les précèdent en vertu de l’une des quinze règles. Par souci de rapidité, on peut également utiliser des règles dérivées (par exemple faire suivre \lnot (A \lor B) par \lnot A \land \lnot B). Une règle dérivée (La dérivée d'une fonction est le moyen de déterminer combien cette fonction varie quand la quantité dont elle dépend, son argument, change. Plus précisément, une dérivée est une expression...) est correcte lorsqu’on peut montrer que tout ce qui peut être déduit avec elle peut aussi être déduit sans elle avec seulement les règles fondamentales.

Tant que les déductions sont formalisées, il est toujours possible de reconnaitre, y compris par un programme, si une déduction est correcte parce que les règles de déduction sont en nombre fini et qu’il est toujours possible de vérifier en un temps (Le temps est un concept développé par l'être humain pour appréhender le changement dans le monde.) fini si une formule est la conséquence d’une ou plusieurs autres en vertu de l’une de ces règles. Cette démarche réalise une partie du programme appelé parfois finitaire proposé par David Hilbert pour résoudre les problèmes des fondements des mathématiques (Cet article discute des fondements des mathématiques. Le problème de la fondation, ou des fondements, des mathématiques est celui des principes et de leur vérité. À partir de quels principes peut-on développer des connaissances...). Hilbert cherchait une méthode efficace qui permette de décider pour tout énoncé mathématique (Les mathématiques constituent un domaine de connaissances abstraites construites à l'aide de raisonnements logiques sur des concepts tels que les nombres, les figures, les...) s'il est un théorème, c’est-à-dire une vérité mathématique. Le calcul des prédicats permettait de ramener le problème à la question de savoir si une formule est une loi logique ou non.

Mais s'il est possible de vérifier la validité d'une déduction conduisant à une formule, à l'inverse (En mathématiques, l'inverse d'un élément x d'un ensemble muni d'une loi de composition interne · notée multiplicativement, est un...), la question de savoir si une formule donnée (Dans les technologies de l'information, une donnée est une description élémentaire, souvent codée, d'une chose, d'une transaction, d'un événement, etc.) est une loi logique ou non ne peut être résolue en général. En effet, il n’existe pas de méthode universelle permettant de dire si une formule est une loi logique ou non. Cet inexistence se déduit du théorème d'incomplétude (On parle de complétude en mathématiques dans des sens très différents. On dit d'un objet mathématiques qu'il est complet pour exprimer que rien ne...) de Gödel. On dit que la question de savoir si une formule est une loi logique est indécidable.

La vérification de la correction des déductions dans la langue courante pose davantage de difficultés. Il faut d’abord traduire les phrases familières dans une langue formalisée du calcul des prédicats. Cette étape pose parfois problème si on a des doutes sur la fidélité de la traduction. Mais la plus grosse difficulté vient de ce que les déductions courantes font en général une large place à l’implicite. Même les relations de dépendance par rapport à une hypothèse ne sont pas toujours explicitées. Les déductions formelles au contraire ne laissent rien dans l’ombre. Celles qui sont ici proposées sont très semblables aux déductions courantes sauf qu’elles explicitent tout. Les méthodes formelles ne suffisent pas en pratique pour savoir toujours reconnaître si les raisonnements d’autrui sont corrects, parce qu’elles requièrent l’explicitation de tout ce qui est implicite. C’est pourquoi souvent il faut beaucoup étudier et connaître tout l’implicite avant de savoir si un raisonnement est correct.

Page générée en 0.255 seconde(s) - site hébergé chez Amen
Ce site fait l'objet d'une déclaration à la CNIL sous le numéro de dossier 1037632
Ce site est édité par Techno-Science.net - A propos - Informations légales
Partenaire: HD-Numérique