Existence of a set of valid Busy-Beaver entries.  In reference to 1961 paper "On Non Computable Functions" by T. Rado. 
Motivation - Scott Aaronson's Who Can Name the Bigger Number?.  
M is an n-state binary Turing machine. A valid BB-n entry is a set $(M,s)$ where M halts in exactly s steps. $E_n$ is the set of all valid BB-n entries. Since one cannot have both $(M,s_1) \in E_n$ and $(M,s_2) \in E_n$ for $s_1\not=s_2$, Rado concludes that $E_n$ is a subset of all possible n-state binary Turing machines which is finite and hence, $E_n$ is an exceptionally well-defined non-empty finite set. He proceeds to prove that some functions defined over $E_n$ are non-computable. 
But because I'm aware of the Halting problem, I am unable to satisfactorily answer the following question : does $E_n$ exist? Let s be the number of steps required by M to halt when started on a blank tape. 
Question 1. Can I say s does not exist?
If the answer is yes, then I can say (M,s) does not exist, and hence $E_n$ does not exist. If not, what can I say about s?
Question 2. If I do not want $E_n$ to exist, and in general sets that admit non-computable functions over them to exist, would I need to yank this statement : "every subset of a set is a set" out of my intuition? Is there an axiomatic system where everything that exists is computable?
I was a bit surprised about how easily Rado assumed the existence of $E_n$. When you can't even construct a set, it is not surprising that some functions over it are non-computable. I ask this question in the similar vein as Scott Aaronson asks Succinctly naming big numbers: ZFC versus Busy-Beaver, i.e "mathematical questions that are ultimately about finite processes" which don't include the likes of "CH, AC, the existence of large cardinals".
 A: The issue your raising is the distinction between existence and computability.
The set $E_n$ is uncomputable, but it clearly exists because every machine must either (A) halt or (B) not halt. A machine cannot both halt AND not halt.
An analogous situation would be if I took 10 coins and put them in a box and shook it and proclaimed that $X$ = the number of heads-up coins in the box before I opened the box. Now clearly $X$ exists and is well-defined, but I cannot know it until I open the box (assuming the coins are suitably random).
A: The question of whether a given fixed Turing machine $M$
halts or not is something that can be independent of our 
fundamental axioms of mathematics. 
For example, let $M$ be the Turing machine that searches
for a proof of a contradiction from ZFC, say, halting only upon
finding one. One could in principle write down the specific
instructions for such a machine.
And in a universe in which ZFC is consistent, then $M$
never halts. But by the incompleteness theorem, if ZFC is
consistent, then there are universes in which ZFC is true,
but Con(ZFC) is false, and in such a universe, $M$ does
halt.
Thus, the question of whether $s$ exists for a given
machine $M$ that we can write down is something that can be
independent of our axioms. And strengthening the theory
doesn't really solve the problem, since the same argument
will apply to the stronger theory.
More generally, although the collection of $n$-state
programs that halt is a finite set, and therefore the
halting times of the programs in this set is definitely
bounded by some finite number, and we can easily prove that
it is bounded, nevertheless the specific lower bounds that
we can provide for how long the computations proceed will
depend on our background theory.
The situation is that stronger and stronger theories may
prove higher and higher lower bounds on the value of how
long $n$-state programs can run while still halting. No theory (computably axiomatized consistent) will be able to prove the optimal values for the busy beaver function, since if there were such a theory, then by searching for proofs we would be able to compute those values, which we provably cannot. So the stronger and stronger theories will continually settle additional halting instances pushing the values of the busy beaver function still higher. 
So we can easily prove that $E_n$ exists, since it is determined by the set of $n$-state programs that halt and their running times. The thing we sometimes cannot prove is whether a given machine $M$ is in $E_n$ or not. A weak theory may not be able to prove that $M$ halts, even when a stronger theory is able to do so.
