Deduction: synthesis and challenges

Summary

This lesson closes the unit devoted to deduction. It rebuilds the deductive chain that runs from the definition of Łukasiewicz's system (three axiom schemas and modus ponens) to the deduction theorem and to the limit of that system in the language of joint denial; from there to the four basic techniques and to the rule of replacement of double negation, which completes the course system; from the fundamental lemma of joint denial to the replacement of equivalents and to the symmetries, and from there to the rules of classical logic and to De Morgan's laws and the distributive laws, pointing out at each link which results it uses and in which lesson it is proved. It distinguishes what the unit proved from what it accepted, places what has been achieved within the plan of the course and explains why the question that the unit leaves open, that of knowing whether what is derivable coincides with what is true, leads to the unit on semantics. It repeats in its exit assessment the skills of the entry assessment, and it ends with six challenges, harder than the problems of the lessons, which require combining the tools of several of them.

Learning objectives

Rebuild the logical order of the results of the unit, identifying the earlier results on which each one rests and the lesson in which it is proved.
Explain how the deduction theorem, double negation, the rule of replacement of double negation, contraposition, the fundamental lemma and the replacement of equivalents are linked, and why the classical rules, De Morgan's laws and the distributive laws depend on them.
Distinguish what the unit proved from what it accepted (the axiom schemas, the two primitive rules, strong and structural induction and unique readability) and from what it left for the following units, in particular the relation between deduction and truth.
Solve problems that combine markings, the rule of replacement of double negation, the deduction theorem, proof by cases, reductio ad absurdum, the replacement of equivalents, De Morgan's laws and the distributive laws.

What the unit achieved

The unit set out to provide the language of the previous unit with a deductive system, that is, with a purely syntactic way of obtaining formulas from others, and to prove with that system, line by line, the techniques with which mathematics reasons. The purpose has been fulfilled with a few reservations, each one declared in its place: the three axiom schemas and the two primitive rules, which are not proved but chosen, and whose right choice is a question that the unit raises without fully answering it; strong and structural induction, unique readability and definition by recursion, which were proved in the previous unit and are used here; and the indispensable minimum of set theory (subsets, unions and finite sets), which was recalled where it was needed. With those reservations, the path travelled can be read as a single deductive chain in four segments.

Łukasiewicz's system and its limit

The lesson on formal deductive systems defined a system as a language, some axioms and some rules, all of them checkable by looking only at the strings, and fixed the first stage of the course system, Łukasiewicz's system: the schemas A1, A2 and A3 and modus ponens as the only rule, which unique readability makes applicable without ambiguity. It defined deduction from a set $\Gamma$ of premises and the relation $\Gamma \vdash \varphi$ , deduced $\vdash (\varphi \rightarrow \varphi)$ in five lines and proved the structural properties: reflexivity, monotonicity, modus ponens between deductions, cut and finiteness. With them and with strong induction on the number of lines it proved the deduction theorem, whose second case requires having deduced $(\varphi \rightarrow \varphi)$ beforehand, and its converse; from them it obtained provable equivalence, which is reflexive, symmetric and transitive. Finally, it established the limit of that system: a marking with values $0$ and $1$ , defined by recursion on the primitive form $(\alpha \downarrow \beta)$ , treats negation and implication as usual, is preserved by A1, A2, A3 and modus ponens, and leaves free the value of formulas such as $(v_{1} \downarrow v_{2})$ . It follows that $((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1})$ is not a theorem of Łukasiewicz's system, and that from $(v_{1} \downarrow v_{2})$ one does not deduce $(\neg\neg v_{1} \downarrow v_{2})$ , nor conversely. Since every marking gives the same value to $\theta$ and to $\neg\neg\theta$ , the lesson also warned that not even double negation, once proved, would remedy that limit.

The four techniques and the new rule

