2. 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.
[…]… pour nos abonnés, l'article se prolonge sur 2 pages…
