Démonstrations toutes équivalentes ?

[invite9617f995]

Bonjour,

Je me suis récemment posé une question qui relève plus de la compréhension du raisonnement mathématique lui-même que des maths à proprement parlé. Je ne connais pas bien la manière dont est étudiée ce sujet, mais il me semble que pour élaborer les mathématiques, on doit partir d'un certains nombres d'axiomes, qui vont permettre de construire par des raisonnements mathématiques des théorèmes, des propriétés et des résultats.

Supposons alors que l'on part d'un certain nombre d'axiomes et que l'on développe une théorie autour. Est-ce que tout résultat ou théorème que l'on peut démontrer dans le cadre de cette théorie découle d'une unique "raison", d'un unique cheminement de raisonnement ?
Certains théorèmes ou résultats ont par exemple plusieurs démonstrations possibles : est-ce que celles-ci sont toutes équivalentes et en fait utilisent les mêmes résultats sans que ça n'apparaisse clairement ?

Je ne sais pas si une telle question a du sens et surtout si on peut y apporter une réponse, mais si quelqu'un a une idée dessus dont le principe peut-être compris sans un niveau trop élevé, je suis preneur.

Merci d'avance,
Cordialement, Silk.
-----

[Médiat]

Bonjour,

Dans le cadre que vous avez donné, le problème est plus simple qu'il n'y paraît : soit une proposition est un théorème (il existe au moins une démonstration), soit elle n'est pas un théorème (il n'existe pas de démonstration).

Une démonstration étant une suite de propositions commençant par des axiomes et dont chaque étape est déduite des précédentes grace à une règle d'inférence (les axiomes de la logique), j'ai un peu simplifié, mais c'est l'idée générale.

[invite9617f995]

Tout d'abord merci pour la réponse. Mais si on considère deux démonstrations d'un même théorème que l'on décompose comme une suite de propositions, est-ce que les propositions de la seconde suite pourrait être décomposé et/ou recomposé pour former la première démonstration ?

(Je sais pas si c'est très clair ce que je raconte).

[invite9cf21bce]

Bonjour.
Je ne comprends pas très bien ce que tu entends par "démonstrations équivalentes".

Admettons que tu te mettes dans le contexte "système de déduction".

Puis admettons, partant du même jeu d'axiomes , que tu démontres une proposition de deux manières différentes via ton système de déduction. Dire que tes deux manières sont "équivalentes" n'a pas trop de sens en soi, car cela relève d'une méta-définition du mot "équivalent" dans le contexte de l'organisation de tes preuves dans ton système de déduction. En particulier, cela dépend de ton système de déduction.

Une question qu'on peut se poser est : pour une logique donnée, existe-t-il une présentation du système de déduction dans laquelle deux démonstrations du même résultat à partir des mêmes axiomes sont forcément identiques (la refactorisation étant elle-même sous-jacente à la présentation du système) ?

Edit : Il semblerait que c'est bien de ça que tu parlais, vu ton nouveau post !

La réponse est oui dans certaines "logiques" simples ad hoc (qui n'ont plus rien à voir avec la logique classique) : il suffit de se placer dans un système formel assez restrictif et de définir une "logique" qui retranscrit le comportement des objets.

Par exemple, tu te mets dans un système ou les seules propositions sont 0, S(0), S(S(0)), S(S(S(0))), etc. et où la seule règle de déduction est d'ajouter un S au début. Il est clair que et qu'il n'y a pas cinquante manières de le prouver.

(ici, on s'est basé les entiers définis par 0 et successeur, qu'on a transcrit dans le langage des propositions et des systèmes de déduction, la déduction n'est autre que la relation inférieur ou égal)

Pour en revenir aux systèmes un peu plus conventionnels (sinon, mon post n'est que du vent), j'ai quelque chose à dire à propos de la logique intuitionniste. Je ne me suis pas assez plongé dans le truc : cependant, il me semble avoir plus ou moins compris qu'en mathématiques constructives, on a longtemps rêvé d'un truc comme ça en matérialisant les preuves elles-mêmes comme des objets typés. C'est le cas en calcul des constructions ; il semblerait que dans tout système de ce type, l'indépendance à la preuve (proof irrelevance) est vouée à l'échec, car (système+proof irrelevance) est strictement plus fort que (système seul), en ce sens que des résultats y sont démontrables qui ne sont pas vrais dans le système seul.

Voir par exemple cet article.

[A voir en vidéo sur Futura]