INTUITIONNISME
La sémantique BHK
Le principal disciple de Brouwer, Heyting, a mis au point une logique non classique qui consigne les principes d'inférence qui sont « fiables » en ce sens. Cette logique, au lieu de décrire sémantiquement les conditions de vérité (au sens classique où la vérité est indépendante de nos capacités de connaissance) des énoncés, en décrit les conditions d'assertabilité, c'est-à-dire les conditions auxquelles nous sommes justifiés à les tenir pour corrects. La sémantique en question, aujourd'hui nommée BHK (Brouwer-Heyting-Kolmogoroff), stipule, par exemple, que la preuve d'une disjonction consiste en la preuve de l'une des deux propositions qui y figurent, ou que la preuve d'une négation consiste en une construction qui transforme toute preuve putative de la proposition niée en preuve d'une absurdité.
Longtemps confinée, comme la doctrine intuitionniste elle-même, à un rôle marginal (selon le mot fameux de Bourbaki, l'école intuitionniste n'était destinée à demeurer qu'à titre de « souvenir historique »), la sémantique BHK s'est révélée crucialement importante pour l'informatique théorique à partir des années 1960, notamment en raison de l'isomorphisme assez naturel qui relie les preuves intuitionnistes ainsi définies et les termes d'un certain calcul sur des termes fonctionnels.
La suite de cet article est accessible aux abonnés
- Des contenus variés, complets et fiables
- Accessible sur tous les écrans
- Pas de publicité
Déjà abonné ? Se connecter
Écrit par
- Jacques-Paul DUBUCS : chargé de recherche au C.N.R.S.
Classification
Autres références
-
BOREL ÉMILE (1871-1956)
- Écrit par Maurice FRÉCHET
- 2 290 mots
...d'articles à la philosophie et à l'histoire des sciences, à la psychologie, à la pédagogie et à l'économie politique. Fervent défenseur de la conception intuitionniste des mathématiques, il a toujours insisté sur la nécessité de ne jamais perdre de vue le « réel » : pour lui, « les mathématiques ne sont... -
BROUWER LUITZEN (1881-1966)
- Écrit par Gabriel SABBAGH
- 117 mots
Logicien et mathématicien hollandais, né à Amsterdam, Brouwer est l'un des fondateurs de la topologie algébrique. Il en a démontré l'un des plus beaux théorèmes, le théorème du point fixe, dont les applications et généralisations, de la théorie des jeux aux équations différentielles, se sont révélées...
-
CONCEPTUALISME, philosophie
- Écrit par Joseph VIDAL-ROSSET
- 1 329 mots
...Contingence (1984), Jules Vuillemin réserve le terme de conceptualisme à ce que l'on a appelé le conceptualisme ontologique, et utilise le terme d'intuitionnisme pour faire référence à une position philosophique qui subordonne la vérité à la méthode par laquelle la raison accède à celle-ci.... -
CONSTRUCTIVISME, mathématique
- Écrit par Jacques-Paul DUBUCS
- 1 372 mots
– l'intuitionnisme de Luitzen Brouwer (1881-1966) et Arend Heyting (1898-1980), qui rejette certains principes de la logique classique, comme celui du tiers-exclu (A ou non A) ; - Afficher les 15 références
