3 ms·
> 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 embedd
by cwzwarich 7y ago
> 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.
- mikorym 7y agoYou 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.
- cwzwarich 7y agoWhy 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.
- mikorym 6y agoYou 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.