corrections for proof-theory

Author: rzach

content/intuitionistic-logic/introduction/axiomatic-derivations.tex

@@ -56,7 +56,8 @@
 \end{defn}
 
 \begin{prop}
-  If $\Gamma \Proves !A$ in intuitionistic logic, $\Gamma \Proves !A$ in
+  If $\Gamma \Proves !A$ in the axiomatic !!{derivation} system for
+  intuitionistic logic, $\Gamma \Proves !A$ also in
   classical logic. In particular, if $!A$ is an intuitionistic
   theorem, it is also a classical theorem.
 \end{prop}

content/intuitionistic-logic/introduction/natural-deduction.tex

@@ -116,12 +116,12 @@ \subsection{Disjunction}
 \end{defish}
 
 If we have a construction~$N_i$ of~$!A_i$ we can turn it into a
-construction~$\tuple{i, N_i}$ of~$!A_1 \lor !A_2$. On the other hand, suppose
-we have a construction of~$!A_1 \lor !A_2$, i.e., a pair $\tuple{i, N_i}$
-where $N_i$ is a construction of~$!A_i$, and also functions $f_1$, $f_2$,
-which turn constructions of $!A_1$, $!A_2$, respectively, into constructions
-of~$!C$. Then $f_i(N_i)$ is a construction of~$!C$, the conclusion
-of~$\Elim\lor$.
+construction~$\tuple{i, N_i}$ of~$!A_1 \lor !A_2$. On the other hand,
+suppose we have a construction of~$!A_1 \lor !A_2$, i.e., a pair
+$\tuple{i, N_i}$ where $N_i$ is a construction of~$!A_i$, and also
+functions $f_1$, $f_2$, which turn constructions of $!A_1$, $!A_2$,
+respectively, into constructions of~$!C$. Then $f_i(N_i)$ is a
+construction of~$!C$, the conclusion of~$\Elim\lor$.
 
 \subsection{Absurdity}
 
@@ -234,9 +234,9 @@ \subsection{Examples of \usetoken{P}{derivation}}
 \end{enumerate}
 
 \begin{prop}
-  If $\Gamma \Proves !A$ in intuitionistic logic, $\Gamma \Proves !A$ in
-  classical logic. In particular, if $!A$ is an intuitionistic
-  theorem, it is also a classical theorem.
+  If $\Gamma \Proves !A$ in natural deduction for intuitionistic
+  logic, $\Gamma \Proves !A$ in classical logic. In particular, if
+  $!A$ is an intuitionistic theorem, it is also a classical theorem.
 \end{prop}
 
 \begin{proof}

content/proof-theory/cut-elimination/ce-topmost.tex

@@ -63,10 +63,11 @@
 induction basis. In the inductive step we assume $\cheight{\pi} > 0$
 or $\cutrank{\pi} > 0$ (or both). We can use the inductive hypothesis,
 namely that the last~\CutCS{} can be removed from any !!{proof} which
-either has at most the same cut rank and a lower cut !!{height}, or
-has a lower cut rank. The case where $\cheight{\pi} = 0$ (both
-premises are axioms) are covered by cases~A and~B. The cases where
-$\cheight{\pi} > 0$ are covered by cases C--D.
+ends in a single~\CutCS{} which either has cut rank $= \cutrank{\pi}$
+and a cut !!{height} $< \cheight{\pi}$, or has cut rank~$<
+\cutrank{\pi}$. The case where $\cheight{\pi} = 0$ (both premises are
+axioms) are covered by cases~A and~B. The cases where $\cheight{\pi} >
+0$ are covered by cases C--D.
 
 \paragraph{Case A:}
 Some $!B$ occurs in both $\Gamma$ and~$\Delta$. 
@@ -144,11 +145,11 @@
 \DisplayProof
 \]
 This only covers the case where $R$~is a right rule with one premise,
-$A$~is not principal on the right, and the !!{formula}~$!D$ which
+$A$~is not the principal !!{formula} of~$R$, and the !!{formula}~$!D$ which
 \emph{is} principal occurs in the succedent of the right premise
 of~\CutCS. If $!D$~occurs in the antecedent (i.e., $R$ is a left rule)
 or in the left premise of~\CutCS, it would look different, of course.
-The !!{formula}s in $\Pi$ and $\Lambda$ represent the active
+The !!{formula}s in $\Pi$ and~$\Lambda$ represent the active
 !!{formula}s of rule~$R$.
 
 We turn this order around and consider !!a{proof}
