I think in your first paragraph you're confusing intuitionistic logic and linear logic --- intuitionistic logic still lets you "clone" and "delete" propositions freely.
The second paragraph is somewhat true --- at its base, the modern use of the term "intuitionistic logic" refers merely to not accepting the law of the excluded middle. However, there are varieties of intuitionism that are very, very inconsistent with classical logic, like those adopting the idea that "every function between real numbers is continuous".
When you separate internal and external logic, for example in topos theory, the external logic is still classical.
For example, any topos has internal logic on subobjects of at least a Heyting algebra. In some cases you specialise to a Boolean algebra.
However, when you write things down such as your arguments around functors and constructions, you argue according to classical mathematics externally. When you enter into the category (which is chosen not to be Boolean) and argue on the subobject structure, then you are entering intuitionistic logic. This is what I mean when I say that classical logic can be argued to have intuitionistic logic embedded in it.
The cardinality of the reals being equal to the cardinality of the naturals is then something you have to construct inside the topos. So you need to construct along the spirit of a natural numbers object (perhaps a real numbers object) and then use the internal logic to argue about continuity.
I think you are right about the comment about linear logic. I must be confusing A U A with A U ^A.
I checked the paper that I was thinking about and the condition that I saw there is distributivity being dropped rather than double negation being dropped.
The second paragraph is somewhat true --- at its base, the modern use of the term "intuitionistic logic" refers merely to not accepting the law of the excluded middle. However, there are varieties of intuitionism that are very, very inconsistent with classical logic, like those adopting the idea that "every function between real numbers is continuous".