De Morgan’s laws and the distributive laws

The previous lessons of this unit built, one upon another, the tools of deduction: the system of axioms and modus ponens, the four basic techniques and the replacement of double negation, the symmetries of the connectives and the techniques of classical logic. This lesson adds no new rule; it puts them to work together. If this is so, its interest lies not so much in the statements, which may already be known from other courses, as in the way of obtaining them: each line must be justified by an axiom, a premise, a definition, one of the two primitive rules or a result already proved, and none may rest on what “seems evident”.

What is used and how it is chained

From the lesson on formal deductive systems are taken Łukasiewicz's axioms A1, A2 and A3, modus ponens (MP), also with premises, reflexivity (Refl: if $\varphi \in \Gamma$, then $\Gamma \vdash \varphi$), monotonicity (Mon), cut (Cut: if $\Gamma \vdash \varphi_i$ for each $i$ and $\Gamma \cup \{\varphi_1, \ldots, \varphi_n\} \vdash \psi$, then $\Gamma \vdash \psi$), the deduction theorem (DT) and provable equivalence ($\varphi \dashv\vdash \psi$ if $\{\varphi\} \vdash \psi$ and $\{\psi\} \vdash \varphi$), with its properties: it is reflexive, symmetric and transitive, and, if $\varphi \dashv\vdash \psi$, then $\Gamma \vdash \varphi$ if and only if $\Gamma \vdash \psi$. From the lesson on the four deduction techniques, double negation (DN: $\varphi \dashv\vdash \neg\neg\varphi$), contraposition (CP), in particular $(\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \neg\varphi)$, and the second primitive rule of the course system, the replacement of double negation (RDN), with which the deduction theorem still holds: 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$, from $\chi$ one infers $\chi'$; the line obtained in this way from line $i$ is justified RDN$(i)$. Among its immediate consequences are $(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi)$, $(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi)$ and, in general, $\chi \dashv\vdash \chi'$ when $\chi'$ results from $\chi$ by RDN; from this it follows that RDN$(i)$ also applies to a line of the form $\chi \dashv\vdash \varphi$, to change a double negation in $\varphi$. From the lesson on the symmetries of the connectives, the replacement of equivalents (Repl) and the symmetries (Sym), among them $(\varphi \vee \psi) \dashv\vdash (\psi \vee \varphi)$ and $(\varphi \wedge \psi) \dashv\vdash (\psi \wedge \varphi)$.

From the lesson on the techniques of classical logic the following rules are taken, all with a set $\Gamma$ of premises. Disjunction introduction ($\vee$I): if $\Gamma \vdash \varphi$, then $\Gamma \vdash (\varphi \vee \psi)$ and $\Gamma \vdash (\psi \vee \varphi)$. Disjunction elimination ($\vee$E, disjunctive syllogism): if $\Gamma \vdash (\varphi \vee \psi)$ and $\Gamma \vdash \neg\varphi$, then $\Gamma \vdash \psi$. Conjunction introduction ($\wedge$I): if $\Gamma \vdash \varphi$ and $\Gamma \vdash \psi$, then $\Gamma \vdash (\varphi \wedge \psi)$. Conjunction elimination ($\wedge$E): if $\Gamma \vdash (\varphi \wedge \psi)$, then $\Gamma \vdash \varphi$ and $\Gamma \vdash \psi$. The excluded middle (EM): $\vdash (\varphi \vee \neg\varphi)$. And proof by cases (Cases) in its two forms: if $\Gamma \cup \{\varphi\} \vdash \chi$ and $\Gamma \cup \{\neg\varphi\} \vdash \chi$, then $\Gamma \vdash \chi$; and if $\Gamma \cup \{\varphi\} \vdash \chi$, $\Gamma \cup \{\psi\} \vdash \chi$ and $\Gamma \vdash (\varphi \vee \psi)$, then $\Gamma \vdash \chi$. In deductions, the first form is cited with two lines, Cases$(i, j)$, and the second, with three, Cases$(i, j, k)$, in the order of the statement: the two cases and, at the end, the disjunction. That lesson also recalls that every rule already proved holds within a context $\Gamma$, and this is how double negation and contraposition are used here.

