What does it mean to find something in Set theory? What is formal-language equivalent of "find"? For example in proof that every real number $x$ has a decimal expression $x=a_0.a_1a_2a_3….$ it says:

so we can find $a_1$ between $0$ and $9$ such that...

https://math.stackexchange.com/a/2625318/360552
What if $x$ is, for example, Chaitin constant where we cannot find $a_n$ that satisfies given condition because we don't know how to compute the digits or exactly how big/small is Chaitin constant but we only know that it exists and is in some fixed interval.
Obviously, find is not the same as compute but I wonder what mathematicians mean by find. Which ZF Axiom is used to find a number that satisfies a certain condition.
Another example is in this Cantor proof that real numbers are uncountable. It says

Find the first two numbers of the given sequence that are in the open interval $(a, b)$.

The problem with this sentence is that if a sequence is a series of uncomputable numbers like Chaitin's constant, how can we "find" those first two numbers that are in the open interval $(a, b)$ if we don't know exact values of those numbers.
So which ZF axiom is used in Cantor's proof to find those first two numbers in a sequence that satisfy a given condition? What does it mean to construct an interval with those 2 numbers if we cannot find those 2 numbers and only know that they exist? It is obvious that I also do not know what a constructive proof means (I thought that I knew).
Obviously, find means something other than what I intuitively think it means so I wonder which axioms are used to find something that satisfies a certain condition like in Cantor's proof. What axioms are required for this Cantor's proof?
Summary:

*

*How could we express find in a formal language?

*Which axioms are used to find an element of a Set that satisfies a certain condition.

 A: It comes down to how you interpret the symbol $\exists$ in "$\exists x. Px$". If you're a constructivist, it means some variant of "I have a witness to the truth of $P$". If you're a normal mathematician, it means something more like "$\neg \forall \neg$". For a normal mathematician, we don't care that equality of reals is undecidable; we just go ahead and assert that $x = y$ or $x \ne y$ anyway.
Constructivists also can have problems even defining many real numbers (depending on quite how constructivist you go), and this is another source of the difference.

The first answer you linked to is https://math.stackexchange.com/a/2625318/360552. This is not constructive in the strictest computational sense, because it relies on being able to compute whether a given real is greater than or equal to some integer $n$. The most highly upvoted answer is https://math.stackexchange.com/a/409706/259262 which makes it more explicit where the noncomputable step is: it says "take the least such $n$", which certainly exists (in the sense that it can't not exist), but which there is no algorithm to compute in general.
The problem with many of the answers on that page is that they rely on being able to output a specific n-ary representation of a real, whereas in fact to do so is uncomputable.
A computable answer might be as follows: if reals are defined as Cauchy sequences of rationals (as they often are in constructive-land, because that definition is extremely friendly), then there is a constructive algorithm to generate a decimal expansion: simply approximate to within $\frac{1}{100}$ to obtain the first digit, then to within $\frac{1}{1000}$ to obtain the second, and so on.
However, this constructive answer is inherently limiting in practice because it requires you to know up front what sequence of rationals converges to the real in question (because a real is such a sequence of rationals - you can't specify a real without specifying that sequence!). So you've already been forced to do all the hard work of approximation already; we've just offloaded the hard work into the definition of what it means to be a real number.
A: As Jacob points out, the phrase 'find an $X$ such that $Y$' is just a replacement of 'since we know there exists an $X$ such that $Y$, we may pick any such $X$'. You seem to think that in order to pick such $X$ we need an axiom that allows you to pick elements, similar to the axioms of ZFC. This is not the case: in classical logic we simply define the phrase `there exists' to be true whenever there is such $X$, and if this is the case we may pick any such $X$ without knowing a way to construct it. You're right that this is very different from a constructive proof.
To answer your question in the comments: I'm not sure whether the the diagonal argument is constructive, but at least what you can show constructively is that there are uncountably many integer sequences: for a given sequence of numbers you can constructively find a new sequence that is not in your list, therefore proving your list was incomplete. See also wiki. (On wiki it says that this proof is a proof by contradiction, but it is still a constructive proof since you really just use the definition of 'uncountable', which is 'not countable', which in turn must be proven by 'if it were countable, it would lead to contradiction'.)
A: At least in your first example, it corresponds to "there exists". Your second example is slightly different, but with some adjustment it is essentially the same. Basically, we can take it as:
"there exists at least two elements of the sequence which are in the interval $(a, b)$. Let $x_{1}, x_{2}$ be the first two."
