Timeline for Why is there a need for ordinal analysis?
Current License: CC BY-SA 4.0
23 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 18, 2022 at 5:43 | comment | added | Thomas Benjamin | @C7X: agreed. Will text you later on chat. | |
| Aug 18, 2022 at 3:20 | comment | added | C7X | @ThomasBenjamin Apologies for my unclear comment. I personally don't have a problem with believing PRA+TI($\varepsilon_0$) consistent, but in case some hypothetical reader does, $Con(PRA+TI(\varepsilon_0))$ can itself be justified by additional Gentzen-style reasoning. Additionally a "turtles all the way down" argument of "how do we know that theory is consistent?" can be justified by even more analysis with larger ordinals. I'm not an expert on MO's rules, so if we continue this discussion is it best to continue in chat? | |
| Aug 17, 2022 at 18:11 | comment | added | Thomas Benjamin | @AndreasBlass: And soundness of $PRA$ is that the axioms of $PRA$ are assumed to be true and that the rules of inference preserve truth, correct? | |
| Aug 17, 2022 at 18:00 | comment | added | Andreas Blass | @ThomasBenjamin What is $PRA'$? If it includes PRA, then PRA can't prove its soundness, or even its consistency, thanks to Gödel. | |
| Aug 17, 2022 at 17:48 | comment | added | Thomas Benjamin | (cont.)/? contacted me last night regarding the alternate view and I asked my question to get clarification regarding that. | |
| Aug 17, 2022 at 17:41 | comment | added | Thomas Benjamin | @AndreasBlass: True, but can $PRA's$ soundness be proven in (say) $PRA$? | |
| Aug 17, 2022 at 17:35 | comment | added | Andreas Blass | @ThomasBenjamin Though I haven't studied it in detail, the discussion at C7X's link seems to be entirely about what is or is not provable in some weak systems, whereas my comment is about what is known to be true (and provable in strong systems, like ZF). | |
| Aug 17, 2022 at 17:29 | comment | added | Thomas Benjamin | @AndreasBlass: That very well might be ( and probably is) true, but C7X (I think) believes otherwise and he/she | |
| Aug 17, 2022 at 16:37 | comment | added | Andreas Blass | @ThomasBenjamin Certainly PRA + TI($\varepsilon_0$) is consistent; its axioms are all true (in the standard natural numbers) and its rules of inference preserve truth. | |
| Aug 17, 2022 at 8:02 | comment | added | Thomas Benjamin | * $PRA$ + $TI$($\epsilon_{0}$) is consistent? | |
| Aug 17, 2022 at 7:55 | comment | added | Thomas Benjamin | @C7X: I see your point (I think). Is it essentially that ordinal analysis of necessity seems to need to presuppose the consistency of $PRA$ + TI($\omega_{1}^{CK}$) (or worse) in order to claim that $PRA$+$TI$$($\epsilon_{0}$)$ is consistent? | |
| Aug 16, 2022 at 22:46 | comment | added | C7X | @ThomasBenjamin If you're still interested in this thread, objecting to consistency of PRA+TI($\varepsilon_0$) may itself be argued by ordinal analysis, as in this relevant question: mathoverflow.net/questions/369254 | |
| S Jul 17, 2022 at 11:30 | history | suggested | C7X | CC BY-SA 4.0 |
PRA and PA have the and language, most salient difference is what operations they prove total. n is correct
|
| Jul 17, 2022 at 7:06 | review | Suggested edits | |||
| S Jul 17, 2022 at 11:30 | |||||
| Dec 4, 2015 at 12:13 | comment | added | Andreas Blass | I don't think Hilbert's school had what they'd consider a finitary proof of the consistency of PRA. By today's standards, "finitary" would mean "formalizable in PRA", and PRA can't prove its own consistency. As far as I know, Gentzen did not try to prove the consistency of PRA + induction for $\varepsilon_0$; rather he just used this theory to prove the consistency of PA. | |
| Dec 4, 2015 at 7:50 | comment | added | Thomas Benjamin | (cont.) of 'numbers'. (Note: the Hilbert quote I used can be found in van Heijenoort, pg. 383). What does this mean? Well,for me, at least, it means that Gentzen's proof of the consistency of $PA$ falls squarely within the letter and spirit of Hilbert's Program (though perhaps not as Hilbert wanted it, exactly....). | |
| Dec 4, 2015 at 7:45 | comment | added | Thomas Benjamin | (cont.) consistency; for, extension by the additions of ideals is legitimate by only if no contradiction is thereby brought about in the old, narrower domain [$PRA$--my comment], that is, if the relations that result for the old objects whenever the ideal objects are eliminated are valid in the old domain [relative consistency result?--my question and comment ] ." Note also that $PRA$ can be recast in terms of concatenation and operations and relations on the strings $e$ (the 'empty' string), |, ||, |||,.., etc., so one can dispense with questions regarding the 'existence' or 'nonexistence' | |
| Dec 4, 2015 at 7:10 | comment | added | Thomas Benjamin | @AndreasBlass: Just to get my facts straight: i) did the "Hilbert School" have what they deemed a 'finitary' proof of the consistency of $PRA$ before the Goedel and Gentzen results; ii) did Gentzen prove the consistency of $PRA$+"Induction principle for $\epsilon_{0}$"? If so then the following principle of Hilbert seems to be relevant (this from "On the Infinite"): "For there is a condition, a single but absolutely necessary one, to which the use of the method of ideal elements [in this case, the induction principle for $\epsilon_{0}$ --my comment] is subject, and that is the proof of | |
| Dec 3, 2015 at 15:55 | comment | added | Andreas Blass | Yes, from the viewpoint of most mathematicians, first-order Peano arithmetic is obviously consistent because all its axioms are true under the standard interpretation (natural numbers with the usual addition and multiplication). | |
| Dec 3, 2015 at 13:22 | comment | added | user3730940 | so to most mathematicians -- those without constructivist or finitist leanings -- gentzen's proof isn't necessary? | |
| Dec 3, 2015 at 13:16 | vote | accept | user3730940 | ||
| Dec 3, 2015 at 11:45 | comment | added | Emil Jeřábek | Very well explained. Definitely not $2n$; I don't remember exactly either, but it's $n$ or $n\pm1$. | |
| Dec 3, 2015 at 11:20 | history | answered | Andreas Blass | CC BY-SA 3.0 |