2.5.5: Examples of Derivations

\(\def\Assign#1#2{ { #1^{\Struct{#2}} } }\)
\(\def\Atom#1#2{ { \mathord{#1}(#2) } }\)
\(\def\Bin{ {\mathbb{B}} }\)
\(\def\cardeq#1#2{ { #1 \approx #2 } }\)
\(\def\cardle#1#2{ { #1 \preceq #2 } }\)
\(\def\cardless#1#2{ { #1 \prec #2 } }\)
\(\def\cardneq#1#2{ { #1 \not\approx #2 } }\)
\(\def\comp#1#2{ { #2 \circ #1 } }\)
\(\def\concat{ { \;\frown\; } }\)
\(\def\Cut{ { \text{Cut} } }\)
\(\def\Discharge#1#2{ { [#1]^#2 } }\)
\(\def\DischargeRule#1#2{ { \RightLabel{#1}\LeftLabel{\scriptsize{#2} } } }\)
\(\def\dom#1{ {\operatorname{dom}(#1)} }\)
\(\def\Domain#1{ {\left| \Struct{#1} \right|} }\)
\(\def\Elim#1{ { {#1}\mathrm{Elim} } }\)
\(\newcommand{\Entails}{\vDash}\)
\(\newcommand{\EntailsN}{\nvDash}\)
\(\def\eq[#1][#2]{ { #1 = #2 } }\)
\(\def\eqN[#1][#2]{ { #1 \neq #2 } }\)
\(\def\equivclass#1#2{ { #1/_{#2} } }\)
\(\def\equivrep#1#2{ { [#1]_{#2} } }\)
\(\def\Exchange{ { \text{X} } }\)
\(\def\False{ { \mathbb{F} } }\)
\(\def\FalseCl{ { \lfalse_C } }\)
\(\def\FalseInt{ { \lfalse_I } }\)
\(\def\fCenter{ { \,\Sequent\, } }\)
\(\def\fdefined{ { \;\downarrow } }\)
\(\def\fn#1{ { \operatorname{#1} } }\)
\(\def\Frm[#1]{ {\operatorname{Frm}(\Lang #1)} }\)
\(\def\fundefined{ { \;\uparrow } }\)
\(\def\funimage#1#2{ { #1[#2] } }\)
\(\def\funrestrictionto#1#2{ { #1 \restriction_{#2} } }\)
\(\newcommand{\ident}{\equiv}\)
\(\newcommand{\indcase}[2]{#1 \ident #2\text{:}}\)
\(\newcommand{\indcaseA}[2]{#1 \text{ is atomic:}}\)
\(\def\indfrm{ { A } }\)
\(\def\indfrmp{ { A } }\)
\(\def\joinrel{\mathrel{\mkern-3mu}}\)
\(\def\lambd[#1][#2]{\lambda #1 . #2}\)
\(\def\Lang#1{ { \mathcal{#1} } }\)
\(\def\LeftR#1{ { {#1}\mathrm{L} } }\)
\(\def\len#1{ {\operatorname{len}(#1)} }\)
\(\def\lexists#1#2{ { \exists #1\, #2 } }\)
\(\def\lfalse{ {\bot} }\)
\(\def\lforall#1#2{ { \forall#1\, #2 } }\)
\(\newcommand{\lif}{\rightarrow}\)
\(\newcommand{\liff}{\leftrightarrow}\)
\(\def\Log#1{ { \mathbf{#1} } }\)
\(\def\ltrue{ {\top} }\)
\(\def\Id#1{ {\operatorname{Id}_#1} }\)
\(\def\Int{ {\mathbb{Z}} }\)
\(\def\Intro#1{ { {#1}\mathrm{Intro} } }\)
\(\def\mModel#1{ { \mathfrak{#1} } }\)
\(\newcommand{\mSat}[3][{}]{\mModel{#2}{#1}\Vdash{#3}}\)
\(\newcommand{\mSatN}[3][{}]{\mModel{#2}{#1}\nVdash{#3}}\)
\(\def\Nat{ {\mathbb{N}} }\)
\(\def\nicefrac#1#2{ {{}^#1/_#2} }\)
\(\def\num#1{ { \overline{#1} } }\)

\(\def\ran#1{ {\operatorname{ran}(#1)} }\)
\(\newcommand{\Obj}[1]{\mathsf{#1}}\)
\(\def\Rat{ {\mathbb{Q}} }\)
\(\def\Real{ {\mathbb{R}} }\)
\(\def\RightR#1{ { {#1}\mathrm{R} } }\)
\(\def\Part#1#2{ { \Atom{\Obj P}{#1, #2} } }\)
\(\def\pto{ { \hspace{0.1 cm}\to\hspace{-0.44 cm}\vcenter{\tiny{\hbox{|}}}\hspace{0.35 cm} } }\)
\(\def\PosInt{ {\mathbb{Z}^+} }\)
\(\def\Pow#1{ {\wp(#1)} }\)
\(\newcommand{\Proves}{\vdash}\)
\(\newcommand{\ProvesN}{\nvdash}\)
\(\def\Relbar{\mathrel{=}}\)
\(\newcommand{\Sat}[3][{}]{\Struct{#2}{#1}\vDash{#3}}\)
\(\newcommand{\SatN}[3][{}]{\Struct{#2}{#1}\nvDash{#3}}\)
\(\newcommand{\Sequent}{\Rightarrow}\)
\(\def\Setabs#1#2{ { \{#1:#2\} } }\)
\(\newcommand{\sFmla}[2]{#1\,#2}\)
\(\def\Struct#1{ {#1} }\)
\(\def\subst#1#2{ { #1/#2 } }\)
\(\def\Subst#1#2#3{ { #1[\subst{#2}{#3}] } }\)
\(\def\TMblank{ { 0 } }\)
\(\newcommand{\TMendtape}{\triangleright}\)
\(\def\TMleft{ { L } }\)
\(\def\TMright{ { R } }\)
\(\def\TMstay{ { N } }\)
\(\def\TMstroke{ { 1 } }\)
\(\def\TMtrans#1#2#3{ { #1,#2,#3 } }\)
\(\def\Trm[#1]{ {\operatorname{Trm}(\Lang #1)} }\)
\(\def\True{ { \mathbb{T} } }\)
\(\newcommand{\TRule}[2]{#2#1}\)
\(\def\tuple#1{ {\langle #1 \rangle} }\)
\(\newcommand{\Value}[3][\,]{\mathrm{Val}_{#1}^{#3}(#2)}\)
\(\def\Var{ { \mathrm{Var} } }\)
\(\newcommand{\varAssign}[3]{#1 \sim_{#3} #2}\)
\(\def\Weakening{ { \text{W} } }\)

Example \(\PageIndex{1}\)

Let’s give a derivation of the sentence \((A \land B) \lif A\).

We begin by writing the desired conclusion at the bottom of the derivation.

Next, we need to figure out what kind of inference could result in a sentence of this form. The main operator of the conclusion is \(\lif\), so we’ll try to arrive at the conclusion using the \(\Intro{\lif}\) rule. It is best to write down the assumptions involved and label the inference rules as you progress, so it is easy to see whether all assumptions have been discharged at the end of the proof.

We now need to fill in the steps from the assumption \(A \land B\) to \(A\). Since we only have one connective to deal with, \(\land\), we must use the \(\land\) elim rule. This gives us the following proof:

We now have a correct derivation of \((A \land B) \lif A\).

Example \(\PageIndex{2}\)

Now let’s give a derivation of \((\lnot A \lor B) \lif (A \lif B)\).

We begin by writing the desired conclusion at the bottom of the derivation.

To find a logical rule that could give us this conclusion, we look at the logical connectives in the conclusion: \(\lnot\), \(\lor\), and \(\lif\). We only care at the moment about the first occurence of \(\lif\) because it is the main operator of the sentence in the end-sequent, while \(\lnot\), \(\lor\) and the second occurence of \(\lif\) are inside the scope of another connective, so we will take care of those later. We therefore start with the \(\Intro{\lif}\) rule. A correct application must look like this:

This leaves us with two possibilities to continue. Either we can keep working from the bottom up and look for another application of the \(\Intro{\lif}\) rule, or we can work from the top down and apply a \(\Elim{\lor}\) rule. Let us apply the latter. We will use the assumption \(\lnot A \lor B\) as the leftmost premise of \(\Elim{\lor}\). For a valid application of \(\Elim{\lor}\), the other two premises must be identical to the conclusion \(A \lif B\), but each may be derived in turn from another assumption, namely the two disjuncts of \(\lnot A \lor B\). So our derivation will look like this:

In each of the two branches on the right, we want to derive \(A \lif B\), which is best done using \(\Intro{\lif}\).

For the two missing parts of the derivation, we need derivations of \(B\) from \(\lnot A\) and \(A\) in the middle, and from \(A\) and \(B\) on the left. Let’s take the former first. \(\lnot A\) and \(A\) are the two premises of \(\Elim{\lnot}\):

By using \(\FalseInt\), we can obtain \(B\) as a conclusion and complete the branch.

Let’s now look at the rightmost branch. Here it’s important to realize that the definition of derivation allows assumptions to be discharged but does not require them to be. In other words, if we can derive \(B\) from one of the assumptions \(A\) and \(B\) without using the other, that’s ok. And to derive \(B\) from \(B\) is trivial: \(B\) by itself is such a derivation, and no inferences are needed. So we can simply delete the assumption \(A\).

Note that in the finished derivation, the rightmost \(\Intro{\lif}\) inference does not actually discharge any assumptions.

Example \(\PageIndex{3}\)

So far we have not needed the \(\FalseCl{}\) rule. It is special in that it allows us to discharge an assumption that isn’t a sub-formula of the conclusion of the rule. It is closely related to the \(\FalseInt{}\) rule. In fact, the \(\FalseInt{}\) rule is a special case of the \(\FalseCl{}\) rule—there is a logic called “intuitionistic logic” in which only \(\FalseInt{}\) is allowed. The \(\FalseCl{}\) rule is a last resort when nothing else works. For instance, suppose we want to derive \(A \lor \lnot A\). Our usual strategy would be to attempt to derive \(A \lor \lnot A\) using \(\Intro{\lor}\). But this would require us to derive either \(A\) or \(\lnot A\) from no assumptions, and this can’t be done. \(\FalseCl{}\) to the rescue!

Now we’re looking for a derivation of \(\lfalse\) from \(\lnot(A \lor \lnot A)\). Since \(\lfalse\) is the conclusion of \(\Elim{\lnot}\) we might try that:

Our strategy for finding a derivation of \(\lnot A\) calls for an application of \(\Intro{\lnot}\):

Here, we can get \(\lfalse\) easily by applying \(\Elim{\lnot}\) to the assumption \(\lnot(A \lor \lnot A)\) and \(A \lor \lnot A\) which follows from our new assumption \(A\) by \(\Intro{\lor}\):

On the right side we use the same strategy, except we get \(A\) by \(\FalseCl\):

Problem \(\PageIndex{1}\)

Give derivations of the following:

1. \(\lnot(A \lif B) \lif (A \land \lnot B)\)
2. \((A \lif C) \lor (B \lif C)\) from the assumption \((A \land B) \lif C\)
3. \(\lnot \lnot A \lif A\)
4. \(\lnot A \lif \lnot B\) from the assumption \(B \lif A\)
5. \(\lnot A\) from the assumption \(( A \lif \lnot A )\)
6. \(A\) from the assumptions \(B \lif A\) and \(\lnot B \lif A\)