8
$\begingroup$

Does the following equivalence

$$\lnot \lnot (A \lor B) \leftrightarrow (\lnot \lnot A \lor \lnot \lnot B)$$

hold in propositional intuitionistic logic? And in propositional minimal logic? (In propositional classical logic this is obvious since $A \leftrightarrow \lnot\lnot A$ is classically provable.)

Actually I have a proof that $(\lnot \lnot A \lor \lnot \lnot B) \to \lnot \lnot (A \lor B)$ holds in propositional minimal logic, so I'm interested in the converse implication:

$$\lnot \lnot (A \lor B) \to (\lnot \lnot A \lor \lnot \lnot B)$$

If it is minimally or/and intuitionistically provable, I would like a (reference to a) direct proof in natural deduction-style.

| cite | improve this question | |
$\endgroup$
  • $\begingroup$ Can you post axiom sets/rules of inference here? I know I can find intuitionistic axioms which seem standard, but I'm not so sure about minimal logic. $\endgroup$ – Doug Spoonwood Nov 10 '15 at 16:13
  • 1
    $\begingroup$ @DougSpoonwood: The list of axioms for (first-order and then, in particular, propositional) intuitionistic logic is available for example here. The list of axioms for (first-order and then, in particular, propositional) minimal logic is just obtained by the list above removing the axiom $\lnot A \to (A \to B)$ (ex-falso-quodlibet). However, I would prefer a direct proof in natural deduction-style (if any), if it is possible. $\endgroup$ – Taroccoesbrocco Nov 10 '15 at 16:27
  • 2
    $\begingroup$ @Taroccoesbrocco A good rule of thumb is that to prove a disjunction intuitionistically, you'll need to be able to prove one of its disjuncts. (I'm excluding cases like $A \to (B \lor C)$ (where you could try to prove $A$ first, and then use conditional elimination) and $A \land (B \lor C)$ (where you could use conjunction elimination).) From the left side, I don't think that you can infer either $\lnot\lnot A$ or $\lnot\lnot B$, so I don't think you'll be able to get the right side. You can get from the right side to the left, though (as you've shown). $\endgroup$ – Joshua Taylor Nov 10 '15 at 17:35
5
$\begingroup$

$\lnot \lnot (A \lor B) \to (\lnot \lnot A \lor \lnot \lnot B)$ is not intuitionistically acceptable. One way of seeing this is by considering the Heyting algebra whose elements are the open subsets of the unit interval $[0, 1] \subseteq \Bbb{R}$, with $A \lor B = A \cup B$, $A \to B = \mathsf{int}(A^c\cup B)$ and $\bot = \emptyset$ (see https://en.wikipedia.org/wiki/Heyting_algebra). In this Heyting algebra, $\lnot\lnot A$ is the interior of the closure of $A$ and $A \to B$ is $\top$ iff $A \subseteq B$. Hence if $A = [0, 1/2)$ and $B = (1/2, 1]$, $\lnot \lnot (A \lor B) = [0, 1]$ while $\lnot \lnot A \lor \lnot \lnot B = [0, 1] \mathop{\backslash} \{1/2\}$ and $\lnot \lnot (A \lor B) \to (\lnot \lnot A \lor \lnot \lnot B)$ is not $\top$.

| cite | improve this answer | |
$\endgroup$
  • 3
    $\begingroup$ Just in case the OP is more familiar with Kripke models than with topological ones, here's a Kripke counterexample. The underlying partially ordered set consists of $a,b,c$ with $c<a$ and $c<b$ while $a$ and $b$ are incomparable. Let $A$ be true only at $a$ and let $B$ be true only at $b$. Then $\neg\neg A$ and $\neg\neg B$ are also true only at $a$ and $b$, respectively, so their disjunction is true at $a$ and $b$ but not at $c$. On the other hand, $\neg\neg(A\lor B)$ is true everywhere, including $c$. $\endgroup$ – Andreas Blass Nov 10 '15 at 20:42
  • $\begingroup$ @RobArthan: Thank you, your answer is very clear! $\endgroup$ – Taroccoesbrocco Nov 10 '15 at 21:10
  • $\begingroup$ @AndreasBlass: also your answer is very clear, thank you! $\endgroup$ – Taroccoesbrocco Nov 10 '15 at 21:15
1
$\begingroup$

By substituting ¬A for B in ¬¬(A∨B)→(¬¬A∨¬¬B) we can easily derive (¬¬A∨¬A) which is certainly not intuitionistically acceptable. Hence ¬¬(A∨B)→(¬¬A∨¬¬B) is also not acceptable.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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