$$
\forall x:
\left (
\substack{\text{student}\\\text{in class}} (x)
\implies
\exists a \exists b:
\left (
\substack{
\text{isMathClass}(a) \,\,\, \land\,\,\, \text{isMathClass}(b)\\\\
\land\,\,\text{Taken}(x,a)\,\, \land\,\, \text{Taken}(x,b)\,\,\,\,\,\,
}
\,\, \land \,\,
\forall c:
\left (
\substack{
\text{isMathClass}(c)\\
\land \quad c \neq a\\
\land \quad c \neq b
}
\implies
\lnot \text{Taken}(x,c)
\right )
\right )
\right )
$$
Reads: For every student $x$ in class, there exist math classes $a$ and $b$ such that $x$ has taken $a$, and $x$ has taken $b$, and for any other math class $c$ $(c\neq a, c\neq b)$, $x$ has not taken $c$.
To negate it, we put an negation sign at the start of the equation, and push it in.
When we push negation sign inwards:
- Forall $(\forall)$ changes to Exists $(\exists)$.
- Exists $(\exists)$ changes to Forall $(\forall)$ .
- And $(\land)$, Or $(\lor)$ change according to De-Morgan's law.
- Implication $(p \implies q)$ changes to $(p \land \lnot q)$
So, Negating the above expression, we get:
$$
\lnot \forall x:
\left (
\substack{\text{student}\\\text{in class}} (x)
\implies
\exists a \exists b:
\left (
\substack{
\text{isMathClass}(a) \,\,\, \land\,\,\, \text{isMathClass}(b)\\\\
\land\,\,\text{Taken}(x,a)\,\, \land\,\, \text{Taken}(x,b)\,\,\,\,\,\,
}
\,\, \land \,\,
\forall c:
\left (
\substack{
\text{isMathClass}(c)\\
\land \quad c \neq a\\
\land \quad c \neq b
}
\implies
\lnot \text{Taken}(x,c)
\right )
\right )
\right )
$$
Pushing the negation inwards, $\lnot \forall x: \,\, (\cdots)$ will become $\exists x: \,\, \lnot (\cdots)$. Note that the negation moves inwards.
$$
\exists x:
\lnot \left (
\substack{\text{student}\\\text{in class}} (x)
\implies
\exists a \exists b:
\left (
\substack{
\text{isMathClass}(a) \,\,\, \land\,\,\, \text{isMathClass}(b)\\\\
\land\,\,\text{Taken}(x,a)\,\, \land\,\, \text{Taken}(x,b)\,\,\,\,\,\,
}
\,\, \land \,\,
\forall c:
\left (
\substack{
\text{isMathClass}(c)\\
\land \quad c \neq a\\
\land \quad c \neq b
}
\implies
\lnot \text{Taken}(x,c)
\right )
\right )
\right )
$$
Now, we have to negate everything inside those big brackets!
The first thing inside is an implication.
Our rules say that Implication $(p \implies q)$ changes to $(p \land \lnot q)$.
So, we get:
$$
\exists x:
\left (
\substack{\text{student}\\\text{in class}} (x)
\land \lnot
\exists a \exists b:
\left (
\substack{
\text{isMathClass}(a) \,\,\, \land\,\,\, \text{isMathClass}(b)\\\\
\land\,\,\text{Taken}(x,a)\,\, \land\,\, \text{Taken}(x,b)\,\,\,\,\,\,
}
\,\, \land \,\,
\forall c:
\left (
\substack{
\text{isMathClass}(c)\\
\land \quad c \neq a\\
\land \quad c \neq b
}
\implies
\lnot \text{Taken}(x,c)
\right )
\right )
\right )
$$
Now, we encounter $\lnot \exists a \exists b (\cdots)$
We push to negation inwards twice like this:
- $\lnot \exists a \exists b (\cdots)$
- $\forall a \lnot \exists b (\cdots)$
- $\forall a \forall b \lnot (\cdots)$
Overall, we get:
$$
\exists x:
\left (
\substack{\text{student}\\\text{in class}} (x)
\land
\forall a \forall b:
\lnot \left (
\substack{
\text{isMathClass}(a) \,\,\, \land\,\,\, \text{isMathClass}(b)\\\\
\land\,\,\text{Taken}(x,a)\,\, \land\,\, \text{Taken}(x,b)\,\,\,\,\,\,
}
\,\, \land \,\,
\forall c:
\left (
\substack{
\text{isMathClass}(c)\\
\land \quad c \neq a\\
\land \quad c \neq b
}
\implies
\lnot \text{Taken}(x,c)
\right )
\right )
\right )
$$
Now we need to negate everything inside that second big brackets!
This time, we have a lot of ANDs.
So, we use the De-Morgan's law!
But hold on..
Notice this cool thing:
$\lnot \Bigl (a b c \, x\Bigr )
\\\\\equiv\quad \lnot \Biggl (\Bigl (a b c\Bigr ) \, \, x\Biggr )
\\\\\\\equiv\quad \lnot \Bigl (a b c\Bigr ) \, \lor \, \lnot x
\\\\\equiv\quad (a b c) \implies \lnot x$
We can use this cool thing to quickly negate all those ANDs we have in the inner big bracket!
Heres what we get:
$$
\exists x:
\left (
\substack{\text{student}\\\text{in class}} (x)
\land
\forall a \forall b:
\left (
\substack{
\text{isMathClass}(a) \,\,\, \land\,\,\, \text{isMathClass}(b)\\\\
\land\,\,\text{Taken}(x,a)\,\, \land\,\, \text{Taken}(x,b)\,\,\,\,\,\,
}
\,\, \implies \,\,
\lnot \forall c:
\left (
\substack{
\text{isMathClass}(c)\\
\land \quad c \neq a\\
\land \quad c \neq b
}
\implies
\lnot \text{Taken}(x,c)
\right )
\right )
\right )
$$
Great, almost done!
Negating that $\lnot \forall c \,\,(\cdots)$ we will get $\exists c \,\,\lnot (\cdots)$
That is, we get:
$$
\exists x:
\left (
\substack{\text{student}\\\text{in class}} (x)
\land
\forall a \forall b:
\left (
\substack{
\text{isMathClass}(a) \,\,\, \land\,\,\, \text{isMathClass}(b)\\\\
\land\,\,\text{Taken}(x,a)\,\, \land\,\, \text{Taken}(x,b)\,\,\,\,\,\,
}
\,\, \implies \,\,
\exists c:
\lnot \left (
\substack{
\text{isMathClass}(c)\\
\land \quad c \neq a\\
\land \quad c \neq b
}
\implies
\lnot \text{Taken}(x,c)
\right )
\right )
\right )
$$
The last bracket now!
Remember what implications change to?
Implication $(p \implies q)$ changes to $(p \land \lnot q)$.
So, we get:
$$
\exists x:
\left (
\substack{\text{student}\\\text{in class}} (x)
\land
\forall a \forall b:
\left (
\substack{
\text{isMathClass}(a) \,\,\, \land\,\,\, \text{isMathClass}(b)\\\\
\land\,\,\text{Taken}(x,a)\,\, \land\,\, \text{Taken}(x,b)\,\,\,\,\,\,
}
\,\, \implies \,\,
\exists c:
\left (
\substack{
\text{isMathClass}(c)\\
\land \quad c \neq a\\
\land \quad c \neq b
}
\land
\lnot \lnot \text{Taken}(x,c)
\right )
\right )
\right )
$$
Notice that we now have two NOTs $(\lnot\lnot)$ in a row!
We know that $\lnot \lnot p \equiv p$
So, we can use that to finally get:
$$
\exists x:
\left (
\substack{\text{student}\\\text{in class}} (x)
\land
\forall a \forall b:
\left (
\substack{
\text{isMathClass}(a) \,\,\, \land\,\,\, \text{isMathClass}(b)\\\\
\land\,\,\text{Taken}(x,a)\,\, \land\,\, \text{Taken}(x,b)\,\,\,\,\,\,
}
\,\, \implies \,\,
\exists c:
\left (
\substack{
\text{isMathClass}(c)\\
\land \quad c \neq a\\
\land \quad c \neq b
}
\land
\text{Taken}(x,c)
\right )
\right )
\right )
$$
Now, lets take a step back and try to read what we just got.
It reads:
There is someone $(x)$ in the class, such that for every two different math classes $(a,b)$ that $x$ has taken, there is atleast one more math class $c$ that $x$ has taken!
Sounds familiar? yupe. Thats what you wanted explanation for!
There is someone in the class such that for every two different math course, these are not the two & only two math courses this person has taken