10
$\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.

$\endgroup$
3
  • $\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, 2015 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, 2015 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, 2015 at 17:35

3 Answers 3

Reset to default
6
$\begingroup$

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

$\endgroup$
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}$ under the subspace topology, 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$.

$\endgroup$
6
  • 4
    $\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, 2015 at 20:42
  • $\begingroup$ @RobArthan: Thank you, your answer is very clear! $\endgroup$
    – Taroccoesbrocco
    Nov 10, 2015 at 21:10
  • $\begingroup$ @AndreasBlass: also your answer is very clear, thank you! $\endgroup$
    – Taroccoesbrocco
    Nov 10, 2015 at 21:15
  • $\begingroup$ My topology is pretty bad, are you certain $\lnot \lnot (A \lor B) = [0, 1]$ ? I am getting $(0, 1)$ according to the definition of interior I'm finding. The third bullet point here: en.wikipedia.org/wiki/Interior_(topology)#Examples . Also how are you defining $\top$ ? Thanks $\endgroup$
    – DanielV
    Nov 9, 2021 at 7:41
  • $\begingroup$ I should have made it clearer that we are working with the subspace topology on $[0, 1]$ here. $[0, 1]$ is open in that topology. Hence $\mathrm{Int}([0, 1]) = [0, 1]$. $\top$ is the open set $[0, 1]$ (it's not open viewed as a subset of $\Bbb{R}$ but it is open in the subspace topology on $[0, 1]$). $\endgroup$
    – Rob Arthan
    Nov 9, 2021 at 21:10
3
$\begingroup$

Before getting down to technicalities, in cases like this it is worth first thinking informally. So, should we expect $\lnot \lnot (A \lor B) \to (\lnot \lnot A \lor \lnot \lnot B)$ to hold intuitionistically, given an informal BHK-style understanding of the connectives? If we are in a position to rule out being able to refute $A \lor B$, does that mean we must already be in a position to rule out being able to refute $A$ or alternatively in a position to to rule out being able to refute $B$?

Intuitively(!) not. So that gives us a motivation for expecting the given wff to fail as an intuitionistic theorem, and hence to look for a Kripke counter model. And as Andreas Blass shows, once you start looking for a suitable model, given the constraints, you'll quickly land on one!

$\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.