This section defines conjunction of two formulas, denoted by infix ""
and read "and". It is defined in terms of implication and negation, which is
possible in classical logic (but not in intuitionistic logic: see iset.mm).
After the definition, we briefly introduce conversion of simple expressions
to and from conjunction. Two simple operations called importation (imp)
and exportation (ex) follow. In the propositions-as-types
interpretation, they correspond to uncurrying and currying respectively. They
are foundational for this section. Most of the theorems proved here trace
back to them, mostly indirectly, in a layered fashion, where more complex
expressions are built from simpler ones. Here are some of these successive
layers:
importation and exportation,
commutativity and associativity laws,
adding antecedents and simplifying,
conjunction of consequents,
syllogisms,
etc.
As indicated in the "note on definitions" in the section comment for logical
equivalence, some theorems containing only implication, negation and
conjunction are placed in the section after disjunction since theirs proofs
use disjunction (although this is not required since definitions are
conservative, see said section comment).