The proof-explanation of logical constants is logically neutral
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...
Guardat en:
| Autor principal: | |
|---|---|
| Format: | Article ou chapitre numérique |
| Idioma: | Français |
| Publicat: |
2004
|
| Accés en línia: | Accès Université d'Orléans et IFPM Accès Université d'Orléans et IFPM |
| Sumari: | 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. |
|---|