Identity and substitution in Intuitionistic Logic

Question

I am a beginner in mathematical logic. I have a basic question about identity propositions in intuitionistic logic. For example, from $(*)$ and $(**)$: $$\Gamma\vdash a=b\quad\quad(*)\quad\quad\quad\quad\quad\quad\Gamma\vdash P(a)\quad\quad(**)$$ we shall deduce that $\Gamma\vdash P(b)$ also holds. But what if we have $(***)$? $$\Gamma\vdash \neg\neg(a=b)\quad\quad(***).$$ My question is: from $(**)$ and $(***)$, shall we conclude $\Gamma\vdash P(b)$ or $\Gamma\vdash\neg\neg P(b)$?

I don't know how to handle identity propositions because I have not met these in my textbook (von Plato, 2014). I would appreciate it a lot if anyone can answer my question and if possible provide some useful references for handling identity propositions. Thanks in advance!

Answer 1

I. From $\Gamma \vdash \neg\neg (a = b)$ and $\Gamma \vdash P(a)$, can we conclude $\Gamma \vdash P(b)$?

No. In the general case, $\Gamma \vdash P(b)$ does not follow from $\Gamma \vdash \neg\neg(a = b)$ and $\Gamma \vdash P(a)$.

Assume that we could conclude $\Gamma \vdash P(b)$ from $\Gamma \vdash \neg\neg(a = b)$ and $\Gamma \vdash P(a)$ for any context $\Gamma$ and formula $P$. Then in particular this would work for $P(x) \leftrightarrow a = x$. We'd have $\Gamma \vdash P(a)$ by the reflexivity of equality, so we would be able to conclude $\Gamma \vdash P(b)$, that is, $\Gamma \vdash a = b$. This would mean that equality is always stable under double-negation, i.e. that $\Gamma \vdash \neg\neg (a = b) \rightarrow a = b$ is provable in every context.

However, we can construct theories (models, topoi) where equality is not $\neg\neg$-stable, e.g. any model of Smooth Infinitesimal Analysis.

II. From $\Gamma \vdash \neg\neg (a = b)$ and $\Gamma \vdash P(a)$, can we conclude $\Gamma \vdash \neg\neg P(b)$?

We can always do this. The trick is to realize that double negation distributes over implication, even in intuitionistic logic.

Since $\Gamma \vdash a = b \rightarrow (P(a) \rightarrow P(b))$ is provable, we can introduce a double negation to get $\Gamma \vdash \neg\neg (a = b \rightarrow P(a) \rightarrow P(b))$, and distribute the double negations to get $\Gamma \vdash \neg\neg (a = b) \rightarrow \neg\neg P(a) \rightarrow \neg\neg P(b)$. Since we already know $\Gamma \vdash \neg\neg (a = b)$, we can conclude that $\Gamma \vdash \neg\neg P(a) \rightarrow \neg\neg P(b)$. Similarly, we already know $\Gamma \vdash P(a)$, from which it follows that $\Gamma \vdash \neg\neg P(a)$. Putting everything together we get $\Gamma \vdash \neg\neg P(b)$, which was to be shown.