@@ -561,6 +562,7 @@
 \]
 (The induction hypothesis applies since the cut !!{formula}
 is~$!B(t)$, so the !!{proof} has lower cut rank than~$\pi$.)
+\item We leave the case $!A \ident \lexists[x][!B(x)]$ as an exercise.
 \end{enumerate}
 \end{proof}
 

content/proof-theory/cut-elimination/interpolation.tex

@@ -25,7 +25,7 @@
 the philosophy of science, since it can be used to study the
 primitives by which a theory can or cannot be axiomatized. It also
 implies Beth's definability theorem, which states that if a theory can
-implicitly define a concept, if can define it explicitly.
+implicitly define a concept, it can define it explicitly.
 
 Like many results in mathematical logic, the interpolation theorem can
 be proved both using the methods of model theory and those of proof
@@ -42,21 +42,24 @@
 \begin{thm}[Craig's Interpolation Theorem]\ollabel{thm:interpolation}
 Let the !!{language} of~$!A$ be $\Lang L(!A)$ and that of $!B$ be
 $\Lang L(!B)$. If $\Log{G3c} \Proves !A \Sequent !B$ then there is
-!!a{formula}~$!C$ in the !!{language}~$\Lang L(!A) \cap \Lang L(!B)$
-such that $\Log{G3c} \Proves !A \Sequent !C$ and $\Log{G3c} \Proves !C \Sequent !B$.
+!!a{formula}~$!C$ in the !!{language}~$\Lang L(!C) \subseteq \Lang
+L(!A) \cap \Lang L(!B)$ such that $\Log{G3c} \Proves !A \Sequent !C$
+and $\Log{G3c} \Proves !C \Sequent !B$.
 \end{thm}
 
 We prove a generalization of the interpolation theorem to make use of
 the structure of !!{proof}s in~\Log{G3c}. To this end, imagine the
 antecendent and succedents of sequents to be separated into two parts
-each. We write $\maeh{\Gamma_1}{\Gamma_2} \Sequent \maeh{\Delta_1}{\Delta_2}$ to
-indicate that $\Gamma_1$ and $\Delta_1$ belong to the first part and
-$\Gamma_2$ and $\Delta_2$ to the second part. The interpolation
-theorem then follows immediately from the following lemma.
+each. We write $\maeh{\Gamma_1}{\Gamma_2} \Sequent
+\maeh{\Delta_1}{\Delta_2}$ to indicate that $\Gamma_1$ and $\Delta_1$
+belong to the first part and $\Gamma_2$ and $\Delta_2$ to the second
+part. The interpolation theorem then follows immediately from the
+following lemma.
 
 \begin{lem}[Maehara's Lemma]\ollabel{lem:maehara} If $\Log{G3c}
 \Proves \maeh{\Gamma_1}{\Gamma_2} \Sequent \maeh{\Delta_1}{\Delta_2}$
-then there is !!a{formula}~$!C$ in the !!{language}~$\Lang L(\Gamma_1,
+then there is !!a{formula}~$!C$ in the !!{language}~$\Lang L(!C)
+\subseteq \Lang L(\Gamma_1,
 \Delta_1) \cap \Lang L(\Gamma_2, \Delta_2)$ such that $\Log{G3c}
 \Proves \Gamma_1 \Sequent \Delta_1, !C$ and $\Log{G3c} \Proves !C,
 \Gamma_2 \Sequent \Delta_2$.
@@ -150,10 +153,10 @@
     already told us that the sequent on the right is !!{provable}, and
     the sequent on the left follows from the sequent we got from the
     inductive hypothesis by~$\RightR{\lnot}$. The inductive hypothesis
-    also tells us that $\Lang L(!C_1) \in \Lang L(!A, \Gamma_1,
+    also tells us that $\Lang L(!C_1) \subseteq \Lang L(!A, \Gamma_1,
     \Delta_1) \cap \Lang L(\Gamma_2, \Delta_2)$. Since $\Lang L(\lnot
     !A) = \Lang L(!A)$ and $\Lang L(!C) = \Lang L(!C_1)$ we have that
-    $\Lang L(!C_1) \in \Lang L(\Gamma_1, \Delta_1, \lnot !A) \cap \Lang
+    $\Lang L(!C_1) \subseteq \Lang L(\Gamma_1, \Delta_1, \lnot !A) \cap \Lang
     L(\Gamma_2, \Delta_2)$.
 
     In the second scenario the situation is slightly different
@@ -169,7 +172,7 @@
     \end{align*}
     These are again exactly the sequents we want to be !!{provable} if
     $!C_1$ is an interpolant; we again let $!C \ident !C_1$. $\Lang
-    L(!C_1) \in \Lang L(\Gamma_1, \Delta_1) \cap \Lang L(\Gamma_2,
+    L(!C_1) \subseteq \Lang L(\Gamma_1, \Delta_1) \cap \Lang L(\Gamma_2,
     \Delta_2, \lnot !A)$ as before.
     \item $\pi$ ends in $\RightR{\lif}$ with principal !!{formula}~$!A
     \lif !B$. We again have two cases, depending on whether $!A \lif
@@ -306,9 +309,9 @@
     !!{formula} built from $!C_1$ and $!C_2$, but this time we need it
     in the antecedent (since we're now dealing with the second part).
     Applying $\LeftR{\land}$ does the trick; we should take $!C \ident
-    (!C_1 \land !C_2)$ as the interpolant.
-    Fortuitously, we can use the remaining sequents (1) and (3) to
-    !!{prove} the corresponding sequent for the other part:
+    (!C_1 \land !C_2)$ as the interpolant. Fortuitously, we can use
+    the remaining sequents (1) and (3) to !!{prove} the corresponding
+    sequent for the other part:
     \[
     \AxiomC{}
     \Deduce$\Gamma_1 \fCenter \Delta_1, !C_1$
@@ -321,8 +324,9 @@
     As before, we have $\Lang L(!C_1 \land !C_2) \subseteq \Lang
     L(\Gamma_1, \Delta_1) \cap \Lang L(\Gamma_2, \Delta_2, !A \lif
     !B)$.
-    \item $\pi$ ends in $\RightR{\lforall}$:
-        \[
+
+    \item $\pi$ ends in $\RightR{\lforall}$ with principal !!{formula}~$\lforall[x][!A(x)]$:
+    \[
     \AxiomC{}
     \RightLabel{$\pi_1$}
     \Deduce$\maeh{\Gamma_1}{\Gamma_2} \fCenter
@@ -362,9 +366,11 @@
     condition.
 
     The other scenario is similar.
-    \item $\pi$ ends in $\RightR{\lexists}$. We again have two
-    scenarios. We consider the scenario where $\lexists[x][!A(x)]$
-    belongs to the first part, and leave the other as an exercise.
+
+    \item $\pi$ ends in $\RightR{\lexists}$ with principal
+    !!{formula}~$\lexists[x][!A(x)]$. We again have two scenarios. We
+    consider the scenario where $\lexists[x][!A(x)]$ belongs to the
+    first part, and leave the other as an exercise.
 
     In the first scenario, $\pi$ ends in
     \[
@@ -454,6 +460,7 @@
     !!{proof} is satisfied because $b \notin \Lang L(\Gamma_2,
     \Delta_2)$, and $!C_1'$ was defined so it does not contain~$b$.
   \end{enumerate}
+  The other cases are similary; we leave them as exercises.
 \end{proof}
 
 \begin{prob}
@@ -527,22 +534,24 @@
   Replace $R'$ everywhere by~$R$ in the !!{proof} of the second sequent
   to get !!a{proof} of}
     !A(c_1, \dots, c_n), \Gamma & \Sequent R(c_1, \dots, c_n)
-  \intertext{Apply \RightR{\lif} and \RightR{\lforall} to get !!a{proof} of}
-    \Gamma & \Sequent \lforall[x_1][\dots\lforall[x_n][(R(x_1,\dots,x_n) \liff !A(x_1, \dots, x_n))]].
   \end{align*}
+  Apply \RightR{\lif} and \RightR{\lforall} to get !!a{proof} of
+  \[
+    \Gamma \Sequent \lforall[x_1][\dots\lforall[x_n][(R(x_1,\dots,x_n) \liff !A(x_1, \dots, x_n))]].
+  \]
   This shows that $!A(x_1, \dots, x_n)$ explicitly defines $!R$
   in~$\Gamma$.
 \end{proof}
 
 A third result which is equivalent to interpolation (and, like it, can
 be proved using Maehara's Lemma) is the following theorem: If two
 consistent theories~$\Gamma_1$, $\Gamma_2$ contain a complete theory
-$\Gamma$ in the language~$\Lang L(\Gamma_1) \cap \Lang L(\Gamma_2)$,
-then $\Gamma_1 \cup \Gamma_2$ is consistent.
+$\Gamma$ in the language~$\Lang L(\Gamma) \subseteq \Lang L(\Gamma_1)
+\cap \Lang L(\Gamma_2)$, then $\Gamma_1 \cup \Gamma_2$ is consistent.
 
 Recall that a complete theory is one such that for every
 !!{sentence}~$!A$ in its language either $\Gamma \Proves !A$ or
-$\Gamma \Proves \lnot !A$. Since $\Gamma_1$, $\Gamma_2$ are consistent
+$\Gamma \Proves \lnot !A$. Since $\Gamma_1$ and~$\Gamma_2$ are consistent
 extensions of~$\Gamma$, $\Gamma$ must be consistent. It follows that
 if $!A$ is !!a{sentence} in the language $\Lang L(\Gamma_1) \cap \Lang
 L(\Gamma_2)$, we can't have $\Gamma_1 \Entails !A$ and $\Gamma_2

content/proof-theory/sequent-calculus/rules-proofs.tex

@@ -58,7 +58,7 @@
 term~$t$ the active !!{formula} in the premise must
 be~$\Subst{!A}{a}{x}$, where $a$ is !!a{constant}. This constant is
 called the \emph{eigenvariable} of the \RightR{\lforall} inference.
-The inference is only correct the lower sequent does not contain~$a$,
+The inference is only correct if the lower sequent does not contain~$a$,
 that is, if $a$ does not occur in $\Gamma$, $\Delta$, or~$!A$. This is
 called the \emph{eigenvariable condition}.
 

content/proof-theory/sequent-calculus/translations.tex

@@ -25,13 +25,13 @@
 
 \begin{proof}
   We show that if $\pi$ is !!a{proof} in \Log{G1c}, then there is
-  !!a{proof}~$\pi'$ of~$S$ in\Log{G3c}. We do this by induction on $n
+  !!a{proof}~$\pi'$ of~$S$ in \Log{G3c}. We do this by induction on $n
   = \pheight{\pi}$.
 
   If $n = 0$, then $\pi$ is an axiom. The axiom $\lfalse \Sequent
   \quad$ is also an axiom in~\Log{G3c} (take the context $\Gamma,
-  \Delta$ to be empty). \Log{G3c} allows axioms $!A \Sequent !A$ with
-  arbitrary, not just atomic~$!A$. But we proved in
+  \Delta$ to be empty). In \Log{G3c}, axioms $!A \Sequent !A$ with
+  arbitrary, not just atomic~$!A$ are allowed. But we proved in
   \olref[ex]{prop:G3c-axioms} that all such sequents are !!{provable}
   in~\Log{G3c}.
 
@@ -75,7 +75,8 @@
   If $\pi$ ends in a rule~$R$, the inductive hypothesis yields
   !!{proof}s in \Log{G1c} of the premises, and we can apply the same
   rule~$R$ to those !!{proof}s. The exceptions are the rules
-  \LeftR{\land} and \RightR{\lor}, which are derivable in \Log{G1c}:
+  \LeftR{\land} and \RightR{\lor}, which differ between \Log{G1c}
+  and~\Log{G3c}. The \Log{G3c} versions are derivable in \Log{G1c} as follows:
   \[
   \Axiom$!A, !B, \Gamma \fCenter \Delta$
   \RightLabel{\LeftR{\land}}

open-logic-config.sty

@@ -221,9 +221,9 @@
 % operator `Op`, e.g., `\Intro{\land}` produces `$\land$Intro`.
 % `\Elim{Op}` does the same for elimination rules.
 
-\DeclareDocumentCommand \Intro { m } {\ensuremath{{#1}\mathrm{Intro}}}
+\DeclareDocumentCommand \Intro { m o } {\ensuremath{{#1}\mathrm{Intro}\IfNoValueTF{#2}{}{_{#2}}}}
 
-\DeclareDocumentCommand \Elim { m } {\ensuremath{{#1}\mathrm{Elim}}}
+\DeclareDocumentCommand \Elim { m o } {\ensuremath{{#1}\mathrm{Elim}\IfNoValueTF{#2}{}{_{#2}}}}
 
 % - `\FalseInt`, `\FalseCl`: produces name or abbreviation for
 % intuitionistic and classical absurdity rule, e.g., ``$\bot_I$,''
@@ -1472,6 +1472,9 @@
 \settexttoken{provability}{derivability}{derivabilities}
 \settexttoken{nonprovability}{non-derivability}{non-derivabilities}
 
+\settexttoken{introduction}*{introduction}{introductions}
+\settexttoken{elimination}*{elimination}{elimination}
+
 % - `tableau`: tableau, tableaux; or truth tree
 
 \settexttoken{tableau}{tableau}{tableaux}