use standard rules for ND (fixes issue #144)

content/first-order-logic/natural-deduction/identity.tex

@@ -41,8 +41,8 @@
 \begin{ex}
 If $s$ and $t$ are closed terms, then $!A(s), \eq[s][t] \Proves !A(t)$:
 \[
-\AxiomC{$!A(s)$}
 \AxiomC{$\eq[s][t]$}
+\AxiomC{$!A(s)$}
 \RightLabel{$\Elim{\eq}$}
 \BinaryInfC{$!A(t)$}
 \DisplayProof

content/first-order-logic/natural-deduction/provability.tex

@@ -51,7 +51,7 @@
 
 \begin{prop}
 \ollabel{prop:provability-contr} If $\Gamma \Proves
-  !A$ and $\Gamma \cup \{!A\} \Proves \lfalse$, then
+  !A$ and $\Gamma \cup \{!A\}$ is inconsistent, then
   $\Gamma$ is inconsistent.
 \end{prop}
 
@@ -60,14 +60,14 @@
   $\delta_1$ and the !!{derivation} of $\lfalse$ from $\Gamma \cup \{!A\}$
   be $\delta_2$. We can then !!{derive}:
 \[
-\AxiomC{}
-\RightLabel{$\delta_1$}
-\DeduceC{$!A$}
 \AxiomC{$\Discharge{!A}{1}$}
 \RightLabel{$\delta_2$}
 \DeduceC{$\lfalse$}
 \DischargeRule{\Intro{\lnot}}{1}
 \UnaryInfC{$\lnot !A$}
+\AxiomC{}
+\RightLabel{$\delta_1$}
+\DeduceC{$!A$}
 \RightLabel{\Elim{\lnot}}
 \BinaryInfC{$\lfalse$}
 \DisplayProof
@@ -77,14 +77,14 @@
 \end{proof}
 
 \begin{prop}
-\ollabel{prop:provability-lnot} If $\Gamma \cup \{!A\} \Proves
-\lfalse$, then $\Gamma \Proves \lnot !A$.
+\ollabel{prop:provability-lnot} If $\Gamma \cup \{!A\}$ is
+inconsistent, then $\Gamma \Proves \lnot !A$.
 \end{prop}
 
 \begin{proof}
-Suppose that $\Gamma \cup \{!A\} \Proves \lfalse$. Then there is a
-  derivation of $\lfalse$ from $\Gamma \cup \{!A\}$.  Let $\delta$ be
-  the !!{derivation} of $\lfalse$, and consider
+Suppose that $\Gamma \cup \{!A\}$ is inconsistent. Then there is
+!!a{derivation} of $\lfalse$ from $\Gamma \cup \{!A\}$.  Let $\delta$
+be the !!{derivation} of $\lfalse$, and consider
 \[
 \AxiomC{$\Discharge{!A}{1}$}
 \RightLabel{$\delta$}
@@ -101,43 +101,44 @@
 \end{prop}
 
 \begin{proof}
-  This is a simple application of the $\Intro{\lfalse}$ rule.
+  This is a simple application of the $\Elim{\lnot}$ rule.
 \end{proof}
 
 
 \begin{prop}
-\ollabel{prop:provability-exhaustive} If $\Gamma \cup \{!A\} \Proves
-\lfalse$ and $\Gamma \cup \{\lnot !A\} \Proves \lfalse$, then $\Gamma
-\Proves \lfalse$.
+\ollabel{prop:provability-exhaustive} If $\Gamma \cup \{!A\}$ is
+inconsistent and $\Gamma \cup \{\lnot !A\}$ is inconsistent, then
+$\Gamma$ is inconsistent.
 \end{prop}
 
 \begin{proof}
 There are !!{derivation}s $\delta_1$ and $\delta_2$ of $\lfalse$ from
-  $\Gamma \cup,\{ !A \}$ and $\lfalse$ from $\Gamma \cup \{ \lnot !A
+  $\Gamma \cup \{ !A \}$ and $\lfalse$ from $\Gamma \cup \{ \lnot !A
   \}$, respectively. We can then !!{derive}
 \[
-\AxiomC{$\Discharge{!A}{1}$}
-\RightLabel{$\delta_1$}
-\DeduceC{$\lfalse$}
-\DischargeRule{\Intro{\lnot}}{1}
-\UnaryInfC{$\lnot !A$}
 \AxiomC{$\Discharge{\lnot !A}{2}$}
 \RightLabel{$\delta_2$}
 \DeduceC{$\lfalse$}
 \DischargeRule{\Intro{\lnot}}{2}
 \UnaryInfC{$\lnot \lnot !A$}
+\AxiomC{$\Discharge{!A}{1}$}
+\RightLabel{$\delta_1$}
+\DeduceC{$\lfalse$}
+\DischargeRule{\Intro{\lnot}}{1}
+\UnaryInfC{$\lnot !A$}
 \RightLabel{\Elim{\lnot}}
 \BinaryInfC{$\lfalse$}
 \DisplayProof
 \]
 Since the assumptions $!A$ and $\lnot !A$ are !!{discharged}, this is
-!!a{derivation} from~$\Gamma$ alone. Hence $\Gamma \Proves \lfalse$.
+!!a{derivation} of~$\lfalse$ from~$\Gamma$ alone. Hence $\Gamma$ is
+inconsistent.
 \end{proof}
 
 \begin{prop}
-\ollabel{prop:provability-lor-left} If $\Gamma \cup \{!A\} \Proves
-\lfalse$ and $\Gamma \cup \{!B\} \Proves \lfalse$, then $\Gamma \cup
-\{!A \lor !B\} \Proves \lfalse$.
+\ollabel{prop:provability-lor-left} If $\Gamma \cup \{!A\}$ and and
+$\Gamma \cup \{!B\}$ are both inconsistent, then $\Gamma \cup \{!A
+\lor !B\}$ is inconsistent.
 \end{prop}
 
 \begin{proof}
@@ -237,11 +238,11 @@
   $\Gamma$. Consider:
 \[
 \AxiomC{}
-\RightLabel{$\delta_1$}
-\DeduceC{$!A$}
-\AxiomC{}
 \RightLabel{$\delta_2$}
 \DeduceC{$!A \lif !B$}
+\AxiomC{}
+\RightLabel{$\delta_1$}
+\DeduceC{$!A$}
 \RightLabel{\Elim{\lif}}
 \BinaryInfC{$!B$}
 \DisplayProof
@@ -263,13 +264,13 @@
   Then there is a !!{derivation}~$\delta$ of $\lnot !A$ from~$\Gamma$.  The
   following !!{derivation} shows that $\Gamma \Proves !A \lif !B$:
 \[
-\AxiomC{$\Discharge{!A}{1}$}
 \AxiomC{}
 \RightLabel{$\delta$}
 \DeduceC{$\lnot !A$}
-\RightLabel{\Intro{\lfalse}}
+\AxiomC{$\Discharge{!A}{1}$}
+\RightLabel{\Elim{\lnot}}
 \BinaryInfC{$\lfalse$}
-\RightLabel{\Elim{\lfalse}}
+\RightLabel{\FalseInt}
 \UnaryInfC{$!B$}
 \DischargeRule{\Intro{\lif}}{1}
 \UnaryInfC{$!A \lif !B$}
@@ -291,7 +292,10 @@
 \DischargeRule{\Intro{\lif}}{1}
 \UnaryInfC{$!A \lif !B$}
 \DisplayProof
-\] }
+\]
+(In fact we can simply add $\Intro{\lif}$ to~$\delta$, since
+$\Intro{\lif}$ may, but does not have to, !!{discharge} the
+assumption~$!A$.)}
 \end{proof}
 
 \begin{probtag}{probIf}