A few questions about intuitionistic mathematics I have to write a paper on Intuitionism for my Philosophy of Science class and I'm struggling with a few concepts I have encountered in my self-study.
The (intuitive) characterization of valid intuitionistic inferences I am familiar with is given by the BHK interpretation. Let $\neg$ denote the strong negation as defined in H4, and $\sim$ denote the weak negation (i.e. $\sim P$ means no proof of $P$ has been found). This is probably a lot to ask for in only one question, but I'll give it a shot:


*

*In this book it says that Gödel proved that every theorem of PA which does not involve the symbols "$\vee$" or "$\exists$" is also a theorem of HA, and given that every statement in classical logic is classically equivalent to one that does not contain those two symbols, we have that every theorem of PA has a version which is acceptable to the intuitionist. 


*

*Is this not true in general, for example when dealing whith real numbers? 

*Isn't it true that, in general, if a statement $P$ is classically valid, then $\neg \neg P$ is intuitionistically valid?


*I was also wondering about which formulations of the Axiom of Choice are acceptable in an intuitionistic framework. The main result in this context is Diaconescu's Theorem, which states that in constructive set theory the full version of AC cannot hold, as it would imply excluded middle.


*

*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 \vee \neg P$? In the same book I was referring to before it says that $$ b_n = \begin{cases} 0 \ \forall n \quad \text{if Goldbach's conjecture is true} \\ 1 \ \forall n \quad \text{if Goldbach's conjecture is false} \end{cases}  $$ "does not define a sequence at all, because it does not tell us how to computes its terms" (page 126). 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?

*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?



Unfortunately, I haven't got the background in Logic and Set Theory to delve into too much technical detail, so I'm getting my information from not-too-technical philosophy books and Wikipedia and Standford Encyclopedia entries. If someone could explain in simple terms what I'm getting wrong that would be great. 
This question came out even longer than I had planned and, of course, partial answers are also very much appreciated. Thank you very much for any help.
21/05/12 I got two very helpful answrs and, although I'm going to accept Kaveh's one since it addresses both 1. and 2., Carl's one was crucial to my understanding 2. I hope these answers get the upvotes they deserve, thank you both!
 A: 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. 
A: 
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.
