Talk:Gentzen's consistency proof

Origin

The text used to start this article was cut from Gödel's incompleteness theorem and pasted here. --Trovatore 04:32, 15 February 2006 (UTC)

Trovatore: thanks for the tip. You are of course right about how we should discuss strength of theories (ie. consistency strength, not theory inclusion, is the more natural notion). IIRC, Gentzen's discussion about his base theory was entirely informal: Goedel later considered the formalisation - having said that it's been a long time since I looked at the original paper. Bill Tait has a decent discussion [1], which covers the question of how to formalise in PRA. --- Charles Stewart^(talk) 16:25, 15 February 2006 (UTC)

Further comments

Some points I didn't comment on above; Trovatore wrote to me:

The exposition needs a lot of work of course, but I'd also like to point your attention to the penultimate paragraph, which I think is misleading. If we denote by T the theory indicated (PRA+transfinite induction; not sure how you formalize that exactly), then perhaps T doesn't prove all the theorems of PA, but that doesn't mean it isn't stronger in the relevant sense, which is consistency strength.

Well, it's obviously true that PRA+Ti^Qf(<) where < is some canonical primitive recursive well-ordering of type epsilon-0, has greater consistency strength than PA, and proves in particular all Pi₁ sentences PA proves. The comment about incomparable strengths was originally made in context of the Gödel's theorems article, in which it is used simply as an illustration of the fact that in order for T' to prove the consistency of T, T' needs to be merely different than T, not necessarily stronger. Usually when this claim is made, strength is understood in the sense that T' is stronger than T if everything provable in T' is provable in T, but not vice versa. I fail to see why consistency strength would be the "relevant sense" here. Aatu 09:55, 16 February 2006 (UTC)

It's the relevant sense in that it fits with the global picture, extending up into large cardinals, that "if you want more you need to assume more" (as Dana Scott puts it in the intro to Bell's book on Boolean-valued models). Stronger theories are the ones with more non-logical content, the ones that provide more opportunities to refute them. This is the ordering according to which large cardinal axioms are observed to be linearly ordered (in the sense that there is no known counterexample). The wellfoundedness of ε₀ can be seen as a very small large-cardinal axiom. --Trovatore 01:11, 17 February 2006 (UTC)

I agree in general, but to go off on a tangent: the large cardinals aren't "observed" to be linearly ordered - most set theorists believe they are, but the realative strength of some LCAs is not established. --- Charles Stewart^(talk) 15:42, 17 February 2006 (UTC)

"Observed", as I said, in the sense that no counterexample is known. No one has shown two LCAs to be of incomparable consistency strength. (It's known where most of them fit; there are a few strange cases like supercompact/strongly compact, which could turn out to be equiconsistent, and then I think some of the ones at list of large cardinal properties listed as unknon probably are known; it's just that none of us working on the article know.) --Trovatore 16:14, 17 February 2006 (UTC)

Actually, for some of the last, it's more a problem of article organization. The &lamba;-extendibles and η-supercompacts interleave, and I could look up the relevant relationship between λ and η to make them interleave, but it's awkward to fit into the current list format. --Trovatore 16:18, 17 February 2006 (UTC)

"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."

Could someone please explain how transfinite induction is not stronger than ordinary mathematical induction? I would have thought the latter could be derived as a consequence of the first. DAVilla (talk) 03:50, 24 August 2015 (UTC)

I think the following should be true: T proves all Π⁰₁ facts that PA does, and some that it doesn't, and IΔ₀ proves Con(T)→Con(PA), but does not prove Con(PA)→Con(T). Do you agree with that? I think all we need for the usual arguments to go through is that, for any Σ⁰₁ sentence σ, IΔ₀ proves "σ → PA proves σ", which I think should be true. --Trovatore 06:28, 15 February 2006 (UTC)

PRA is corresponds to a stronger fragment of arithmetic, with sigma-0-1 induction. (Charles Parsons proved in 1971 that the functions of PRA are the same as those functions provably total in PA only using this induction scheme).

Let's call S PA with induction restricted to sigma-0-1 fmlae, and T=S+wf(epsilon-0): it's easier to work with T in the language of PA, then one doesn't need to worry about Herbrandising formulae: but maybe we want to stick to a PRA-like formulation to get more striking theorems? We really want to have the same definable functions in the two systems: we'd like T to prove the same Pi-0-2 formulae. I'm guessing next you want is S proves "con(T) implies con(PA)" but not the converse. --- Charles Stewart^(talk) 19:26, 15 February 2006 (UTC)

About proof theory in general

I don't know how helpful it is to concentrate on Gentzen's result in isolation. Wouldn't it be better to explain such things as ordinal notation systems, cut elimination, infinitary proofs, subsystems of PA, subsystems of Z_2 and so forth, and then present Gentzen's result as just one of the ordinal analyses, providing whatever historical details are deemed necessary? For example, I doubt that there is any need to explain Gentzen's original proof, which was not presented in terms of epsilon-0 at all, but it might be in order to mention it. All this explicit talk about PRA, quantifier free induction and what not is, as far as I recall, due to Kreisel. Aatu 09:55, 16 February 2006 (UTC)

