L'intuitionnisme est une position philosophique vis-à-vis des mathématiques proposée par le mathématicien hollandais Luitzen Egbertus Jan Brouwer comme une alternative à l'approche dite classique. Elle a été ensuite formalisée, sous le nom de logique intuitionniste, par ses élèves V. Glivenko et Arend Heyting. Kurt Gödel a montré que l'on pouvait représenter la logique classique dans la logique intuitionniste, corroborant le fait que la logique intuitionniste n'est pas une logique à part, mais fait bien partie de la logique. Gerhard Gentzen en a formalisé les règles de déduction dans le cadre de la déduction naturelle.
Les travaux récents, notamment la correspondance de Curry-Howard, lui ont donné un statut central dans la logique et dans l'informatique, en faisant d'elle historiquement la première des logiques constructives. Des travaux la concernant, effectués par Gödel et Andreï Kolmogorov au sujet de la « non-non interprétation » (interprétation de la double négation) ont ouvert la porte de l'interprétation de la logique classique dans les termes de la logique intuitionniste. L'étude de la logique intuitionniste est la clé pour bien comprendre la logique classique et ses subtilités.
Cet article écrit par ces auteurs est issu de Wikipédia et est conforme aux termes de la GFDL.
Catégories : Logique mathématique 
Théorie des types
Page imprimée jeudi 17 mai 2012 à partir de l'url :
« http://www.science-et-vie.net/definition-logique-intuitionniste-1065.html »
Site déclaré à la Commission Nationale de l'Informatique et des Libertés (CNIL) sous le n°871314
© 2002-2012 www.science-et-vie.net