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

And I will be busy for the next two weeks so I might not be around much.

Oh, good luck with whatever it is

Thanks! See you soon!

Good afternoon!

Hello

Hi.

Would you happen to know a lot about lattices?

Not really a lot, @MaliceVidrine (hello!) will probably know more

Basically i'm trying to prove something regarding distributive lattices and i've ran out of ideas.

So i'm looking for new intuitions . . .

I can't claim to know a huge amount about lattices, but I can give it a try.

Hi.

And thanks.

hello!

Consider the following property:

For all a, b, and c. If sup(a,c) = sup(b,c) and inf(a,c) = inf(b,c), then a = b.

I'm trying to prove that a lattice is distributive if and only if that property holds.

I believe the property is equivalent to the Forbidden Sublattices Characterization of Distributive Lattices.

The "if" part was easy. Is the "only if" part that got me stuck.

I'm mainly looking for intuitions that could get me started thinking again.

Hmm...

The most recent intuition i had about it is that if a lattice is distributive and x is an element of the lattice.

You could define an homomorphism between the lattice and the ideal of x.

And the filter of x too of course.

Fair warning, I've just woken up, so my brain is being sluggish.

It's ok.

:)

Do you know someone how knows a lot about lattices?

Not off hand, no. There are a few people like Noah Schweber who have an incredibly well rounded knowledge base (mine is still getting there) who might have more to say, but that's just me stabbing in the dark because they seem to know the answers to everything :P

Not for any lattice-specific knowledge that I know of.

Also chances are our friendly neighborhood @user21820 might be able to think of someone/say more.

Thanks, sorry for the delay; i'll keep them in mind to importuna... to politely ask them for help.

If i see them.