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

@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!