Names of a string and equivalent formulas

Recall, from the lesson on the language of propositional logic, that the connectives other than $\downarrow$ are abbreviations with an official and unique definition: $\neg\varphi := (\varphi \downarrow \varphi)$, $(\varphi \vee \psi) := \neg(\varphi \downarrow \psi)$, $(\varphi \wedge \psi) := \neg(\neg\varphi \vee \neg\psi)$, $(\varphi \rightarrow \psi) := (\neg\varphi \vee \psi)$, $(\varphi \leftrightarrow \psi) := ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi))$ and $(\varphi \veebar \psi) := \neg(\varphi \leftrightarrow \psi)$. A definition asserts nothing about formulas: it gives a second name to a string that already existed. From this it follows that, if two expressions designate the same string, one can be put in place of the other anywhere, also inside a larger formula, because what is written is the same sequence of circles and disks. Thus $\neg(\varphi \wedge \psi)$ and $\neg\neg(\neg\varphi \vee \neg\psi)$ are the same string: the second results from writing, inside the first, the unfolding of the conjunction. In deductions, this change of name is justified with “Def”, followed by the connective that is unfolded or folded.

Now, a provable equivalence is not an identity. That $\varphi \dashv\vdash \neg\neg\varphi$ means that each one is deduced from the other, not that they are the same string: $\neg\neg\varphi$ is much longer than $\varphi$. Therefore, knowing that $\varphi \dashv\vdash \varphi'$ does not by itself authorize writing $\varphi'$ in place of $\varphi$ inside a larger formula. Nor does it authorize “negating both sides”: that $\varphi \dashv\vdash \varphi'$ yields $\neg\varphi \dashv\vdash \neg\varphi'$ is a theorem, the replacement of equivalents, whose proof uses contraposition, and not an evident operation. There is a single case in which the system authorizes replacement directly, at any place in a formula: that of $\theta$ by $\neg\neg\theta$, or conversely, which is the rule RDN; and the lesson on deductive systems showed, with the marking, that not even that case is deduced from the axioms and modus ponens, so that it had to be postulated. This care is not pedantry; it is what distinguishes a proof from a manipulation of symbols that could, applied to other connectives or in other systems, lead to falsehoods.

Two results fix precisely what is permitted. The first is the proposition on the properties of provable equivalence from the lesson on formal deductive systems: if $\Gamma \vdash \varphi$ and $\varphi \dashv\vdash \varphi'$, then $\Gamma \vdash \varphi'$, so that a provable equivalence can be applied to the whole formula of a line; and provable equivalence is reflexive, symmetric and transitive, so that equivalences are chained (if $\chi \dashv\vdash \varphi$ and $\varphi \dashv\vdash \varphi'$, then $\chi \dashv\vdash \varphi'$) and two expressions that designate the same string are, by reflexivity, provably equivalent. The second, the following lemma, gathers for convenient citation the extension of the replacement of equivalents to disjunction and conjunction, which the lesson on the symmetries proves for negation, implication and joint denial and extends to these two connectives in one of its solved problems.

From now on, “Repl” designates the replacement of equivalents in any of its forms, including those of this lemma, and it can be applied several times in succession, layer by layer, to reach a subformula located at any depth. When a line is obtained from line $i$ by applying an equivalence already proved, either to the whole formula or, with Repl, to one of its parts, it is justified with the name of that equivalence and the number of the line: DN$(i)$, “Repl, DM$(i)$”. A change of name, which applies no equivalence but rewrites the same string, is justified in the same way, with Def followed by the connective that is unfolded or folded: Def $\wedge$ $(i)$. The proposition of the lesson on formal deductive systems guarantees that such lines are justified, whether line $i$ asserts $\Gamma \vdash \varphi$ or asserts an equivalence $\chi \dashv\vdash \varphi$ that is being extended.