Forum de mathématiques - Bibm@th.net

tibo

Membre expert

Inscription : 23-01-2008

Messages : 1 097

Définition de "démonstration"

Je trouve la question intéressante mais je ne veux pas polluer la discussion où elle a été lancée.
Je résume ce qui a été dit:

Une démonstration est un procédé qui à partir de propositions postulées comme vraies démontre la véracité d'une nouvelle proposition.

"On rédige une démonstration pour être lue et convaincre les lecteurs, et le niveau de détail nécessaire n'est pas le même suivant les connaissances de ceux-ci. Cependant avec l'avènement des ordinateurs et des systèmes d'aide à la démonstration, certains mathématiciens contemporains rédigent des démonstrations qui sont amenées à être vérifiées par des programmes."

J'ai fait exprès de poser cette question sachant la difficulté d'y répondre.
J'ai moi-même l'habitude de démontrer des trucs mais je ne pense pas être capable d'en donner une définition précise. Essayons tout de même :
Suite finie d’assertions dont les premières sont des assertions postulées (des axiomes) ou des assertions déjà démontrées, la dernière assertion est le théorème et le passage d'un rang au suivant doit suivre des règles logiques.
Reste à définir ces règles mais il y en a trop je pense ^^

Sinon une citation de René THOM je crois:
Est rigoureuse toute démonstration, qui, chez tout lecteur suffisamment instruit et préparé, suscite un état d'évidence qui entraîne l'adhésion."

Barbichu

Membre actif

Inscription : 15-12-2007

Messages : 405

Re : Définition de "démonstration"

Salut tibo,

Suite finie d’assertions dont les premières sont des assertions postulées (des axiomes) ou des assertions déjà démontrées, la dernière assertion est le théorème et le passage d'un rang au suivant doit suivre des règles logiques.
Reste à définir ces règles mais il y en a trop je pense ^^

En fait il n'y en a pas tant que cela. Il y a de nombreux systèmes logiques avec plus ou moins de règles, plus ou moins d'axiomes, suivant des formulations plus ou moins élaborées. L'un des premiers à avoir étudié la question formellement est Gottlob Frege, puis ont suivi Hilbert, Whitehead, Russel, Gentzen…

Dans un système basé sur une axiomatisation, parfois appelé système à la Hilbert, il faut très peu de règles pour assembler les axiomes (au choix, mais il faut au moins inclure les axiomes du calcul des prédicats) et former de nouveaux théorèmes: le modus ponens et la règle de généralisation.

Il y a d'autres façons de présenter les choses, notamment la déduction naturelle et le calcul des séquents. On peut bien sûr aussi poser des axiomes dans des systèmes baées sur ces formulations, mais c'est parfois plus élégant de ne pas en poser, les règles de déductions étant suffisantes pour commencer à générer des théorèmes.

Il y a des systèmes plus expressifs que d'autres (B est plus expressif que A si tout ce que je peux déduire dans A, je peux le déduire dans B). Par exemple, si je prend les axiomes d'Euclide avec les règles du calcul des prédicats, tout ce que je peux en déduire, je peux en fait le déduire en théorie des ensembles.
Personnellement, j'utilise au quotidien une théorie des types (implémentée par Coq), qui est une extension du lambda calcul et qui peut-être présenté comme un calcul des séquents.

Si tu t'intéresses à ce sujet, c'est toute une branche de la logique, à l'interface entre les mathématiques et l'informatique théorique qui s'ouvre à toi : il s'agit de la théorie de la démonstration.

A+

Dernière modification par Barbichu (31-10-2013 00:08:07)