Intuitionnisme

Imaginez que l'on affirme : « Il existe un nombre entier naturel, pair et supérieur à 10. » Pour l'intuitionnisme, cette existence devient établie lorsqu'on peut produire un nombre précis, par exemple 12, puis vérifier les propriétés annoncées.

Cette exigence change le sens d'une preuve : démontrer revient à construire ou à donner une procédure vérifiable. Dire qu'une proposition ne peut pas être fausse ne suffit donc pas toujours à démontrer qu'elle est vraie.

L'intuitionnisme est une philosophie fondationnelle des mathématiques développée par Brouwer au début du XX^e siècle. Une affirmation mathématique y est liée à une construction qui en constitue la preuve. Pour établir qu'un objet existe, il faut donc fournir cet objet ou une méthode qui permet de le construire.

La logique intuitionniste n'admet pas comme règle générale le principe du tiers exclu. Pour une proposition notée P, ce principe affirme que P est vraie ou que sa négation est vraie : $P\vee \mathrm{\neg }PP\; \backslash lor\; \backslash neg\; P$. Sans preuve de l'une des deux branches, cette alternative ne peut pas être utilisée automatiquement. De même, obtenir une contradiction à partir de la négation de P prouve la double négation de P, mais ne fournit pas en général une preuve de P.

Ce cadre est plus restrictif que les mathématiques classiques, sans interdire tout raisonnement par contradiction. Il impose surtout une vigilance pour les conclusions positives et existentielles. La logique intuitionniste sous-tend aussi la théorie des types et l'informatique théorique grâce à la correspondance de Curry-Howard, qui rapproche preuves et constructions calculables.

On veut établir qu'il existe un entier naturel pair strictement supérieur à 10. Les données sont la borne 10 et la propriété « être pair », c'est-à-dire être le double d'un entier naturel.

1. Choisissons le témoin n = 12.

2. Vérifions les deux conditions :Le nombre 6 étant un entier naturel, la première égalité montre que 12 est pair. La seconde comparaison établit qu'il dépasse strictement 10.

3. Le même objet satisfait les deux propriétés. Le témoin 12, accompagné de ces vérifications, constitue donc une preuve constructive de l'existence demandée.

Le contrôle est refaisable : diviser 12 par 2 donne exactement 6, sans reste, puis comparer 12 à 10 confirme l'inégalité.

Devant une preuve d'existence, cherchez le témoin produit. Dans l'exemple, le nombre 12 joue ce rôle et les deux vérifications permettent de contrôler immédiatement la conclusion.

Devant une alternative « P ou non-P », demandez quelle branche a été démontrée. Si aucune procédure ne permet de trancher P, la logique intuitionniste ne retient pas automatiquement le tiers exclu, contrairement à la logique classique.

En informatique théorique, une preuve constructive se lit comme une construction exploitable. La correspondance de Curry-Howard relie ainsi la logique intuitionniste à la théorie des types : une preuve porte une information de calcul, plutôt qu'un simple verdict d'existence.

Logique intuitionniste et logique classique. La logique classique autorise sans condition le tiers exclu et le passage de « non-non-P » à P. La logique intuitionniste exige une preuve de P pour ce second passage. Une démonstration fondée uniquement sur cette élimination de la double négation sépare donc les deux cadres.

Intuitionnisme et simple intuition. L'intuitionnisme n'est pas l'acceptation d'une idée parce qu'elle paraît évidente. Son critère est au contraire vérifiable : une affirmation doit être soutenue par une construction ou une preuve conforme aux règles intuitionnistes. Le témoin 12 et ses contrôles tranchent ce cas.

Ne pas lire le refus du tiers exclu comme sa négation. Ne pas disposer d'une preuve de « P ou non-P » ne signifie pas avoir prouvé que cette alternative est fausse. Il faut conserver la distinction entre absence de construction et réfutation.

Le tiers exclu peut être établi dans un cas particulier. Lorsqu'une procédure finie décide effectivement P, elle fournit l'une des deux branches. Par exemple, le calcul du reste de 12 dans la division par 2 décide que 12 est pair.

La contradiction n'est pas entièrement bannie. Elle établit directement une négation lorsqu'on montre qu'une hypothèse conduit à l'impossible. Le piège consiste à en tirer une affirmation positive ou existentielle sans construction correspondante.

Un candidat sans contrôle ne suffit pas. Donner 12 ne prouve l'énoncé de l'exemple qu'après avoir vérifié 12 = 2 × 6 et 12 > 10. Le témoin et la preuve de ses propriétés forment ensemble la construction exigée.

La fiche Brouwer Luitzen Egbertus Jan situe le mathématicien à l'origine de l'école intuitionniste.

Le Principe du tiers exclu approfondit précisément la règle logique dont l'emploi général distingue logique classique et logique intuitionniste.

La fiche constructivisme - philosophie - permet de replacer l'exigence de construction dans une famille philosophique plus large.