DÉMONSTRATION THÉORIE DE LA
Le calcul des séquents
L'ontologie hilbertienne se fondait sur les énoncés Π01 . À bien des égards, la classe duale (Σ01 ) a un bien meilleur comportement ; par exemple, tout énoncé Σ01 vrai est prouvable par des méthodes élémentaires. À partir de cela, l'analogue du programme de Hilbert pour les énoncés Σ01 devient démontrable pour les théories courantes ; mais la démonstration n'est pas élémentaire ! Σ01 est la complexité logique de la démonstrabilité dans les systèmes de logique usuelle (finitaire). Les travaux de Gentzen, vers 1935, ont permis de démontrer un principe de pureté des méthodes pour le calcul des prédicats, c'est-à-dire la logique pure, sans axiomes. En quelque sorte, ce que Hilbert voulait faire avec les mathématiques élémentaires, Gentzen le réalisa dans le cadre du calcul des prédicats.
Système LK
Dans ce qui suit, L est un langage du premier ordre arbitraire. Un séquent est une expression formelle Γ ⊢Δ, où Γ et Δ sont des suites finies d'énoncés de L. L'interprétation intuitive de A1, ..., An ⊢ B1, ..., Bm, c'est que la conjonction des Ai implique la disjonction des Bj. En particulier, ⊢ A veut dire A, et A ⊢ veut dire ¬ A ; quant au séquent vide ⊢, il signifie l'absurdité. Dans les systèmes séquentiels, la cohérence sera toujours interprétée par la non-prouvabilité de ⊢. Dans la formulation qui suit du calcul des séquents LK, on utilise la virgule pour dénoter la mise bout à bout (concaténation) de suites, par exemple Γ, Λ ; on utilise Γ, A au lieu de Γ, {A}.
Théorie de la démonstration
Encyclopædia Universalis France
Les règles représentées dans le tableau ci-après sont divisées en quatre groupes ; mais elles sont d'importance inégale. En particulier, les règles structurelles sont de peu d'intérêt ; il convient cependant de ne pas mépriser l'importance des règles de contraction. Dans les groupes II et III, les règles sont divisées en droites et gauches : pour toutes ces règles (sauf l'échange), on a une « formule principale » : il s'agit de la formule écrite explicitement en conclusion ; sa localisation par rapport à ⊢ détermine le caractère gauche ou droit de la règle ; dans la règle de coupure, A est la formule de coupure.
Théorème de complétude. Le séquent Γ ⊢ Δ est vrai dans tout modèle de L si et seulement s'il est démontrable dans LK. En particulier, si on se restreint aux séquents de la forme ⊢ A, LK est équivalent au calcul des prédicats.
Théorème d'élimination des coupures ( Hauptsatz de Gentzen). Dans LK, la règle de coupure (C) est inutile, autrement dit tout théorème de LK est démontrable sans coupures.La démonstration de ce résultat, assez longue et délicate, consiste à remplacer toute coupure de formule principale A par de nombreuses coupures dont les formules de coupure sont des sous-formules (voir leur définition plus bas) strictes de A.
Donnons quelques exemples :
Le Hauptsatz a pour corollaire la propriété de la sous-formule. Par définition, une sous-formule de A est soit A elle-même, soit :
– dans le cas où A est ¬B, toute sous-formule de B,
– dans le cas où A est B ∨ C, B & C, B → C, toute sous-formule de B et/ou de C,
– dans le cas où A est ∀x B[x], ∃x B[x], toute sous-formule des formules B[t], t étant un terme quelconque.
Théorème. La « propriété de la sous-formule » s'exprime[...]
La suite de cet article est accessible aux abonnés
- Des contenus variés, complets et fiables
- Accessible sur tous les écrans
- Pas de publicité
Déjà abonné ? Se connecter
Écrit par
- Jean-Yves GIRARD : docteur ès sciences, maître de recherche au C.N.R.S.
Classification
Média
Théorie de la démonstration
Encyclopædia Universalis France
Autres références
-
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...
-
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...
-
HILBERT DAVID (1862-1943)
- Écrit par Rüdiger INHETVEEN , Jean-Michel KANTOR et Christian THIEL
- 14 726 mots
- 2 médias
...Hilbert s'est donné pour but de sauver la position classique de la mathématique et, en même temps, de forger de nouveaux outils permettant de donner une démonstration absolue de non-contradiction de l'arithmétique d'abord, puis de l'analyse. Il se proposa d'établir la non-contradiction absolue d'un système... -
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...
