2.2: Deductions
- Page ID
- 9687
\( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)
\( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)
\( \newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\)
( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\)
\( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\)
\( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\)
\( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\)
\( \newcommand{\Span}{\mathrm{span}}\)
\( \newcommand{\id}{\mathrm{id}}\)
\( \newcommand{\Span}{\mathrm{span}}\)
\( \newcommand{\kernel}{\mathrm{null}\,}\)
\( \newcommand{\range}{\mathrm{range}\,}\)
\( \newcommand{\RealPart}{\mathrm{Re}}\)
\( \newcommand{\ImaginaryPart}{\mathrm{Im}}\)
\( \newcommand{\Argument}{\mathrm{Arg}}\)
\( \newcommand{\norm}[1]{\| #1 \|}\)
\( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\)
\( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\AA}{\unicode[.8,0]{x212B}}\)
\( \newcommand{\vectorA}[1]{\vec{#1}} % arrow\)
\( \newcommand{\vectorAt}[1]{\vec{\text{#1}}} % arrow\)
\( \newcommand{\vectorB}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)
\( \newcommand{\vectorC}[1]{\textbf{#1}} \)
\( \newcommand{\vectorD}[1]{\overrightarrow{#1}} \)
\( \newcommand{\vectorDt}[1]{\overrightarrow{\text{#1}}} \)
\( \newcommand{\vectE}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash{\mathbf {#1}}}} \)
\( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)
\( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)
\(\newcommand{\avec}{\mathbf a}\) \(\newcommand{\bvec}{\mathbf b}\) \(\newcommand{\cvec}{\mathbf c}\) \(\newcommand{\dvec}{\mathbf d}\) \(\newcommand{\dtil}{\widetilde{\mathbf d}}\) \(\newcommand{\evec}{\mathbf e}\) \(\newcommand{\fvec}{\mathbf f}\) \(\newcommand{\nvec}{\mathbf n}\) \(\newcommand{\pvec}{\mathbf p}\) \(\newcommand{\qvec}{\mathbf q}\) \(\newcommand{\svec}{\mathbf s}\) \(\newcommand{\tvec}{\mathbf t}\) \(\newcommand{\uvec}{\mathbf u}\) \(\newcommand{\vvec}{\mathbf v}\) \(\newcommand{\wvec}{\mathbf w}\) \(\newcommand{\xvec}{\mathbf x}\) \(\newcommand{\yvec}{\mathbf y}\) \(\newcommand{\zvec}{\mathbf z}\) \(\newcommand{\rvec}{\mathbf r}\) \(\newcommand{\mvec}{\mathbf m}\) \(\newcommand{\zerovec}{\mathbf 0}\) \(\newcommand{\onevec}{\mathbf 1}\) \(\newcommand{\real}{\mathbb R}\) \(\newcommand{\twovec}[2]{\left[\begin{array}{r}#1 \\ #2 \end{array}\right]}\) \(\newcommand{\ctwovec}[2]{\left[\begin{array}{c}#1 \\ #2 \end{array}\right]}\) \(\newcommand{\threevec}[3]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \end{array}\right]}\) \(\newcommand{\cthreevec}[3]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \end{array}\right]}\) \(\newcommand{\fourvec}[4]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}\) \(\newcommand{\cfourvec}[4]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}\) \(\newcommand{\fivevec}[5]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}\) \(\newcommand{\cfivevec}[5]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}\) \(\newcommand{\mattwo}[4]{\left[\begin{array}{rr}#1 \amp #2 \\ #3 \amp #4 \\ \end{array}\right]}\) \(\newcommand{\laspan}[1]{\text{Span}\{#1\}}\) \(\newcommand{\bcal}{\cal B}\) \(\newcommand{\ccal}{\cal C}\) \(\newcommand{\scal}{\cal S}\) \(\newcommand{\wcal}{\cal W}\) \(\newcommand{\ecal}{\cal E}\) \(\newcommand{\coords}[2]{\left\{#1\right\}_{#2}}\) \(\newcommand{\gray}[1]{\color{gray}{#1}}\) \(\newcommand{\lgray}[1]{\color{lightgray}{#1}}\) \(\newcommand{\rank}{\operatorname{rank}}\) \(\newcommand{\row}{\text{Row}}\) \(\newcommand{\col}{\text{Col}}\) \(\renewcommand{\row}{\text{Row}}\) \(\newcommand{\nul}{\text{Nul}}\) \(\newcommand{\var}{\text{Var}}\) \(\newcommand{\corr}{\text{corr}}\) \(\newcommand{\len}[1]{\left|#1\right|}\) \(\newcommand{\bbar}{\overline{\bvec}}\) \(\newcommand{\bhat}{\widehat{\bvec}}\) \(\newcommand{\bperp}{\bvec^\perp}\) \(\newcommand{\xhat}{\widehat{\xvec}}\) \(\newcommand{\vhat}{\widehat{\vvec}}\) \(\newcommand{\uhat}{\widehat{\uvec}}\) \(\newcommand{\what}{\widehat{\wvec}}\) \(\newcommand{\Sighat}{\widehat{\Sigma}}\) \(\newcommand{\lt}{<}\) \(\newcommand{\gt}{>}\) \(\newcommand{\amp}{&}\) \(\definecolor{fillinmathshade}{gray}{0.9}\)We begin by fixing a language \(\mathcal{L}\). Also assume that we have been given a fixed set of \(\mathcal{L}\)-formulas, \(\Lambda\), called the set of logical axioms, and a set of ordered pairs \(\left( \Gamma, \phi \right)\), called the rules of inference. (We will specify which formulas are elements of \(\Lambda\) and which ordered pairs are rules of inference in the next two sections.) A deduction is going to be a finite sequence, or ordered list, of \(\mathcal{L}\)-formulas with certain properties.
Suppose that \(\Sigma\) is a collection of \(\mathcal{L}\)-formulas and \(D\) is a finite sequence \(\left( \phi_1, \phi_2, \ldots, \phi_n \right)\) of \(\mathcal{L}\)-formulas. We will say that \(D\) is a deduction from \(\Sigma\) if for each \(i\), \(1 \leq i \leq n\), either
- \(\phi_i \in \Lambda\) (\(\phi_i\) is a logical axiom), or
- \(\phi_i \in \Sigma\) (\(\phi_i\) is a nonlogical axiom), or
- There is a rule of inference \(\left( \Gamma, \phi_i \right)\) such that \(\Gamma \subseteq \{ \phi_i, \phi_2, \ldots, \phi_{i - 1} \}\).
If there is a deduction from \(\Sigma\), the last line of which is the formula \(\phi\), we will call this a deduction from \(\Sigma\) of \(\phi\), and write \(\Sigma \vdash \phi\).
Chaff: Well, we have now established what we mean by the word justified. In a deduction we are allowed to write down any \(\mathcal{L}\)-formula that we like, as long as that formula is either a logical axiom or is listed explicitly in a collection \(\Sigma\) of nonlogical axioms. Any formula that we write in a deduction that is not an axiom must arise from previous formulas in the deduction via a rule of inference.
You may have gathered that there are many different deductive systems, depending on the choices that are made for \(\Lambda\), and the rules of inference. As a general rule, a deductive system will either have lots of rules of inference and few logical axioms, or not too many rules and a lot of axioms. In developing the deductive system for us to use in this book, we attempt to pursue a middle course.
Also notice that \(\vdash\) is another metalinguistic symbol. It is not part of the language \(\mathcal{L}\)
Example 2.2.2. Suppose, for starters, that we don't want to make any assumptions. So, let \(\Sigma = \emptyset\), let \(\Lambda = \emptyset\), and write down a deduction from \(\Sigma\). Don't be shy. Go ahead. We'll wait.
Still nothing? Right. There are no deductions from the empty set of axioms. (Actually, after we set up our rules of inference, there will be some deductions from the empty set of axioms, but that comes later.) This is a problem that the English logician Bertrand Russell found particularly annoying as he began to learn mathematics.
At the age of eleven, I began Euclid, with my brother as my tutor. This was one of the great events of my life, as dazzling as first love. I had not imagined that there was anything so delicious in the world. ...From that moment until Whitehead and I finished Principia Mathematica, when I was thirty-eight, mathematics was my chief interest, and my chief source of happiness. Like all happiness, however, it was not unalloyed. I had been told that Euclid proved things, and was much disappointed that he started with axioms. At first I refused to accept them unless my brother could offer me some reason for doing so, but he said: "If you don't accept them we cannot go on," and as I wished to go on, I reluctantly admitted them pro tem. The doubt as to the premisses of mathematics which I felt at that moment remained with me, and determined the course of my subsequent work. [Russell 67, p. 36]
What we have managed to do with our definition of deduction, though, is to be up front about our need to make assumptions, and we will acknowledge our axiom set in every deduction that we write.
Example 2.2.3. Let us work in the language \(\mathcal{L} = \{ P \}\), where \(P\) is a binary relation symbol. Let \(\Sigma\), our set of axioms, be
\[\begin{align} \Sigma + &\{ \forall x P \left( x, x \right), \\ &P \left( u, v \right), \\ &P \left( u, v \right) \rightarrow P \left( v, u \right), \\ &P \left( v, u \right) \rightarrow P \left( u, u \right) \}. \end{align}\]
We will let \(\Lambda = \emptyset\) for now. We also need to have a set of rules of inference. So temporarily let our set of rules of inference be
\[\{ \{ \{ \alpha, \alpha \rightarrow \beta \}, \beta \} | \alpha \: \text{and} \: \beta \: \text{are formulas of} \: \mathcal{L} \}.\]
This is just the rule modus ponens, which says that from the formulas \(\alpha\) and \(\alpha \rightarrow \beta\) we may conclude \(\beta\).
Now we can write a deduction from \(\Sigma\) of the formula \(P \left( u, u \right)\), as follows:
\[\begin{align} &P \left( u, v \right) \\ &P \left( u, v \right) \rightarrow P \left( v, u \right) \\ &P \left( v, u \right) \\ &P \left( v, u \right) \rightarrow P \left( u, u \right) \\ &P \left( u, u \right). \end{align}\]
You can easily see that every formula in our deduction is either explicitly listed among the elements of our axiom set \(\Sigma\), or follows from modus ponens from previously listed formulas in the deduction.
Notice, however, that we cannot use the universal statement \(\forall x P \left( x, x \right)\) to derive our needed formula \(P \left( u, u \right)\). Even a statement that seems like it ought to follow from our axioms, \(P \left( v, v \right)\), for example, will not be deducible from \(\Sigma\) until we either add to our rules of inference or include some additional axioms. Our definition of a deduction is very limiting - we cannot even use standard logical tricks such as universal instantiation [from \(\forall x blah \left( x \right)\) deduce \(blah \left( t \right)\)]. These logical axioms will be gathered together in Section 2.3.
Chaff: It is really tempting here to write down the incorrect deduction
\[\begin{align} &\forall x P \left( x, x \right) \\ &P \left( u, u \right) \end{align}\]
Please don't say things like that until we have built our collection of logical axioms. Remember, what we are trying to do here is to have a definition of deduction that is entirely syntactic, that does not depend on the meanings of the symbols. Where you are likely to run into trouble is when you start thinking too much about the meanings of the things that you write down. Our definition gives us deductions that are easily verifiable: Given an alleged deduction from \(\Sigma\), as long as we can decide what formulas are in \(\Sigma\) we can decide if the alleged deduction is correct. In fact, we could easily program a computer to check the deduction for us. However, this ease in verification comes with a price: Deductions are difficult to write and hard to motivate.
Definition 2.2.1 is a "bottom-up" definition. It defines a deduction in terms of its parts. Another way to define a collection of things is to take a "top-down" approach. The next proposition does just that, by showing that we can think of the collection of deductions from \(\Sigma\) (called Thm\(_\Sigma\)) as the closure of the collection of axioms under the application of the rules of inference.
Fix sets of \(\mathcal{L}\)-formulas \(\Sigma\) and \(\Lambda\) and a collection of rules of inference. the set Thm\(_\Sigma = \{ \phi | \Sigma \vdash \phi \}\) is the smallest set \(C\) such that
- \(\Sigma \subseteq C\).
- \(\Lambda \subseteq C\).
- If \(\left( \Gamma, \theta \right)\) is a rule of inference and \(\Gamma \subseteq C\), then \(\theta \in C\).
This proposition makes two separate claims about the set Thm\(_\Sigma\). The first claim is that Thm\(_\Sigma\) satisfies the three criteria. The second claim is that Thm\(_\Sigma\) is the smallest set to satisfy the criteria. We tackle these claims one at a time.
First, let us look at the criteria in order, and make sure that Thm\(_\Sigma\) satisfies them. So to begin, we must show that \(\Sigma \subseteq\) Thm\(_\Sigma\). But certainly if \(\sigma \in \Sigma\), there is a deduction-from-\(\Sigma\) of \(\sigma\), for example this one-line deduction: \(\sigma\). Similarly, to show that \(\Lambda \subseteq\) Thm\(_\Sigma\). To finish this part of the proof, we must show that if \(\left( \Gamma, \theta \right)\) is a rule of inference and \(\Gamma \subseteq\) Thm\(_\Sigma\), then \(\theta \in\) Thm\(_\Sigma\). But to produce a deduction-from-\(\Sigma\) of \(\theta\), all we have to do is write down deductions of each of the \(\gamma\)'s in \(\Gamma\), followed by the formula \(\theta\). This is a valid deduction, as \(\theta\) follows from \(\Gamma\) by the rule of inference \(\left( \Gamma, \theta \right)\). Thus Thm\(_\Sigma\) satisfies the three criteria of the proposition.
Now we must show that Thm\(_\Sigma\) is the smallest such set. This is quite easy to prove once you figure out what you have to do. What is claimed is that if \(C\) is a collection of formulas satisfying the given requirements, then Thm\(_\Sigma\) \(\subseteq C\). So we assume that \(C\) is a class satisfying the conditions, and we attempt to show that every element of Thm\(_\Sigma\) is in \(C\).
If \(\phi \in\) Thm\(_\Sigma\), there is a deduction from \(\Sigma\) with last line \(\phi\). If the entry \(\phi\) is justified by virtue of \(\phi\) being either a logical or nonlogical axiom, then \(\phi\) is explicitly included in the set \(C\). If \(\phi\) is justified by reference to a rule of inference \(\left( \Gamma, \phi \right)\), then each \(\gamma \in \Gamma\) is an element of \(C\) (this is really a proof by induction, and here is where we use the inductive hypothesis), and thus, by the third requirement on \(C\), \(\phi \in C\), as needed.
Since Thm\(_\Sigma\) \(\subseteq C\) for all such sets \(C\), Thm\(_\Sigma\) is the smallest such set, as claimed.
\(\square\)
Here is what we will do in the next few sections: We will define \(\Lambda\), the fixed set of logical axioms; we will establish our collection of rules of inference; we will prove some results about deductions; and finally, we will discuss some examples of sets of nonlogical axioms.
Exercises
- Let the collection of nonlogical axioms be
\[\Sigma = \{ \left( A \left( x \right) \land A \left( x \right) \right) \rightarrow B \left( x, y \right), A \left( x \right), B \left( x, y \right) \rightarrow A \left( x \right) \},\]
and let the rule of inference be modus ponens, as in Example 2.2.3. For each of the following, decide if it is a deduction. If it is not a deduction, explain how you know that it is not a deduction.
(a)
\[\begin{align} &A \left( x \right) \\ &A \left( x \right) \land A \left( x \right) \\ &\left( A \left( x \right) \land A \left( x \right) \right) \rightarrow B \left( x, y \right) \\ &B \left( x, y \right) \end{align}\]
(b)
\[\begin{align} &B \left( x, y \right) \rightarrow A \left( x \right) \\ &A \left( x \right) \\ &B \left( x, y \right) \end{align}\]
(c)
\[\begin{align} &\left( A \left( x \right) \land A \left( x \right) \right) \rightarrow B \left( x, y \right) \\ &B \left( x, y \right) \rightarrow A \left( x \right) \\ &\left( A \left( x \right) \land A \left( x \right) \right) \rightarrow A \left( x \right) \end{align}\] - Consider the axiom system \(\Sigma\) of Example 2.2.3. It is implied in that example that there is no deduction from \(\Sigma\) of the formula \(P \left( v, v \right)\). Prove this fact.
- Carefully write out the proof of Proposition 2.2.4, worrying about the inductive step. [Suggestion: You may want to proceed by induction on the length of the shortest deduction of \(\phi\).]
- Let \(\mathcal{L}\) be a language that consists of a single unary predicate symbol \(R\), and let \(B\) be the infinite set of axioms
\[\begin{align} B = &\{ R \left( x_1 \right), \\ &R \left( x_1 \right) \rightarrow R \left( x_2 \right), \\ &R \left( x_2 \right) \rightarrow R \left( x_3 \right), \\ &\: \: \: \: \: \: \: \: \: \: \: \: \: \: \: \vdots \\ &R \left( x_i \right) \rightarrow R \left( x_{i + 1} \right), \\ &\: \: \: \: \: \: \: \: \: \: \: \: \: \: \: \vdots \\ &\: \: \: \: \: \: \: \: \: \: \: \: \: \: \: \: \: \: \}. \end{align}\]
Using modus ponens as the only rule of inference, prove by induction that \(B \vdash R \left( x_j \right)\) for each natural number \(j \geq 1\).