DÉMONSTRATION THÉORIE DE LA
Carte mentale
Élargissez votre recherche dans Universalis
La logique Π12
L'extension des résultats obtenus par Takeuti, Pohlers, Buchholz... pour le schéma de compréhension Π11 à des systèmes plus forts nécessite de remplacer la ω-logique par des logiques correspondant à de plus grandes complexités logiques, Π21 et plus généralement Π1n . Le problème de la B-règle, posé par Mostowski est le suivant : Caractériser les énoncés qui sont vrais dans tout modèle dans lequel les objets d'un type distingué Ω sont interprétés par un ordinal α et où la relation ≤ distinguée entre objets de type Ω est interprétée par l'ordre de α (B-modèles). Une réponse simple est donnée par : pour tout α, nous avons une démonstration au moyen de la α-règle, qui est l'analogue de la ω-règle, obtenu en remplaçant ω par α. Cela dit, une famille (Pα) de α-démonstrations indexées par tous les ordinaux ne constitue pas spécialement un objet syntaxique ! On définit la catégorie ON des ordinaux en prenant pour morphismes les ensembles I(α, β) d'applications strictement croissantes de α vers β. Si P est une β-démonstration, on peut, dans certaines conditions, définir, si f ∈ I(α, β), une α-démonstration f -1(P). Si on demande que la famille (Pα) soit telle que f -1(Pβ) = Pα, alors cette famille est appelée une B-démonstration. Une B-démonstration apparaît, en fait, comme un foncteur de la catégorie ON dans une catégorie DEM de démonstrations et on vérifie qu'un tel foncteur préserve les limites directes (c'est-à-dire inductives filtrantes) et les produits fibrés. En particulier, la donnée de la famille (Pn), pour n fini, détermine uniquement (par unicité du prolongement par limites directes) la famille (Pα). Il devient alors possible de parler de B-démonstration récursive, autrement dit nous avons un concept syntaxique. (Mais l'ensemble des indices de B-démonstrations est Π12 .) Et Girard a pu établir en 1978 la B-complétude :
Théorème. Γ ⊢ Δ est vrai dans tout B-modèle si et seulement s'il y a une B-démonstration récursive de ce séquent.
Un concept proche est celui de dilatateur : un dilatateur est un foncteur de ON dans ON préservant les limites directes e [...]
1
2
3
4
5
…
pour nos abonnés,
l’article se compose de 10 pages
Écrit par :
- Jean-Yves GIRARD : docteur ès sciences, maître de recherche au C.N.R.S.
Classification
Autres références
« DÉMONSTRATION THÉORIE DE LA » est également traité dans :
GENTZEN GERHARD (1909-1945)
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)
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)
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)
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
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 25 janvier 2021. URL : https://www.universalis.fr/encyclopedie/theorie-de-la-demonstration/