Editing Exclusive or (section)

==Equivalences, elimination, and introduction==
Exclusive disjunction essentially means 'either one, but not both nor none'. In other words, the statement is true [[if and only if]] one is true and the other is false. For example, if two horses are racing, then one of the two will win the race, but not both of them. The exclusive disjunction <math>p\nleftrightarrow q</math>, also denoted by <math>p\operatorname{?}q</math> or <math>Jpq</math>, can be expressed in terms of the [[logical conjunction]] ("logical and", <math>\and</math>), the [[disjunction]] ("logical or", <math>\vee</math>), and the [[negation]] (<math>\neg</math>) as follows:
: <math>\begin{matrix}
  p\nleftrightarrow q & = & (p\vee q)\and\neg(p\and q)
\end{matrix}</math>

The exclusive disjunction <math>p \nleftrightarrow q</math> can also be expressed in the following way:
: <math>\begin{matrix}
  p \nleftrightarrow q & = & (p \land \lnot q) \lor (\lnot p \land q)
\end{matrix}</math>

This representation of XOR may be found useful when constructing a circuit or network, because it has only one <math>\lnot</math> operation and small number of <math>\land</math> and <math>\lor</math> operations. A proof of this identity is given below:
: <math>\begin{matrix}
  p \nleftrightarrow q & = & (p \land \lnot q) & \lor & (\lnot p \land q) \\[3pt]
             & = & ((p \land \lnot q) \lor \lnot p) & \land & ((p \land \lnot q) \lor q) \\[3pt]
             & = & ((p \lor \lnot p) \land (\lnot q \lor \lnot p)) & \land & ((p \lor q) \land (\lnot q \lor q)) \\[3pt]
             & = & (\lnot p \lor \lnot q) & \land & (p \lor q) \\[3pt]
             & = & \lnot (p \land q) & \land & (p \lor q)
\end{matrix}</math>

It is sometimes useful to write <math>p \nleftrightarrow q</math> in the following way:
: <math>\begin{matrix}
  p \nleftrightarrow q & = & \lnot ((p \land q) \lor (\lnot p \land \lnot q))
\end{matrix}</math>
or:
: <math>\begin{matrix}
  p \nleftrightarrow q & = & (p \lor q) \land (\lnot p \lor \lnot q)
\end{matrix}</math>

This equivalence can be established by applying [[De Morgan's laws]] twice to the fourth line of the above proof.

The exclusive or is also equivalent to the negation of a [[logical biconditional]], by the rules of material implication (a [[material conditional]] is equivalent to the disjunction of the negation of its [[Antecedent (logic)|antecedent]] and its consequence) and [[If and only if|material equivalence]].

In summary, we have, in mathematical and in engineering notation:
: <math>\begin{matrix}
  p \nleftrightarrow q & = & (p \land \lnot q) & \lor & (\lnot p \land q) & = & p\overline{q} + \overline{p}q \\[3pt]
             & = & (p \lor q) & \land & (\lnot p \lor \lnot q) & = & (p + q)(\overline{p} + \overline{q}) \\[3pt]
             & = & (p \lor q) & \land & \lnot (p \land q) & = & (p + q)(\overline{pq})
\end{matrix}</math>