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. Gentzen argued that it avoids the questionable modes of inference contained in Peano arithmetic and that its consistency is therefore less controversial. Gentzen's theorem is concerned with first-order arithmetic: the theory of the natural numbers, including their addition and multiplication, axiomatized by the first-order Peano axioms. This is a "first-order" theory: the quantifiers extend over natural numbers, but not over sets or functions of natural numbers. The theory is strong enough to describe recursively defined integer functions such as exponentiation, factorials or the Fibonacci sequence. Gentzen showed that the consistency of the first-order Peano axioms is provable over the base theory of primitive recursive arithmetic with the additional principle of quantifier-free transfinite induction up to the ordinal ε0. Primitive recursive arithmetic is a much simplified form of arithmetic that is rather uncontroversial. The additional principle means, informally, that there is a well-ordering on the set of finite rooted trees. Formally, ε0 is the first ordinal such that , i.e. the limit of the sequence It is a countable ordinal much smaller than large countable ordinals. To express ordinals in the language of arithmetic, an ordinal notation is needed, i.e. a way to assign natural numbers to ordinals less than ε0. This can be done in various ways, one example provided by Cantor's normal form theorem.

À 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 (24)

Cours associés (2)

Séances de cours associées (20)

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.

Gentzen's consistency proof

Ordinal analysis

In proof theory, ordinal analysis assigns ordinals (often large countable ordinals) to mathematical theories as a measure of their strength. If theories have the same proof-theoretic ordinal they are often equiconsistent, and if one theory has a larger proof-theoretic ordinal than another it can often prove the consistency of the second theory. The field of ordinal analysis was formed when Gerhard Gentzen in 1934 used cut elimination to prove, in modern terms, that the proof-theoretic ordinal of Peano arithmetic is ε0.

Discrete mathematics is a discipline with applications to almost all areas of study. It provides a set of indispensable tools to computer science in particular. This course reviews (familiar) topics a

This course is intended to give a brief overview of how to prove consistency results in nonparametric regression. In particular, we will focus on least-square regression estimators. Some connections t

Bases de données HTAP : innovations et défis

Discuter des innovations et des défis dans les bases de données HTAP, en mettant l'accent sur les conceptions adaptatives du PLO et sur le concept de système d'exploitation de la base de données.

Cohérence événementielle : principes de la programmation réactive

Explore la cohérence éventuelle des systèmes distribués, en soulignant l'importance de structures de données appropriées comme les CRDT.

Bosons de Goldstone : Mécanisme de Higgs

Explore les bosons de Goldstone et le mécanisme de Higgs, révélant comment la brisure spontanée de symétrie génère une masse pour les bosons de jauge.