The set of all finite sequences in RCA0

59 Views Asked by At

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?