3
$\begingroup$

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

$\endgroup$
4
  • $\begingroup$ I'm not sure what you're asking, but it seems like you might be interested in intermediate logics: en.wikipedia.org/wiki/Intermediate_logic $\endgroup$ Oct 8, 2016 at 20:30
  • $\begingroup$ Could you please explain what do you mean by standard logic? Answers are obvious yes for classical and (almost as) obvious no for intuitionistic logic $\endgroup$ Oct 8, 2016 at 20:39
  • 1
    $\begingroup$ You write that tauto cannot prove ¬¬A -> A => (A v ¬A). This is because it is false in intuitionistic logic. The open sets of topological spaces give an interpretation of intuitionistic logic, where or and and are given by union and intersection, and ¬ is interpreted as the interior of the complement. Then (0,1) in the reals gives a counterexample, ¬¬(0,1) = (0,1) but (0,1) v ¬(0,1) is not equal to R. In fact for topological spaces the statement you suggested is equivalent to "all regular open sets are clopen". $\endgroup$ Oct 9, 2016 at 13:34
  • $\begingroup$ As Robert said, the implication $(\neg\neg A \Rightarrow A) \Longrightarrow (A \vee \neg A)$ is not provable in intuitionistic logic. However the related formula $(\forall A{:}\,(\neg\neg A \Rightarrow A)) \Longrightarrow (\forall A{:}\,(A \vee \neg A))$ is. This is because we have $\neg\neg(A \vee \neg A)$. $\endgroup$ Dec 2, 2016 at 18:52

1 Answer 1

3
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Nice example. Seems I just misinterpreted the ArXiv reference I gave. $\endgroup$ Oct 9, 2016 at 17:28
  • 2
    $\begingroup$ There are also infinitely many one variable cases for question 2 - just take any incomparable pair above level 2 of the Rieger-Nishimura lattice, e. g. $\neg A\lor\neg\neg A$ and $\neg\neg A\to A$ $\endgroup$ Oct 11, 2016 at 5:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.