Théorème d'élimination des coupures

En logique mathématique, le théorème d'élimination des coupures (ou Hauptsatz de Gentzen) est le résultat central établissant l'importance du calcul des séquents. Il a été initialement prouvé par Gerhard Gentzen en 1934 dans son article historique « Recherches sur la déduction logique » pour les systèmes LJ et LK formalisant la logique intuitionniste et classique, respectivement. Le théorème d'élimination des coupures stipule que toute déclaration qui possède une preuve dans le calcul des séquents, faisant usage de la règle de coupure, possède aussi une preuve sans coupure, à savoir, une preuve qui ne fait pas usage de la règle de coupure. règle de coupure Un séquent est une expression logique concernant plusieurs phrases, sous la forme , qui est lu prouve , et (comme déclaré par Gentzen) doit être compris comme équivalente à la proposition « Si ( et et ...) alors ( ou ou ...). » Notez que le côté gauche (CG) est une conjonction (et) et le côté droit (CD) est une disjonction (ou). Le CG peut avoir arbitrairement plus ou moins de formules; lorsque le CG est vide, le CD devient une tautologie. Dans LK, le CD peut aussi avoir un certain nombre de formules, s'il n'en a pas, le CG est une contradiction, alors que dans LJ, le CD ne peut avoir soit qu'une formule, soit aucune: nous voyons ici qu'avoir plus d'une formule du CD est équivalent, en présence de la règle de contraction droite, à l'admissibilité du principe du tiers exclu (car est alors prouvable). Depuis la logique LC de Jean-Yves Girard, il est facile d'obtenir une formalisation assez naturelle de la logique classique où le CD contient au plus une formule. La « coupure » est une règle du calcul des séquents, et est équivalente à une variété de règles d'autres théories de la démonstration, ce qui, étant donné et permet de déduire Autrement dit, il « coupe » les occurrences de la formule hors de la relation d'inférence. Le théorème d'élimination des coupures stipule que, pour un système donné, tout séquent prouvable en utilisant la règle de coupure peut être prouvé sans l'utilisation de cette règle.

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Concepts associés (18)

Cours associés (3)

Séances de cours associées (12)

Méthode des tableaux

vignette|200px|Représentation graphique d'un tableau propositionnel partiellement construit En théorie de la démonstration, les tableaux sémantiques sont une méthode de résolution du problème de la décision pour le calcul des propositions et les logiques apparentées, ainsi qu'une méthode de preuve pour la logique du premier ordre. La méthode des tableaux peut également déterminer la satisfiabilité des ensembles finis de formules de diverses logiques. C'est la méthode de preuve la plus populaire pour les logiques modales (Girle 2000).

Gentzen's consistency proof

Gentzen's consistency proof is a result of proof theory in mathematical logic, published by Gerhard Gentzen in 1936. It shows that the Peano axioms of first-order arithmetic do not contain a contradiction (i.e. are "consistent"), as long as a certain other system used in the proof does not contain any contradictions either. This other system, today called "primitive recursive arithmetic with the additional principle of quantifier-free transfinite induction up to the ordinal ε0", is neither weaker nor stronger than the system of Peano axioms.

Théorème d'élimination des coupures

Explore la preuve de la formule de caractère de Weyl pour les représentations tridimensionnelles des algèbres semi-simples de Lie.

Couvre les bases et les applications du calcul séquentiel en logique et théorie des preuves, y compris l'élimination des coupes et l'analyse des preuves pratiques.

Couvre le processus de formulation de programmes entiers et d'amélioration des solutions.

MATH-381: Mathematical logic

Branche des mathématiques en lien avec le fondement des mathématiques et l'informatique théorique. Le cours est centré sur la logique du 1er ordre et l'articulation entre syntaxe et sémantique.

CS-250: Algorithms

The students learn the theory and practice of basic concepts and techniques in algorithms. The course covers mathematical induction, techniques for analyzing algorithms, elementary data structures, ma

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u