# 1.12.3 Disequality

Finally, let us also say something about disequality,
which is negation^{} of equality:^{1}^{1}We use “inequality”
to refer to $$ and $\le $. Also, note that this is negation of the *propositional* identity type.
Of course, it makes no sense to negate judgmental equality $\equiv $, because judgments are not subject to logical operations^{}.

$$(x{\ne}_{A}y):\equiv \mathrm{\neg}(x{=}_{A}y).$$ |

If $x\ne y$, we say that $x$ and $y$ are unequal or not equal. Just like negation, disequality plays a less important role here than it does in classical mathematics. For example, we cannot prove that two things are equal by proving that they are not unequal: that would be an application of the classical law of double negation, see §3.4 (http://planetmath.org/34classicalvsintuitionisticlogic).

Sometimes it is useful to phrase disequality in a positive way. For example,
in Theorem 11.2.4 (http://planetmath.org/1122dedekindrealsarecauchycomplete#Thmprethm1) we shall prove that a real number $x$ has an inverse^{} if,
and only if, its distance from $0$ is positive, which is a stronger requirement than $x\ne 0$.

Title | 1.12.3 Disequality |
---|---|

\metatable |