Gfilui

Wikipedia states that a definable (real) number is a number "that can be uniquely specified by its description". I naïvely thought that this was the same as "a number which may be computed", but elsewhere in math.SE I found out that it is not the case, because for example numbers related to Chaitin's $Omega$ are definable but not computable. Could someone explain me what a specification is, then? I always thought that $Omega$ was a probability value, which was not a real specification.

"Definable" is always relative to some particular language the definition is expressed in.

A number is definable if there is a property expressed in that language that is satisfied for that number but by no other numbers.

There is no particular expectation that the language we use for the definition is "executable" enough to pinpoint the number with any particular precision. As one example, we can consider definitions in the full first-order language of set theory, where
$$ (x=1landtextthe Riemann Hypothesis is true)lor(x=-1landtextthe Riemann Hypothesis is false)$$
can be expressed as a perfectly good property that defines a nonzero integer $x$ -- but we don't even know the sign of the number that is defined.

Chaitin's constant is actually not a single constant but depends on selecting a representation of Turing machines first. Slightly simplified, once we have selected an enumeration $T_n$ of Turing machines, we get a Chaitin constant
$$ Omega = sum_n=1^infty begincases 2^-n & textif T_ntext terminates \ 0 & textotherwise endcases $$
which again is a perfectly good definition (whether a given Turing machine terminates is a well-defined property), but we cannot compute the constant because whether a given Turing machine terminates is not computable.

(This can also be interpreted as a probability: Go through all of the Turing machines in sequence, flipping a coin for each and select the first machine where you get tails; what is the probability that this randomly chosen machine will terminate? But being a probability has, in itself, no bearing on whether the number is well-defined and/or computable).

The definable numbers depend on how one defines them. Since "the least positive integer not specifiable in fewer than twelve words" is an eleven-word phrase, we get something called Berry's paradox unless we recognise that the specification standard must preclude reference to itself. Formally, this separation relies on an object language and a metalanguage for talking about it, so "the least positive integer not specificable in fewer than sixteen words of that object language" can exist as a description in the metalanguage, but not in the object language; but this forces definability to be relative.

The important point is this: no matter what specification you formalise, if you're only allowed finite-length descriptions in a language with a countable alphabet, you'll only be able to define countably many things. (Roughly speaking, this is because $sum_n=0^inftyaleph_0^n=aleph_0$.) Since $mathbbR$ is uncountable, you'll definitely leave out something.

"Definable" as a very precise meaning. Given a structure $M$ on a first-order language $mathcal L$, an element $ain M$ is definable if and only if there exists a formula $varphi(x)$ in one variable such that
$$ M models forall x, varphi(x) leftrightarrow (x=a)$$

In particular "definable" is always relative to the language of specification. For example, given $M$ as before, an element $ain M$ is always definable in (the induced structure on) $M$ over the language $mathcal L sqcup c_a$ where the new constant $c_a$ is interpreted as $a$ (the wanted $varphi(x)$ is just "$x=c_a$"). Even if $a$ was not definable over $mathcal L$.

When saying "Is the real number $a$ definable?", it is probable that people mean: given a model $mathcal S$ of ZFC, is (the set corresponding to) the real number $a$ (in the usual encoding of reals in ZFC) definable over the language $in$?

As nobody know an explicit model of ZFC, there is a good chance that "the real number $a$" is actually already a shortcut for the formula $varphi(x)$. To go back to your question, when people say "Chaitin's constant", they do not refer to a specific element of a God-given model of ZFC, they refer to the construction you probably know: enumerates the countably infinite Turing's machines as $m_1,dots$ and affect the value $t_i=0$ if $m_i$ terminates or $t_i=1$ otherwise then creates the number $sum_i=1^infty t_i10^-i$. All of that is completely expressable in the language $in$ under the axioms of ZFC. In particular, what is bothering you is the "if $m_i$ terminates", but termination of a Turing machine is a property that can be encoded into ZFC once the notion of Turing machine is encoded into ZFC. (ZFC would be making a poor job as a foundation of mathematics if such things was not expressable.)