I'm reading Peter Smith's Goedel's Theorems and am embarrassingly suspicious of the claim (theorem 3.1) that all finite sets are effectively decidable. For example, the set $\{BB(7918)\}$ has one member (which I think is definable in arithmetic), the value of which is independent of ZFC.
The proof given in the book seems to rely on a finite set consisting of a concrete list of concrete numbers (rather than being defined by a predicate), and hence having a decidable characteristic function that simply checks the argument against all members of the set. What am I missing? If I'm not missing anything, what do we lose by realising that some finite sets aren't decidable?
Best Answer
We have to distinguish between sets and definitions of sets.
A set is decidable (or computable, or recursive - the subject has unfortunately redundant terminology!) iff some Turing machine decides it. Every finite set is decidable since we can always "hard-code" a Turing machine to accept a given finite set: fixing $a_1,...,a_n$, just write a program which on input $k$ checks whether $k=a_1$, whether $k=a_2$,... , whether $k=a_n$, and outputs "YES" if the answer to one of these questions is YES and outputs "NO" otherwise.
However, some definitions of very simple sets appear computationally intractable. For example, for any sentence $\varphi$ let $$True_\varphi=\{x: (x=0\mbox{ and $\varphi$ is true})\mbox{ or } (x=1\mbox{ and $\varphi$ is false})\}.$$ Obviously $True_\varphi$ defines a decidable set (either $\{0\}$ or $\{1\}$), but we don't know which. This suggests the following notion (the terminology below is my own, I don't know if there's a more common one):
(I'm being a bit vague here about what exactly I mean by "definition" - it doesn't really matter, but if you like we can take it to mean "formula in the language of set theory with one free variable which $\mathsf{ZFC}$ proves only ever holds of natural numbers.")
Before moving on, let me give a quick caveat:
Not every decidable set has a concrete description!
The concretely-describable sets form a proper subclass of the decidable sets; every finite set is indeed concretely describable, though, so for now this is a reasonable thing to think about. (See the end of this answer for more on this.)
The point, then, is the following:
In particular, "The set containing exactly the $7918$th value of the Busy Beaver function" is not a concrete definition of a set; however, the set it defines is finite and does in fact have some concrete definition, we just don't know what it is.
OK, now let me get back to the point above about concrete describability vs. decidability.
Since we can search through $\mathsf{ZFC}$-proofs (and assuming $\mathsf{ZFC}$ is sound), we can compute an enmeration $(M_i)_{i\in\mathbb{N}}$ of all Turing machines which $\mathsf{ZFC}$ proves decide a set - that is, which $\mathsf{ZFC}$ proves always halt on all inputs. But now we can diagonalize against these: the set $$D_{\mathsf{ZFC}}=\{i: M_i(i)=0\}$$ is decidable but has no concrete description.
It's a good exercise to check why the above definition of $D_{\mathsf{ZFC}}$ is not in fact concrete! Also, note that $\mathsf{ZFC}$ isn't really important here - we can replace $\mathsf{ZFC}$ throughout with any other "appropriate" theory, like first-order Peano arithmetic.
In particular, "The set of numbers decided by machine $M$" is not concrete in general ... since maybe $\mathsf{ZFC}$ doesn't prove that $M$ actually decides a set!
This is one of many situations in computability theory where semidecidability (or computable enumerability, or recursive enumerability) is a much tamer notion than decidability: while it's hard to tell whether a Turing machine decides a set, every Turing machine definitely accepts a set, so "is $\mathsf{ZFC}$-provably equivalent to a definition of the form 'the set of numbers accepted by $M$'" is a much better-behaved notion of concreteness than "is $\mathsf{ZFC}$-provably equivalent to a definition of the form 'the set of numbers decided by $M$.'"
(Incidentally, this winds up connecting with the topic of what functions a given theory - such as $\mathsf{ZFC}$ - can prove to be total. There's a vast literature on this, mostly in proof theory but spilling into computability theory and the study of models of arithmetic, but for a starting point see Beklemishev, Induction rules, reflection principles, and provably recursive functions.)