The lesson on the four deduction techniques first proved the lemma “from result to rule”: if $\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta$ , the same conclusion is obtained from any $\Gamma$ that deduces each $\alpha_{i}$ , and moreover $\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots))$ . That lemma is what allows each technique to be used in three presentations (from premises, as a theorem and as a rule), and the lessons on the symmetries and on De Morgan, which put together chains of equivalences with cut, rest for this on the properties of provable equivalence from the first lesson, which are the same idea applied to a single premise; in the chain each result appears only once, where it is proved. With it, the lesson deduced hypothetical syllogism from A1 and A2 in seven lines, interchange of premises with the deduction theorem, double negation (whose first direction applies A3 twice to an implication manufactured with A1, and whose second applies the first to $\neg\varphi$ and A3) and contraposition in its three forms, which distribute in three ways the negations of an implication; all four already hold in Łukasiewicz's system.

Once double negation had been proved, the lesson completed the course system with a second primitive rule, replacement of double negation (RDN): from $\chi$ one infers $\chi'$ when $\chi'$ results from replacing in $\chi$ an occurrence of a subformula $\theta$ by $\neg\neg\theta$ , or one of $\neg\neg\theta$ by $\theta$ . The rule must be postulated, because the marking $m_{1}$ gives $1$ to the theorems of double negation and yet separates $(v_{1} \downarrow v_{2})$ from $(\neg\neg v_{1} \downarrow v_{2})$ ; RDN does not preserve $m_{1}$ , and that is why it enlarges what is derivable, but it preserves the honest marking, and that is why it does not enlarge it too much. The rule acts on the string of the base language, where a negation duplicates its argument: $(\varphi \rightarrow \psi)$ contains the subformula $\neg\varphi$ twice, and putting a double negation before its antecedent requires two applications. That same observation supports the extension of the deduction theorem: if a line is obtained by the rule, the induction hypothesis gives the implication whose consequent is the previous line, and two applications of the rule, one in each copy of that consequent, give the required implication; the other structural properties hold with the same proof. The first consequences are that a formula is equivalent to every formula that results from it by the rule, in particular $(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi)$ and $(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi)$ , and that the corresponding implications, which other systems take as axioms, are theorems here.

Connectives and replacement

The lesson on the symmetries of the connectives faced the difficulty peculiar to the language of circles and disks: Łukasiewicz's axioms speak only of negations and implications, and almost no joint denial is one or the other. The fundamental lemma, $(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi)$ , builds the bridge: since $\neg(\neg\varphi \rightarrow \psi)$ is $\neg\neg(\neg\neg\varphi \downarrow \psi)$ , the rule RDN puts in the inner double negation and double negation, the outer one; in the reverse direction, double negation and the rule remove them. With it, the replacement of equivalents, proved first under negation and on both sides of implication with contraposition and hypothetical syllogism, was extended to both arguments of joint denial and, from there, to disjunction and conjunction. The rule and the replacement do not make each other superfluous: the rule only interchanges $\theta$ and $\neg\neg\theta$ , whereas the replacement admits any equivalents; and the replacement, proved with the fundamental lemma, rests in turn on the rule. The lesson then proved that the forms that other texts take as definitions are equivalences: $(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi)$ , which requires two applications of the rule, one in each copy that the outer negation creates, and $(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi)$ , which requires double negation; on the other hand, $(\varphi \wedge \psi)$ and $\neg(\varphi \rightarrow \neg\psi)$ are the same string. Finally, it proved the five symmetries in the order imposed by the definitions: that of joint denial with the fundamental lemma and contraposition, and each of the others with the previous one, carried with the replacement under negation when needed.

The classical rules and the laws

