-3

Can ZFC define the busy beaver(BB) function? That is to say, is there a formula $A(x,y)$ in the language of ZFC such that $A(x,y)$ holds precisely when $x$ and $y$ are natural numbers and $y=BB(x)$?

user107952
  • 20,508
  • 8
    Why wouldn't it? How do you think we can define it at all, if we wouldn't? – Asaf Karagila Oct 01 '20 at 06:29
  • 1
    @AsafKaragila I am asking because the Busy Beaver function is not computable. Also, it can't be defined in Peano Arithmetic, so maybe it can't be defined in ZFC either. – user107952 Oct 01 '20 at 20:30
  • 1
    How would we reason about it, in general? Also, since ZFC proves that there is a continuum size set of total functions from $\Bbb N$ to itself, and it can even define many of them (e.g. the truth predicate of $\Bbb N$), it can surely reason non-arithmetic functions. – Asaf Karagila Oct 01 '20 at 20:31
  • 2
    @user107952 It can be defined in Peano arithmetic. See here (the graph of the Busy Beaver function is $\Pi^0_1$). – Noah Schweber Oct 02 '20 at 03:50

1 Answers1

5

Per the comments, this question appears based on a misconception: the Busy Beaver function is in fact already definable in the language of arithmetic, and basic facts about it (although not more than a few of its specific values) can be proved in $\mathsf{PA}$. The relevant tool here is Post's theorem, which gives us bounds on how complicated a set/function is to define in the language of arithmetic based purely on its computability-theoretic complexity - and in particular lets us show that the Busy Beaver function is definable in the language of arithmetic, since it has Turing degree ${\bf 0'}$. The expressive power of arithmetic is really quite vast.

The discussion here may be helpful.

Noah Schweber
  • 245,398