# The set of all finite sequences in RCA0

In the book "subsystems of second order arithmetic", page 68, Simpson claimed that the set of all codes of finite sequences (denoted by "Seq") exists by sigma 0-0 comprehension. I tried to write a sigma 0-0 formula like A(t) to express that t is code of a finite sequence, but I failed. The only formula I could write was the formula that using existential set quantifier. Can anybody help me with this?

• You should be able to bound everything by the code $t$ itself. E.g. if $t$ is a code for a sequence, then the length of that sequence and each term of that sequence is smaller than $t$. (This might have finitely many exceptions, but those can be explicitly treated - e.g. maybe we need $t>2$.) Jul 1, 2022 at 15:00
• @NoahSchweber thanks. But if we want to say that t is a code of a sequence X, the natural way is to use "∃X such that...". How can I get rid of this existential set quantifier? Jul 2, 2022 at 1:09
• That's not the natural way to do it. $X$ ranges over possibly infinite sets, not finite sequences. Forget about second-order quantifiers entirely, this is just "Godel-style" thinking: how would you talk about finite sequences in first-order arithmetic? For example (I'm not sure which method Simpson uses), think about representing the string $$\langle 13,4,65,0\rangle$$ by the number $$2^{13+1}3^{4+1}5^{65+1}7^{0+1}.$$ This generalizes to an appropriate coding system for all strings. Jul 2, 2022 at 1:20
• If we use the method I just outlined, we have $x\in \mathsf{Seq}$ iff whenever $p,q$ are primes with $p<q$ and $q\vert x$ we also have $p\vert x$. Do you see why? Now prima facie that's $\Sigma^0_1$ ... but of course we can restrict attention to $p,q\color{red}{<x}$ to make it $\Sigma^0_0$. Jul 2, 2022 at 1:22
• @NoahSchweber Yes I understand. Thanks. Simpson proved this: for any finite set X, there is three natural number k,m,n such that for all i, i∈X iff i<k and m(i+1)+1 divides n. then Code (X) is the least (k,(m,n)). By this coding, how can I express t∈Seq? Jul 2, 2022 at 3:23