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 bi […]
… pour nos abonnés, l'article se prolonge sur 9 pages…
