Is equality $\neg \neg$-stable?

Question

In an essay by Andrej Bauer, I read the following statement : "A statement built from the universal quantifier ∀, conjunction ∧, implication ⇒, and numerical equality = is ¬¬-stable, as can be easily verified"

I could of course verify that the set of $\neg\neg$-stable sentences (i.e. sentences $\varphi$ such that $\vdash \neg\neg\varphi \to \varphi$ is intuitionistically derivable) is stable under these constructions ($\forall, \land, \implies$), it's relatively easy; but I could not prove that for terms $s,t$, $\vdash \neg\neg(s=t) \to s=t$ was actually derivable, and it actually seemed wrong, because of what follows.

Indeed it would be surprising if it were true because right after it, when talking about synthetic differential geometry, he notes that an infinitesimal $d$ ($d^2= 0$) is not unequal to $0$, i.e. $\neg\neg(d=0)$ holds, but obviously if $d=0$ held it would be uninteresting for synthetic differential geometry. So I'm guessing there's something I misunderstood about the first statement. If so, what does it mean more precisely, what's wrong with my understanding ?

ADDED: Here's a link to the paper in question, the quote is from a note on page 3.

As suggested in the comments, the problem is probably related to the adjective "numerical" in the quote, but I can't really make sense of it. Note that this isn't about Heyting arithmetic (where $m=n \lor m\neq n$ is provable by induction) since the statement here is applied to the laws of physics, laws that usually require at least the real numbers

Answer 1

Andrej was referring to equality on real numbers, since he was referring to physical laws, which are usually formulated using real numbers. It's true that equality cannot be shown to be stable in general, but it is stable for real numbers.

Here is a bit more background.

• Equality on natural numbers is stable, even decidable, that is for any given natural numbers $n$ and $m$, we have $n = m$ or $\neg(n = m)$. This can be proven by induction.
• Equality on rational numbers is decidable.

• Equality on real numbers can fail to be decidable, constructively. (The intuition for this failure is: Given a number $x$ in the form of a machine which can output more and more digits of $x$, it's not possible to determine in finite time whether $x = 0$ or $\neg(x = 0)$, because $x$ might start like $0.00000000$. This intuition can be made precise using realizability theory or the effective topos. If we would allow machines to run for longer than infinity, the situation is different. See these slides for more.)

  However equality on real numbers is still stable. This has a deeper reason: The fundamental relation on real numbers is not actually equality, but apartness, written $\#$. Numbers are apart from each other if and only if they have a positive distance (which is if and only if a rational number fits strictly inbetween the given numbers). It then turns out that $x = y$ iff $\neg(x \# y)$. (We say that the apartness is tight.) Hence $\neg\neg(x = y)$ is $\neg\neg\neg(x \# y)$, and three negations can always be simplified to one.

• Equality on complex numbers is stable but might fail to be decidable, for the same reasons.
• Equality on algebraic numbers is (stable and) decidable! The extra information contained in a witness of algebraicity (a monic polynomial with rational coefficients) suffices to make the case distinction.