Fix typos in Syntax and Semantics (of Second-order Logic)

Author: FnControlOption

content/second-order-logic/syntax-and-semantics/expressive-power.tex

@@ -13,7 +13,7 @@
 Quantification over second-order variables is responsible for an
 immense increase in the expressive power of the language over that of
 first-order logic.  Second-order existential quantification lets us
-say that functions or relations with certain properties exists. In
+say that functions or relations with certain properties exist. In
 first-order logic, the only way to do that is to specify a non-logical
 symbol (i.e., !!a{function} or !!{predicate}) for this
 purpose. Second-order universal quantification lets us say that all

content/second-order-logic/syntax-and-semantics/inf-count.tex

@@ -50,8 +50,8 @@
   $\Sat{M}{\lforall[x][\lforall[y][(\eq[u(x)][u(y)] \lif \eq[x][y])]]
     \land \lexists[y][\lforall[x][\eq/[y][u(x)]]]}[s]$ for
   some~$s$. If it does, $s(u)$ is !!a{injective} function, and some $y
-  \in \Domain{M}$ is not in the domain of~$s(u)$. Conversely, if there
-  is !!a{injective} $f\colon \Domain{M} \to \Domain{M}$ with $\dom{f}
+  \in \Domain{M}$ is not in the range of~$s(u)$. Conversely, if there
+  is !!a{injective} $f\colon \Domain{M} \to \Domain{M}$ with $\ran{f}
   \neq \Domain{M}$, then $s(u) = f$ is such a variable
   assignment.
 \end{proof}

content/second-order-logic/syntax-and-semantics/satisfaction.tex

@@ -157,7 +157,7 @@
   \liff \lnot \Atom{Y}{z})])}[\Subst{s}{N}{Y}]$. And that is the case
   for any $N \neq \emptyset$ (so that
   $\Sat{M}{\lexists[y][\Atom{Y}{y}]}[\Subst{s}{N}{Y}]$) and, as in the
-  previous example, $M = \Domain{M} \setminus s(X)$. In other words,
+  previous example, $N = \Domain{M} \setminus s(X)$. In other words,
   $\Sat{M}{\lexists[Y][(\lexists[y][\Atom{Y}{y}] \land
   \lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})])]}[s]$ iff
   $\Domain{M} \setminus s(X)$ is non-empty, i.e., $s(X) \neq

content/second-order-logic/syntax-and-semantics/terms-formulas.tex

@@ -66,7 +66,7 @@
 \begin{defn}[Second-order \usetoken{s}{formula}]
 The set of \emph{second-order !!{formula}s}~$\FrmSOL[L]$ of the
 language~$\Lang L$ is defined by adding to
-\olref[fol][syn][frm]{defn:terms} the clauses
+\olref[fol][syn][frm]{defn:formulas} the clauses
 \begin{enumerate}
 \item If $X$ is an $n$-place predicate variable and $t_1$, \dots,
   $t_n$ are second-order terms of~$\Lang L$, then