I tried to prove that $\lnot(a \neq b)$ doesn't imply $a=b$ in intuitionistic logic.
I used LEM for this proof:
$\lnot(a \neq b)$ :
$a=b$ $\lor$ $a \neq b$
Let $a=b$. Then statement $a \neq b$ is false and we use statement $\lnot(a \neq b)$. For this statement we don't have that $a=b$ but we have values of $\lnot(a \neq b)$ when it's true.
Is it correct proof?
If it's not correct proof then how to prove that $\lnot(a \neq b)$ doesn't imply $a=b$ in intuitionistic logic?
Thanks.
I'm giving you a slow rundown for how to break this sort of implications by minimal example and end in a semantic "why".
That line of reduced-to-the-bone counter example works with many theories (you didn't specify much, apart from it having equality). I'm using set theoretic equality and subset comprehension here, but you can do the same shebang using strict equality of sequence definitions instead. Something similar would be to talk about the apartness of some particularly Cauchy reals. In these contexts, you can pick some unfriendly ($\Pi_1^0$-) proposition $U:=\big(\forall n.f(n)=0\big)$ and bake it into your mathematical objects (sets, real numbers). Demanding your proof calculus is more explicit than classical logic, you run into those unresolvable double-negations.
In logic, I'm going to make use of the fact that intuitionistic logic alone never disproves a theorem of classical logic. What's more, note that $\neg \neg (P\lor \neg P)$ is merely the special case of $([P\lor [P\to Q]]\to Q)\to Q$ for $Q=\bot$, and intuitionistic logic proves this: Assuming that $[P\lor [P\to Q]]$ proves $Q$, we have that in particular that $P$ proves $Q$ (which is to say $P\to Q$ holds). And so using the assumption again now with this implication, we got $Q$. QED. This argument made basic use of $\to$ and used minimal assumptions on how $\lor$ works as antecedent.
In set theory, I'm going to make use of $a\subset b$, standing for $\forall (z\in a). (z\in b)$. Adopting equality through set extensionality (two sets are the same if they exactly share their elements), two sets $a$ and $b$ have $a=b$ iff $(a\subset b)\land (b\subset a)$. Further, $0:=\emptyset$ and $1:=\{0\}$ as usual.
Let $U$ be some sentence independent in some set theory, meaning neither $U$ nor $\neg U$ can be proven. (Say the arithmetized consistency claim of a consistent and sound theory.) Assume further that the theory has the disjunction property, meaning that if it proves a disjunction $A\lor B$, then it also proves the proposition $A$ or proves the proposition $B$. With this, the theory can't prove $U\lor \neg U$. (So that theory is necessarily not classical btw.) But given what we just saw above, we grant that it's double negation is provable.
Say the theory allows for subset comprehension with this disjunction (that's not much to ask) and define the subset $1_U:=\{x\in 1\mid U\lor \neg U\}$. If it should need a proof, here's how $1_U\subset 1$ indeed: Note that the sentence $z\in 1_U$ just means $z=0\land (U\lor \neg U)$. For any $z$, by left $\land$-elimination we see that the proposition $z\in 1_U$ implies the proposition $z=0$, which also means $z\in 1$.
Given $0=0$ holds trivially, you similarly find that if you write down what $0\in 1_U$ means, you're left with $U\lor \neg U$. That is to say, using comprehension, we crafted an unprovable membership statement $0\in 1_U$. But the latter may also be expressed as $\forall (z\in 1). (z\in 1_U)$, which is to say $1\subset 1_U$ and so we got an unprovable subset statement. Given the extensional definition of equality, we arrived at the insight that also $1=1_U$ is equivalent to the unprovable (and classically trivial) $U\lor \neg U$.
It's not too hard to understand what just happened: In set theory, given a member $s\in C$ in a set $C$, to prove $s$ is also a member of a subset $D:=\{x\in C\mid W(x)\}$ of $C$, where $W(x)$ is some predicate, we need to validate the proposition $W(s)$. Consider the case where $C$ is a classroom of 20 students and $V(x)$ means "$x$ is vaccinated" and $W(x):=V(x)\lor\neg V(x)$. In the classical reading, this set $D:=\{x\in C\mid W(x)\}$ denotes "the subset of students which are vaccinated or not vaccinated", and $C=D$ is trivial. In the constructive reading, that same set denotes "the subset of students which we can certify (verify) to be vaccinated or certify (verify) to be not vaccinated" and to claim $C\subset D$ is to say that for each student you got some certificate. It may not be possible to establish the latter, in which you fail to prove $C=D$. Albeit in this semantic example as given, it's also reasonable not to rule getting all the certificates, at one point.
As per my construction, the subset $1_U:=\{x\in 1\mid U\lor \neg U\}$ can never be proven to equal $1$, but provably the negation of this equality is false as well.