The lesson on the techniques of classical logic proved, all of them with a set $\Gamma$ of premises carried from line to line, the introduction and elimination of disjunction and of conjunction, the excluded middle and non-contradiction, explosion, reductio ad absurdum in its two forms and proof by cases, with a formula and its negation and with an arbitrary disjunction. The order of dependencies is strict: explosion rests on the rules of disjunction; classical reductio ad absurdum, on explosion and on A3; proof by cases, on contraposition and on reductio ad absurdum. None of those proofs invokes the rule RDN directly: the rule acts through the equivalent forms and the replacement of equivalents. The lesson on De Morgan’s laws and the distributive laws put these rules to work together: the first De Morgan law results from the definition of conjunction and from double negation; the second requires entering joint denial, where the rule RDN intervenes twice, once in each argument and with no need for symmetry, and from it it follows that $(\varphi \downarrow \psi)$ is equivalent to $(\neg\varphi \wedge \neg\psi)$ , the reading “neither $\varphi$ nor $\psi$ ” that the previous unit had stipulated; the variants include $\neg(\varphi \rightarrow \psi) \dashv\vdash (\varphi \wedge \neg\psi)$ . The two distributive laws were proved in both directions by cases, choosing in each the form of proof by cases that suits it.

The following figure gathers the four segments into a single chain. Each node of the column is a definition or a result, numbered according to the logical order and joined by an arc to the earlier links that its proof uses; around them float the supports, that is, the principles and tools to which the chain turns again and again, each joined by a solid line to the links that rest on it and by a dotted one to the link where it is established, except those that this chain does not prove (the axiom schemas, which are accepted, and the tools of the previous unit), which are drawn as rings. The rule of replacement of double negation, although it too is accepted without proof, appears joined to the link that introduces it, because that is where it is explained why it must be postulated. Clicking a support highlights all the links that use it, and each link refers to the lesson in which it is proved. Note that the deduction theorem and double negation are, after the axioms, the most visited supports of the unit, and that the new rule supports everything the unit says about joint denial: the extended deduction theorem, the fundamental lemma, the equivalent forms and the second De Morgan law.

Supports of the chain

AUnique readability and recursion. If $\sigI\varphi\psi = \sigI\varphi'\psi'$ , with all four strings formulas, then $\varphi = \varphi'$ and $\psi = \psi'$ ; whence a rule that computes the value of $\sigI\varphi\psi$ from $\varphi$ , from $\psi$ and from their values defines a single function on formulas. It was proved in the previous unit. Admitted without proof in this unit.
BStrong induction. If a property holds for a natural number whenever it holds for all smaller ones, it holds for all natural numbers. It was deduced from simple induction in the previous unit, and here it is applied to the number of lines of a deduction. Admitted without proof in this unit.
CŁukasiewicz's axioms. The schemas A1, $(\varphi \rightarrow (\psi \rightarrow \varphi))$ ; A2, $((\varphi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi)))$ ; and A3, $((\neg\psi \rightarrow \neg\varphi) \rightarrow (\varphi \rightarrow \psi))$ . They are accepted. Admitted without proof in this unit.
DReplacement of double negation. Second primitive rule of the course system: from $\chi$ one infers $\chi'$ if $\chi'$ results from $\chi$ by replacing an occurrence of a subformula $\theta$ by $\neg\neg\theta$ , or one of $\neg\neg\theta$ by $\theta$ . It is postulated after double negation has been proved. Established in: 8. Replacement of double negation.
EDeduction theorem. $\Gamma \cup \{\varphi\} \vdash \psi$ if and only if $\Gamma \vdash (\varphi \rightarrow \psi)$ ; it is proved in Łukasiewicz's system and holds, with one more case, in the course system. Established in: 3. Deduction theorem and provable equivalence.
FFrom result to rule. If $\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta$ and $\Gamma \vdash \alpha_{i}$ for each $i$ , then $\Gamma \vdash \beta$ : every technique proved from premises applies under any set of premises. Established in: 5. From result to rule.
GDouble negation. $\varphi \dashv\vdash \neg\neg\varphi$ , with the theorems $\vdash (\neg\neg\varphi \rightarrow \varphi)$ and $\vdash (\varphi \rightarrow \neg\neg\varphi)$ . Established in: 7. Double negation.
HReplacement of equivalents. If $\varphi \dashv\vdash \varphi'$ , $\varphi'$ may be put in place of $\varphi$ under a negation, on either side of an implication, of a joint denial, of a disjunction and of a conjunction, without altering the equivalence. Established in: 12. Replacement of equivalents.

