.. _logic: Logic ===== In the course of :numref:`Chapter %s <proofs_with_structure>` and :numref:`Chapter %s <proofs_with_structure_ii>` we learned the "grammar" of the various logical symbols, like :math:`\land`, :math:`\forall` and :math:`\to`. In those chapters, logical reasoning took place in fairly concrete mathematical situations: problems about equalities and inequalities in the natural numbers, the rational numbers, and so on. In this chapter, we take a more abstract point of view, studying the process of logical reasoning in its own right. The central concept is the concept of *logical equivalence*: transformations to the logical structure of a statement which are always valid, because the "before" and "after" can be deduced from each other using only abstract logical reasoning, not anything specific to the mathematical situation at hand. The most important logical equivalences are those covered in the final section of the chapter, :numref:`Section %s <negation_normalize>`. These are logical equivalences which move a negation symbol (:math:`\lnot`) to a deeper position in a logical statement. Taken together, these transformations give us a way to delay and minimize our encounters with :math:`\lnot`, the most awkward logical symbol. .. include:: ch05_Logic/01_Logical_Equivalence.inc .. include:: ch05_Logic/02_Excluded_Middle.inc .. include:: ch05_Logic/03_Negation_Algorithm.inc