 If \(A\mid B \Leftrightarrow_\textrm{df} \lnot(A\land B)\) is added as a definition to SL, then the result is a conservative extension, and it becomes provable that for any formula \(A(p_0,\ldots,p_n)\) (i.e., for a formula containing the displayed propositional variables and some connectives) there is a formula \(B(p_0,\ldots,p_n)\) containing only the connective \(\mid\), and \(B(p_0,\ldots,p_n)\Leftrightarrow A(p_0,\ldots,p_n)\) itself is provable. \(\mid\) is, of course, interpreted as the “nand” truth function.  “Nand” as a binary connective or as a binary truth function is of the same sort of object as conjunction, disjunction, etc.