Talk:Gentzen's consistency proof

From Wikipedia, the free encyclopedia

Contents 1 Origin 2 Further comments 3 About proof theory in general 4 Definition of ε0

[edit] 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)

[edit] 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)

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)

[edit] 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)

[edit] Definition of ε₀

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

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. α^ω > α 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 γ-th ordinal α such that ω^α = α is written . 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 α, such that α^ω = α". 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)