Demostració de consistència de Gentzen

La demostració de consistència de Gentzen de l'aritmètica de primer orde és un resultat pioner de la teoria de la demostració en llògica matemàtica publicat per Gerhard Gentzen en 1936. El resultat demostra que els Els axioma de Peano d'aritmètica de primer orde no contenen cap contradicció, és dir, són "consistents", sempre i quan un atre sistema utilisat en la pròpia demostració tampoc continga cap contradicció (és dir, es tracta d'una demostració de "consistència relativa"). Este atre sistema, hui cridat aritmètica recursiva primitiva, junt en el principi adicional d'inducció transfinita lliure de quantificadors fins al ordinal llímit ε₀", no és ni més fort ni més dèbil que el propi sistema de axioma de Peano. Gentzen va argumentar que la seua demostració evitava els modos qüestionables d'inferència continguts en l'aritmètica de Peano i que, per lo tant, la seua consistència és menys controvertida.

Teorema de Gentzen

La teorema de Gentzen s'ocupa de l'aritmètica de primer orde: la teoria dels número natural, incloent la seua suma i multiplicació, axiomatizada pels axioma de Peano de primer orde. Esta és una teoria de "primer orde": els quantificadorés s'estén sobre número natural, pero no sobre conjunts o funcions d'número natural. La teoria és lo suficientment forta com per a descriure funcions de sancers definides recursivamente com la exponenciación, els factorials o els números de Fibonacci.

Gentzen va demostrar que la consistència dels axioma de Peano de primer orde és demostrador a partir de l'aritmètica recursiva primitiva en el principi adicional d'inducció transfinita lliure de quantificador fins al ε₀. L'aritmètica recursiva primitiva és una forma molt simplificada d'aritmètica que és prou incontrovertida. El principi adicional significa, informalmente, que hi ha un ben ordenat en el conjunt d'arbres de raïls finitas. Formalment, ε₀ és el primer ordinal $\alpha$ tal que ${\omega }^{\alpha }=\alpha$, és dir, el llímit de la seqüència

És un ordinal numerable molt més chicotet que els ordinals numerables grans. Per a expressar ordinals en el llenguage de l'aritmètica, es necessita una notació ordinal, és dir, una forma d'assignar número natural a ordinals menors que ε₀. Açò es pot fer de vàries maneres, un eixemple proporcionat per teorema de la forma normal de Cantor. La demostració de Gentzen es basa en la següent suposició: per a qualsevol fòrmula lliure de quantificadors A(x) , si hi ha un ordinal a < ε₀ per al qual A(a) és fals, llavors hi ha un ordinal mínim en dita propietat.

Gentzen definix una noció de "procediment de reducció" per a les demostracions en l'aritmètica de Peano. Per a una demostració donada, tal procediment produïx un arbre de demostracions, en la donada servint com la raïl de l'arbre, i sent les atres demostracions "més simples" en cert sentit que la donada inicialment. Esta creixent simplicitat es formalisa adjuntant un < ordinal ε₀ a cada demostració, i mostrant que, a mida que un es mou cap a avall en l'arbre, estos ordinals es fan més menuts a cada pas. Després mostra que si hi haguera una demostració d'una contradicció, el procediment de reducció resultaria en una seqüència infinita estrictament descendent d'ordinals menors que ε₀ produïda per una operació recursiva primitiva sobre proves corresponents a una fòrmula lliure de quantificadors.

Relació en el programa de Hilbert i la teorema de Gödel

La demostració de Gentzen resalta un aspecte comunament passat per alt del segona teorema de incompletitud de Gödel. A voltes s'afirma que la consistència d'una teoria matemàtica només pot ser demostrada en una teoria més forta. No obstant, la teoria de Gentzen obtinguda agregant inducció transfinita sense quantificadors a l'aritmètica recursiva primitiva demostra la consistència de l'aritmètica de Peano de primer orde (PA), pero no conté a PA. Per eixemple, no demostra l'inducció matemàtica ordinària per a totes les fòrmules, mentres que PA sí ho fa (ya que totes les instàncies d'inducció són axioma de PA). No obstant, la teoria de Gentzen tampoc està continguda en PA, ya que pot provar un fet teòric numèric, la consistència de PA, que PA no pot. Per lo tant, les dos teories són, en cert sentit, incomparables.

