typos; fixes #89

forallx-yyc-fol.tex

@@ -696,11 +696,11 @@ \section{The order of quantifiers}\label{ss:OrderQuant}
 \begin{itemize}
 \item A function $f$ is \emph{pointwise continuous} if
 \[
-\forall \epsilon\forall x\forall y\exists \delta(\left|x - y\right| < \delta \to \left|\atom{F}{x} - f(y)\right| < \epsilon)
+\forall \epsilon\forall x\forall y\exists \delta(\left|x - y\right| < \delta \to \left|f(x) - f(y)\right| < \epsilon)
 \]
 \item A function $f$ is \emph{uniformly continuous} if
 \[
-\forall \epsilon\exists \delta\forall x\forall y(\left|x - y\right| < \delta \to \left|\atom{F}{x} - f(y)\right| < \epsilon)
+\forall \epsilon\exists \delta\forall x\forall y(\left|x - y\right| < \delta \to \left|f(x) - f(y)\right| < \epsilon)
 \]
 \end{itemize}
 

forallx-yyc-interpretations.tex

@@ -335,7 +335,7 @@ \section{When the main logical operator is a quantifier}
 allow formulas such as `$\exists x(\forall x\,\atom{F}{x} \eif
 \atom{G}{x})$', where different quantifiers bind the same variables.
 We consider only `$\forall x\,\atom{F}{x} \eif \atom{G}{e}$' as a
-susbstitution instance of this formula, and not `$\atom{F}{e} \eif
+substitution instance of this formula, and not `$\atom{F}{e} \eif
 \atom{G}{e}$', because the `$x$' in `$\atom{F}{x}$' is not free---it
 is bound by `$\forall x$'. (You may want to review \cref{s:FreeVars}
 in this connection.)

forallx-yyc-prooffol.tex

@@ -66,7 +66,7 @@ \section{Existential introduction}\label{s:existsIntro}
 \metav{c}\ldots)$'. We will write `$\metav{A}(\ldots \metav{x} \ldots
 \metav{c}\ldots)$' to indicate any formula obtained by replacing
 \emph{some or all} of the instances of the name \metav{c} with the
-variable~\metav{x} (provided provided $\metav{c}$, wherever it is
+variable~\metav{x} (provided~$\metav{c}$, wherever it is
 replaced, does not occur in the scope of a quantifier
 binding~$\metav{x}$). Armed with this, our introduction rule is:
 \factoidbox{
@@ -349,7 +349,7 @@ \section{Quantifier rules and vacuous quantification}
 In \cref{s:existsIntro}, we said that we use `$\metav{A}(\ldots
 \metav{x} \ldots \metav{c}\ldots)$' to indicate any formula obtained
 by replacing \emph{some or all} of the instances of the name \metav{c}
-with the variable~\metav{x} \emph{provided provided $\metav{c}$,
+with the variable~\metav{x} \emph{provided~$\metav{c}$,
 wherever it is replaced, does not occur in the scope of a quantifier
 binding~$\metav{x}$}. The emphasized restriction prohibiting the
 replacement of $\metav{c}$ in some cases is somewhat subtle. You