Is the following true?
- In a category whose internal logic does not support the law of excluded middle, the Dedekind real object can be proven externally to be nonisomorphic to the Cauchy real.
Can you show me such proof and/or explain to me why is that the internal logic being weaker serves as an obstruction to the existence of an isomorphism in a stronger logic?
I'll be extra happy if someone can explain to me the significance and "usage" of internal logic.
Actually, can I think about it this way: when one proves something, say the nonequivalence above, using an external logic, say the classical one, what one's actually doing is imposing a particular set-theoretic model to the theory of Dedekind and Cauchy reals, thus breaking some kind of "atomicity"/"model agnosticity"(?), and drawing a conclusion which is only true in the set-theoretic models? I.e. one of the advantages of the internal logics is "model agnosticity"?
This is emphatically not true. If we work constructively, we merely require the following choice principle: for all $f : 2 \times \mathbb{N} \to \mathbb{N}$, if $f$ is surjective, then there exists $g : \mathbb{N} \to 2 \times \mathbb{N}$ such that $f \circ g = 1_\mathbb{N}$. This choice principle is a very weak form of countable choice and is implied by the law of excluded middle.
So we could, for instance, take any model of $ZF + \neg AC$ (which is dramatic overkill). In this model, the Cauchy and Dedekind reals would coincide.
Edit: presheaf toposes satisfy countable choice, so in any presheaf topos (including those that don’t support excluded middle - that is, all presheaves over any non-groupoid category), the Dedekind and Cauchy reals coincide. So the fact that LEM fails does not necessarily mean that the Dedekind and Cauchy reals don’t coincide.