Before I ask my question, let me give you a mini-preamble: in 2006, during an animated discussion on feasibility, ultrafinitism, and what else on FOM, I introduced (informally, and to speak the tuth, quite vaguely) a seemingly new notion: UNUTTERABILITY (see here for ref).
By that I roughly meant the following: take for instance the number
$BIG$ is certainly a huge number, in the obvious sense: if you try to expand it out as $SSSS...0$ you end up with a monumentally huge string. On the other hand, this "number" is rather small as a term, in fact I just wrote it: it denoting term above is small (of course, in case I talk to a martian who does not know the recursive definition of exp I will have to add that to the cost, but that does not make my BIG number much bigger, as far as its denotation is concerned).
So, this means that beyond the usual take on feasibility, there should be (or so it seems to me) another notion, namely utterability :
a number is utterable if there is at least one of its denoting terms which is feasible.
Obviously what I just stated is not a definition:to turn this into serious math, let us say that one operates in some extension $T$ of basic arithmetics $Q$, and that one has fixed a rigid notion of feasibility, say a number is feasible if it is less than $BIG$ above. Finally, one can take a formalized version of Kolmogorov-Chaitin complexity for the last part: a number $n$ in the ambient theory T is $BIG$-utterable iff its kolmogorov complexity as a symbol is less than $BIG$: a computer whose resources are bounded by $BIG$ and which knows the rules of $T$ can at least utter that number, ie print and store one of its denoting terms.
All right, now my question(s):
can I find a $T$ where it is consistent to postulate the existence of unutterable numbers? And if yes, what can be said of their distribution?
PS obvious post-scriptum: BIG is there just as an example, you can either choose your favorite version of a big number (Graham, Friedmann's TREE, or what else), or even let it undefined, and simply add a F(x) predicate for feasible, a' la Parikh.