8.5: More Rules
- Page ID
- 223906
\( \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}\)Here are a few more rules to flesh out our natural deduction system. Your instructor may or may not want you to devote the time and energy to learning them.
The first rule fills a gap in our current system: we have no way of dealing with biconditionals! That’s a pretty glaring omission. Without rules like this one, we’re stuck treating biconditionals as unbreakable units or atoms that are more or less useless aside from what they can do as a whole. We’ve used biconditionals before, but we’ve never looked inside of a biconditional while doing natural deduction. This rule fixes that problem. Treat it as a rule of replacement:
Biconditional (Bc):
\[(\varphi \leftrightarrow \chi) :: [(\varphi \rightarrow \chi ) \wedge (\chi \rightarrow \varphi )]\nonumber\]
You can replace any biconditional statement with a conjunction of both corresponding conditional statements. After using Biconditional (a sort of combination of “biconditional introduction” and “biconditional elimination”), you can simplify the conjunction to get a single direction of the conditional. You might be able to see intuitively that we could do biconditional modus ponens and biconditional modus tollens. Some more powerful systems have these as rules. We won’t make a separate rule for them here, but they are perfectly valid rules that simply bypass the steps of using Biconditional and then Simplification.
Here's a second biconditional rule you may want to make use of. It’s a bit more counterintuitive in that it rests on the fact that it’s a material biconditional and material biconditionals are sort of weird:
Bc2:
\[(\varphi \leftrightarrow \chi) :: [(\varphi \wedge \chi ) \vee (\sim \varphi \wedge \sim \chi )]\nonumber\]
Also, Associativity works for biconditionals too:
Associativity:
\[[(\Delta \leftrightarrow (\Omega \leftrightarrow \Phi )] :: [(\Delta \leftrightarrow \Omega ) \leftrightarrow \Phi ]\nonumber\]
There are a few more sort of standard rules that your instructor may want to include:
Exportation:
\[[(\varphi \wedge \chi) \rightarrow \Psi ] :: [(\varphi \rightarrow \chi) \rightarrow \Psi ]\nonumber\]
Distribution:
\[[(\varphi \wedge (\chi \vee \Psi )] :: [(\varphi \wedge \chi) \vee (\varphi \wedge \Psi )]\nonumber\]
\[[(\varphi \vee (\chi \wedge \Psi )] :: [(\varphi \vee \chi) \wedge (\varphi \vee \Psi )]\nonumber\]
Negation of Conditional:
\[\sim (\varphi \rightarrow \chi ) :: (\varphi \wedge \sim \chi)\nonumber\]
Negation of Biconditional:
\[\sim (\varphi \leftrightarrow \chi ) :: (\varphi \leftrightarrow \sim \chi)\nonumber\]
You might also find useful certain sorts of axiomatic or trivial rules. Here are a few that your instructor might want to make use of:
Trivial Implication:
\[\begin{align*} & \chi \\ & \overline{(\varphi \rightarrow \chi )} \end{align*}\]
Excluded Middle MP:
\[\begin{align*} & (\varphi \rightarrow \chi ) \\ & \underline{(\sim \varphi \rightarrow \chi )} \\ & \chi \end{align*}\]
Tautology 1 (T1):
Notice that you don’t need any premise to posit a tautology. The justification would be “T1”.
\[(\chi \rightarrow \chi)\nonumber\]
Tautology 2 (T2):
Notice that you don’t need any premise to posit a tautology. The justification would be “T2”.
\[(\chi \vee \sim \chi)\nonumber\]
Tautology 3 (T3):
\[\begin{align*} & \chi \\ & \overline{(\chi \wedge \chi)}\end{align*}\]
Or
\[\begin{align*} & \chi \\ & \overline{(\chi \vee \chi)}\end{align*}\]