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.