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?
$\begingroup$
$\endgroup$
5
-
2$\begingroup$ 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$.) $\endgroup$– Noah SchweberCommented Jul 1, 2022 at 15:00
-
$\begingroup$ @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? $\endgroup$– Mohammad tahmasbi zadeCommented Jul 2, 2022 at 1:09
-
1$\begingroup$ 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. $\endgroup$– Noah SchweberCommented Jul 2, 2022 at 1:20
-
1$\begingroup$ 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$. $\endgroup$– Noah SchweberCommented Jul 2, 2022 at 1:22
-
$\begingroup$ @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? $\endgroup$– Mohammad tahmasbi zadeCommented Jul 2, 2022 at 3:23
Add a comment
|