Does V[ω.2] satisfy ZFC/Σ0R (ZFC with Σ0-replacement)?

By which property of supremum there exists $\eta$?

@FreeMind supremum of set of ordinals(cardinals) is the union of the set(of course this require a proof)

@Holo What I am asking is, in the proof it claims that there exists $\eta'\in A$ , but I don't know what properties of supremum is used?

@Holo I am asking a question about part of proof in the above topic.

@Holo the $\eta '$ in the Le Anh Dung answer specifically.

@FreeMind you have $\eta<\sigma\notin A$, so if $\eta'$ doesn't exists $\sup A=\eta$

Which is contradiction to the assumption

@Holo Oh Yeah! Thanks!

@user21820 I read about the worm function, it is pretty cool. I found the original paper of Beklemishev, and will try to read it soon

@LeakyNun No. Let BR stand for bounded replacement, namely Σ0-replacement. Let Q(k,x) ≡ ( x is an ordinal isomorphic to the concatenation of ω and k ), for each k∈ω. Then we can prove by induction that ∀k∈ω ∃!x ( Q(k,x) ). Also Q can be expressed as a Σ0-sentence because we only need a countable bijection. Thus by Σ0-replacement ∃S ∀k∈ω ∀x ( Q(k,x)⇔x∈S ). But S ⊇ ω+ω, so V[ω+ω] cannot be a model of ZC+BR.

I think a similar argument shows that any model of ZC+BR must be closed under definable ω-sequences. An obvious standard model would be V[ω[1]], but that may not be the shortest possible height. If your specification schema also permits only bounded quantifiers, then the whole system is known as bounded ZFC.

Actually, bounded ZFC is very strong, and yet somewhat non-circularly justifiable via the cumulative hierarchy. Hence my comment in the past:

And practically no mathematics outside of set theory will venture beyond bounded ZFC.

@user21820 "isomorphic to" is Σ1 no?

@LeakyNun Yes in general, that's why I have to add the remark that we can make do with a countable bijection here.

Hmm maybe countable bijection isn't enough, unlike what I thought. Let me try another way. Let Q(k,x) ≡ ( x is an ordinal with exactly 1 nonzero member with no predecessor ). Then again we would be able to construct ω+ω by BR.

Wait... That's not even using BR...

Hmm need to do a bit more... Hold on.

Let Q(k,x) ≡ ( x is a set of pairs (j,y) such that j∈k and y is an ordinal and ∀i,j∈ω ∀p,q∈x ( i<j ∧ p[1]=i ∧ q[1]=j ⇒ p[2]∈q[2] ) ).

Then Q is a Σ0-sentence, since Kuratowski pair recognition and projection is Σ0.

Gah... too late to edit; forgot to insert the ω into Q.

Let Q(k,x) ≡ ( x is a set of pairs (j,y) with j∈k ∧ y is an ordinal containing ω ∧ ∀i,j∈ω ∀p,q∈x ( i<j ∧ p[1]=i ∧ q[1]=j ⇒ p[2]∈q[2] ) ).

Q(k,x) basically says that x is a strictly-increasing length-k sequence of ordinals containing ω. Now we can prove by induction that ∀k∈ω ∃!x ( Q(k,x) ).

Oops not unique.

Let Q(k,x) ≡ ( x is a set of pairs (j,y) with j∈k ∧ y is an ordinal containing ω ∧ ∀i∈ω ∀p,q∈x ( p[1]=i ∧ q[1]=i+1 ⇒ succ(p[2])=q[2] ) ).

Where ( succ(x)=y ) expands to x∈y ∧ ∀z∈y ( z∈x ⇔ z≠x ).

I think that works now.

ZFC encoding is so troublesome...

Oops need to start from ω to make it unique.

Let Q(k,x) ≡ ( x is a set of pairs (j,y) with j∈k ∧ y is an ordinal ∧ ∀i∈ω ∀p,q∈x ( p[1]=i ∧ q[1]=i+1 ⇒ succ(p[2])=q[2] ) ∧ ∀p∈x ( p[1]=0 ⇒ p[2]=ω ) ).

I wish I can stop writing in set-theory encoding.

Basically I just want Q(k,x) to say that x is the initial segment of ordinals from ω to less than ω+k.

@LeakyNun: Does this sound right now? Or have I made another mistake?

sounds reasonable

@Holo I can sketch my proof if you wish. I also thought of the natural extension to worms comprising bigger ordinals than just natural numbers, where each step you decrease the head and then duplicate the bad part. But my proof method doesn't work even for just up to ω.

For example: ωω → ω2ω2 → ω2ω12ω1 → ω2ω12ω012ω → ω2ω12ω01233 → ...

It is more or less obvious that ω is bigger than anything without ω, and ωω is bigger than anything that does not have consecutive ω, and so on. It's not obvious to me what each of them is, though.

@user21820 I am on a bus right now, so I can't really concentrate on this, but in a few hours I would love to(my internet was cut off while sending similar msg, not sure if it reached you so I am sending this to make sure)

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