DÉMONSTRATION THÉORIE DE LA

Carte mentale

Élargissez votre recherche dans Universalis

La théorie de la démonstration est la logique de la logique. En contraste avec d'autres sous-domaines tels que la théorie des modèles, les grandes questions qui ont tant passionné nos pères ont laissé une trace vivace dans cette discipline, qui s'occupe essentiellement (c'est là la définition technique de la théorie de la démonstration) de l'aspect syntaxique de la logique. Au début, grâce au programme de Hilbert, la théorie de la démonstration avait des visées claires et nettes ; mais, après l'échec du programme (1931), tout devint beaucoup moins simple. En particulier, plus question de répondre de manière simpliste aux grandes interrogations ontologiques sur la nature des mathématiques... Faute de pierre philosophale, la discipline aurait pu disparaître ; s'il n'en a rien été, c'est sans doute que l'étude générale des relations des objets finis aux objets infinis :

– dans la dénotation d'objets (infinis) par des constructions syntaxiques (finies),

– dans les preuves de propriétés d'objets (infinis) au moyen de démonstrations (finies), constitue, par-delà les querelles d'école et les tentatives éphémères du genre de celle que fit Hilbert, le véritable objet de la théorie.

Les avancées en théorie de la démonstration semblent liées à un progrès quant aux méthodes utilisées, plus précisément quant à leur complexité logique :

– Hilbert tenta d'élaborer une théorie élémentaire de la démonstration (« élémentaire » signifiant : de complexité logique nulle, cf. chap. 1) ;

– Gentzen a introduit les méthodes essentielles pour l'analyse des systèmes logiques finis (complexité logique Σ01 , cf. chap. 2) ;

– plus tard, on a considéré des logiques généralisées (infinies) ; la plus connue d'entre elles est la logique avec ω-règle (complexité logique Π11 , cf. chap. 3) ; mais de nouvelles logiques de plus grande complexité (Π12 , voire Π1n : cf. chap. 4) sont maintenant utilisées de manière intensive.

Cette question de complexité logique fait l'objet de nombreux contresens ; aussi importe-t-il de dire bien clairement en quoi elle intervient :

– individuellement, les objets considérés sont effectivement calculables, ils sont en pratique récursifs ; il en est de même des opérations définies sur ces objets ; par exemple les ω-démonstrations sont toujours récursives et peuvent être normalisées (par élimination des coupures) effectivement. On voit donc que, pour les objets, la complexité logique ne joue pas ;

– par contre, l'ensemble de tous les objets du genre considéré est logiquement complexe (l'ensemble des ω-démonstrations récursives est Π11 ; cette complexité logique intervient de manière décisive dans la démonstration du théorème d'élimination des coupures, à savoir que la fonction effective qui élimine les coupures remplit bien son rôle) ;

– dans la pratique, la complexité logique joue surtout un double rôle ; elle a un rôle « hygiénique » : assurer que tout se passe bien, que les opérations définies ont les propriétés attendues ; elle joue aussi un rôle de révélateur : voir des problèmes simples de manière inhabituelle ; le détour par des problèmes de très grande complexité logique peut permettre d'y voir clair dans des situations élémentaires embrouillées.

Une dernière mise en garde : ne pas croire que la complexité logique d'un problème soit un gage de profondeur...

Le programme de Hilbert

David Hilbert a proposé un programme de démonstration d'une opinion philosophique : le formalisme. La prétention de Hilbert à démontrer son point de vue a pour contrepartie évidente la possibilité de le réfuter ; la philosophie s'accommode rarement de conclusions aussi tranchées ! Même réfuté, le formalisme garde ses adeptes, notamment en France, avec Bourbaki : on sait bien que les idéologies simplistes ont un pouvoir d'attraction qui persiste même après leur échec patent ; la réfutation de Hilbert par Gödel ne nous propose en aucune manière une vision de même nature : Gödel a détruit l'espoir de donner une réponse claire et nette à certaines interrogations essentielles, mais il n'a pas donné les bases d'un nouveau credo. Les mathématiques doivent être analysées comme une activité sans signification, semblable à un jeu, tel le jeu d'échecs : il s'agit de règles formelles fixées à l'avance et permettant de construire certains assemblages de symboles, à savoir les énoncés mathématiques et leurs démonstrations.

Voilà [...]

1  2  3  4  5
pour nos abonnés,
l’article se compose de 10 pages

Écrit par :

Classification

Autres références

«  DÉMONSTRATION THÉORIE DE LA  » est également traité dans :

GENTZEN GERHARD (1909-1945)

  • Écrit par 
  • Gabriel SABBAGH
  •  • 133 mots

Logicien allemand, né à Greifswald et mort à Prague lors de son emprisonnement par les Soviétiques. Gentzen a développé l'étude des systèmes de déduction naturelle et établi un théorème d'élimination des coupures. Gerhard Gentzen a également donné une démonstration de consistance de l'arithmétique du premier ordre fondée sur l'induction transfinie jusqu'au premier nombre ordinal inaccessible pour […] Lire la suite

HERBRAND JACQUES (1908-1931)

  • Écrit par 
  • Gabriel SABBAGH
  •  • 87 mots

Logicien et mathématicien français né à Paris et mort à Saint-Christophe-en-Oisans dans un accident de montagne. La brève carrière de Jacques Herbrand est marquée par sa démonstration, essentiellement correcte, d'un théorème central du calcul des prédicats du premier ordre, qui a des rapports étroits avec le théorème de complétude et les travaux de Gentzen, ainsi que par d'intéressantes contributi […] Lire la suite

HILBERT DAVID (1862-1943)

  • Écrit par 
  • Rüdiger INHETVEEN, 
  • Jean-Michel KANTOR, 
  • Christian THIEL
  •  • 14 856 mots
  •  • 1 média

Dans le chapitre « Programme de Hilbert et théorie de la démonstration »  : […] Pour deux raisons, la non-contradiction de l'arithmétique par rapport à une autre théorie ne semblait plus démontrable. D'une part, les démonstrations relatives de non-contradiction utilisaient toutes déjà des moyens arithmétiques ; d'autre part, la seule théorie par rapport à laquelle une telle démonstration aurait pu être menée – la logique développée autour d'une théorie classique des ensembles […] Lire la suite

POST EMIL LEON (1897-1954)

  • Écrit par 
  • Bernard JAULIN
  •  • 622 mots

Mathématicien américain né à Augustów (Pologne) et mort à New York. Arrivé aux États-Unis en 1904, Emil Post obtint son Ph.D. à l'université Columbia de New York en 1920. Il était membre de l'American Mathematical Society depuis 1918 et de l'Association for Symbolic Logic dès sa fondation en 1935. Sa thèse de doctorat, publiée en 1921, porte sur le calcul propositionnel de A. N. Whitehead et B. Ru […] Lire la suite

RÉCURSIVITÉ, logique mathématique

  • Écrit par 
  • Kenneth Mc ALOON, 
  • Bernard JAULIN, 
  • Jean-Pierre RESSAYRE
  •  • 9 371 mots

Dans le chapitre « Indécidabilité de propriétés classiques »  : […] Propriété b . Pour tout ensemble non vide A ⊂ F R ( p ) , l'ensemble ϕ −1 (A) est non récursif. Ainsi, si on considère une propriété des fonctions calculables définissant un ensemble non vide A ⊂ *F R ( p ) , l'ensemble ϕ −1 (A) des programmes permettant de calculer (ou qui définissent) ces fonctions n'est pas récursif. Par exemple, pour p  = 1, si : ϕ −1 (A) est l'ensemble des programmes qui s' […] Lire la suite

Voir aussi

Pour citer l’article

Jean-Yves GIRARD, « DÉMONSTRATION THÉORIE DE LA », Encyclopædia Universalis [en ligne], consulté le 11 août 2022. URL : https://www.universalis.fr/encyclopedie/theorie-de-la-demonstration/