Intérêt des différentes logiques?
Il existe la logique minimale, l'intuitionniste, la classique, la (les) modale(s), la linéaire et bien d'autres encore. Quel est pour chacune son intérêt pour le "working mathematician" ou même pour le logicien lui même?(Est-ce que ça sert à renforcer ou préciser les fondements de ce sur quoi on travaille?)
Merci d'avance.
Cordialement.
Jean-Louis.
Merci d'avance.
Cordialement.
Jean-Louis.
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
- Maxtimax dit souvent que dans son domaine, il est très content quand il a une démonstration intuitionniste de quelque chose, parce qu'il a un moyen d'en tirer de manière automatique plein de corollaires intéressants qu'il n'aurait pas sinon.
- Le recherche de logiques de plus en plus faibles permet de sonder la logique classique : si j'enlève ceci, qu'est-ce qu'il me reste ? Au minimum, ça permet d'avoir du recul sur les axiomes !
- Une branche de la logique s'intéresse à un lien très profond entre la logique et la programmation. Eh bien, considérer différentes logiques, c'est un peu comme considérer différents paradigmes de programmation, et le va-et-vient y est fructueux.
- Une des logiques remet en question le fait qu'on puisse dupliquer des hypothèses : si j'ai un euro, je peux m'acheter un croissant et je peux m'acheter un petit pain ; par contre, je ne peux pas m'acheter un croissant et un petit pain (puisque l'euro est dépensé). Bien sûr, si moi j'utilise le théorème de Pythagore, tu peux l'utiliser ensuite ! Mais la question a quand même un sens. Il se passe un phénomène similaire en mécanique quantique, où on peut démontrer qu'il n'est pas possible de cloner des choses.
1/ Tout d'abord, elles ont un intérêt mathématique en elle-même (comme les groupes, les evt, etc). Je ne détaille pas
2/ Depuis récemment, du fait de la découverte (probablement la plus importante de tous les temps) de la correspondance de Curry Howard, on est tous plongés littéralement dans l'ingénierie du fait de construire pour chaque preuve les traçages agressifs de résistance de la Nature à la réalisation de sa conclusion.
Quand tu fais une hypothèse H une fois mais que la preuve l'utilise $10^{403}$ fois (ce qui va vite, de nombreuses preuves sont dans cette situation) bien que la conclusion soit irréfutablement prouvée à partir des hypothèses, il est vain à l'avance de se demander, au moment de l'implémentation de la machine concrète, si on va tirer quelque chose du fait que
le bras H va rompre à la
90236436187136883873163748673.1567413631065817368.610368713687 ième sollicitation
puisqu'on le devine à l'avance
Les logiques affines et linéaires viennent alors naturellement combler ce clivage. Etc, etc.
Pour les mêmes raisons, la relativité n'est pas REPRODUCTIBLEMENT en contradiction formelle avec la TQ du fait qu'on ne peut cloner les comportements libres. Et là encore idem, une preuve affine ou linéaire passe le filtre quantique, mais pas l'intuitionniste ni le classique.
Mais effectivement, différents "univers" fonctionnent sous différentes logiques, et ces univers divers et variés peuvent apparaître même dans le boulot des "working mathematicians" (typiquement, la catégorie des faisceaux sur un espace topologique a une logique interne intuitionniste, c'est de ça qu'on peut tirer des choses, notamment pour les faisceaux sur un schéma)
Les logiques modales, par exemple, peuvent être interprétées dans les relations entre différentes extensions de forcing en théorie des ensembles; je crois que Joel David Hamkins bosse parfois là dessus.
Un autre exemple est celui de la géométrie différentielle synthétique : si tu t'autorises à changer de logique, tu peux te permettre de supposer tes rêves les plus fous ("toute fonction est différentiable") - ça peut paraître pas très concret, mais ensuite en choisissant des modèles bien adaptés, tu peux en déduire des informations sur les variétés au sens usuel : celles qui sont bien concrètes et qui intéressent beaucoup de gens.
Sinon je suis d'accord avec ce que raconte GA sur le recul que ça apporte; et aussi sur l'aspect "lien avec l'informatique": le point le plus important est certainement effectivement le lien entre la logique fondamentale et l'informatique. ça se traduit notamment par Curry-Howard, mais aussi par exemple par le fait que si on se place dans le monde des choses "calculables", ce dernier est intuitionniste.
(une petite remarque : les utilisations de logique en maths "usuelles" comme par exemple la géométrie différentielle synthétique sont peu développées pour une raison simple : les matheux-ses classiques n'aiment pas trop la logique et donc ne s'aventurent pas dans ce genre de choses, et les logicien-ne-s restent souvent en logique)
Tu as une culture mathématique impressionante pour ton age.
(Ce qui m'impressionne encore plus c'est que 3 ans auparavant, tu posais deja la question des cardinaux singuliers sous AD en première année à Ulm...)
Cordialement.
Blague à part, merci, mais ce n'est qu'une impression que je donne (:P)
La logique classique est la science des vérités éternelles.
La logique intuitionniste est la science du manque d'information ("je ne suis pas en possession de la certitude de A ni de celle de non A; je ne sais pas laquelle des deux est vraie")
La logique linéaire est la science des ressources limitées et des déchets non jetables (et autres pénalités incompressibles).
("si j'ai 100 euros et si j'ai 100 euros, je peux acheter cette paire de chaussures" à comparer avec "si j'ai 100 euros (seulement) je ne peux pas l'acheter", ou encore: "je peux acheter ce portable" vs -toutes choses égales par ailleurs- "si j'ai une amende de 300 euros, je peux (encore) acheter ce portable?")
(En ces temps obscurantistes, je préfère préciser)
Je suis curieux peut-tu préciser ce que tu entend par " plus faible " ?
Je serais très intéressé par ton argument.
Cordialement
C'est tout.
En espérant que tout le monde se porte bien.