Proof theory is not my field, but I'd think just for its historical importance, Gentzen's result should have its own article (not necessarily with a complete proof, of course). There's no reason the article couldn't include later reinterpretations of the proof; these could even be presented as primary, with just a little gloss about the original technique (certainly the analogous thing is done for forcing; actually I don't think ramified forcing is even mentioned in any of our articles, possibly because no one knows it and it's hard to find writeups).

For the more general discussion of structural proof theory, maybe the skeletal article structural proof theory could be expanded, with sections pointing via {{main article}} templates to the other topics you mention. (There's already one for cut-elimination theorem.) --Trovatore 15:00, 16 February 2006 (UTC)

It maybe easier to start an article on ordinal analysis (a redlink of proof theory), and farm out this article when there is enough coverage, though I'm inclined to grow the two side by side. I certainly think the result deserves an independent article: it's one of the results one hears most often among logician's drunken shortlists of most important results in mathematical logic.

I agree with Trovatore that the article need not be narrowly concerned with exactly the formulations in the two original papers, but may also take in reformulations of the idea - though it should be clear about which is which! --- Charles Stewart^(talk) 21:31, 16 February 2006 (UTC)

Definition of ε₀

Most other articles define ε₀ as the least ordinal $\alpha$ such that $\omega ^{\alpha }=\alpha$, not such that $\alpha ^{\omega }=\alpha$. Are these two definitions equivalent? If we use the definition of ε₀ at ordinal number, then isn't it true that:

${\varepsilon _{0}}^{\omega }=(\omega ^{\varepsilon _{0}})^{\omega }=\omega ^{\varepsilon _{0}\omega }=\omega ^{(\omega ^{\varepsilon _{0}})\omega }=\omega ^{\omega ^{\varepsilon _{0}+1}}>\omega ^{\omega ^{\varepsilon _{0}}}=\varepsilon _{0}$

I don't really know anything about ordinals, I'm just using the rules at ordinal arithmetic, so I might have made a mistake. Can anyone verify this? BrentG 19:01, 17 August 2006 (UTC)

Those expressions are not equivalent. $\alpha ^{\omega }>\alpha$ holds for all ordinals α except 0 and 1. However, I am not aware of anything to the contrary at ordinal number. Please name the section or subsection and paragraph number where you saw it. I do see "... the $\gamma$-th ordinal $\alpha$ such that $\omega ^{\alpha }=\alpha$ is written $\varepsilon _{\gamma }$. These are called the 'epsilon numbers'." which is correct. JRSpriggs 03:36, 18 August 2006 (UTC)

Nothing at ordinal number contradicts that. It's this article (Gentzen's consistency proof) that says "ε₀ is the first ordinal $\alpha$, such that $\alpha ^{\omega }=\alpha$". I figured it was a mistake, but I didn't want to edit a technical detail on a subject I don't know that much about without getting someone else's opinion. I'll switch it to the correct definition. BrentG 06:15, 19 August 2006 (UTC)

Sorry that I misunderstood you. I looked at this article, but I guess that I just saw what I expected to see. Especially since the line below it with the sequence of powers of omega looked OK. Thanks for fixing this article. JRSpriggs 08:09, 19 August 2006 (UTC)

I have erased the sentence which said "In itself, the result is rather trivial, since the consistency of first-order arithmetic has a very easy proof: the axioms are true—in a mathematically defined sense—the rules of predicate calculus preserve truth and no contradiction is true, hence no contradiction follows from the axioms of first-order arithmetic." The part about the "very easy proof" is correct but I don't believe that it follows from that that Gentzen's result in itself is trivial. The "very easy proof" has to be carried out in set theory as far as I know and it's possible that set theory is inconsistent. 81.106.197.184 (talk) 02:58, 23 August 2008 (UTC)

The proof is not "very easy" but it is not carried out in set theory, it's carried out in a very weak fragment of second-order arithmetic. 66.127.55.192 (talk) 07:22, 10 February 2010 (UTC)

Primitive Recursive Arithmetic

In what sense is the proof based on Primitive Recursive Arithmetic? Gentzen's original papers prove the consistency of Peano Arithmetic (albeit using the axioms of PRA in the 1938 version). The proofs are completely unformalized and Gentzen does not say anything specific about formalization. Maybe it would be more appropriate to say that "Gentzen's proof can be carried out in" PRA+TI(epsilon0)?--141.70.13.27 (talk) 11:28, 6 January 2012 (UTC)

External links modified

Hello fellow Wikipedians,

I have just modified one external link on Gentzen's consistency proof. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://web.archive.org/web/20110607104500/http://folk.uio.no/herman/bevisteori.ps to http://folk.uio.no/herman/bevisteori.ps

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 18 January 2022).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 09:18, 9 January 2017 (UTC)

UNDUE growth of sections of this article

Little of this article is actually about Gentzen's proof. The additional content is mostly useful but some rebalancing of the article needs to be done.

I'll note the existence of a recent survey of work on the theory of consistency that could be useful in this task: Yong Cheng (2021) Current research on ON Gödel’s incompleteness theorems, which in particular has an interesting discussion of the recently added article of Artemov on p40.