typos reported by students

Author: rzach

content/proof-theory/natural-deduction/translation-G2i.tex

@@ -22,7 +22,7 @@
 \begin{prop}\ollabel{prop:G2i-to-N2i}
 If $\Log{G2i} + \Cut \Proves \Gamma \Sequent \Delta$ then $\Log{N2i}
 \Proves \Gamma' \Sequent !C$, where $!C \ident \lfalse$ if $\Delta$ is
-empty and $\Delta = \{!C\}$ otherwise, and $\Gamma'$ corresponds
+empty and $\Delta = \{!A\}$ otherwise, and $\Gamma'$ corresponds
 to~$\Gamma$.
 \end{prop}
 

content/proof-theory/natural-deduction/translation-N2i.tex

@@ -14,7 +14,7 @@
 If $\Log{N2ci} \Proves \Gamma \Sequent !A$ then $\Log{G2ci} + \Cut \Proves
 \Gamma' \Sequent \Delta$ where $\Gamma'$ is the multiset of
 !!{formula}s resulting from $\Gamma$ by removing labels, and $\Delta =
-\{!C\}$ if $!A$ is not~$\lfalse$, and $\Delta = \emptyset$ if it is.
+\{!A\}$ if $!A$ is not~$\lfalse$, and $\Delta = \emptyset$ if it is.
 \end{prop}
 
 \begin{proof}

content/proof-theory/normalization/introduction.tex

@@ -12,7 +12,7 @@
 
 If you have !!{prove}d a conditional~$!A \lif !B$, you might be in a
 position to use it in !!a{proof} of~$!B$ by using~\Elim{\lif}. This
-would of course also a require !!a{proof}~$\delta_1$ of~$!A$. Your
+would of course also require !!a{proof}~$\delta_1$ of~$!A$. Your
 !!{proof}~$\delta_1$ of~$!A \lif !B$, more likely than not, ends
 in~\Intro{\lif}, which turns !!a{proof}~$\delta_2$ of~$!B$ from the
 open assumption~$!A$ into one of~$!A \lif !B$. If it does, in your

content/proof-theory/normalization/permutations.tex

@@ -12,7 +12,7 @@
 
 Cuts in \Log{N1i} are segments that end in the major premise of
 !!a{elimination} rule. One case in the normalization proof is to
-reduce the length of critical cuts, and with it the cut length of the
+reduce the length of maximal cuts, and with it the cut length of the
 !!{proof}. A cut of length $>1$ can end in many ways depending on
 whether the last !!{formula} occurrence of~$!A$ in the cut is the
 conclusion of (\Elim{\lor} or \Elim{\lexists}) and depending on the

content/proof-theory/normalization/segments.tex

@@ -101,7 +101,7 @@
 rank}~$\cutrank{\delta}$ of !!a{proof}~$\delta$ is the maximal rank of
 cuts in~$\delta$. A cut is \emph{maximal} in~$\delta$ if its rank
 is~$\cutrank{\delta}$, i.e., it has maximal rank. The \emph{cut length}
-of~$\delta$ is the sum of the lengths of all its critical cuts.
+of~$\delta$ is the sum of the lengths of all its maximal cuts.
 \end{defn}
 
 \end{document}

content/proof-theory/normalization/translations.tex

@@ -33,7 +33,7 @@
 \end{cor}
 
 \begin{proof}
-By inspection of the proof of \ollabel[nat][tgi]{prop:G2i-to-N2i}: we
+By inspection of the proof of \olref[nat][tgi]{prop:G2i-to-N2i}: we
 add !!{introduction} rules to the end of !!{proof}s, and
 !!{elimination} rules only at the top of !!{proof}s, so never
 introduce an !!{introduction} rule above !!a{elimination} rule.
@@ -73,7 +73,7 @@
 If $\delta$ is a normal $\Log{N2ci}$-!!{proof} of~$\Gamma \Sequent !A$
 then there is a (cut-free) $\Log{G2ci}$-!!{proof}~$\pi$ of $\Gamma'
 \Sequent \Delta$, where $\Gamma'$ is the multiset of !!{formula}s
-resulting from $\Gamma$ by removing labels, and $\Delta = \{!C\}$ if
+resulting from $\Gamma$ by removing labels, and $\Delta = \{!A\}$ if
 $!A$ is not~$\lfalse$, and $\Delta = \emptyset$ if it is.
 \end{prop}
 

content/proof-theory/propositions-as-types/introduction.tex

@@ -45,11 +45,11 @@
 the \emph{typed} $\lambd$-calculus. In the typed $\lambd$-calculus not
 every expression $(\lambd[x][N]M)$ is legal, but only those where the
 ``types'' of $\lambd[x][N]$ and $M$ fit together, i.e., $\lambd[x][N]$
-has type $A \lif B$ and $M$ has type~$A$. In fact, not every term
-$(M_1M_2)$ is legal only if $x$ is of type $A$ and $N$ is of type only
-those where $M_1$ has type $A \to B$ and $M_2$ has type~$A$; if so,
-then $(M_1M_2)$ has type~$B$. And if the type of $x$ is $A$ and the
-type of $N$ is $B$ then the type of $\lambd[x][N]$ is $A \to B$.
+has type $A \lif B$ and $M$ has type~$A$. The type of $\lambd[x][N]$
+is $A \to B$ only if the type of $x$ is $A$ and the type of $N$
+is~$B$. In general, not every expression $(M_1M_2)$ is legal. Only
+those terms $(M_1M_2)$ are legal where $M_1$ has type $A \to B$ and
+$M_2$ has type~$A$; if so, then $(M_1M_2)$ has type~$B$. 
 
 These typing rules now clearly correspond to !!{derivation}s in
 natural deduction, where the types are represented by !!{formula}s,