Fix typos related to axiomatic derivations (#409)

* Fix typo in Section 12.1 of the Open Logic Text

* Fix typo in Section 12.2 of the Open Logic Text

* Fix typos in Section 12.3 of the Open Logic Text

* Fix typo in Section 12.5 of the Open Logic Text

* Fix typo in Section 22.11 of the Open Logic Text

* Fix typos in proof of Theorem 22.36

* Add line break for screen reading

In Section 27.4: The Definability Theorem

Author: FnControlOption

content/first-order-logic/axiomatic-deduction/axioms-rules-propositional.tex

@@ -10,7 +10,7 @@
       {\olfileid{fol}{axd}{prp}}
       {\olfileid{pl}{axd}{prp}}
 
-\olsection{Axiom and Rules for the Propositional Connectives}
+\olsection{Axioms and Rules for the Propositional Connectives}
 
 \begin{defn}[Axioms]
 The set of $\PAx$ of \emph{axioms} for the propositional connectives comprises

content/first-order-logic/axiomatic-deduction/deduction-theorem.tex

@@ -68,7 +68,7 @@
 is an axiom, then $\Gamma \Proves !B$. We also have that $\Gamma
 \Proves !B \lif (!A \lif !B)$ by \olref[prp]{ax:lif1}, and
 \olref{prop:mp} gives $\Gamma \Proves !A \lif !B$. If $!B \in \{ !A\}$
-then $\Gamma \Proves !A \lif !B$ because then last !!{sentence}~$!A
+then $\Gamma \Proves !A \lif !B$ because the last !!{sentence}~$!A
 \lif !B$ is the same as $!A \lif !A$, and we have !!{derive}d that in
 \olref[pro]{ex:identity}.
 

content/first-order-logic/axiomatic-deduction/provability-quantifiers.tex

@@ -27,7 +27,7 @@
 \begin{proof}
 By the deduction theorem, $\Gamma \Proves \ltrue \lif !A(c)$. Since
 $c$ does not occur in $\Gamma$ or~$\top$, we get $\Gamma \Proves
-\ltrue \lif !A(c)$. By the deduction theorem again, $\Gamma \Proves
+\ltrue \lif \lforall[x][!A(x)]$. By the deduction theorem again, $\Gamma \Proves
 \lforall[x][!A(x)]$.
 \end{proof}
 

content/first-order-logic/axiomatic-deduction/proving-things.tex

@@ -32,7 +32,7 @@
   1. &  $\lnot !D \lif (!D \lif !E)$ & \olref[prp]{ax:lnot2} \\
   2. & $(\lnot !D \lif (!D \lif !E)) \lif {}$\\
   &\qquad $((!E \lif (!D \lif !E)) \lif ((\lnot !D \lor !E) \lif (!D \lif !E)))$ & \olref[prp]{ax:lor3}\\
-  3. & $((!E \lif (!D \lif !E)) \lif ((\lnot !D \lor !E) \lif (!D \lif !E))$ & 1, 2, \MP\\
+  3. & $(!E \lif (!D \lif !E)) \lif ((\lnot !D \lor !E) \lif (!D \lif !E))$ & 1, 2, \MP\\
   4. & $!E \lif (!D \lif !E)$ & \olref[prp]{ax:lif1}\\
   5. & $(\lnot !D \lor !E) \lif (!D \lif !E)$ & 3, 4, \MP
 \end{derivation}
@@ -111,10 +111,10 @@
   lines 3--7 of the !!{derivation} in the preceding example. This is
   !!a{derivation} of $!A \lif !C$---which is the last line of the new
   !!{derivation}---from~$\Gamma$. Note that the justifications of
-  lines 4 and~7 remain valid if the reference to line number~2 is
+  lines 4 and~7 remain valid if the reference to line number~1 is
   replaced by reference to the last line of the !!{derivation} of~$!A
-  \lif !B$, and reference to line number~1 by reference to the last
-  line of the !!{derivation} of~$B \lif !C$.
+  \lif !B$, and reference to line number~2 by reference to the last
+  line of the !!{derivation} of~$!B \lif !C$.
 \end{proof}
 
 \begin{prob} 

content/first-order-logic/axiomatic-deduction/rules-and-proofs.tex

@@ -73,8 +73,8 @@
 \item for some $j < i$, $!A_j$ is $!B \lif !A_i$, and for some $k < i$,
   $!A_k$ is~$!B$.
 \end{enumerate}
-The last clause says that $!A_i$ follows from~$!A_j$ ($!B$) and $!A_k$
-($!B \lif !A_i$) by modus ponens. If we can go from $1$ to~$n$, and
+The last clause says that $!A_i$ follows from~$!A_j$ ($!B \lif !A_i$) and $!A_k$
+($!B$) by modus ponens. If we can go from $1$ to~$n$, and
 each time we find !!a{formula}~$!A_i$ that is either in~$\Gamma$, an
 axiom, or which a rule of inference tells us that it is a correct
 inference step, then the entire sequence counts as a correct

content/first-order-logic/axiomatic-deduction/soundness.tex

@@ -69,7 +69,7 @@
 ponens, then there are !!{formula}s $!B$ and $!B \lif !A$ in the
 !!{derivation}, and the induction hypothesis applies to the part of
 the !!{derivation} ending in those !!{formula}s (since they contain at
-least one fewer steps justified by an inference).  So, by induction
+least one fewer step justified by an inference).  So, by induction
 hypothesis, $\Gamma \Entails !B$ and $\Gamma \Entails !B \lif
 !A$. Then $\Gamma \Entails !A$ by
 \iftag{FOL}
@@ -80,7 +80,7 @@
 \QR. Then that step has the form $!C \lif \lforall[x][B(x)]$ and
 there is a preceding step $!C \lif !B(c)$ with $c$ not in $\Gamma$,
 $!C$, or $\lforall[x][B(x)]$. By induction hypothesis, $\Gamma
-\Entails !C \lif \lforall[x][B(x)]$. By
+\Entails !C \lif !B(c)$. By
 \olref[syn][sem]{thm:sem-deduction}, $\Gamma \cup \{!C\} \Entails
 !B(c)$.
 
@@ -95,9 +95,9 @@
 not occur in~$\Gamma$ or~$!C$, $\Sat{M'}{\Gamma \cup \{!C\}}$ by
 \olref[syn][ext]{cor:extensionality-sent}. Since $\Gamma \cup \{!C\}
 \Entails !B(c)$, $\Sat{M'}{B(c)}$.  Since $!B(c)$ is !!a{sentence},
-$\Sat{M}{!B(c)}[s]$ by
+$\Sat{M'}{!B(c)}[s]$ by
 \olref[syn][ass]{prop:sentence-sat-true}. $\Sat{M'}{!B(x)}[s]$ iff
-$\Sat{M'}{!B(c)}$ by \olref[syn][ext]{prop:ext-formulas} (recall that
+$\Sat{M'}{!B(c)}[s]$ by \olref[syn][ext]{prop:ext-formulas} (recall that
 $!B(c)$ is just $\Subst{!B(x)}{c}{x}$). So,
 $\Sat{M'}{!B(x)}[s]$. Since $c$ does not occur in~$!B(x)$, by
 \olref[syn][ext]{prop:extensionality}, $\Sat{M}{!B(x)}[s]$. But $s$

content/model-theory/interpolation/definability.tex

@@ -103,7 +103,7 @@
 By Craig's Interpolation Theorem there is !!a{sentence} $!C(c_1,\dots, c_n)$
 not containing $P$ or $P'$ such that:
 \begin{align*}
-  !D(P) \land \Atom{P}{c_1, \dots, c_n} & \Entails !C(c_1,\dots, c_n); &
+  !D(P) \land \Atom{P}{c_1, \dots, c_n} & \Entails !C(c_1,\dots, c_n); \\
   !C(c_1,\dots, c_n) & \Entails !D(P') \to \Atom{P'}{c_1, \dots, c_n}.
 \end{align*}
 From the former of these two entailments we have: $!D(P) \Entails