A few questions about intuitionistic mathematics
This is an answer to some of the questions from the OP.
The set $\{U,V\}$ constructed in the proof of Diaconescu's theorem looks finite from a classical perspective. But the definition of "finite" is that there is a bijection with some natural number (this is true in both classical and constructive settings). Because the sets $U$ and $V$ are constructed in such a way that it is not known whether $U = V$ or $U \not = V$, there cannot be any constructive proof that such a bijection exists, because the bijection would let you tell whether the sets are equal. In fact the set $\{U,V\}$ is not finite (constructively).
Diaconescu's theorem is particular to constructive set theory. In that theory, they allow comprehension axioms even when membership in the constructed set is not decidable. So for example they would accept $$W = \{ x \in \{1\} : \text{the Riemann hypothesis holds}\}$$ as a valid definition of a set. Of course they have no idea whether this set is empty, or whether it is $\{1\}$, because the Riemann hypothesis is an open question. There are other settings for constructive mathematics in which the set membership relation is always decidable; in those settings it is not possible to form sets like $W$ in the first place.
Gödel proved that every theorem of PA which does not involve the symbols "$\lor$" or "$\exists$" is also a theorem of HA
I think you are talking about Godel's negative translation
Is this not true in general, for example when dealing whith real numbers?
The theorem holds if the theory itself is closed under the translation and double negation of the atomic formulas are equivalent to them, then translation is identity over the part not containing "$\lor$" and "$\exists$".
Isn't it true that, in general, if a statement P is classically valid, then ¬¬P is intuitionistically valid?
No, we need to remove the constructive content from all internal parts, just doing at the outside will not suffice. (If you know Kripke models, then a double negation in the front means that the statement inside will be eventually forced i.e. constructively correct).
First of all I am not confortable with the proof of such theorem: how can the sets U and V (defined in the Wikipedia page) be intuitionistically well defined, if we cannot, in general, assert P∨¬P? [...] So how can the sets U and V be well defined if P is a statement we cannot prove or refute, like the Goldbach Conjecture?
I guess your question is "why we accept the axiom of specification as constructive?". These kind of confusions arise usually because people not familiar with constructive concepts try to interpret them classically. Different constructive theories use conceptually different but similar looking concepts and the difference is not visible when looking at them as classical objects. The best reference I know of that has a good treatment of these issues and explanation of what each of them means is Beeson's book "Foundations of Constructive Mathematics", 1980.
In this case you are using an argument about not-well-definedness of a number (not a sequence!, $n$ is not playing about role here) in constructive number theory to argue against about the well-definedness of a set in a particular set theory.
It can become even more confusing (for people not familiar with the fact that these theories might use conceptually different concepts), a constructive axiom about some concepts in a constructive theory may destroy the constructiveness of another theory. There is nothing wrong about each one, the problem is that the underlining concepts are different and each satisfy different constructive axioms. A good illustrative example is "functions" and "operations". If you want to know more about their difference check Beeson's book.
It says here that, even though the full AC is not intuitionistically acceptable "there are, however, certain restricted axioms of choice that are acceptable for the intuitionist", like the Axiom of Countable Choice or of Dependent Choice. But the choice used in Diaconescu's reasoning isn't only countable, it's finite! So how can the cardinality of the family of sets we are chosing from have anything to do with the intuitionistic validity of our choice principle?
Be careful about calling them finite, $U$ and $V$ are finite only if you have constructive proof of it, and here it would mean giving a natural number and a bijection between the set and that number. You are again mixing the classical views with constructive views and that can cause confusion.
Second thing is that you are not clear about the context. There quite a few axioms of choice, some of them may destroy the constructive content of a constructive theory if you are not careful about what are the real underlining objects they are talking about. The countable axiom of choice might be talking about countable "set" of subsets of natural numbers not general sets.
In summery,
remember that there is not a constructive mathematics, there are a many constructive mathematics, and they disagree about the axioms,
be careful when combining constructive axioms from different constructive theories, understand what kind of objects they are really taking about (what information is given when an object is given?) and understand what is the justification for constructiveness of the axiom about those objects, then check if that justification still applies to the objects in the theory you want to add the axiom to it.