Logique intuitionniste

La logique intuitionniste est une logique qui diffère de la logique classique par le fait que la notion de vérité est remplacée par la notion de preuve constructive. Une proposition telle que « la constante d'Euler-Mascheroni est rationnelle ou la constante d'Euler-Mascheroni n'est pas rationnelle » n'est pas démontrée de manière constructive (intuitionniste) dans le cadre de nos connaissances mathématiques actuelles, car la tautologie classique « P ou non P » (tiers exclu) n'appartient pas à la logique intuitionniste. La logique intuitionniste établit, entre autres, un distinguo entre « être vrai » et « ne pas être faux » (formulation plus faible) car ¬¬P → P n'est pas non plus démontrable en logique intuitionniste. L'intuitionnisme a d'abord été une position philosophique vis-à-vis des mathématiques proposée par le mathématicien hollandais Luitzen Egbertus Jan Brouwer comme une possibilité différant de l'approche dite classique ; cela l'a conduit à ne pas inclure certaines formes du raisonnement mathématique traditionnel, qu'il jugeait contre-intuitives : Le tiers exclu, qui consiste à dire qu'étant donnée une proposition , on a soit ou alors non ; L'existentiel non constructif. Brouwer veut que quand un mathématicien affirme il existe tel que , il donne aussi un moyen de construire qui satisfait . Brouwer a prôné une mathématique qui rejetterait le tiers exclu et n'accepterait que lexistentiel constructif. Cette attitude a été assez violemment critiquée par des mathématiciens comme David Hilbert tandis que d'autres comme Hermann Weyl y ont souscrit. Elle a été ensuite formalisée, sous le nom de logique intuitionniste, par ses élèves V. Glivenko et Arend Heyting, ainsi que par Kurt Gödel et Andreï Kolmogorov. L'interprétation de Brouwer-Heyting-Kolmogorov ou simplement interprétation BHK est essentiellement la mise en évidence du caractère constructif de l'implication intuitionniste : Quand un mathématicien intuitionniste affirme , il veut dire qu'il fournit un procédé de « construction » d'une démonstration de à partir d'une démonstration de .

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Concepts associés (115)

Cours associés (16)

Séances de cours associées (143)

EE-110: Logic systems (for MT)

Ce cours couvre les fondements des systèmes numériques. Sur la base d'algèbre Booléenne et de circuitscombinatoires et séquentiels incluant les machines d'états finis, les methodes d'analyse et de syn

MATH-381: Mathematical logic

Branche des mathématiques en lien avec le fondement des mathématiques et l'informatique théorique. Le cours est centré sur la logique du 1er ordre et l'articulation entre syntaxe et sémantique.

CS-101: Advanced information, computation, communication I

Discrete mathematics is a discipline with applications to almost all areas of study. It provides a set of indispensable tools to computer science in particular. This course reviews (familiar) topics a

Systèmes logiques : multiplexeurs et flip-flops EE-110: Logic systems (for MT)

Explique les circuits de verrouillage SR, les verrous D, les bascules D, les signaux d'horloge et les multiplexeurs dans les systèmes logiques.

Algèbre booléenne : propriétés et optimisation EE-110: Logic systems (for MT)

Explore les propriétés de l'algèbre booléenne et les techniques d'optimisation en utilisant les diagrammes de Karnaugh et les théorèmes de De Morgan.

SR Latch et D Flip-Flop: Éléments de mémoire dans les systèmes logiques EE-110: Logic systems (for MT)

Explore le verrou SR, la bascule D, les multiplexeurs, les portes XOR et les portes tristates dans les systèmes logiques.

Logique combinatoire

En logique mathématique, la logique combinatoire est une théorie logique introduite par Moses Schönfinkel en 1920 lors d'une conférence et développée dès 1929 par Haskell Brooks Curry pour supprimer le besoin de variables en mathématiques, pour formaliser rigoureusement la notion de fonction et pour minimiser le nombre d'opérateurs nécessaires pour définir le calcul des prédicats à la suite de Henry M. Sheffer. Plus récemment, elle a été utilisée en informatique comme modèle théorique de calcul et comme base pour la conception de langages de programmation fonctionnels.

Logique intuitionniste

Logique

La logique — du grec , qui est un terme dérivé de signifiant à la fois « raison », « langage » et « raisonnement » — est, dans une première approche, l'étude de l'inférence, c'est-à-dire des règles formelles que doit respecter toute argumentation correcte. Le terme aurait été utilisé pour la première fois par Xénocrate. La logique antique se décompose d'abord en dialectique et rhétorique. Elle est depuis l'Antiquité l'une des grandes disciplines de la philosophie, avec l'éthique (philosophie morale) et la physique (science de la nature).