Thursday, 29 October 2015

lo.logic - Is there a name for a family of finite sequences that block all infinite sequences?

Let ${bf N}^omega = bigcup_{m=1}^infty {bf N}^m$ denote the space of all finite sequences $(N_1,ldots,N_m)$ of natural numbers. For want of a better name, let me call a family ${mathcal T} subset {bf N}^omega$ a blocking set if every infinite sequence $N_1,N_2,N_3,N_4,ldots$ of natural numbers must necessarily contain a blocking set $(N_1,ldots,N_m)$ as an initial segment. (For the application I have in mind, one might also require that no element of a blocking set is an initial segment of any other element, but this is not the most essential property of these sets.)



One can think of a blocking set as describing a machine that takes a sequence of natural number inputs, but always halts in finite time; one can also think of a blocking set as defining a subtree of the rooted tree ${bf N}^omega$ in which there are no infinite paths. Examples of blocking sets include



  1. All sequences $N_1,ldots,N_m$ of length $m=10$.

  2. All sequences $N_1,ldots,N_m$ in which $m = N_1 + 1$.

  3. All sequences $N_1,ldots,N_m$ in which $m = N_{N_1+1}+1$.

The reason I happened across this concept is that such sets can be used to pseudo-finitise a certain class of infinitary statements. Indeed, given any sequence $P_m(N_1,ldots,N_m)$ of $m$-ary properties, it is easy to see that the assertion




There exists an infinite sequence $N_1, N_2, ldots$ of natural numbers such that $P_m(N_1,ldots,N_m)$ is true for all $m$.




is equivalent to




For every blocking set ${mathcal T}$, there exists a finite sequence $(N_1,ldots,N_m)$ in ${mathcal T}$ such that $P_m(N_1,ldots,N_m)$ holds.




(Indeed, the former statement trivially implies the latter, and if the former statement fails, then a counterexample to the latter can be constructed by setting the blocking set ${mathcal T}$ to be those finite sequences $(N_1,ldots,N_m)$ for which $P_m(N_1,ldots,N_m)$ fails.)



Anyway, this concept seems like one that must have been studied before, and with a standard name. (I only used "blocking set" because I didn't know the existing name in the literature.) So my question is: what is the correct name for this concept, and are there some references regarding the structure of such families of finite sequences? (For instance, if we replace the natural numbers ${bf N}$ here by a finite set, then by Konig's lemma, a family is blocking if and only if there are only finitely many finite sequences that don't contain a blocking initial segment; but I was unable to find a similar characterisation in the countable case.)

No comments:

Post a Comment