Fix typos related to Second-order Logic and Lindström's Theorem

content/model-theory/lindstrom/abstract-logics.tex

@@ -81,8 +81,8 @@
   and $!E \in L(\Lang{L})$ there is a $!F \in L(\Lang{L})$ such
   that
   \[
-  \Mod[L'](L){!F} = \Setabs{\Struct{M}}{\Expan{M}{a}} \in
-  \Mod[L](L){!E} \text{ for some } a \in \Domain{M} \},
+  \Mod[L'](L){!F} = \Setabs{\Struct{M}}{\Expan{M}{a} \in
+  \Mod[L](L){!E} \text{ for some } a \in \Domain{M}},
   \]
   where $\Lang{L'} = \Lang{L} \setminus \{c\}$ and $\Expan{M}{a}$
   is the expansion of $\Struct{M}$ to $\Lang{L}$ assigning $a$
@@ -93,7 +93,7 @@
   called the \emph{relativization} of $!E$ to $\Atom{R}{x, c_1, \dots c_n}$,
   such that for each !!{structure}~$\Struct{M}$:
   \[
-  \Expan{M}{X, b_1, \ldots, b_n} \models_L !F) \text{ if and
+  \Expan{M}{X, b_1, \ldots, b_n} \models_L !F \text{ if and
     only if } \Struct{N} \models_L !E,
   \]
   where $\Struct{N}$ is the substructure of $\Struct{M}$ with !!{domain}

content/second-order-logic/metatheory/introduction.tex

@@ -14,7 +14,7 @@
 decidable, but at least it is axiomatizable. That is, there are proof
 systems for first-order logic which are sound and complete, i.e., they
 give rise to !!a{derivability} relation~$\Proves$ with the property
-that for any set of !!{sentence}s~$\Gamma$ and !!{sentence}~$!Q$,
+that for any set of !!{sentence}s~$\Gamma$ and !!{sentence}~$!A$,
 $\Gamma \Entails !A$ iff $\Gamma \Proves !A$.  This means in
 particular that the validities of first-order logic are !!{computably
   enumerable}. There is a computable function~$f\colon \Nat \to

content/second-order-logic/metatheory/second-order-arithmetic.tex

@@ -33,7 +33,7 @@
 consists of the first eight axioms above plus the (second-order)
 \emph{induction axiom}:
 \[
-\lforall[X][(X(\Obj 0) \land \lforall[x][(X(x) \lif X(x'))]) \lif \lforall[x][X(x)]].
+\lforall[X][((X(\Obj 0) \land \lforall[x][(X(x) \lif X(x'))]) \lif \lforall[x][X(x)])].
 \]
 It says that if a subset~$X$ of the !!{domain}
 contains~$\Assign{\Obj{0}}{M}$ and with any~$x \in \Domain{M}$ also
@@ -60,8 +60,8 @@
 Now for inclusion in the other direction. Consider a variable
 assignment $s$ with $s(X) = N$. By assumption,
 \begin{align*}
-\Sat{M}{\lforall[X][(X(\Obj 0) \land \lforall[x][(X(x)
-      \lif X(x'))]) \lif \lforall[x][X(x)]]}, & \text{ thus}\\
+\Sat{M}{\lforall[X][((X(\Obj 0) \land \lforall[x][(X(x)
+      \lif X(x'))]) \lif \lforall[x][X(x)])]}, & \text{ thus}\\
 \Sat{M}{(X(\Obj 0) \land \lforall[x][(X(x) \lif X(x'))]) \lif
   \lforall[x][X(x)]}[s]. & 
 \end{align*}

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