If two things are not equal, are they equal?

Question

If there are two meanings in Agda or some other obsessive language, you can prove that v₁ not equal to v₂ , can you prove v₁ equals v₂ ?

How, is there a function like ((v₁ ≡ v₂ → ⊥) → ⊥) → v₁ ≡ v₂ ?

This is similar to something that can be added as an axiom if it cannot be proved, since there can be no more than one value v₁ ≡ v₂ .

Interestingly, double negation ( (a → ⊥) → ⊥ ) forms monad . Usually you cannot extract values ​​from it, but you can get certain values ​​from it, for example ⊥ (if you get a contradiction in the classical logical monad, you have a contradiction). I was wondering if equality could be achieved.

Answer 1

I think the law is not provable in Agda or Kok.

Roughly, we have only one hypothesis

 (v1 = v2 -> False) -> False 

and we need to prove the thesis v1 = v2 .

Consider the inconclusive evidence of what is in the evidence-based system of evidence. What will be the last rule?

This cannot be the introduction of v1 = v2 , because Refl does not have this type ( v1,v2 are various variables).

Thus, this should be the 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 indeed provable, we must also have

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

from which it is deduced

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

which is equivalent

 |- v1 = v2 -> False 

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

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

which is clearly wrong.

On the other hand, I believe that Agda / Coq / ... complies with the Law of the Excluded Middle, which implies the proposed law. Consequently, the law cannot break the sequence.

Answer 2

The doubling of double negation is unprovable in the theory of the intuitionistic type, as presented here, but its negation is also unprovable, so it can be assumed consistently.

However, although classical axioms are not provable for all types, they are provable for decidable types. Decidable types are those that are supposedly inhabited or uninhabited:

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

Given Decidable A , you can implement the double negation exception on A : just matching the pattern on Either A (A -> False) , and if we get A , then we finish, 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 provable if (ab : A) -> Decidable (a = b) , i. e. A has a decidable equality.

As for the continuation monad (A -> False) -> False , when we work inside this monad, we get some form of classical reasoning, since the monadic connection here corresponds to the "quaternary" elimination of negation, therefore not (not (not (not A))) -> not (not A)) . We can also use callCC , which complies with Pierce's law , another classic statement.

An interesting remark about this: we can take any classical proof, raise all sentences to Cont False (in other words, double their negation), and we will get the corresponding constructive proof proving the double negation of the original sentence. This means that constructive logic can prove that the classical logic can modulo classical logical equivalence, since a sentence and its double negation are classically equivalent.