Why is $ (a \lor b \lor c) \oplus ( a \lor b)$ equivalent to $\lnot a \land \lnot b \land c$?

Question

I'm having a hard time understanding why $(a \lor b \lor c) \oplus (a \lor b)$ (where $\oplus$ stands for XOR) is equivalent to $\lnot a \land \lnot b \land c$ in propositional logic. Any help would be appreciated!

Answer 1

Using $\oplus$ for XOR, $\lor$ for OR, $\land$ for AND, and $\lnot$ for NOT

We know that $p\oplus q ~\equiv~ \lnot (p\land q)\land(p\lor q)$, as its the definition of XOR.

Hence $$\begin{align}(a\lor b\lor c)\oplus(a\lor b)~&\equiv~ \lnot((a\lor b\lor c)\land(a\lor b))~\land~((a\lor b\lor c)\lor(a\lor b))\\ &~~\vdots\\ &\equiv \lnot a\land\lnot b\land c \end{align}$$

---

Or if you like: $(a\lor b\lor c)\oplus(a\lor b)$ is true exactly when either disjunction is true but not when both are. However $(a\lor b\lor c)$ is true then $a\lor b$ is, so $(a\lor b)$ cannot be true when the statement is.   Conversely, .... and so $(a\lor b\lor c)\oplus(a\lor b)$ is true when $\lnot a$, $\lnot b$, and $c$ are.

Thus: $\lnot a\land\lnot b\land c$ is true exactly when $(a\lor b\lor c)\oplus(a\lor b)$ is.

Answer 2

You can show this formally using Boolean algebra, or you can just think about this a little bit:

The XOR is true when exactly one of the sides is true, and the other one is false. Now, notice that if either $a$ or $b$ is true, then immediately both sides are true, and hence the XOR would not hold true. So, both $a$ and $b$ need to be false. But that means that the right side is false, meaning that the left side should be true, and given that $a$ and $b$ are both false, that works if (and only if ) $c$ Is true.

So, there you have it: the XOR statement is true if and only if $a$ and $b$ are both false, and $c$ is true.

Answer 3

For completeness, though perhaps not very helpful, here is a proof in about fifty lines of machine-checked Agda. Only the last thirteen lines are really contentful, and they were mostly generated interactively by the compiler. Try it here!

data False : Set where

infix 15 _∨_∨_
data _∨_∨_ (A B C : Set) : Set where
  inA : A → A ∨ B ∨ C
  inB : B → A ∨ B ∨ C
  inC : C → A ∨ B ∨ C

infix 15 _&_&_
record _&_&_ (A B C : Set) : Set where
  field
    one : A
    two : B
    three : C

infix 10 _||_
data _||_ (A B : Set) : Set where
  inl : A → A || B
  inr : B → A || B

infix 15 _&&_
record _&&_ (A B : Set) : Set where
  constructor _,,_
  field
    fst : A
    snd : B

exFalso : {A : Set} → False → A
exFalso ()

lemm1 : (a b c : Set) → (a ∨ b ∨ c) && ((a || b) → False) || ((a || b) && ((a ∨ b ∨ c) → False)) → (a → False) & (b → False) & c
lemm1 a b c (inl (inA x ,, snd)) = record { one = λ z → snd (inl z) ; two = λ z → snd (inr z) ; three = exFalso (snd (inl x)) }
lemm1 a b c (inl (inB x ,, snd)) = record { one = λ z → snd (inl z) ; two = λ z → snd (inr z) ; three = exFalso (snd (inr x)) }
lemm1 a b c (inl (inC x ,, snd)) = record { one = λ z → snd (inl z) ; two = λ z → snd (inr z) ; three = x }
lemm1 a b c (inr (inl x ,, snd)) = record { one = λ z → snd (inA z) ; two = λ z → snd (inB z) ; three = exFalso (snd (inA x)) }
lemm1 a b c (inr (inr x ,, snd)) = record { one = λ z → snd (inA z) ; two = λ z → snd (inB z) ; three = exFalso (snd (inB x)) }

lemm2 : (a b c : Set) → (a → False) & (b → False) & c → ((a ∨ b ∨ c) && ((a || b) → False)) || ((a || b) && ((a ∨ b ∨ c) → False))
lemm2 a b c record { one = fst ; two = fst2 ; three = snd } = inl (inC snd ,, help fst fst2)
  where
    help : (a → False) → (b → False) → (a || b → False)
    help nota notb (inl x) = nota x
    help nota notb (inr x) = notb x