The symmetries of the connectives

What is used and what has to be proved

The lesson on formal deductive systems fixed Łukasiewicz's system: the axioms A1, A2 and A3 and modus ponens. It also established 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 its converse (CDT), and provable equivalence, $\varphi \dashv\vdash \psi$, which means that $\{\varphi\} \vdash \psi$ and $\{\psi\} \vdash \varphi$; and it showed, with a marking that the axioms and modus ponens preserve, that this system does not deduce certain formulas about joint denial. The lesson on the four deduction techniques added hypothetical syllogism (HS: $\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)$), interchange of premises (IP), double negation (DN: $\varphi \dashv\vdash \neg\neg\varphi$, with its two theorems $\vdash (\neg\neg\varphi \rightarrow \varphi)$ and $\vdash (\varphi \rightarrow \neg\neg\varphi)$) and contraposition (CP) in its three forms:

Once double negation had been proved, that same lesson completed the course system with a second primitive rule, replacement of double negation (RDN): if $\chi'$ results from $\chi$ by replacing an occurrence of a subformula $\theta$ by $\neg\neg\theta$, or an occurrence of a subformula $\neg\neg\theta$ by $\theta$, then from $\chi$ one infers $\chi'$. The line obtained in this way from line $i$ is justified with RDN$(i)$. From that point on, $\vdash$ refers to the course system (A1 to A3, modus ponens and RDN), in which Refl, Mon, Cut, DT and CDT still hold. The rule acts on the string of the base language, so that it also reaches the occurrences that an abbreviation hides, and in either of the two arguments of a joint denial; among its immediate consequences are

and, in general, $\chi \dashv\vdash \chi'$ whenever $\chi'$ results from $\chi$ by RDN. A line of equivalence of this form is justified with “RDN”, without a line number, in the same way as a line “DN” or “CP” cites an equivalence already proved. As there, a theorem already proved can be written as a line of a deduction, because its own deduction can be inserted at that place; and, by the lemma “from result to rule” of that lesson, each technique is also applied as a rule under any set $\Gamma$ of premises, cited with the numbers of the lines to which it is applied, such as CP$(i)$ or HS$(i, j)$. In deductions about deductions, “Premise” designates a hypothesis of the rule being proved.

The official abbreviations, fixed in the lesson on the language of propositional logic, are the only definitions of the connectives:

A line justified with “Def” deduces nothing: it writes the same formula under another name, and the annotation says which abbreviation is unfolded or folded (“Def $\rightarrow$”, “Def $\vee$”). It is worth recalling the phenomenon observed in the lesson on the formalization of natural language: one and the same formula admits several names, so that a conjunction is also, as a string, a disjunction. For example, by unfolding the implication with $\neg\varphi$ in place of $\varphi$, one obtains

and the double negation that appears in front of $\varphi$, hidden by the abbreviation, is the reason why the rule RDN will intervene in everything that follows.

Provable equivalence as an equality

The proofs of this lesson are, almost all of them, chains of equivalences: $\varphi_{1} \dashv\vdash \varphi_{2}$, $\varphi_{2} \dashv\vdash \varphi_{3}$, and so on. For one to conclude $\varphi_{1} \dashv\vdash \varphi_{n}$ from a chain, provable equivalence must behave like an equality, and that is what was established by the proposition on the properties of provable equivalence in the lesson on formal deductive systems: the relation is reflexive ($\varphi \dashv\vdash \varphi$), symmetric (if $\varphi \dashv\vdash \psi$, then $\psi \dashv\vdash \varphi$) and transitive (if $\varphi \dashv\vdash \psi$ and $\psi \dashv\vdash \chi$, then $\varphi \dashv\vdash \chi$), and two provably equivalent formulas are interchangeable as conclusions (if $\Gamma \vdash \varphi$ and $\varphi \dashv\vdash \varphi'$, then $\Gamma \vdash \varphi'$, for every set $\Gamma$ of formulas). It is worth recalling how the last two were proved, because the whole lesson rests on them: from $\{\varphi\} \vdash \varphi'$ one passes, by monotonicity, to $\Gamma \cup \{\varphi\} \vdash \varphi'$, and from this and from $\Gamma \vdash \varphi$, by cut, to $\Gamma \vdash \varphi'$; transitivity results from applying this with $\Gamma = \{\varphi\}$ in one direction and with $\Gamma = \{\chi\}$ in the other.

From now on, the step that gathers a chain of equivalences into a single one is justified with “Cut”, which is the instrument of that proposition. Now, each link $\varphi_{i} \dashv\vdash \varphi_{i+1}$ contains the two deductions, the forward one and the backward one; hence a chain of equivalences proves both directions of its conclusion at once, and nothing is left “as an exercise”.