Four deduction techniques

The starting tools

In the lesson on formal deductive systems, Łukasiewicz's system was fixed. Its language is the language of circles and disks, written with the official abbreviations of the lesson on the language of propositional logic; its axioms are all the instances of the following three schemas, where $\varphi$, $\psi$ and $\chi$ are arbitrary formulas, and its only rule is modus ponens.

• A1: $(\varphi \rightarrow (\psi \rightarrow \varphi))$.
• A2: $((\varphi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi)))$.
• A3: $((\neg\psi \rightarrow \neg\varphi) \rightarrow (\varphi \rightarrow \psi))$.
• MP: from $\varphi$ and $(\varphi \rightarrow \psi)$ one deduces $\psi$.

A deduction of $\varphi$ from a set $\Gamma$ of formulas is a finite sequence of formulas that ends in $\varphi$ and in which each formula is an axiom, an element of $\Gamma$ or the result of applying modus ponens to two earlier formulas; if one exists, we write $\Gamma \vdash \varphi$, and if $\Gamma$ is empty, $\vdash \varphi$, and we say that $\varphi$ is a theorem. In that same lesson the metatheorems that we shall use here were proved: reflexivity (Refl: if $\varphi \in \Gamma$, then $\Gamma \vdash \varphi$), monotonicity (Mon: if $\Gamma \subseteq \Delta$ and $\Gamma \vdash \varphi$, then $\Delta \vdash \varphi$), modus ponens between deductions (if $\Gamma \vdash \varphi$ and $\Gamma \vdash (\varphi \rightarrow \psi)$, then $\Gamma \vdash \psi$), cut (Cut: if $\Gamma \vdash \varphi_{i}$ for each $i$ from $1$ to $n$ and $\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi$, then $\Gamma \vdash \psi$), finiteness (if $\Gamma \vdash \varphi$, some finite subset of $\Gamma$ suffices), the deduction theorem (DT: if $\Gamma \cup \{\varphi\} \vdash \psi$, then $\Gamma \vdash (\varphi \rightarrow \psi)$) and its converse (CDT), and the theorem $\vdash (\varphi \rightarrow \varphi)$, which we shall abbreviate Id in the justifications. Finally, $\varphi \dashv\vdash \psi$ (provable equivalence) means that $\{\varphi\} \vdash \psi$ and $\{\psi\} \vdash \varphi$.

It is worth recalling that $\neg$ and $\rightarrow$ are not symbols of the base language, but abbreviations: $\neg\varphi$ is the string $(\varphi \downarrow \varphi)$, and $(\varphi \rightarrow \psi)$ is $(\neg\varphi \vee \psi)$, that is, $\neg(\neg\varphi \downarrow \psi)$. The three axioms speak only of negations and implications, and the same lesson showed, with a marking with values $0$ and $1$ that they and modus ponens preserve, the limit that follows from this: in Łukasiewicz's system, from $(v_{1} \downarrow v_{2})$ one does not deduce $(\neg\neg v_{1} \downarrow v_{2})$, and joint denial lies partly beyond its reach. This lesson therefore proceeds in two stages. Up to and including double negation, $\vdash$ refers to Łukasiewicz's system, and nothing that is proved depends on unfolding the abbreviations. Once double negation has been proved, a second primitive rule is added to the system, replacement of double negation, which acts on the unfolded string; from that point on, $\vdash$ refers to the course system, Łukasiewicz's system plus that rule. Since every deduction of the former is also a deduction of the latter, nothing proved before is lost.

Two styles of deduction

There are two ways of writing a deduction, and both will be used. The first is the deduction proper, a sequence of formulas in which each line is an axiom, a premise or the result of modus ponens; each line is justified with A1, A2, A3, Premise or MP$(i, j)$, where line $i$ is the antecedent and line $j$ is the implication whose antecedent is exactly line $i$ (and, once the new rule has been introduced, RDN$(i)$). The second is the deduction about deductions, whose lines are not formulas but statements of the form $\Gamma \vdash \varphi$; each of them is justified with a metatheorem already proved, and the whole sequence is a reasoning in the metalanguage that guarantees that a deduction of the first style exists, even though it does not write it down. The justifications of this second style are read as follows.

• Refl: the formula on the right belongs to the set on the left.
• A1, A2, A3: the formula on the right is an instance of the schema; an instance of an axiom is deduced from any $\Gamma$ with a one-line deduction.
• MP$(i, j)$: modus ponens between deductions, applied to line $i$, $\Gamma \vdash \varphi$, and to line $j$, $\Gamma \vdash (\varphi \rightarrow \psi)$, with the same $\Gamma$.
• DT$(i)$ and CDT$(i)$: the deduction theorem or its converse, applied to line $i$.
• The name of a theorem already proved, such as Id or DN: the formula on the right is an instance of that theorem, and it is deduced from any $\Gamma$ by monotonicity, because the empty set is contained in $\Gamma$.
• Premise, in a deduction about deductions: the line is one of the hypotheses of the rule being proved.

Every result of this lesson is stated with metavariables and therefore holds for arbitrary formulas: its proof is a schema, and substituting a formula for each metavariable in it yields another proof, because the instances of an axiom schema remain instances of it and each application of modus ponens remains one (the same will hold for each application of the new rule). Thus, from $\vdash (\varphi \rightarrow \varphi)$ follows $\vdash (\neg\psi \rightarrow \neg\psi)$, with $\neg\psi$ in place of $\varphi$. This device, applying a result to a formula more complex than the one in the statement, is the one that pays off most in what follows.

From result to rule

The techniques of this lesson are proved from fixed premises, such as $\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)$; but they are used in the middle of deductions with other premises, where $(\varphi \rightarrow \psi)$ and $(\psi \rightarrow \chi)$ are not premises but formulas already deduced. The following lemma, a direct consequence of monotonicity and cut, authorizes that use once and for all.

It follows that each technique proved from premises has three presentations: the result itself, the theorem obtained by discharging its premises and the rule that is applied under any $\Gamma$. In a deduction about deductions, the rule is invoked with the name of the technique and the numbers of the lines to which it is applied, as in HS$(3, 4)$, and the lemma guarantees that the step is legitimate.