Timeline for Why do stacked quantifiers in PA correspond to ordinals up to $\epsilon_0$?
Current License: CC BY-SA 3.0
24 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 8, 2021 at 7:33 | comment | added | user21820 | Hi! Do you think the stopping time sequence for the Collatz iteration grows no faster than $f_k$ for some $k < ε_0$? I feel it ought to be so, but am curious to know what logicians believe. In particular, if it is not so but the Collatz conjecture is true, then PA will not be able to prove the conjecture. I just can't believe such a simple definition can be that fast-growing... Thanks for any insight you may have! =) | |
| Aug 21, 2013 at 2:47 | history | bounty ended | Qiaochu Yuan | ||
| Aug 21, 2013 at 2:42 | history | edited | Henry Towsner | CC BY-SA 3.0 |
added 221 characters in body
|
| Aug 21, 2013 at 0:54 | vote | accept | Eliezer Yudkowsky | ||
| Aug 21, 2013 at 0:54 | comment | added | Eliezer Yudkowsky | I expect I'll need to work through this for a while before I properly understand, but it is extremely hope-inducing. Answer accepted. | |
| Aug 21, 2013 at 0:16 | comment | added | Henry Towsner | @EliezerYudkowsky: Since it might be helpful to others as well (and there are far too few worked examples of cut-elimination), I've written up an attempt at a fairly mild case of the Ackermann function at sas.upenn.edu/~htowsner/AckermannCutElimination.pdf | |
| Aug 20, 2013 at 19:38 | comment | added | Eliezer Yudkowsky | And if we can use some actual particular function like "$\phi(n)$ = Ackermann(n) which is in $\Sigma_2$"(?) that might also be very helpful. | |
| Aug 20, 2013 at 19:31 | comment | added | Eliezer Yudkowsky | A single concrete example at the $\Pi_2$ level might be really helpful here. How would we eliminate a cut and introduce new cuts and go from, say, $\omega^3$ to $6\omega^2$? Though maybe I should be asking about $\Pi_3$ and $\omega^{\omega^2}$ to e.g. $\omega^{2\omega + 3}$ in case the answer to the former is just "repeat 6 copies of the induction-step proof to get to $SSSSSS0$". | |
| Aug 20, 2013 at 15:06 | comment | added | Henry Towsner | In other words, in the finitary version, we put in a finite number of new cuts, but we can't fix in advance how many, and we don't do them all at once. (That's what all the messy bookkeeping in Gentzen's version is keeping track of.) We put in some new copies, get some constructive information (values of $y$ corresponding to values of $x$), and this tells us how many copies to create in the next round. | |
| Aug 20, 2013 at 15:04 | comment | added | Henry Towsner | @EliezerYudkowsky: In the finitary version: we have the same $\Pi_2$ cut we've been discussing, and it's positioned with height $\alpha$ in the proof. When we carry out one step of elimination, we get a copy of the proof of $\exists y\phi(n)$ for some $n$ and we might get new versions of the original cut at positions with $\alpha'<\alpha$. The proof of $\exists y\phi(n)$ involves some value $y(n)$. Later, when we eliminate another copy of that cut, the value of $x$ might involve $y(n)$ (thus, iteration). But how many times we do this is finite because the ordinals keep decreasing. | |
| Aug 20, 2013 at 5:18 | comment | added | Eliezer Yudkowsky | ...I'm sorry and this is probably my fault, but I still can't see how in the non-infinitary version, this turns short finite proofs into huge finite proofs. To be clear, my difficulty is that to turn short finite proofs into huge finite proofs, we should be putting in a finite number of new cuts. I can only see how this works with infinite copies of the proof, not with some finite number of copies. | |
| Aug 18, 2013 at 18:08 | comment | added | Eliezer Yudkowsky | let us continue this discussion in chat | |
| Aug 18, 2013 at 14:15 | comment | added | Henry Towsner | This is an important point I wasn't that clear about above: iteration here means making separate copies. We're making multiple copies of a well-founded tree and placing them inside the second proof which is also a well-founded tree; the most complicated configuration of copies of the first proof we could get is basically a tree of copies with the same height as the second proof. Each time we iterate the first proof, we end up moving from one copy to a new copy closer to the axioms of the second proof. | |
| Aug 18, 2013 at 14:06 | comment | added | Henry Towsner | Your other two questions are about the same issue. We're taking copies of the first proof and "pasting" them inside the second proof. The back-and-forth/iteration happen when we place multiple copies of the first proof inside the second proof in places where they will later be cut together themselves; for instance, when I say we get a value of y from the first proof and then use it to compute a new candidate for x, that means that at some stage of cut-elimination, we ended up with a (lower rank) cut with (portions of) different copies of the first proof above each side. | |
| Aug 18, 2013 at 13:58 | comment | added | Henry Towsner | @EliezerYudkowsky: 1) Ordinals are assigned to proofs, not to formulas. In the infinitary version, $\exists$ introduction only adds one to the ordinal. 2) Given a proof of False in PA, it embeds as a proof of False in the "infinitary" system, and cut-elimination gives a cut-free "infinitary" proof of False. But False has no universal quantifiers and the proof is cut-free, so there are universal quantifiers anywhere in the proof, so the proof couldn't have used the computable branching rule, so the resulting proof of False is actually a conventional cut-free proof. | |
| Aug 18, 2013 at 4:12 | comment | added | Eliezer Yudkowsky | Similarly, in your last paragraph, I don't understand how the second proof is iterating the first proof at some particular rate (vs. forever). Maybe if I understood this, I'd understand how adding more quantifiers climbs past $\omega^\omega$. | |
| Aug 18, 2013 at 4:08 | comment | added | Eliezer Yudkowsky | I probably also don't really understand the idea of back-and-forth. Where does the back-and-forth terminate and leave us with a copy of $(\psi \vee \psi')$? Or we had a proof that originally produced $\psi \vee \psi'$ via cut, but now we're eliminating the cut, and this produces a new proof which... I can't currently visualize. | |
| Aug 18, 2013 at 4:00 | comment | added | Eliezer Yudkowsky | "The infinitary proof takes the perspective that a proof of ∀xϕ(x) should be a computable function f so that, for each n, f(n) is a proof of ϕ(n)." I haven't heard about this perspective before - it sounds ultimately finitary which is very good. Two questions are, (1) what does it mean to assign an ordinal to $\exists x\phi(x)$ and (2) how does this relate to cut-elimination as used to prove PA's consistency? I.e. how would we use this to prove that if there was a short proof of False, there must be a much longer proof of False with the equivalent of no cuts? | |
| Aug 15, 2013 at 7:25 | comment | added | Qiaochu Yuan | @Steven: you can think of a set as a one-player game where the player chooses an element of the set, which determines the set of next possible moves. In particular von Neumann ordinals are such sets. | |
| Aug 14, 2013 at 21:26 | comment | added | Steven Stadnicki | The whole notion of '$\omega$ stands for choosing some finite number' reminds me a lot of the definition of numbers in combinatorial game theory; I wonder if there's a better intuition based around there somewhere. | |
| Aug 14, 2013 at 18:03 | comment | added | David E Speyer | The following link may require a login for some people, but, for those for whom it works, Chapter 1 (the relevant one) of Pohler's book is at link.springer.com/content/pdf/10.1007%2F978-3-540-46825-7_2.pdf | |
| Aug 14, 2013 at 13:19 | history | edited | Henry Towsner | CC BY-SA 3.0 |
added 3231 characters in body
|
| Aug 14, 2013 at 4:13 | comment | added | Eliezer Yudkowsky | I confess that I am more fond of finitary proofs than infinitary ones, and I usually think of $\omega$ as standing for "any finite number". However, leaving that aside, I can't yet see why 'going back and forth' along this two-sequent cut should yield some fast-growing process on the order of $\omega^{\omega^\alpha}$ rather than $\omega^2$. As I understand it, the size of these proofs should be blowing up very fast, $\omega^2$ is the ordinal of Conway's chained arrow notation and this should be blowing up much faster than that. How? | |
| Aug 11, 2013 at 2:05 | history | answered | Henry Towsner | CC BY-SA 3.0 |