Dit açò, hi ha atres formes més precises de comparar la força de les teories, la més important de les quals es definix en térmens de la noció d'interpretabilidad. Es pot demostrar que, si una teoria T és interpretable en una atra B, llavors T és consistent si B ho és. (De fet, est és un gran punt de la noció de interpretabilidad). I, suponent que T no és extremadament dèbil, T mateixa serà capaç de demostrar açò condicionalmente: Si B és consistent, llavors també ho és T. Per lo tant, T no pot provar que B és consistent, per la segona teorema de incompletitud, mentres que B be pot ser capaç de provar que T és consistent. Açò és lo que motiva l'idea d'usar la interpretabilidad per a comparar teories, és dir, el pensament de que, si B interpreta T, llavors B és a lo manco tan forta (en el sentit de "força de consistència") com T.

Una forma forta de la segona teorema de incompletitud, demostrat per Pavel Pudlák, que es basava en el treball anterior de Solomon Feferman, afirma que cap teoria consistent T que continga aritmètica de Robinson, Q, pot interpretar Q més que En(T), l'afirmació de que T és consistent. Pel contrari, Q+En(T) interpreta T, per una forma forta del [[teorema de completitud de Gödel|teorema de completitud]. Aixina que Q+En(T) és sempre més llògicament forta que T. Pero la teoria de Gentzen interpreta trivialmente Q+En(PA), ya que conté Q i demostra En(PA), i aixina la teoria de Gentzen interpreta PA. Pero, segons el resultat de Pudlák, PA "no pot" interpretar la teoria de Gentzen, ya que la teoria de Gentzen, com s'acaba de dir, interpreta Q + En (PA), i la interpretabilidad és transitiva. És dir: si PA interpretara la teoria de Gentzen, llavors també interpretaria Q+En(PA) i per lo tant seria inconsistente, segons el resultat de Pudlák. Llavors, en el sentit de força de consistència, caracterisada per la interpretabilidad, la teoria de Gentzen seria més forta que l'aritmètica de Peano.

Hermann Weyl va fer el següent comentari en 1946 sobre l'importància del resultat de consistència de Gentzen, despuix de l'impacte devastador del resultat incompletitud de Gödel de 1931 en el pla de Hilbert per a provar la consistència de les matemàtiques.

És provable que tots els matemàtics hagueren acceptat finalment l'enfocament de Hilbert si haguera segut capaç de portar-ho a terme en èxit. Els primers passos varen ser inspiradores i prometedors. Pero després Gödel li va assestar un colp terrible (1931), del que encara no s'ha recuperat. Gödel va enumerar els símbols, fòrmules i seqüències de fòrmules en el formalisme de Hilbert de certa manera, i aixina va transformar l'afirmació de consistència en una proposició aritmètica. Va poder demostrar que esta proposició no pot ser provada ni refutada dins del formalisme. Açò pot significar només dos coses: o be el raonament pel qual es dona una demostració de consistència deu contindre algun argument que no tinga contrapartida formal dins del sistema, és dir, no hem conseguit formalisar completament el procediment d'inducció matemàtica; o l'esperança d'una demostració estrictament "finitista" de consistència deu ser abandonada per complet. Quan G. Gentzen finalment va conseguir provar la consistència de l'aritmètica, va traspassar eixos llímits en afirmar com a evident un tipo de raonament que penetra en la "segona classe de números ordinals" de Cantor.

Kleene (2009, p. 479) va fer el següent comentari en 1952 sobre l'importància del resultat de Gentzen, particularment en el context del programa formaliste iniciat per Hilbert.

