@Holo I'm going off soon, but my proof rests on a simple core lemma: Given any well-ordering S, the set of all finite non-increasing sequences from S are well-ordered under lexicographic order.

By iterating this lemma on ω, you get a simple computable well-ordering of nested lists, and it turns out we can interpret each worm as a nested list in a way that it is reduced on each step.

@user21820 can you explain to me how you use the iteration of the lemma on ω solve this?

@Holo Each worm is interpreted as a nested sequence in the following way: 0 is the separator, and each term is encoded by adding 1. A string of k zeroes encodes k. For example, v(203313) ↦ [v(1),v(2202)] ↦ [[v(0)],[v(11),v(1)]] ↦ [[1],[[v(00)],[v(0)]]] ↦ [[1],[[2],[1]]].

@user21820 idk it just looks like the hydra or the goodstein theorem or its variants

@LeakyNun Natural number worms are supposed to reach ε0, and indeed you can prove the hydra game termination using the exact same lemma I'm using. But I never realized how the worms worked until recently.

And I now understand that worms up to ω will reach ε[ω]. But I have no idea what it would reach if I have nested worms... It seems it will reach φ[2](0), the same limit I reached with my super-trees.

@Holo: Nested sequences are compared lexicographically, with higher-nested sequence being bigger. For example 0 < 1 < 2 < ... < [0] < [0,0] < [0,0,0] < ... < [1] < [1,0] < [1,0,0] < ... < [1,1] < ... < [1,1,1] < ... < [2] < ... < [3] < ... < [[0]].

Yes

Then we check that the bad part is the last term in the sequence at some nesting level, so duplicating it after reducing it will preserve the invariant that the nested sequence is non-increasing at all levels.

So every worm stops growing eventually.

What do you mean by "the bad part is the last term in the sequence at some nesting level"?

@Holo Take an example... 22 → 2121 → 2120212. 22 ↦ [[2]] with bad part [2]. 2121 ↦ [[1,1,0]] with bad part [1,1,0]. 2120212 ↦ [[1,1],[1,1]] with bad part [1,1].

Oh, taking the last sequence in the interpretation

v is the interpretation. Each worm has a unique interpretation. And in fact we know which nesting level by the last term of the good part, since it 'blocks' the bad part.

The key idea is that if you just look at the original sequence, then clearly duplicating the bad part doesn't preserve monotonicity. But under the interpretation, duplicating the bad part merely duplicates the last term at some nesting level, after reducing it, so you can check that at every level it remains monotonic.

def next_aux (N : nat) : list nat -> nat
| [] := 0
| (hd :: tl) := if hd < N then 0 else next_aux tl + 1

def next (m : nat) : list nat -> list nat
| [] := []
| (0 :: tl) := tl
| ((n+1) :: tl) := let index := next_aux (n+1) tl,
    B := n :: list.take index tl,
    G := list.drop index tl in
    ((++ B)^[m+1] B) ++ G

def worm_step (initial : nat) : Π step : nat, list nat
| 0 := [initial]
| (m+1) := next m (worm_step m)

#eval (list.range 4).map (worm_step 1)
#eval (list.range 52).map (worm_step 2)

17:0: information: eval result
[[1], [0, 0], [0], []]
18:0: information: eval result
[[2], [1, 1], [0, 1, 0, 1, 0, 1], [1, 0, 1, 0, 1], [0, 0, 0, 0, 0, 0, 1, 0, 1], [0, 0, 0, 0, 0, 1, 0, 1], [0, 0, 0, 0, 1, 0, 1], [0, 0, 0, 1, 0, 1], [0, 0, 1, 0, 1], [0, 1, 0, 1], [1, 0, 1], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1], [0, 0, 0, 0, 0, 0, 0, 0, 0, 1], [0, 0, 0, 0, 0, 0, 0, 0, 1], [0, 0, 0, 0, 0, 0, 0, 1], [0, 0, 0, 0, 0, 0, 1], [0, 0, 0, 0, 0, 1], [0, 0, 0, 0, 1], [0, 0, 0, 1], [0…

I implemented the function in Lean :P

Lol!

@LeakyNun Can you prove in Lean that the function terminates? =D

I see, but how to show the last part is monotonic? Also, I am not completely sure I get the v, because v(2121)→[v(1010)]→[[v(0)],[v(0)]]→[[1],[1]] no?

@Holo v(2121) ↦ [v(1010)] ↦ [[v(0),v(0),v()]] ↦ [[1,1,0]].

Two 0s means three terms.

Oh, I see

@user21820 have you ever thought about PA with Π1-induction?

And how you prove the last term is monotonic decreasing?

@LeakyNun You mean PA with induction restricted to Π1-sentences?

right

@Holo Let the bad part be the last term at nesting level k. Higher nesting levels are clearly not affected. The sequence at level k obviously remains monotonic. If k>0, then the sequence at level k−1 after the bad duplication will in the worst case be [...,[...,x,y],[...,x,y',y',...,y']] where y' < y. The better case is if the last two terms at level k−1 were different.

At levels less than k−1 I think there is nothing to worry about.

@LeakyNun But I believe induction via meta-reasoning, so why would I stick to only Π1-induction?

More precisely, if there is a problem with the full induction schema, it must be that the system without the induction schema is itself already unsound.

That's why I (and some logicians such as Peter Smith) argue that it is unnatural to stop at ACA0 since the philosophical reasoning justifying ACA0 over PA also applies to justify ACA (which has the full induction schema).

Similarly, it's unnatural to stop at PA−, because any model of PA− has an initial segment (comprising of the interpretation of the numerals) that satisfies PA.

Of course, reverse mathematics studies the hierarchy of induction schemas and boundedness schemas.

but we can ask questions such as "what is the proof strength of Q+Δ0-induction"

@LeakyNun Absolutely, that's why my comment that reverse mathematics studies the (strict) hierarchy. Though often we use PA− rather than Q.

I've not heard of Π1-induction, so presumably it can be recovered from Δ0-induction... The hierarchy is given as BΣ1 < IΣ1 < BΣ2 < IΣ2 < ...

what's the difference between PA- and Q?

PA− is stronger. Q cannot even prove basic stuff like commutativity of +,·.

I know why nobody talks about Π1-induction per se, because Δ0-induction permits free parameters, so it covers Π1-induction. But Google tells me that people have looked at Π1-induction without parameters.

Got to go. Back later!

@Holo So do you get it? =)

Not really, you take $w$(worm), then you take $v(w)$, look at the last sequence in $v(w)$, and then what?

I didn't say you look at the last sequence in v(w). I said that on each step (of the worm game) v(w) is reduced, because "the bad part is the last term in the sequence at some nesting level", and "we know which nesting level by the last term of the good part, since it 'blocks' the bad part".

You have to look carefully at what the step does to observe this.

If you're not sure what's happening, try performing one step on a random worm made up of 0,1,2,3,4,5 that ends with 2.

@Holo: More symbolically, letting b be the bad part, v(w) must be of the form [...,[...,v(b)]...] where there are only "]" in the last "...".

I think I have a confusion from the terminology, you take w, then v(w) gives as a finite sequence, you look at the last part of some stage of this sequence?

@Holo Let w = 31415243532. Tell me what is v(w) and what part of it the bad part of w, and we'll go from there.

v(31415243532)→[v(20304132421)]→[[v(1)],[v(2)],[v(3021310)]], so [v(3021310)] is the bad part

→ 4 messages moved to ­Trash

@Holo Right right! Almost by definition of the interpretation v, the bad part will be the last term of some sequence at some level. I said wrongly that the nesting level is determined by the good part, but it's actually determined by the head of the worm, which is 2 in this case, which is why the bad part is the last term after going in 2 levels from the right.

[[v(1)],[v(2)],[ v(3021310) ]]

So now it only remains to check that if w → w' then v(w) > v(w').

The main outline is here:

Say w' = 3141 5243531 5243531. Then v(w) = [[v(1),v(2),v(3021310)]] and v(w') = [[v(1),v(2),v(302131),v(302131),]].

