I almost convinced myself that ¬¬A ⇒ A is reasonable. Suppose one had a λ-term of type (A ⇒ ⊥) ⇒ ⊥ (i.e. of type ¬¬A). What must this λ-term look like? Well, it must return something of type ⊥. Assuming our system is consistent then there is no way to construct ⊥ so it must use the its parameter f of type A ⇒ ⊥ to get a ⊥. Therefore the λ-term must look something like λf:A ⇒ ⊥ . f e for some λ-term e of type A. Hence, every time there is a λ-term of type ¬¬A, there exists (as a sub-expression) a λ-term of type A. One concludes that adding ¬¬A ⇒ A as an axiom would be as reasonable as adding the axiom that says that every function is continuous.
The above reasoning is clearly flawed because there is a λ-term of type ¬¬(((A ⇒ B) ⇒ A) ⇒ A) but there is no λ-term of type ((A ⇒ B) ⇒ A) ⇒ A. The reason is because the (sub-)expression e in the above argument has access to the parameter f. As strange as it may sound, it is possible for the function f to use itself to make the parameter it needs to generate ⊥. This is exactly what happens in the proof of ¬¬(((A ⇒ B) ⇒ A) ⇒ A).
Suppose one had a function f of type (((A ⇒ B) ⇒ A) ⇒ A) ⇒ ⊥. Because ⊥ implies anything, there is a function g of type ⊥ ⇒ B. Also it is easy to find a function h of type A ⇒ ((A ⇒ B) ⇒ A) ⇒ A. So one can compose these three functions together to get g ∘ f ∘ h of type A ⇒ B. Now with this in hand, one can make a function of type ((A ⇒ B) ⇒ A) ⇒ A. One takes a function s of type (A ⇒ B) ⇒ A, and applies our composition to it, resulting in s (g ∘ f ∘ h) of type A.
This is how one can use f to generate a parameter to apply to itself. To get ⊥ from f one can use the λ-term f λs:(A ⇒ B) ⇒ A . s (g ∘ f ∘ h). Notice how f is part of the term being passed into f.
This circularity of passing f into itself isn’t too troubling. There cannot be any functions of type (((A ⇒ B) ⇒ A) ⇒ A) ⇒ ⊥. Indeed that is the very thing being proved.