A countable definable set of reals containing no definable elements

TL;DR

This paper constructs a model using Jensen forcing where a countable, non-empty, definable set of reals contains no real that is definable from ordinals, highlighting limitations of definability.

Contribution

It introduces a novel forcing construction to produce a countable definable set of reals with no ordinal-definable elements.

Findings

Existence of a countable non-empty Pi^1_2 set with no OD real

Use of finite support product of Jensen forcing

Demonstrates limitations of definability in set theory

Abstract

We make use of a finite support product of Jensen forcing to define a model in which there is a countable non-empty lightface $\Pi^1_2$ set of reals containing no ordinal-definable real.