The quantified definition for a proper subset can be found here.
$A \subset B \leftrightarrow \forall x [x \in A \rightarrow x \in B] \land \exists x [x \notin A \land x \in B]$
I want to determine $A \not \subset B$ (A not proper subset B). Can I simply negate $A \subset B$ for $A \not \subset B$? $$\neg \Big(\forall x [x \in A \rightarrow x \in B] \land \exists x [x \notin A \land x \in B]\Big) \\ \leftrightarrow \neg \Big(\forall x [\neg (x \in A) \vee x \in B] \land \exists x [x \notin A \land x \in B]\Big) \\ \leftrightarrow \exists x [x \in A \wedge x \notin B] \vee \forall x [x \in A \vee x \notin B]$$ The part before the first $\vee$ looks correct, but I'm not so sure for the second part: $... \vee \forall x [x \in A \vee x \notin B]$
$\endgroup$ 42 Answers
$\begingroup$Yes, that's the correct negation, though you can take one more step and express the last universal as a quantified implication .
$$\begin{array}{rcl} &&\neg \Big(\big(\forall x~[x \in A \to x \in B]\big) ~\land~ \big(\exists x~[x \notin A \land x \in B]\big)\Big) \\ &\iff& \big(\exists x~[x \in A \wedge x \notin B]\big)~\vee~\big(\forall x~[x \in A \vee x \notin B]\big)\\&\iff&\big(\exists x~[x \in A \wedge x \notin B]\big)~\vee~\big(\forall x~[x\in B\to x \in A]\big)\end{array}$$
Which looks similar to the original, except that it is a disjunction.
$A$ is not a subset of $B$ iif there is an element in $A$ that is not in $B$, or every element in $B$ is in $A$. That effectively says: "There are bits of $A$ outside $B$ or they are actually the same set".
$$\begin{array}{rcl} \neg(A\subset B) &\iff&\neg(A\subseteq B~\wedge~B\nsubseteq A ) \\ A\not\subset B&\iff& A\nsubseteq B~\vee~B\subseteq A\end{array}$$
$\endgroup$ $\begingroup$The second quantifier is needed to handle cases where $A=B$ (i.e. the equivalence case that distinguishes $\subset$ from $\subseteq$). It is easy to check that in this case, the first quantifier is false but the second one is true.
$\endgroup$ 2
