Style de Fitch pour la déduction naturelle

Exemple 1 : ${\displaystyle (\lnot A\land \lnot B)\to \lnot (A\lor B)}$

${\displaystyle 01\quad \quad \lnot A\land \lnot B}$ (hypothèse provisoire)

${\displaystyle 02\quad \quad \lnot A}$ (élimination de la conjonction 01)

${\displaystyle 03\quad \quad \lnot B}$ (élimination de la conjonction 01)

${\displaystyle 04\quad \quad \quad A\lor B}$ (hypothèse provisoire)

${\displaystyle 05\quad \quad \quad \quad A}$ (hypothèse provisoire)

${\displaystyle 06\quad \quad \quad \quad \bot }$contradiction entre 02 et 05

${\displaystyle 07\quad \quad \quad A\to \bot }$ (introduction de l'implication entre 05 et 06)

${\displaystyle 08\quad \quad \quad \quad B}$ (hypothèse provisoire)

${\displaystyle 09\quad \quad \quad \quad \bot }$ contradiction entre 03 et 08

${\displaystyle 10\quad \quad \quad B\to \bot }$ (introduction de l'implication entre 08 et 09)

${\displaystyle 11\quad \quad \quad \bot }$ (élimination de la disjonction entre 04, 07, 10)

${\displaystyle 12\quad \quad \lnot (A\lor B)}$ (introduction de la négation entre 04 et 11)

${\displaystyle 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 ${\displaystyle \lnot (A\lor B)\to (\lnot A\land \lnot B)}$ est également valide. On montre également que ${\displaystyle (\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 : ${\displaystyle A\to \lnot \lnot A}$

${\displaystyle 01\quad \quad A}$ (hypothèse provisoire)

${\displaystyle 02\quad \quad \quad \lnot A}$ (hypothèse provisoire)

${\displaystyle 03\quad \quad \quad \bot }$ (élimination de la négation entre 01 et 02)

${\displaystyle 04\quad \quad \lnot \lnot A}$ (introduction de la négation entre 02 et 03)

${\displaystyle 05\quad A\to \lnot \lnot A}$ (introduction de l'implication entre 01 et 04, fin de la déduction)

La réciproque ${\displaystyle \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 ${\displaystyle \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 : ${\displaystyle \lnot \lnot \lnot A\to \lnot A}$

${\displaystyle 01\quad \quad \lnot \lnot \lnot A}$ (hypothèse provisoire)

${\displaystyle 02\quad \quad \quad A}$ (hypothèse provisoire)

${\displaystyle 03\quad \quad \quad A\to \lnot \lnot A}$ (théorème de l'exemple 2)

${\displaystyle 04\quad \quad \quad \lnot \lnot A}$ (élimination de l'implication ou modus ponens entre 02 et 03)

${\displaystyle 05\quad \quad \quad \bot }$ (élimination de la négation entre 01 et 04)

${\displaystyle 06\quad \quad \lnot A}$ (introduction de la négation entre 02 et 05)

${\displaystyle 07\quad \lnot \lnot \lnot A\to \lnot A}$ (introduction de l'implication entre 01 et 06, fin de la déduction)

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 : ${\displaystyle \lnot (A\land B)\to (\lnot A\lor \lnot B)}$

${\displaystyle 01\quad \quad \lnot (A\land B)}$ (hypothèse provisoire [raisonnement par l'absurde])

${\displaystyle 02\quad \quad \quad \lnot (\lnot A\lor \lnot B)}$ (hypothèse provisoire)

${\displaystyle 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)

${\displaystyle 04\quad \quad \quad \lnot \lnot A\land \lnot \lnot B}$ (élimination de l'implication ou modus ponens entre 02 et 03)

${\displaystyle 05\quad \quad \quad A\land B}$ (élimination de la double négation dans 04)

${\displaystyle 06\quad \quad \quad \bot }$ (élimination de la négation entre 01 et 05)

${\displaystyle 07\quad \quad \lnot \lnot (\lnot A\lor \lnot B)}$ (introduction de la négation entre 02 et 06)

${\displaystyle 08\quad \quad \lnot A\lor \lnot B}$ (élimination de la double négation dans 07)

${\displaystyle 09\quad \lnot (A\land B)\to (\lnot A\lor \lnot B)}$ (introduction de l'implication entre 01 et 08)

Exemple 5 : si ${\displaystyle (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 ${\displaystyle (\lnot B\to \lnot A)\to (A\to B)}$.

Exemple 6: On peut démontrer que ${\displaystyle \lnot A\to (A\to B)}$. En effet si on ${\displaystyle \lnot A}$ et ${\displaystyle A}$, on a ${\displaystyle \bot }$ (faux) et donc on a ${\displaystyle B}$.

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

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

Exemple 7 connu sous le nom de loi de Peirce : ${\displaystyle ((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 ${\displaystyle ((A\to B)\to A)}$. D'après le tiers exclu:

• ou bien on a ${\displaystyle A}$,

• ou bien on a ${\displaystyle \lnot A}$ et donc on a ${\displaystyle A\to B}$ (exemple 6) et puisqu'on a ${\displaystyle ((A\to B)\to A)}$ avec le modus ponens, on a ${\displaystyle A}$.

Les règles de déduction pour les opérateurs universels et existentiels gouvernent l’usage des noms de variable. Cet usage donne à une théorie la puissance de la généralité, c’est-à-dire la possibilité de connaître non chaque individu 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. 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 ... 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 sous la forme d’une algèbre 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.

La règle d'introduction du quantificateur universel ou règle de généralisation é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.

${\displaystyle 1\quad P(x)}$

${\displaystyle 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.

${\displaystyle 1\quad \forall x\;P(x)}$

${\displaystyle 2\quad P(t)}$ (élimination de quel que soit)

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.

${\displaystyle 1\quad P(t)}$

${\displaystyle 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.

${\displaystyle 1\quad \exists x\;P(x)}$ (hypothèse)

${\displaystyle 2\quad \quad P(y)}$ (y variable nouvelle)

${\displaystyle 3\quad \quad R}$ (déduction à partir de 2, R ne faisant pas intervenir y)

${\displaystyle 4\quad R}$ (élimination de il existe dans 1 et 3)

Exemple 1 ${\displaystyle (\exists x\;\lnot A(x))\to (\lnot \forall x\;A(x))}$

${\displaystyle 1\quad \quad \exists x\;\lnot A(x)}$(hypothèse provisoire)

${\displaystyle 2\quad \quad \quad \forall x\;A(x)}$(hypothèse provisoire)

${\displaystyle 3\quad \quad \quad \quad \lnot A(y)}$ (y variable nouvelle à partir de 1)

${\displaystyle 4\quad \quad \quad \quad A(y)}$(élimination de quel que soit dans 2)

${\displaystyle 5\quad \quad \quad \quad \bot }$(élimination de la négation 3, 4)

${\displaystyle 6\quad \quad \quad \bot }$(élimination de il existe entre 1 et 5)

${\displaystyle 7\quad \quad \lnot (\forall x\;A(x))}$(introduction de la négation entre 2 et 6)

${\displaystyle 8\quad (\exists x\;\lnot A(x))\to (\lnot \forall x\;A(x))}$(introduction de l'implication 1, 7)

Exemple 2 : on a également ${\displaystyle \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.