Présentation

Après avoir rappelé que l'intuitionnisme tire sa justification ultime d'une certaine idée de la vérité, on montre les répercussions de celle-ci sur les mathématiques puis sur la logique. On oublie souvent que Brouwer ne reconnaissait à peu près aucune valeur à la logique et que ses efforts visaient avant tout à donner une bonne théorie du continu À cette fin. il a développé une mathématique originale qui introduit le devenir dans l'univers jusqu'alors statique des mathématiques. Toutefois, c'est en logique que l'intuitionnisme est aujourd'hui le plus présent. Dans l'interprétation intuitionniste des constantes logiques, la conditionnelle est une fonction. Le lien qui en résulte entre calcul lambda typé et logique intuitionniste a conduit au principe de la proposition comme type, dont les conséquences philosophiques ne sont pas moins considérables que les applications informatiques. Elles concernent non seulement notre idée de la preuve, mais aussi les concepts fondamentaux de la logique : le formalisme aujourd'hui dominant doit être rejeté et certaines distinctions traditionnelles un temps oubliées demandent à être réactivées.