Let N be the set of natural numbers. We consider explicit and implicit first-order definability over the structure (N,+,x,=). Let N^N be the Baire space, i.e., the space of total functions X : N -> N. A point X in N^N is said to be explicitly definable if X = {(i,j) in N x N | (N,+,x,=) satisfies Phi(i,j)} for some first-order formula Phi(i,j). More generally, for X, Y in N^N we say that X is explicitly definable from Y if X = {(i,j) in N x N | (N,+,x,=,Y) satisfies Phi(i,j,Y)} for some first-order formula Phi(i,j,Y). A subset P of N^N is said to be explicitly definable if P = {X in N x N | (N,+,x,=,X) satisfies Psi(X)} for some first-order formula Psi(X). Note that a point X or a set P is explicitly definable if and only if it is arithmetical, i.e., Pi^0_n for some n in N. A point X in N^N is said to be implicitly definable or implicitly arithmetical or an arithmetical singleton if the singleton set {X} is arithmetical.

The Tarski Truth Theorem provides an example of a point which is implicitly definable but not explicitly definable. The Kleene/Souslin Theorem implies that a point is hyperarithmetical if and only if it is explicitly definable from some implicitly definable point. Cohen forcing provides an implicitly definable pair of points such that neither point is implicitly definable. A 1972 theorem of H. Tanaka says that every countable, nonempty, explicitly definable set of points contains an implicitly definable point. A 1975 theorem of Harrington provides a pair of implicitly definable points such that neither point is explicitly definable from the other. A 1976 theorem of Harrington provides a countable, explicitly definable set of points such that not every point in the set is implicitly definable. The proofs of Harrington's theorems involve a remarkable application of the Recursion Theorem.