Les propostes originals dels formalistes per a assegurar les matemàtiques clàssiques per mig d'una demostració de consistència no contemplaven que un método com l'inducció transfinita fins a ε₀ tindria que ser utilisat. Fins a quin punt la demostració de Gentzen pot ser acceptada com a assegurament de la teoria clàssica de números en el sentit de que la formulació del problema és, en l'estat actual de les coses, un assunt per al juí individual, depenent de cuán llest estiga un per a acceptar l'inducció fins a ε₀ com un método finitario.

En contrast, Bernays (1967) va comentar si el confinament de Hilbert a métodos finitarios era massa restrictiu:

Per lo tant, es va fer evident que el "Standpunkt finito" no és l'única alternativa a les formes clàssiques de raonament i no està necessàriament implícit en l'idea de la teoria de la demostració. Per lo tant, es va sugerir una ampliació dels métodos de la teoria de la demostració: en lloc d'una reducció a métodos finitistas de raonament, solament es requeria que els arguments anaren de caràcter constructiu, lo que nos permetera tractar en formes més generals d'inferència.

Atres demostracions de consistència aritmètica

La primera versió de Gentzen de la seua demostració de consistència no es va publicar durant la seua vida perque Paul Bernays s'havia opost a un método utilisat implícitament en la demostració. La demostració modificada, descrita anteriorment, va ser publicada en 1936 en els Anals de Matemàtiques| Anals]]. Gentzen va publicar dos demostracions de consistència adicionals, una en 1938 i una atra en 1943. Tots estos estan continguts en Plantilla:Harv.

Kurt Gödel va reinterpretar la demostració de Gentzen de 1936 en una conferència en 1938 en lo que es va conéixer com l'interpretació sense contraeixemple. Tant la demostració original com la reformulación poden entendre's en térmens de teoria de jocs.Plantilla:Harv.

En 1940 Wilhelm Ackermann va publicar una atra demostració de consistència per a l'aritmètica de Peano, també usant l'ordinal ε₀.

Una atra demostració de consistència de l'aritmètica va ser publicada per I. N. Khlodovskii, en 1959.

No obstant, atres demostracions de consistència de l'aritmètica varen ser publicades per: T. J. Stępeuń i Ł. T. Stępeuń (en 2018) i per S. Artemov (en 2019). En l'artícul de Stępeuńs s'ha afirmat que la demostració de consistència (publicada allí), del Sistema Aritmètic, es realisa dins d'este Sistema.

En l'artícul de Artemov s'ha afirmat que la demostració publicada allí és formalisable en l'aritmètica de Peano.

Referències

Bibliografia

• Plantilla:Cite arXiv
• (1936).«Die Widerspruchsfreiheit der regnen Zahlentheorie».Mathematische Annalen.112

493–565.doi:10.1007/BF01565428. – Translated as "The consistency of arithmetic", in Plantilla:Harv.

• (1938).«Neue Fassung dones Widerspruchsfreiheitsbeweises für die regne Zahlentheorie».Forschungen zur Logik und zur Grundlegung der Exakten Wissenschaften.4

19–44. – Translated as "New version of the consistency proof for elementary number theory", in Plantilla:Harv.

• (1969).«Collected Papers of Gerhard Gentzen».North-Holland.Amsterdam: - an English translation of papers.
• (2001).«Kurt Gödel: Collected Works».Oxford University Press Inc..III Unpublished Essays and Lectures

87–113.

• (1999).«A course in proof theory».
• (1959).«A new proof of the consistency of arithmetic».Uspekhi Mat. Nauk.14(6(90))

105–140.

• (1982).«Accessible independence results for Peano arithmetic».Bull. London Math. Soc..14(4)

285–293.doi:10.1112/blms/14.4.285.

• (2009) Introduction to metamathematics, Ishi Press International. ISBN 978-0-923891-57-2.
• Plantilla:Cite arXiv
• (2005).«Gödel's reformulation of Gentzen's first consistency proof for arithmetic: the no-counterexample interpretation».The Bulletin of Symbolic Logic.11(2)

225–238.ISSN 1079-8986.doi:10.2178/bsl/1120231632.

• (2012) Levels of infinity: Selected writings on mathematics and philosophy, New York: Dover Publications. ISBN 978-0-486-48903-2.