Segment 1 Łukasiewicz's system and its limit
- Recognize the instances of the schemas and decide whether a sequence of formulas is a deduction from a set of premises.
- Prove the structural properties of deduction and the deduction theorem by strong induction on the number of lines.
- Build deductions about deductions with reflexivity, monotonicity, cut, the deduction theorem and its converse.
- Prove that a formula is not deduced by means of a marking that the axioms and modus ponens preserve, and explain with it the limit of Łukasiewicz's system.
1. System, deduction and identity. The axioms of Łukasiewicz's system are the uniform instances of A1 to A3, and its only rule is modus ponens. $\Gamma \vdash \varphi$ if there is a finite sequence of formulas ending in $\varphi$ , each of which is an axiom, an element of $\Gamma$ or obtained by modus ponens from two earlier ones. The first theorem, $\vdash (\varphi \rightarrow \varphi)$ , is deduced in five lines with A1 and A2.
  Rests on: A (Unique readability and recursion), C (Łukasiewicz's axioms). Proved in: Formal deductive systems.
2. Structural properties. If $\varphi \in \Gamma$ , $\Gamma \vdash \varphi$ ; if $\Gamma \subseteq \Delta$ and $\Gamma \vdash \varphi$ , $\Delta \vdash \varphi$ ; from $\Gamma \vdash \varphi$ and $\Gamma \vdash (\varphi \rightarrow \psi)$ follows $\Gamma \vdash \psi$ ; if $\Gamma \vdash \varphi_{i}$ for each $i$ and $\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{r}\} \vdash \psi$ , $\Gamma \vdash \psi$ ; and if $\Gamma \vdash \varphi$ , some finite subset of $\Gamma$ suffices.
  Uses: 1. System, deduction and identity. Proved in: Formal deductive systems.
3. Deduction theorem and provable equivalence. $\Gamma \cup \{\varphi\} \vdash \psi$ if and only if $\Gamma \vdash (\varphi \rightarrow \psi)$ , by strong induction on the number of lines, with A1, A2 and identity. From it, provable equivalence, $\varphi \dashv\vdash \psi$ , is reflexive, symmetric and transitive, and two equivalent formulas are deduced from the same sets.
  Uses: 1. System, deduction and identity, 2. Structural properties. Rests on: B (Strong induction), C (Łukasiewicz's axioms). Proved in: Formal deductive systems.
4. Limit of Łukasiewicz's system. A marking with values $0$ and $1$ defined by recursion satisfies $m(\neg\varphi) = 1 - m(\varphi)$ and $m((\varphi \rightarrow \psi)) = 1 - m(\varphi) \left( 1 - m(\psi) \right)$ , and A1, A2, A3 and modus ponens preserve marking $1$ ; whence $((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1})$ is not a theorem of Łukasiewicz's system, and $\{(v_{1} \downarrow v_{2})\} \nvdash (\neg\neg v_{1} \downarrow v_{2})$ , nor conversely. Since every marking gives $1$ to double negation, the replacement must be postulated.
  Uses: 1. System, deduction and identity. Rests on: A (Unique readability and recursion), B (Strong induction), C (Łukasiewicz's axioms). Proved in: Formal deductive systems.
Segment 2 The four techniques and the new rule
- Turn a result from premises into a theorem and into a rule applicable under any set of premises.
- Chain implications, reorder antecedents, put in and remove double negations and choose the form of contraposition that corresponds to each implication.
- Apply the rule of replacement of double negation, locating the occurrences that the abbreviations hide and repeating it in each copy that a negation creates.
- Explain with the marking why the rule is postulated, and prove that the deduction theorem holds with it.
1. From result to rule. If $\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta$ , then from $\Gamma \vdash \alpha_{1}$ , $\ldots$ , $\Gamma \vdash \alpha_{n}$ follows $\Gamma \vdash \beta$ , and $\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots))$ ; in particular, if $\alpha \dashv\vdash \alpha'$ , $\Gamma \vdash \alpha$ if and only if $\Gamma \vdash \alpha'$ .
  Uses: 2. Structural properties. Rests on: E (Deduction theorem). Proved in: Four deduction techniques.
