Fix typos in Metatheory of Second-order Logic

Author: FnControlOption

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*}