Three questions about intuitionistic logic If $A$ is a theorem of classical logic, is it the case that $\neg \neg A$ is a theorem of intuitionistic logic? And secondly, if $A  \to B$ is a theorem of classical logic, is $\neg B \to \neg A$ a theorem of intuitionistic logic. Third, is $\neg A \vee \neg \neg A$ a theorem schema of intuitionistic logic?
 A: The answer to the first question, 

If $A$ is a theorem of classical logic, is it the case that $\lnot \lnot A$ is a theorem of intuitionistic logic?

is "yes" when we are talking about propositional logic. This is a very classical result of Glivenko. 
For first-order logic, it is not enough to merely preface the formula with two negations. However, there are a number of so-called negative translations that accomplish a similar thing in a more complicated way: to each first-order formula $\phi$ is associated another formula $\phi^*$ such that if $\phi$ is provable in classical first-order logic then $\phi^*$ is provable in intuitionistic first-order logic. 
This use of negative translations is very well studied in proof theory, and is a standard method that has become commonly used. However, there is no truly accessible literature on proof theory. The Wikipedia article linked above has some graduate-level references. 
A: For an intuitionistically valid proof of $A \to B \vdash \lnot B \to \lnot A$ with Natural Deduction :
1) $A \to B$ --- premise
2) $\lnot B$ --- assumed [a]
3) $A$ --- assumed [b]
4) $B$ --- from 1) and 3) by $\to$-elimination
5) $\bot$ --- from 2) and 4) by $\to$-elimination : $\lnot B$ is an abbreviation for : $B \to \bot$ 
6) $\lnot A$ --- from 3) and 5) by $\to$-introduction, discharging [b]

7) $\lnot B \to \lnot A$ --- from 2) and 6) by $\to$-introduction, discharging [a].

Nowhere in the derivation we have used Exluded Middle, nor Double Negation; thus, the proof is intuitionistically valid.
Now the issue is :

if $\vdash_K A \to B$, then $\vdash_J ¬B \to ¬A$ or not ?

Whe can apply the Gödel–Gentzen translation to $⊢_K A \to B$ and we have that : $⊢_J ¬¬A \to ¬¬B$.
But this is simply a "double contraposition"; thus, it seems that $⊢_J ¬B \to ¬A$.

Regarding $\lnot A \lor \lnot \lnot A$, it is not intuitionistically provable.
The counter-example with Kripke semantics is a structure with three nodes : $0,1,2$ such that $0 \le 1$ and $0 \le 2$, where $A$ holds only in $1$ (i.e. $1 \Vdash A$).
We have that $2 \Vdash \lnot A$, and thence, by the semantical clause : $k \Vdash \lnot A$ iff for all $k' \ge k : (k' \nVdash A)$ :

$0 \nVdash \lnot \lnot A$.

But since $1 \Vdash A$, also $0 \nVdash \lnot A$, and thus :


$0 \nVdash \lnot A \lor \lnot \lnot A$.