2. Hypothetical syllogism and interchange. $\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)$ , with a deduction of seven lines from A1 and A2; and $\{(\varphi \rightarrow (\psi \rightarrow \chi))\} \vdash (\psi \rightarrow (\varphi \rightarrow \chi))$ .
  Uses: 1. System, deduction and identity. Rests on: C (Łukasiewicz's axioms), E (Deduction theorem), F (From result to rule). Proved in: Four deduction techniques.
3. Double negation. $\vdash (\neg\neg\varphi \rightarrow \varphi)$ , applying A3 twice to an implication that A1 manufactures from $\neg\neg\varphi$ ; $\vdash (\varphi \rightarrow \neg\neg\varphi)$ , applying the former to $\neg\varphi$ and A3; whence $\varphi \dashv\vdash \neg\neg\varphi$ , already in Łukasiewicz's system.
  Rests on: C (Łukasiewicz's axioms), E (Deduction theorem). Proved in: Four deduction techniques.
4. Replacement of double negation. The rule RDN is postulated, because the marking gives $1$ to double negation and not to replacement inside a joint denial. If $\chi'$ results from $\chi$ by the rule, $\chi \dashv\vdash \chi'$ ; in particular, $(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi)$ and $(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi)$ .
  Uses: 3. Deduction theorem and provable equivalence, 4. Limit of Łukasiewicz's system. Rests on: G (Double negation). Proved in: Four deduction techniques.
5. Deduction theorem in the course system. Reflexivity, monotonicity, cut and finiteness hold with the new rule, and so does $\Gamma \cup \{\varphi\} \vdash \psi$ if and only if $\Gamma \vdash (\varphi \rightarrow \psi)$ : in the new case, since $(\varphi \rightarrow \chi)$ is $((\neg\varphi \downarrow \chi) \downarrow (\neg\varphi \downarrow \chi))$ , the rule is applied twice, once in each copy of $\chi$ . From it, $\vdash ((\varphi \downarrow \psi) \rightarrow (\neg\neg\varphi \downarrow \psi))$ and its converse are theorems.
  Uses: 2. Structural properties, 3. Deduction theorem and provable equivalence. Rests on: B (Strong induction), D (Replacement of double negation). Proved in: Four deduction techniques.
6. Contraposition. $(\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \neg\varphi)$ , $(\neg\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \varphi)$ and $(\varphi \rightarrow \neg\psi) \dashv\vdash (\psi \rightarrow \neg\varphi)$ : the members change sides, and each one changes sign on crossing over.
  Uses: 6. Hypothetical syllogism and interchange. Rests on: C (Łukasiewicz's axioms), E (Deduction theorem), G (Double negation), F (From result to rule). Proved in: Four deduction techniques.
Segment 3 Connectives and replacement
- Unfold the abbreviations to decide whether two expressions designate the same string or formulas whose equivalence requires a deduction.
- Translate joint denial into negation and implication with the fundamental lemma.
- Carry an equivalence into the interior of a formula with the replacement of equivalents, distinguish it from the rule of replacement of double negation and chain equivalences.
- Prove the five symmetries in the order imposed by the definitions.
1. Fundamental lemma. $(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi)$ : since $\neg(\neg\varphi \rightarrow \psi)$ is $\neg\neg(\neg\neg\varphi \downarrow \psi)$ , the rule RDN puts in the inner double negation and double negation, the outer one; in the reverse direction, double negation and the rule remove them.
  Rests on: D (Replacement of double negation), G (Double negation). Proved in: The symmetries of the connectives.
2. Replacement of equivalents. If $\varphi \dashv\vdash \varphi'$ , then $\neg\varphi \dashv\vdash \neg\varphi'$ , $(\varphi \rightarrow \psi) \dashv\vdash (\varphi' \rightarrow \psi)$ and $(\psi \rightarrow \varphi) \dashv\vdash (\psi \rightarrow \varphi')$ ; with the fundamental lemma, the same on both sides of joint denial, and from there, of disjunction and of conjunction. Unlike the rule RDN, it admits any equivalents.
  Uses: 6. Hypothetical syllogism and interchange, 10. Contraposition, 11. Fundamental lemma. Rests on: E (Deduction theorem). Proved in: The symmetries of the connectives.
3. Equivalent forms. $(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi)$ , with two applications of the rule RDN, one in each copy that the outer negation creates; $(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi)$ , by double negation; and $(\varphi \wedge \psi)$ is the same string as $\neg(\varphi \rightarrow \neg\psi)$ .
  Rests on: D (Replacement of double negation), G (Double negation). Proved in: The symmetries of the connectives.
4. The five symmetries. $(\varphi \downarrow \psi) \dashv\vdash (\psi \downarrow \varphi)$ , by the fundamental lemma and contraposition; from it, successively, the symmetries of $\vee$ , $\wedge$ , $\leftrightarrow$ and $\veebar$ , each one with the previous one, carried with the replacement under negation when needed.
  Uses: 11. Fundamental lemma, 10. Contraposition. Rests on: H (Replacement of equivalents). Proved in: The symmetries of the connectives.
Segment 4 The classical rules and the laws
- Prove with premises the introduction and elimination of disjunction and of conjunction, the excluded middle and non-contradiction.
- Prove explosion, reductio ad absurdum and proof by cases with premises, and explain why they do not suffice without them.
- Prove by deduction De Morgan's laws, their variants and the distributive laws in both directions.
- Transform formulas into simple normal forms by means of chains of justified equivalences.
1. Rules of the connectives. With any $\Gamma$ : from $\varphi$ follows $(\varphi \vee \psi)$ ; from $(\varphi \vee \psi)$ and $\neg\varphi$ , $\psi$ ; from $\varphi$ and $\psi$ , $(\varphi \wedge \psi)$ ; from $(\varphi \wedge \psi)$ , $\varphi$ and $\psi$ ; moreover, $\vdash (\varphi \vee \neg\varphi)$ and $\vdash \neg(\varphi \wedge \neg\varphi)$ .
  Uses: 1. System, deduction and identity, 2. Structural properties, 6. Hypothetical syllogism and interchange, 10. Contraposition, 13. Equivalent forms, 14. The five symmetries. Rests on: C (Łukasiewicz's axioms), E (Deduction theorem), F (From result to rule), G (Double negation). Proved in: The techniques of classical logic.
2. Explosion and reductio ad absurdum. If $\Gamma \vdash \varphi$ and $\Gamma \vdash \neg\varphi$ , then $\Gamma \vdash \psi$ for every $\psi$ ; if $\Gamma \cup \{\neg\varphi\}$ deduces $\psi$ and $\neg\psi$ , then $\Gamma \vdash \varphi$ ; and if $\Gamma \cup \{\varphi\}$ deduces them, $\Gamma \vdash \neg\varphi$ .
  Uses: 1. System, deduction and identity, 2. Structural properties, 15. Rules of the connectives. Rests on: C (Łukasiewicz's axioms), E (Deduction theorem), G (Double negation). Proved in: The techniques of classical logic.
3. Proof by cases. If $\Gamma \cup \{\varphi\} \vdash \psi$ and $\Gamma \cup \{\neg\varphi\} \vdash \psi$ , then $\Gamma \vdash \psi$ ; and if $\Gamma \cup \{\varphi\} \vdash \chi$ , $\Gamma \cup \{\psi\} \vdash \chi$ and $\Gamma \vdash (\varphi \vee \psi)$ , then $\Gamma \vdash \chi$ .
  Uses: 2. Structural properties, 10. Contraposition, 15. Rules of the connectives, 16. Explosion and reductio ad absurdum. Rests on: E (Deduction theorem). Proved in: The techniques of classical logic.
4. De Morgan's laws. $\neg(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \vee \neg\psi)$ , by the definition and double negation; $\neg(\varphi \vee \psi) \dashv\vdash (\neg\varphi \wedge \neg\psi)$ , with one application of the rule RDN in each argument of joint denial; whence $(\varphi \downarrow \psi) \dashv\vdash (\neg\varphi \wedge \neg\psi)$ and $\neg(\varphi \rightarrow \psi) \dashv\vdash (\varphi \wedge \neg\psi)$ .
  Rests on: D (Replacement of double negation), G (Double negation), H (Replacement of equivalents). Proved in: De Morgan’s laws and the distributive laws.
5. Distributive laws. $(\varphi \wedge (\psi \vee \chi)) \dashv\vdash ((\varphi \wedge \psi) \vee (\varphi \wedge \chi))$ and $(\varphi \vee (\psi \wedge \chi)) \dashv\vdash ((\varphi \vee \psi) \wedge (\varphi \vee \chi))$ , each one in both directions by cases; with the symmetries, also from the right.
  Uses: 14. The five symmetries, 15. Rules of the connectives, 17. Proof by cases. Rests on: H (Replacement of equivalents). Proved in: De Morgan’s laws and the distributive laws.

Towards semantics. The chain stops where deduction reaches all the techniques with which mathematics reasons. It remains to know whether what is deduced is exactly what is true under every valuation: the next unit will define truth, and the last one will compare both notions.

The abbreviations of the justifications

The deductions of the unit justify each line with an abbreviation, the same in all the lessons. They are gathered here, ordered by the lesson that introduces them. “Premise” designates a hypothesis of the statement and, in deductions about deductions, a hypothesis of the rule being proved. The numbers in parentheses cite the lines to which the rule is applied; an equivalence already proved is cited without a number when it is written as a line, and with the number of the line it transforms when it is applied to that line, also to one of its parts with “Repl”.

First lesson: A1, A2 and A3 (the axiom schemas); MP $(i, j)$ (modus ponens); Def (unfolding or folding of an abbreviation, with the connective that is unfolded: “Def $\vee$ ”, “Def $\dashv\vdash$ ”); Id (identity, the theorem $\vdash (\varphi \rightarrow \varphi)$ ); Refl (reflexivity: if $\varphi \in \Gamma$ , then $\Gamma \vdash \varphi$ ); Mon (monotonicity); Cut (what has been deduced can be used as a premise); Fin (finiteness); DT (deduction theorem) and CDT (its converse).
Second lesson: HS (hypothetical syllogism); IP (interchange of premises); DN (double negation); RDN $(i)$ (replacement of double negation in line $i$ ; RDN without a number cites the equivalence between a formula and the one that results from it by the rule); CP (contraposition, in any of its three forms); “Solved $n$ ” (a result of solved problem $n$ of the same lesson, written as a line).
Third lesson: FL (fundamental lemma, $(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi)$ ); Repl (replacement of equivalents, in any of its forms, followed by the equivalence applied: “Repl, DM $(i)$ ”); Eq (equivalent forms of disjunction and conjunction, $(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi)$ and $(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi)$ ); Sym (symmetry of a connective).
Fourth lesson: $\vee$ I and $\vee$ E (disjunction introduction and elimination); $\wedge$ I and $\wedge$ E (conjunction introduction and elimination); EM (excluded middle); NC (non-contradiction; the abbreviation names the theorem, but justifies no line of the unit); Exp (explosion); Cases $(i, j)$ and Cases $(i, j, k)$ (proof by cases, with a formula and its negation or with a disjunction); “Cases without premises” (the proof by cases without a set $\Gamma$ , which appears only in one problem); RAA (reductio ad absurdum, in its two forms).
Fifth lesson: DM (De Morgan's laws); Dist (distributivity); Assoc (associativity of disjunction); Instance $(i)$ (line $i$ , which holds for arbitrary formulas, written again with other formulas in place of its metavariables; the substitution is indicated).
Challenges of this lesson: M3 (the schema that the third challenge puts in place of A3).