Intérêt des différentes logiques?

Je réponds sans trop m'y connaître, mais pour lancer des pistes :
- 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.

Georges: ce n'est pas mon domaine, c'est en géométrie algébrique :-D
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)

axexe : j'ai posé cette question moi ? :-D
Blague à part, merci, mais ce n'est qu'une impression que je donne (:P)

De mon téléphone pour les visiteurs. Je précise que TOUTES LES LOGIQUES évoquées sont PLUS FAIBLES que la logique classique.

(En ces temps obscurantistes, je préfère préciser)

@petitepsilon : il n'y a pas d'argument, c'est une définition. On dit qu'une logique $L$ est plus faible qu'une logique $L'$ si tout ce qui est démontrable par $L$ l'est aussi par $L'$, et s'il existe au moins un énoncé qui est démontrable par $L'$ mais pas par $L$.
C'est tout.

@Christophe : pour une fois que je peux répondre à ta place, ce fut un plaisir...