@Did: Hi! We're talking about worms right now...

It is not hard to see that v(3021310) > v(302131). Now at the bad part's level itself we have [x,y,z] > [x,y,z',z',0] so that sequence decreases. We don't even need what I said in my quoted comment, because at outer levels the last term decreases.

@Holo: I guess I shouldn't have left it blank. v(w') = [[v(1),v(2),v(302131),v(302131),v()]].

The black comes after the first different element so it doesn't matter to the order

@user21820 Seems an interesting game -- about which I am quite illiterate. Thanks for the link though.

@Holo It only matters that the blank is less than everything else, so that the sequence remains non-increasing.

@Did It's a simple kind of game whose termination in general cannot be proven by PA. It has similar flavour to the hydra game, if you've heard of that.

@Holo: So once we prove that each step reduces the worm under v, then necessarily it must terminate because we already knew that the nested non-increasing lists is well-ordered.

Very very nice

It is clear that we go outside of PA here, is there a simple explanation as for why it is impossible to prove inside of PA?

@Holo Apparently, the easiest way is to prove that you can use PA plus well-ordering of ε0 to prove Con(PA). And then the incompleteness theorem finishes the job.

But I'm not familiar with Gentzen's proof so I can't fill that bit in for you. I can only say that these worms can encode the computable ordinal ε0, so if you can prove that the worm game always terminates, you would have proven well-ordering of ε0.

I see

Well, yea, your construction (of repeating nested well ordering) are basically computable ordinals

Yup. Not really mine though; Beklemishev's. =)

:D

Though I did think of those nested lists much earlier in SBA's room, but never saw the connection.

Ok I need to go for about 30 min. See you later!

Bye

@LeakyNun @Holo: Related to the above, I think it can be formalized in ACA0 that "for every well-ordering W, the set of non-increasing finite sequences from W is well-ordered under lex-order". More precisely, "∀S⊆N ∀W⊆S×S ( W encodes a well-ordering of S ⇒ { f : n∈N ∧ f∈S^n } is well-ordered under lex-order )" where we use standard encoding for S×S and { f : n∈N ∧ f∈S^n } as subsets of N. Now observe that we can iterate this lemma any finite number of times in our proof in ACA0.

So for any particular fixed k, ACA0 can actually prove that all worms with numbers at most k will stop growing. Now since ACA0 is conservative over PA, and worm growth is an arithmetically definable process (since we use the step number to dictate the number of duplicates), worm stopping is also an arithmetical sentence, and hence PA can actually prove that the worms stop growing for every worm with numbers at most k.

So this is another example of ω-incompleteness of PA besides the Godel one I mentioned here.

So PA proves that bounded worms die, interesting

More strikingly, PA proves that every worm given explicitly dies.

But PA just cannot prove that every worm dies.

Also I think (but didn't verify the details) that ACA proves that all worms terminate, since ACA has the full induction schema and can happily induct using the lemma.

@Holo Oh well, maybe yours is more striking, since it is a universal statement, whereas for any single worm we could just run the program until it stops and just get PA to prove the program trace.

Heh...

Your method is perfect! run it on [TREE(3)]^TREE(3), and let me know how it goes

=O

You're right!

:)

I don't want to run it. I want to run away. =)

Anyway, I really got to run now. =D

See you later!