0
$\begingroup$

Please show that $\lnot(a\vee b) = \lnot a\wedge \lnot b$ for any Heyting algebra. [Corrected: exchanged $\vee$ and $\wedge$.]

(I prefer to receive the answer is dual terminology, that is about co-Heyting algebras.)

$\endgroup$
  • $\begingroup$ Are you sure about the question? it is not a theorem in Heyting Logic $\endgroup$ – Willemien Aug 29 '13 at 9:35
  • $\begingroup$ @Willemien: It is exercise (i) in I.1.11 of "Stone Spaces" book $\endgroup$ – porton Aug 29 '13 at 9:43
  • $\begingroup$ @Willemien: I confused $\vee$ and $\wedge$. Sorry $\endgroup$ – porton Aug 29 '13 at 9:44
  • $\begingroup$ It seems that there is an error in this question: see groups.google.com/forum/#!topic/sci.math/Gqoyc_2IdYM $\endgroup$ – porton Aug 29 '13 at 11:04
  • $\begingroup$ See here for the correctness of de Morgan's laws in intuitionistic logic. $\endgroup$ – Zhen Lin Aug 29 '13 at 11:19
4
$\begingroup$

I will prove that the corresponding formulae are logically equivalent in intuitionistic propositional logic.

First, suppose $\lnot (a \lor b)$; we wish to prove $\lnot a \land \lnot b$. Assume $a$. Then $a \lor b$, which is a contradiction, so we discharge $a$ and deduce $\lnot a$. Similarly, we may deduce $\lnot b$. Thus $\lnot a \land \lnot b$.

Conversely, suppose $\lnot a \land \lnot b$. Assume $a \lor b$. Since $\lnot a$ and $\lnot b$, we use $\lor$-elimination to deduce that $a \lor b \to \bot$, i.e. $\lnot (a \lor b)$.


Here is the proof spelled out in the language of Heyting algebras. To show that $x = y$ in a poset, it is enough to show that both $x \le y$ and $y \le x$.

First, notice that $a \land \lnot (a \lor b) \le (a \lor b) \land \lnot (a \lor b) \le \bot$, so $a \land \lnot (a \lor b) \le \bot$, so $\lnot (a \lor b) \le \lnot a$. Similarly, $\lnot (a \lor b) \le \lnot b$. It follows that $\lnot (a \lor b) \le \lnot a \land \lnot b$.

On the other hand, $\lnot a \land \lnot b \land (a \lor b) = (\lnot a \land \lnot b \land a) \lor (\lnot a \land \lnot b \land b)$ by the distributive law, and $\lnot a \land \lnot b \land a = \lnot a \land \lnot b \land b = \bot$, so $\lnot a \land \lnot b \land (a \lor b) = \bot$. Thus, $\lnot a \land \lnot b \le \lnot (a \lor b)$.

$\endgroup$
  • $\begingroup$ I don't understand something: Do you use contradiction in intuitionistic propositional logic? $\endgroup$ – porton Aug 29 '13 at 11:32
  • $\begingroup$ Sure. That's the only way to prove a negative. $\endgroup$ – Zhen Lin Aug 29 '13 at 12:38
  • $\begingroup$ I'm finally confused. Could you clear? (especially whether the original formula is true in all Heyting algebras) $\endgroup$ – porton Aug 29 '13 at 12:43
  • $\begingroup$ Yes, the original equation is true in all Heyting algebras. $\endgroup$ – Zhen Lin Aug 29 '13 at 12:45
  • 2
    $\begingroup$ The definition of $\lnot a$ is $a \to \bot$, so by the deduction theorem, to prove $\lnot a$, it is enough to show that a contradiction follows from $a$. Now, once we have shown that two formulae are logically equivalent in propositional intuitionistic logic, it follows that the corresponding equation is true in all Heyting algebras. $\endgroup$ – Zhen Lin Aug 29 '13 at 12:55

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.