From f52cc580ccb6237a580c11e4c10d9c69e3d7fb59 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?fn=20=E2=8C=83=20=E2=8C=A5?=
 <70830482+FnControlOption@users.noreply.github.com>
Date: Fri, 31 Oct 2025 12:46:18 -0700
Subject: [PATCH 1/7] Fix typo in Section 12.1 of the Open Logic Text

---
 .../axiomatic-deduction/rules-and-proofs.tex                  | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/content/first-order-logic/axiomatic-deduction/rules-and-proofs.tex b/content/first-order-logic/axiomatic-deduction/rules-and-proofs.tex
index 0c5a52d5..29cce925 100644
--- a/content/first-order-logic/axiomatic-deduction/rules-and-proofs.tex
+++ b/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

From 5d7f297b268dd5ca7cc5e0cb34b74f8413fd9313 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?fn=20=E2=8C=83=20=E2=8C=A5?=
 <70830482+FnControlOption@users.noreply.github.com>
Date: Fri, 31 Oct 2025 12:50:25 -0700
Subject: [PATCH 2/7] Fix typo in Section 12.2 of the Open Logic Text

---
 .../axiomatic-deduction/axioms-rules-propositional.tex          | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/first-order-logic/axiomatic-deduction/axioms-rules-propositional.tex b/content/first-order-logic/axiomatic-deduction/axioms-rules-propositional.tex
index ef9b9153..c9e0eb0c 100644
--- a/content/first-order-logic/axiomatic-deduction/axioms-rules-propositional.tex
+++ b/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

From 14fb0f2cfe71295b60fb207685241afff8f96cd8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?fn=20=E2=8C=83=20=E2=8C=A5?=
 <70830482+FnControlOption@users.noreply.github.com>
Date: Fri, 31 Oct 2025 12:57:41 -0700
Subject: [PATCH 3/7] Fix typos in Section 12.3 of the Open Logic Text

---
 .../axiomatic-deduction/proving-things.tex                | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/content/first-order-logic/axiomatic-deduction/proving-things.tex b/content/first-order-logic/axiomatic-deduction/proving-things.tex
index a7767789..d3dcd567 100644
--- a/content/first-order-logic/axiomatic-deduction/proving-things.tex
+++ b/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} 

From 8892e104cb160ca19feb5384583628973d5c3010 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?fn=20=E2=8C=83=20=E2=8C=A5?=
 <70830482+FnControlOption@users.noreply.github.com>
Date: Fri, 31 Oct 2025 13:02:54 -0700
Subject: [PATCH 4/7] Fix typo in Section 12.5 of the Open Logic Text

---
 .../first-order-logic/axiomatic-deduction/deduction-theorem.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/first-order-logic/axiomatic-deduction/deduction-theorem.tex b/content/first-order-logic/axiomatic-deduction/deduction-theorem.tex
index b6b26a01..2e2ee013 100644
--- a/content/first-order-logic/axiomatic-deduction/deduction-theorem.tex
+++ b/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}.
 

From a0e6552ae9ab28f3a822a5854ebe19f7866dc93f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?fn=20=E2=8C=83=20=E2=8C=A5?=
 <70830482+FnControlOption@users.noreply.github.com>
Date: Fri, 31 Oct 2025 13:08:58 -0700
Subject: [PATCH 5/7] Fix typo in Section 22.11 of the Open Logic Text

---
 .../axiomatic-deduction/provability-quantifiers.tex             | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/first-order-logic/axiomatic-deduction/provability-quantifiers.tex b/content/first-order-logic/axiomatic-deduction/provability-quantifiers.tex
index 02957caa..2e60b409 100644
--- a/content/first-order-logic/axiomatic-deduction/provability-quantifiers.tex
+++ b/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}
 

From ca51c72354fd20c809e97ab062acf328a6e1975f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?fn=20=E2=8C=83=20=E2=8C=A5?=
 <70830482+FnControlOption@users.noreply.github.com>
Date: Fri, 31 Oct 2025 13:19:16 -0700
Subject: [PATCH 6/7] Fix typos in proof of Theorem 22.36

---
 .../first-order-logic/axiomatic-deduction/soundness.tex   | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/content/first-order-logic/axiomatic-deduction/soundness.tex b/content/first-order-logic/axiomatic-deduction/soundness.tex
index 6fe04524..ff619e70 100644
--- a/content/first-order-logic/axiomatic-deduction/soundness.tex
+++ b/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$

From dfaf322dbeefee74e68bfc48dc49b70d3132b403 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?fn=20=E2=8C=83=20=E2=8C=A5?=
 <70830482+FnControlOption@users.noreply.github.com>
Date: Fri, 31 Oct 2025 19:41:30 -0700
Subject: [PATCH 7/7] Add line break for screen reading

In Section 27.4: The Definability Theorem
---
 content/model-theory/interpolation/definability.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/model-theory/interpolation/definability.tex b/content/model-theory/interpolation/definability.tex
index 00c62edf..54f506dd 100644
--- a/content/model-theory/interpolation/definability.tex
+++ b/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