I'm playing with the proof assistant Coq (which assumes ex falso quodlibet, but neither double negative or tertium non datur) and can easily prove (A∨¬A) ⇒ (¬¬A→A). I can not prove (¬¬A→A) ⇒ (A∨¬A), and neither can "tauto" of Coq (although the statement is true). tauto can prove (¬¬A→A) ⇔ ((¬A→A)→A) (although I don't have any idea how it does it for either direction, after prove\_imp there is no cut - uhm, I'm just a beginner, does anyone know how to print out the steps tauto takes?). At least I want to know the "official" truth, so here my question: Let P1 and P2 be any two statements that are true in standard but not in minimal logic (plus ex falso), i.e. ¬¬P1 and ¬¬P2 are tautologies. Does always P1⇔P2 hold? If not, does always at least one direction P1⇒P2 or P2⇒P1 hold?  

Relevant: <https://arxiv.org/abs/1304.0272>



Glivenko's theorem implying all "weakly true" statements created equal?
No.


For question 1, let
$$P\_1 = A \vee \neg A,$$
$$P\_2 = \neg\neg A \vee \neg A.$$
Their double negations are both tautologies, but $P\_1$ and $P\_2$ are not equivalent.


For question 2, let
$$P\_1 = (A \wedge \neg\neg B) \vee (A \wedge \neg B) \vee \neg A,$$ 
$$P\_2 = (\neg\neg A \wedge B) \vee (\neg\neg A \wedge \neg B) \vee \neg A.$$ 
Their double negations are both tautologies, but neither $P\_1$ nor $P\_2$ implies the other.


