https://en.formulasearchengine.com/api.php?action=feedcontributions&feedformat=atom&user=65.255.37.171formulasearchengine - User contributions [en]2026-04-14T11:55:52ZUser contributionsMediaWiki 1.43.0-wmf.28https://en.formulasearchengine.com/index.php?title=Criterion-referenced_test&diff=12875Criterion-referenced test2013-12-22T14:39:36Z<p>65.255.37.171: /* Comparison of criterion-referenced and norm-referenced tests */</p>
<hr />
<div>{{Expert-subject|Mathematics|date=November 2008}}<br />
<br />
'''Gentzen's consistency proof''' is a result of [[proof theory]] in [[mathematical logic]]. It "reduces" the consistency of a simplified part of mathematics, not to something that could be proved in that same simplified part of mathematics (which would contradict the basic results of [[Kurt Gödel]]), but rather to a simpler logical principle.<br />
<br />
==Gentzen's theorem==<br />
In 1936 [[Gerhard Gentzen]] proved the consistency of [[first-order arithmetic]] using combinatorial methods. Gentzen's proof shows much more than merely that first-order arithmetic is [[consistent]]. Gentzen showed that the consistency of first-order arithmetic is provable, over the base theory of [[primitive recursive arithmetic]] with the additional principle of quantifier-free [[transfinite induction]] up to the [[ordinal number|ordinal]] [[epsilon zero|ε<sub>0</sub>]]. Informally, this additional principle means that there is a [[well-ordering]] on the set of finite rooted [[tree (mathematics)|tree]]s.<br />
<br />
The principle of quantifier-free transfinite induction up to ε<sub>0</sub> says that for any formula A(x) with no bound variables transfinite induction up to ε<sub>0</sub> holds. ε<sub>0</sub> is the first ordinal <math>\alpha</math>, such that <math>\omega^\alpha = \alpha</math>, i.e. the limit of the sequence:<br />
:<math>\omega,\ \omega^\omega,\ \omega^{\omega^\omega},\ \ldots</math><br />
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 ε<sub>0</sub>. This can be done in various ways, one example provided by Cantor's normal form theorem. That transfinite induction holds for a formula A(x) means that A does not define an infinite descending sequence of ordinals smaller than ε<sub>0</sub> (in which case ε<sub>0</sub> would not be well-ordered). Gentzen assigned ordinals smaller than ε<sub>0</sub> to proofs in first-order arithmetic and showed that if there is a proof of contradiction, then there is an infinite descending sequence of ordinals < ε<sub>0</sub> produced by a [[primitive recursive]] operation on proofs corresponding to a quantifier-free formula.<br />
<br />
==Relation to Gödel's theorem==<br />
Gentzen's proof also highlights one commonly missed aspect of [[Gödel's second incompleteness theorem]]. It is sometimes claimed that the consistency of a theory can only be proved in a stronger theory. The theory obtained by adding quantifier-free transfinite induction to primitive recursive arithmetic proves the consistency of first-order arithmetic but is not stronger than first-order arithmetic. For example, it does not prove ordinary mathematical induction for all formulae, while first-order arithmetic does (it has this as an axiom schema). The resulting theory is not weaker than first-order arithmetic either, since it can prove a number-theoretical fact - the consistency of first-order arithmetic - that first-order arithmetic cannot. The two theories are simply incomparable.<br />
<br />
Gentzen's proof is the first example of what is called proof-theoretical [[ordinal analysis]]. In ordinal analysis one gauges the strength of theories by measuring how large the (constructive) ordinals are that can be proven to be well-ordered, or equivalently for how large a (constructive) ordinal can transfinite induction be proven. A constructive ordinal is the order type of a [[recursive set|recursive]] well-ordering of natural numbers.<br />
<br />
[[Laurence Kirby]] and [[Jeff Paris]] proved in 1982 that [[Goodstein's theorem]] cannot be proven in Peano arithmetic based on Gentzen's theorem.<br />
<br />
==References==<br />
*{{Citation|last1=Gentzen|doi=10.1007/BF01565428|first1=Gerhard|author-link=Gerhard Gentzen|title=Die Widerspruchsfreiheit der reinen Zahlentheorie|journal=Mathematische Annalen|volume=112|year=1936|publisher=|pages=493–565|url=http://gdz.sub.uni-goettingen.de/dms/resolveppn/?PPN=GDZPPN002278391}} - Translated as 'The consistency of arithmetic', in {{Harv|Gentzen|Szabo|1969}}.<br />
*{{Citation|last1=Gentzen|first1=Gerhard|author-link=Gerhard Gentzen|title=Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie|journal=Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften|volume=4|year=1938|publisher=|pages=19–44}} - Translated as 'New version of the consistency proof for elementary number theory', in {{Harv|Gentzen|Szabo|1969}}.<br />
*{{Citation|last=Gentzen|first=Gerhard|editor-last=M. E.|editor-first=Szabo|editor-link=M. E. Szabo|year=1969|title=Collected Papers of Gerhard Gentzen|publisher=North-Holland|location=Amsterdam|edition=Hardcover|series=Studies in logic and the foundations of mathematics|isbn=0-7204-2254-X|ref={{Harvid|Gentzen|Szabo|1969}}}} - an English translation of papers.<br />
*{{Citation|last=Gödel|first=K.|author-link=Kurt Gödel|editor1-last=Feferman|editor1-first=Solomon|editor1-link=Solomon Feferman|origyear=1938|year=2001|title=Kurt Gödel: Collected Works|chapter=Lecture at Zilsel’s|publisher=Oxford University Press Inc.|pages=87–113|edition=Paperback|volume=vol.III Unpublished Essays and Lectures|isbn=0-19-514722-7|ref={{Harvid|Gödel|Feferman et al.|2001}}}}<br />
*{{Citation|last=Jervell|first=Herman Ruge|author-link=Herman Ruge Jervell|year=1999|title=A course in proof theory|edition=textbook draft|url=http://folk.uio.no/herman/bevisteori.ps}}<br />
*{{Citation|last1=Kirby|first1=L.|author1-link=Laurie Kirby|last2=Paris|first2=J.|author2-link=Jeff Paris|year=1982|title=Accessible independence results for Peano arithmetic|journal=[[Bull. London Math. Soc.]]|publisher=[[London Mathematical Society|LMS]]|pages=285–293|volume=14|url=http://blms.oxfordjournals.org/content/14/4/285.full.pdf|format=PDF}}<br />
*{{Citation|last=Tait|first=W. W.|author-link=William W. Tait|year=2005|title=Gödel's reformulation of Gentzen's first consistency proof for arithmetic: the no-counterexample interpretation|journal=The Bulletin of Symbolic Logic|volume=11|issue=2|publisher=[[Association for Symbolic Logic|ASL]]|pages=225–238|url=http://home.uchicago.edu/~wwtx/GoedelandNCInew1.pdf|format=PDF|issn=1079-8986}}<br />
<br />
[[Category:Metatheorems]]<br />
[[Category:Proof theory]]</div>65.255.37.171