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.

> But remember that (as far as I know) you can do intuitionist mathematics in classical mathematics, but not the other way around.

There are a number of embeddings of classical logic into intuitionistic logic. The most popular/obvious is the double-negation embedding that maps a proposition to its double negation.

You shouldn't be mapping propositions, you should be mapping theories. See my comment below on the internal logic of a topos.

What you are referring to as a proposition is an element of the Heyting algebra or the Boolean algebra.

Why do you think the same thing doesn't apply to theories? Since you mention topos theory, the double-negation topology is actually a basic construction in topos theory, used to construct a dense Boolean subtopos of a given topos.

You can always generate substructures with closure properties. The subobject structure comes from all the subobjects—so it is the default logic of the topos. Of course you can do the same thing here as you mentioned since it is a Heyting algebra at the least.

My point is something else: I don't know of a way to have a intuitionistic exterior logic and a classical internal logic.

It's the other way around, classical logic is a restriction of intuitionistic logic that arises when you affirm the Law of Excluded Middle.

I think you're both right in a certain sense. The set of provable statements in intuitionist logic is a subset of what is provable in classical logic, which is what I believe the parent was referring to.

You're certainly right that any constructively provable statement is classically provable, that follows from intuitionism/constructivism generalizing classical logic. But I don't see how we could interpret the following to mean that.

> you can do intuitionist mathematics in classical mathematics