Logique intuitionniste et constructivisme
La logique intuitionniste rejette le principe du tiers exclu, considérant qu'une proposition mathématique n'est vraie que si l'on peut en construire une preuve.
Definition
La logique intuitionniste est la logique de la preuve constructive, dans laquelle une disjonction exige la preuve d'un des disjoncts et une affirmation existentielle exige la construction d'un témoin, de sorte que le principe du tiers exclu et la preuve par contradiction pour les affirmations d'existence ne sont généralement pas valides.
Scope
Ce sujet couvre la logique intuitionniste et la philosophie constructiviste des mathématiques qui la motive. Il aborde la conception de Brouwer des mathématiques comme construction mentale, la formalisation de Heyting et l'interprétation des connecteurs basée sur la preuve (BHK), l'échec du principe du tiers exclu et de l'élimination de la double négation, les sémantiques de Kripke et topologiques pour la logique intuitionniste, ainsi que l'argument sémantique de Dummett selon lequel l'anti-réalisme concernant la vérité soutient généralement la logique intuitionniste.
Core questions
- Pourquoi le principe du tiers exclu devrait-il échouer, et pour quelles propositions ?
- Quelle est l'interprétation constructive des connecteurs logiques ?
- L'argument en faveur de l'intuitionnisme est-il spécifiquement mathématique, ou se généralise-t-il via la théorie de la signification ?
- Comment les modèles de Kripke et topologiques éclairent-ils la validité intuitionniste ?
Key concepts
- principe du tiers exclu
- preuve constructive
- interprétation BHK
- traduction en double négation
- modèles de Kripke pour l'intuitionnisme
- vérificationnisme
Key theories
- Interprétation BHK (basée sur la preuve)
- L'interprétation de Brouwer-Heyting-Kolmogorov explique chaque connecteur par ce qui constitue une preuve d'une proposition composée, de sorte que 'A ou B' exige une preuve de A ou une preuve de B, ce qui bloque le principe du tiers exclu illimité.
- L'argument anti-réaliste de Dummett
- Dummett soutient qu'une théorie de la signification contrainte par ce que les locuteurs peuvent manifester privilégie une sémantique basée sur les conditions de vérification plutôt que sur les conditions de vérité, et que cet anti-réalisme impose la logique intuitionniste de manière générale, et pas seulement en mathématiques.
History
Brouwer a fondé l'intuitionnisme dans les années 1900-1920 comme un rejet constructiviste des mathématiques classiques ; Heyting a formalisé la logique intuitionniste en 1930. Le calcul des problèmes de Kolmogorov et l'interprétation BHK ont clarifié sa signification, Kripke a ensuite fourni une sémantique relationnelle, et Dummett a reformulé l'intuitionnisme comme une conséquence générale de l'anti-réalisme sémantique.
Debates
- L'anti-réalisme généralise-t-il l'intuitionnisme au-delà des mathématiques ?
- La question de savoir si l'argument sémantique de Dummett étend avec succès l'argument en faveur de la logique intuitionniste des mathématiques au discours en général, ou si la motivation originale est essentiellement liée à la nature constructive des objets mathématiques.
Key figures
- L. E. J. Brouwer
- Arend Heyting
- Michael Dummett
- Andrey Kolmogorov
- Per Martin-Lof
Related topics
Seminal works
- heyting1956
- dummett2000
Frequently asked questions
- La logique intuitionniste rejette-t-elle toutes les preuves par contradiction ?
- Pas toutes. Les intuitionnistes acceptent de prouver une négation en dérivant une contradiction de l'hypothèse, puisque c'est ainsi que la négation est définie. Ce qu'ils rejettent, c'est l'établissement d'une affirmation d'existence positive ou d'une disjonction simplement en réfutant sa négation, car cela ne produit aucun témoin constructif et repose sur l'élimination de la double négation, qui n'est pas valide intuitionnistiquement.