If two things are not not equal, are they equal?

Question

If two values in Agda, or some other dependently typed language, you can prove that v₁ is not not equal to v₂, can you prove v₁ equals v₂?

Like, is there a function of the type ((v₁ ≡ v₂ → ⊥) → ⊥) → v₁ ≡ v₂?

This seems like something that is safe to add as axiom if it can't be proven, since there can be at most one value of v₁ ≡ v₂.

A reason this is interesting is that double negation ((a → ⊥) → ⊥) forms a monad. Usually you can't extract values from it, but you can certain values, like ⊥ from it (if you derive a contradiction in classical logic monad, you have a contradiction). I was wondering if equality was a thing that could be extracted.

Answer 1

Double negation elimination is unprovable in intuitionistic type theory, as chi presented here, but its negation is also unprovable, so it can be assumed consistently.

However, while classical axioms aren't provable for all types, they are provable for decidable types. Decidable types are those which are provably inhabited or uninhabited:

Decidable : Type -> Type
Decidable A = Either A (A -> False)

Given Decidable A, one can implement double negation elimination on A: just pattern match on Either A (A -> False), and if we get an A, then we're done, if we get A -> False, then we apply (A -> False) -> False and use ex falso.

As a special case ((a = b -> False) -> False) -> a = b is provable if (a b : A) -> Decidable (a = b), i. e. A has decidable equality.

As to the (A -> False) -> False continuation monad, when we work inside this monad we get some form of classical reasoning, since monadic join here corresponds to "quadruple" negation elimination, so not (not (not (not A))) -> not (not A)). We can also use callCC, which corresponds to Peirce's law, another classical statement.

There's an interesting observation about this: we can take any classical proof, lift all propositions to Cont False (in other words, double negate them), and we get a corresponding constructive proof that proves the double negation of the original proposition. This means that constructive logic can prove everything classical logic can, modulo classical logical equivalence, since a proposition and its double negation are classically equivalent.

Answer 2

I think that law is not provable in Agda or Coq.

Roughly, we only have one hypothesis

(v1 = v2 -> False) -> False

and we need to prove the thesis v1 = v2.

Consider a cut-free proof of that in a sequent-based proof system. What would the last rule be?

It can not be an introduction of v1 = v2, because Refl has not that type (v1,v2 are distinct variables).

So, it must be an elimination of the hypothesis, i.e.

H1: (v1 = v2 -> False) -> False |- v1 = v2 -> False
H2: (v1 = v2 -> False) -> False , False |- v1 = v2
---------------------------------------------------  (->E)
(v1 = v2 -> False) -> False |- v1 = v2

However, if H1 is indeed provable, we must also have

(v1 = v2 -> False) -> False |- False

from which we derive

|- ((v1 = v2 -> False) -> False) -> False

which is equivalent to

|- v1 = v2 -> False

which is clearly not provable without any other assumptions on v1,v2. Indeed, otherwise we could generalize that to

|- forall v1 v2, v1 = v2 -> False

which is clearly wrong.

On the other hand, I believe that Agda/Coq/... are consistent with the Law of Excluded Middle, which implies the proposed law. Hence, the law can not violate consistency.