Some sources define logical connectives by their truth tables. These are
tables that give the truth value of the composed expression for all possible
combinations of the truth values of their arguments. In this section, we
show that our definitions and axioms produce equivalent results for all the
logical connectives we have introduced (either axiomatically or by a
definition): implication wi, negation wn, biconditional df-bi,
conjunction df-an, disjunction df-or, alternative denial df-nan,
exclusive disjunction df-xor.