typos

Author: rzach

first-order-logic/sequent-calculus/provability.tex

@@ -28,7 +28,7 @@
 \begin{prop}\ollabel{prop:provability}
 \begin{enumerate}
 \item \ollabel{prop:provability-contr} If $\Gamma \Proves[\Log{LK}]
-  !A$ and $\Gamma \cup \{ \lnot !A\} \Proves[\Log{LK}] \lfalse$, then
+  !A$ and $\Gamma \cup \{ !A\} \Proves[\Log{LK}] \lfalse$, then
   $\Gamma$ is inconsistent.
 
 \item \ollabel{prop:provability-lnot} If $\Gamma \cup \{!A\}

incompleteness/arithmetization-syntax/proofs-in-lk.tex

@@ -162,7 +162,7 @@
 \begin{enumerate}
 \item $\fn{FollowsBy}_{\land\text{right}}(s, s', s'')$,
 \item $\fn{FollowsBy}_{\eq}(s, s')$,
-\item $\fn{FollowsBy}_{\lforall\text{right}}(s, s', s'')$.
+\item $\fn{FollowsBy}_{\lforall\text{right}}(s, s')$.
 \end{enumerate}
 \end{prob}
 

incompleteness/incompleteness-provability/tarski-thm.tex

@@ -53,13 +53,13 @@
 \begin{proof}
 Let $H$ be the halting relation, i.e.,
 \[
-H = \Setabs{x}{\lexists[y][T(\num e, x, y)]}.
+H = \Setabs{\tuple{e,x}}{\lexists[s][T(e, x, s)]}.
 \]
 Let $!D_T$ define $T$ in $\Struct{N}$. Then
 \[
-H = \Setabs{x}{\Sat{N}{\lexists[y][!D_T(\num e, \num x, y)]}},
+H = \Setabs{\tuple{e,x}}{\Sat{N}{\lexists[s][!D_T(\num e, \num x, s)]}},
 \]
-so $\lexists[y][!D_T(\num e, x, y)]$ defines~$H$ in $\Struct{N}$. 
+so $\lexists[s][!D_T(z, x, s)]$ defines~$H$ in $\Struct{N}$. 
 \end{proof}
 
 \begin{prob}