Let $\eta$ denote an explicitly defined incomputable real number (the bounty text is faulty, and does not mention incomputability of $\eta$). Then I think that no (recursively ennumerable) formal system can pin down $\eta$ to arbitrarily many decimal places. If this is true, I'd enjoy reading a rigorous proof, since my argument is fluffy and could use more precision and generality. If its false, I'd like to see an explicit definition of an incomputable number that $\mathrm{ZFC}$ can pin down to arbitrary precision.
Here are my thoughts, restricted to the specific case of $\mathrm{ZFC}$ (or rather, formal systems implementing $\mathrm{ZFC}$). Let $\varphi$ denote an explicit definition of an incomputable real number $\eta$ in the language of set theory. So in particular, we're assuming that $\varphi$ is an $\in$-formula with one free variable $\eta$, and that $\mathrm{ZFC}$ proves the following.
- There exists unique $\eta$ such that $\varphi.$
- If $\varphi$, then $\eta \in \mathbb{R}$ and $\eta$ is incomputable.
Now suppose for a contradiction that $\mathrm{ZFC}+\varphi$ pins down the numerical value of $\eta$ to arbitrary precision. More formally, we're assuming that for every rational number $x \in \mathbb{Q}$, the theory $\mathrm{ZFC}+\varphi$ either proves $x \leq \eta$ or else proves that $\eta \leq x$. Then we can assign to every rational number $\varepsilon > 0$ an algorithm that computes $\eta$ to $\varepsilon$-precision; this involves systematically going through all the theorems of ZFC until we find a theorem of the form "the rational number $x-\eta \leq \varepsilon$ (which is explicitly described) is within a distance $\varepsilon$ of $\eta$." I think that, by hypothesis, this only takes finitely many steps, so we're allowed to do it repeatedly, for $\varepsilon$ equal to $1,\frac{1}{2},\frac{1}{4},\frac{1}{8}$ etc. Then we have an algorithm that hones into the numerical value of $\eta$ to arbitrary precision, contradicting its incomputability.
Motivation. I was thinking that maybe we can numerically evaluate the strength of various large cardinal assumptions by studying the extent to which they narrow down the values of certain incomputable numbers. For example, it would be cool to be able to make statements like: "this large cardinal axiom makes $\mathrm{ZFC}$ at least 1000x as strong with respect to Chaitin's constant, in the sense that $\mathrm{ZFC}+\mbox{Axiom}$ can pin down every possible Chaitin's constant with at least 1000 times the precision than $\mathrm{ZFC}$."
Your argument is correct. Here's why:
There exists a computer program that can verify (in polynomial time, in fact) whether a string of statements in a system with finitely many axioms is a correct proof of a given theorem of that system. Therefore, the computational problem "Is $x$ a theorem?" is recursively enumerable. In particular, it is possible to write a program that, given a theorem, will eventually prove it. I would venture to guess that for most interesting theorems this is almost certainly infeasible, but there's no question that it is possible. Assuming the law of the excluded middle, this means we can determine whether or not a decidable statement in ZFC is true in a finite amount of time by simultaneously trying to prove the statement and its negation; eventually we will prove one of them.
We can also enumerate with a computer program all ordered pairs of decimal numbers of finite length that are within $\epsilon/2$ of each other if $\epsilon$ is rational. Numbers with this sort of representation are dense in $\mathbb{R}$. In our situation we have that there is a predicate $P$ that uniquely specifies a real number $y$, and we want to produce a decimal representation of $y$ that is within $\epsilon$ of $y$. Therefore we run through all pairs $(x_1,x_2)$ of decimal numbers of finite length within $\epsilon/2$ of each other and invoke our proof-finding program up to twice for each pair: once to prove $P(y)\implies x_1\leq y$ and once to prove $P(y)\implies x_2\geq y$. Eventually, if ZFC can prove these theorems, we will end up with two decimal representations of $y$ that are correct to within $\epsilon$, though likely not before the heat death of the universe.
Thus, if there is no computer program that will compute $y$ to arbitrary precision, there must be some (in fact infinitely many) statements of the form $P(y)\implies x_1\leq y$ or $P(y)\implies x_2\geq y$ that are undecidable.