From 44797b8e4012a041c98ea16d6436f1ce2b006db1 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:09:19 +0200
Subject: [PATCH 01/53] Update introduction.tex

---
 .../inductive-defs-proofs/introduction.tex                      | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/sets-functions-relations/inductive-defs-proofs/introduction.tex b/content/sets-functions-relations/inductive-defs-proofs/introduction.tex
index bca5e4f3..1dd4f06c 100644
--- a/content/sets-functions-relations/inductive-defs-proofs/introduction.tex
+++ b/content/sets-functions-relations/inductive-defs-proofs/introduction.tex
@@ -19,7 +19,7 @@
 In general, what induction allows one to do is prove a universal claim; that
 is, show that every object of a certain kind has some property. In particular,
 induction is often useful where a ``universal introduction'' method of proof
-is too complicated. Induction only works on matehmatical objects that are
+is too complicated. Induction only works on mathematical objects that are
 constructed in special ways: if every element in the set is either basic or is
 built up from basic elements, then we can use induction on it. More precisely:
 \end{explain}

From dd885508af0f849fd5c9e6ec5f6df4e47e982bfa Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:09:22 +0200
Subject: [PATCH 02/53] Update proofs-about-sets.tex

---
 content/sets-functions-relations/sets/proofs-about-sets.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/content/sets-functions-relations/sets/proofs-about-sets.tex b/content/sets-functions-relations/sets/proofs-about-sets.tex
index 9c4b4140..09043fd9 100644
--- a/content/sets-functions-relations/sets/proofs-about-sets.tex
+++ b/content/sets-functions-relations/sets/proofs-about-sets.tex
@@ -10,7 +10,7 @@
 \olsection{Proofs about Sets}
 
 \begin{editorial}
-This section is superceded by \verb|content/method/proofs| and has
+This section is superseded by \verb|content/method/proofs| and has
 been removed from this chapter by default.
 \end{editorial}
 
@@ -33,7 +33,7 @@
 A proof of a general claim like ``every !!{element}~$z$ of $X \cap (X
 \cup Y)$ is also an !!{element} of $X$'' is proved by first assuming
 that an arbitrary $z \in X \cap (X \cup Y)$ is given, and proving from
-this assumtion that $z \in X$. You may know this pattern as ``general
+this assumption that $z \in X$. You may know this pattern as ``general
 conditional proof.''  In this proof we'll also have to make use of the
 definitions involved in the assumption and conclusion, e.g., in this
 case of ``$\cap$'' and ``$\cup$.''  So case (a) would be argued as

From 6259e9bef2b16e1e7708496a20304030569de493 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:09:25 +0200
Subject: [PATCH 03/53] Update enumerability.tex

---
 content/sets-functions-relations/size-of-sets/enumerability.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/sets-functions-relations/size-of-sets/enumerability.tex b/content/sets-functions-relations/size-of-sets/enumerability.tex
index 102cdfa0..0ca9030a 100644
--- a/content/sets-functions-relations/size-of-sets/enumerability.tex
+++ b/content/sets-functions-relations/size-of-sets/enumerability.tex
@@ -239,7 +239,7 @@
   \to A$. If $A$ has infinitely many !!{element}s, then for any $i$
   there must be !!a{element} of~$A$ in the enumeration $f(1)$, $f(2)$,
   \dots, which is not already among $g(1)$, \dots, $g(i)$. In this
-  case we have defined a funtion $g\colon \PosInt \to A$.
+  case we have defined a function $g\colon \PosInt \to A$.
   
   The function $g$ is !!{surjective}, since any element of~$A$ is
   among $f(1)$, $f(2)$, \dots{} (since $f$ is !!{surjective}) and so

From 2264ad4814e6c2ca1bc4aa1ad67de89cdf78c698 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:09:30 +0200
Subject: [PATCH 04/53] Update size-of-sets.tex

---
 content/sets-functions-relations/size-of-sets/size-of-sets.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/sets-functions-relations/size-of-sets/size-of-sets.tex b/content/sets-functions-relations/size-of-sets/size-of-sets.tex
index e1215d41..20eb1c05 100644
--- a/content/sets-functions-relations/size-of-sets/size-of-sets.tex
+++ b/content/sets-functions-relations/size-of-sets/size-of-sets.tex
@@ -10,7 +10,7 @@
 \begin{editorial}
 This chapter discusses enumerations, countability and uncountability.
 The text includes two versions of a few sections, a more elementary
-version and a more advancced version for use if set theory is
+version and a more advanced version for use if set theory is
 discussed in more detail. This file only includes the elementary
 versions. The more advanced versions are included in \verb|size-of-sets-complete|.
 \end{editorial}

From 7d5160e537b0626aa11029e3d4bd18e1b7f86bb8 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:09:33 +0200
Subject: [PATCH 05/53] Update representing-tms.tex

---
 .../turing-machines/machines-computations/representing-tms.tex  | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/turing-machines/machines-computations/representing-tms.tex b/content/turing-machines/machines-computations/representing-tms.tex
index 772abcb7..7336ab8c 100644
--- a/content/turing-machines/machines-computations/representing-tms.tex
+++ b/content/turing-machines/machines-computations/representing-tms.tex
@@ -255,7 +255,7 @@
 \end{ex}
 
 \begin{prob}
-Choose an arbitary input and trace through the configurations of the
+Choose an arbitrary input and trace through the configurations of the
 doubler machine in \olref[tur][mac][rep]{ex:doubler}.
 \end{prob}
 

From 86dd7324536237c1c1b1c0b99624aa351ebf1656 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:09:36 +0200
Subject: [PATCH 06/53] Update enumerating-tms.tex

---
 content/turing-machines/undecidability/enumerating-tms.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/turing-machines/undecidability/enumerating-tms.tex b/content/turing-machines/undecidability/enumerating-tms.tex
index 5ff9ed15..ce7d9110 100644
--- a/content/turing-machines/undecidability/enumerating-tms.tex
+++ b/content/turing-machines/undecidability/enumerating-tms.tex
@@ -19,7 +19,7 @@
 argument pairs for which it is defined.
 
 This is true as far as it goes, but there is a subtle difference. The
-definition of Turing machines made no resriction on what !!{element}s
+definition of Turing machines made no restriction on what !!{element}s
 the set of states and tape alphabet can have. So, e.g., for every real
 number, there technically is a Turing machine that uses that number as
 a state. However, the \emph{behavior} of the Turing machine is

From 6cc8963b21188ca864c1e0ba5c6a37e3b3d341b3 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:09:38 +0200
Subject: [PATCH 07/53] Update halting-problem.tex

---
 content/turing-machines/undecidability/halting-problem.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/turing-machines/undecidability/halting-problem.tex b/content/turing-machines/undecidability/halting-problem.tex
index 9b3fe4e6..34f105b5 100644
--- a/content/turing-machines/undecidability/halting-problem.tex
+++ b/content/turing-machines/undecidability/halting-problem.tex
@@ -127,7 +127,7 @@
 
 \begin{prob}
 We proved that the halting problem is unsolvable if the input is a
-number~$e$, which identifies a Turing machine~$M_e$ via an enumaration
+number~$e$, which identifies a Turing machine~$M_e$ via an enumeration
 of all Turing machines.  What if we allow the description of Turing
 machines from \olref[tur][und][enu]{sec} directly as input?  Can there
 be a Turing machine which decides the halting problem but takes as

From fef4101ccfcc5d51a35517918a4aaad444d898e3 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:09:41 +0200
Subject: [PATCH 08/53] Update representing-tms.tex

---
 content/turing-machines/undecidability/representing-tms.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/turing-machines/undecidability/representing-tms.tex b/content/turing-machines/undecidability/representing-tms.tex
index 1d2c2fbd..65df9ff2 100644
--- a/content/turing-machines/undecidability/representing-tms.tex
+++ b/content/turing-machines/undecidability/representing-tms.tex
@@ -88,7 +88,7 @@
 \item Axioms describing the input configuration:
 \begin{enumerate}
 \item After $0$~steps---before the machine starts---$M$ is in
-  the inital state~$q_0$, scanning square~$1$:
+  the initial state~$q_0$, scanning square~$1$:
 \[
 \Obj Q_{q_0}(\num{1}, \num{0})
 \]

From 264ed11dc64010cd0896b3703005c27eacfba3fb Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:09:45 +0200
Subject: [PATCH 09/53] Update verification.tex

---
 content/turing-machines/undecidability/verification.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/turing-machines/undecidability/verification.tex b/content/turing-machines/undecidability/verification.tex
index 546f98d5..02f48f64 100644
--- a/content/turing-machines/undecidability/verification.tex
+++ b/content/turing-machines/undecidability/verification.tex
@@ -183,7 +183,7 @@
 Now suppose $m=k$. In that case, after $n+1$ steps, the tape head has
 also visited square~$k+1$, which now is the right-most square
 visited.  So $!C(M, w, n+1)$ has a new conjunct, $\Obj
-S_\TMblank(\num{k}',\num{n}')$, and the last conjuct is
+S_\TMblank(\num{k}',\num{n}')$, and the last conjunct is
 $\lforall[x][(\num{k}' < x \lif \Obj S_\TMblank(x, \num{n}'))]$. We
 have to verify that these two !!{sentence}s are also implied.
 

From b565a3c8682e7748460b493f9918405572418d33 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:09:48 +0200
Subject: [PATCH 10/53] Update open-logic-enderton-envs.sty

---
 courses/enderton/open-logic-enderton-envs.sty | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/courses/enderton/open-logic-enderton-envs.sty b/courses/enderton/open-logic-enderton-envs.sty
index 6d3eefde..da883f88 100644
--- a/courses/enderton/open-logic-enderton-envs.sty
+++ b/courses/enderton/open-logic-enderton-envs.sty
@@ -120,19 +120,19 @@ headformat={\NUMBER}]{problem}
 \def\theprop{\arabic{chapter}\arabic{section}\Alph{prop}}
 \def\thecor{\arabic{chapter}\arabic{section}\Alph{cor}}
 
-% Other Enviroments
+% Other Environments
 % -----------------
 
 % OLP texts make use of a number of environments to encapsulate types
 % of discursive text.  By default, these environments simply print
 % their content without any special treatment. If you want to typeset
-% any of them differntly, you can change the definition of the
-% environment here. E.g., you might want digressions in asmaller font
+% any of them differently, you can change the definition of the
+% environment here. E.g., you might want digressions in a smaller font
 % and indented.  Refer to the \LaTeX\ documentation for how to
 % accomplish this.
 
 % OLP will provide two custom mechanisms for treating environments:
-% supressing and deferring. Environments can be supressed by
+% suppressing and deferring. Environments can be suppressed by
 % redefining them as the `comment` environment. For instance, to not
 % print any digressions at all, add the lines
 % ```
@@ -146,7 +146,7 @@ headformat={\NUMBER}]{problem}
 
 \newenvironment{explain}{}{}
 
-% - `intro`: for comments and comparisions to other introductory
+% - `intro`: for comments and comparisons to other introductory
 % texts, e.g., regarding terminology, conventions, or proof methods.
 
 \newenvironment{intro}{}{}
@@ -178,7 +178,7 @@ headformat={\NUMBER}]{problem}
 \newenvironment{defish}{\par\noindent}{\par}
 
 % - `derivation`: for derivations, a tabular environment with three
-% colums for line number, formula, and justification.
+% columns for line number, formula, and justification.
 
 \newenvironment{derivation}{%
   ~\begin{trivlist}

From 349feb230d87b76b91911ea5bb1c635d1e071a23 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:20:08 +0200
Subject: [PATCH 11/53] Update ce-sets.tex

---
 content/computability/computability-theory/ce-sets.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/computability/computability-theory/ce-sets.tex b/content/computability/computability-theory/ce-sets.tex
index e6f49b4e..1318e500 100644
--- a/content/computability/computability-theory/ce-sets.tex
+++ b/content/computability/computability-theory/ce-sets.tex
@@ -15,7 +15,7 @@
 \end{defn}
 
 \begin{history}
-Computably enumarable sets are also called \emph{recursively
+Computably enumerable sets are also called \emph{recursively
   enumerable} instead. This is the original terminology, and today
 both are commonly used, as well as the abbreviations ``c.e.'' and
 ``r.e.''

From fd9775b2594eb59a9a3a06436fdb852d5075abf0 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:20:11 +0200
Subject: [PATCH 12/53] Update computability-theory.tex

---
 .../computability/computability-theory/computability-theory.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/computability/computability-theory/computability-theory.tex b/content/computability/computability-theory/computability-theory.tex
index 7afe639b..05e443d5 100644
--- a/content/computability/computability-theory/computability-theory.tex
+++ b/content/computability/computability-theory/computability-theory.tex
@@ -9,7 +9,7 @@
 
 \begin{editorial}
   Material in this chapter should be reviewed and expanded. In
-  paticular, there are no exercises yet.
+  particular, there are no exercises yet.
 \end{editorial}
 
 \olimport{introduction}

From 9812e8de846ae3113ef6f7e5de38955eb3275aa7 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:20:14 +0200
Subject: [PATCH 13/53] Update fixed-point-thm.tex

---
 .../computability/computability-theory/fixed-point-thm.tex    | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/content/computability/computability-theory/fixed-point-thm.tex b/content/computability/computability-theory/fixed-point-thm.tex
index 2b2ef96b..b18d516c 100644
--- a/content/computability/computability-theory/fixed-point-thm.tex
+++ b/content/computability/computability-theory/fixed-point-thm.tex
@@ -155,7 +155,7 @@
 string functions. In particular, suppose your programming language has
 a function $\fn{diag}$ which works as follows: given an input
 string~$s$, $\fn{diag}$ locates each instance of the symbol `x'
-occuring in~$s$, and replaces it by a quoted version of the original
+occurring in~$s$, and replaces it by a quoted version of the original
 string. For example, given the string
 \begin{quote}
 \begin{verbatim}
@@ -189,7 +189,7 @@
 \end{quote}
 prints itself out $y$ times, on input $y$. Replacing the
 $\fn{getinput}$---$\fn{print}$---$\fn{diag}$ skeleton by an
-arbitrary funtion $g(x,y)$ yields
+arbitrary function $g(x,y)$ yields
 \begin{quote}
 \begin{verbatim}
 g(diag('g(diag(x), y)'), y)

From a94e9ad66100226791ce437bcd64c72dbe61c79e Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:20:18 +0200
Subject: [PATCH 14/53] Update notation-pr-functions.tex

---
 .../computability/recursive-functions/notation-pr-functions.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/computability/recursive-functions/notation-pr-functions.tex b/content/computability/recursive-functions/notation-pr-functions.tex
index df9282b2..44c4552f 100644
--- a/content/computability/recursive-functions/notation-pr-functions.tex
+++ b/content/computability/recursive-functions/notation-pr-functions.tex
@@ -1,6 +1,6 @@
 % Part: computability
 % Chapter: recursive-functions
-% Section: noations-pr-functions
+% Section: notations-pr-functions
 
 \documentclass[../../../include/open-logic-section]{subfiles}
 

From f650c5177286646bb33b918717f4030fa436961e Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:20:21 +0200
Subject: [PATCH 15/53] Update counterfactuals.tex

---
 content/counterfactuals/counterfactuals.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/counterfactuals/counterfactuals.tex b/content/counterfactuals/counterfactuals.tex
index 06ad8dbb..b38fe358 100644
--- a/content/counterfactuals/counterfactuals.tex
+++ b/content/counterfactuals/counterfactuals.tex
@@ -1,4 +1,4 @@
-% Part: conunterfactuals
+% Part: counterfactuals
 
 \documentclass[../../include/open-logic-part]{subfiles}
 

From db88172e1d0deac01e156b5fc31f72af0570b008 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:20:27 +0200
Subject: [PATCH 16/53] Update antecedent-strengthening.tex

---
 .../minimal-change-semantics/antecedent-strengthening.tex       | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/counterfactuals/minimal-change-semantics/antecedent-strengthening.tex b/content/counterfactuals/minimal-change-semantics/antecedent-strengthening.tex
index cffd912a..b2ad2139 100644
--- a/content/counterfactuals/minimal-change-semantics/antecedent-strengthening.tex
+++ b/content/counterfactuals/minimal-change-semantics/antecedent-strengthening.tex
@@ -28,7 +28,7 @@
 world where I light the match and I do so in outer space is much
 further removed from the actual world than the closest world where I
 light the match is. So although it's true that the match lights in the
-latter, it is not in the former. And that is as it schould be.
+latter, it is not in the former. And that is as it should be.
 
 \begin{ex}
   The sphere semantics invalidates the inference, i.e., we have $p

From da860cb3b139563ca89e6cb28c94a18220c464a3 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:20:30 +0200
Subject: [PATCH 17/53] Update proof-theoretic-notions.tex

---
 .../axiomatic-deduction/proof-theoretic-notions.tex             | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/first-order-logic/axiomatic-deduction/proof-theoretic-notions.tex b/content/first-order-logic/axiomatic-deduction/proof-theoretic-notions.tex
index 41d2ce2a..ea696f18 100644
--- a/content/first-order-logic/axiomatic-deduction/proof-theoretic-notions.tex
+++ b/content/first-order-logic/axiomatic-deduction/proof-theoretic-notions.tex
@@ -14,7 +14,7 @@
 
 \begin{explain}
 Just as we've defined a number of important semantic notions
-(\iftag{FOL}{validity}{tautology}, entailment, satisfiabilty), we now
+(\iftag{FOL}{validity}{tautology}, entailment, satisfiability), we now
 define corresponding \emph{proof-theoretic notions}.  These are not
 defined by appeal to satisfaction of !!{sentence}s in !!{structure}s,
 but by appeal to the !!{derivability} or !!{nonderivability} of

From f0434d52eac14a792c7521206427f0a5bb5dfeed Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:20:33 +0200
Subject: [PATCH 18/53] Update higher-order-logic.tex

---
 content/first-order-logic/beyond/higher-order-logic.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/content/first-order-logic/beyond/higher-order-logic.tex b/content/first-order-logic/beyond/higher-order-logic.tex
index 0accdc06..772c81c3 100644
--- a/content/first-order-logic/beyond/higher-order-logic.tex
+++ b/content/first-order-logic/beyond/higher-order-logic.tex
@@ -33,7 +33,7 @@
 truth values, ``true'' and ``false,'' and a type $\Nat$ of natural
 numbers. In that case, you can think of objects of type $\Nat \to
 \Omega$ as unary relations, or subsets of $\Nat$; objects of type
-$\Nat \to \Nat$ are functions from natural numers to natural numbers;
+$\Nat \to \Nat$ are functions from natural numbers to natural numbers;
 and objects of type $(\Nat \to \Nat) \to \Nat$ are ``functionals,''
 that is, higher-type functions that take functions to numbers.
 
@@ -116,7 +116,7 @@
 starting with $\Nat$, one can define real numbers, continuous
 functions, and so on. It is also particularly attractive in the
 context of intuitionistic logic, since the types have clear
-``constructive'' intepretations. In fact, one can develop constructive
+``constructive'' interpretations. In fact, one can develop constructive
 versions of higher-type semantics (based on intuitionistic, rather
 than classical logic) that clarify these constructive interpretations
 quite nicely, and are, in many ways, more interesting than the

From 2c698904f67cbe9e06f004cc186bd4d01cafba88 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:20:36 +0200
Subject: [PATCH 19/53] Update intuitionistic-logic.tex

---
 content/first-order-logic/beyond/intuitionistic-logic.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/content/first-order-logic/beyond/intuitionistic-logic.tex b/content/first-order-logic/beyond/intuitionistic-logic.tex
index c52562df..64bc101c 100644
--- a/content/first-order-logic/beyond/intuitionistic-logic.tex
+++ b/content/first-order-logic/beyond/intuitionistic-logic.tex
@@ -10,7 +10,7 @@
 
 \olsection{Intuitionistic Logic}
 
-In constrast to second-order and higher-order logic, intuitionistic
+In contrast to second-order and higher-order logic, intuitionistic
 first-order logic represents a restriction of the classical version,
 intended to model a more ``constructive'' kind of reasoning. The
 following examples may serve to illustrate some of the underlying
@@ -180,7 +180,7 @@
 To show that a sentence or propositional !!{formula} is intuitionistically
 valid, all you have to do is provide a proof. But how can you show
 that it is not valid? For that purpose, we need a semantics
-that is sound, and preferrably complete. A semantics
+that is sound, and preferably complete. A semantics
 due to Kripke nicely fits the bill.
 
 We can play the same game we did for classical logic: define the

From 4f9753c9f18b24aeb095066df8ae2886526bb4cb Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:20:38 +0200
Subject: [PATCH 20/53] Update second-order-logic.tex

---
 content/first-order-logic/beyond/second-order-logic.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/first-order-logic/beyond/second-order-logic.tex b/content/first-order-logic/beyond/second-order-logic.tex
index b989a40d..d1d13fa9 100644
--- a/content/first-order-logic/beyond/second-order-logic.tex
+++ b/content/first-order-logic/beyond/second-order-logic.tex
@@ -114,7 +114,7 @@
   full !!{structure}s only.
 \end{enumerate}
 When logicians do not specify the !!{derivation} system or the semantics they
-have in mind, they are usually refering to the second item on each
+have in mind, they are usually referring to the second item on each
 list. The advantage to using this semantics is that, as we will see,
 it gives us categorical descriptions of many natural mathematical
 structures; at the same time, the !!{derivation} system is quite strong, and

From 2f6460db4e48cf44f9c40e49a871b476ad6e0882 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:20:42 +0200
Subject: [PATCH 21/53] Update compactness.tex

---
 content/first-order-logic/completeness/compactness.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/first-order-logic/completeness/compactness.tex b/content/first-order-logic/completeness/compactness.tex
index 6d335baa..ab2cd8f7 100644
--- a/content/first-order-logic/completeness/compactness.tex
+++ b/content/first-order-logic/completeness/compactness.tex
@@ -108,7 +108,7 @@
 terms. Let $a \in \Domain{M}$ be !!a{element} of $\Domain{M}$ not
 picked out by any of them, and let $\Struct{M'}$ be the !!{structure}
 that is just like $\Struct{M}$, but also $\Assign{c}{M'} = a$. Since
-$a \neq \Value{t}{M}$ for all~$t$ occuring in~$\Delta'$,
+$a \neq \Value{t}{M}$ for all~$t$ occurring in~$\Delta'$,
 $\Sat{M'}{\Delta'}$. Since $\Sat{M}{\Gamma}$, $\Gamma' \subseteq
 \Gamma$, and $c$ does not occur in~$\Gamma$, also
 $\Sat{M'}{\Gamma'}$. Together, $\Sat{M'}{\Gamma' \cup \Delta'}$ for

From f7457bf3936f4602b5481964cc1d8f5f9dca3ae9 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:22:51 +0200
Subject: [PATCH 22/53] Update downward-ls.tex

---
 content/first-order-logic/completeness/downward-ls.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/first-order-logic/completeness/downward-ls.tex b/content/first-order-logic/completeness/downward-ls.tex
index e40967e1..0e731887 100644
--- a/content/first-order-logic/completeness/downward-ls.tex
+++ b/content/first-order-logic/completeness/downward-ls.tex
@@ -40,7 +40,7 @@
 \begin{proof}
 If $\Gamma$ is consistent and contains no sentences in which identity
 appears, then the !!{structure}~$\Struct M$ delivered by the proof of
-the completness theorem has a domain $\Domain{M}$ identical to the set
+the completeness theorem has a domain $\Domain{M}$ identical to the set
 of terms of the language~$\Lang L'$. So $\Struct{M}$ is
 !!{denumerable}, since $\Trm[L']$ is.
 \end{proof}

From cb48bae51c04cf0cf749b59103a6dec0551fbb8f Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:22:54 +0200
Subject: [PATCH 23/53] Update maximally-consistent-sets.tex

---
 .../completeness/maximally-consistent-sets.tex                  | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/first-order-logic/completeness/maximally-consistent-sets.tex b/content/first-order-logic/completeness/maximally-consistent-sets.tex
index e5b8088f..8ce29e7d 100755
--- a/content/first-order-logic/completeness/maximally-consistent-sets.tex
+++ b/content/first-order-logic/completeness/maximally-consistent-sets.tex
@@ -3,7 +3,7 @@
 % Section: maximally-consistent-sets
 
 % Definition of maximally consistent sets. Properties of mcs required
-% for completeness proved are in maximally-consistsnt-sets.tex in the
+% for completeness proved are in maximally-consistent-sets.tex in the
 % chapter on the proof system used.
 
 \documentclass[../../../include/open-logic-section]{subfiles}

From 4018cd2fe1a3a7ba84aa52aab01cc0bb7e3917e6 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:37:26 +0200
Subject: [PATCH 24/53] Update axiomatic-deduction.tex

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

diff --git a/content/first-order-logic/proof-systems/axiomatic-deduction.tex b/content/first-order-logic/proof-systems/axiomatic-deduction.tex
index 0194b9b6..dc56f923 100644
--- a/content/first-order-logic/proof-systems/axiomatic-deduction.tex
+++ b/content/first-order-logic/proof-systems/axiomatic-deduction.tex
@@ -48,7 +48,7 @@
 !!{sentence}~$!A$ as its last formula (and $\Gamma$ is taken as the
 set of !!{sentence}s in that derivation which are justified by~(2) above).  $!A$
 is a theorem if~$!A$ has !!a{derivation} where~$\Gamma$ is empty,
-i.e., every !!{sentence} in the derivation is justfied either by (1)
+i.e., every !!{sentence} in the derivation is justified either by (1)
 or~(3). For instance, here is !!a{derivation} that shows that $\Proves
 !A  \lif (!B \lif (!B \lor !A))$:
 \begin{derivation}

From 0bdeaa26f639a27367bfa9155a6a55c4a7cbb489 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:45:18 +0200
Subject: [PATCH 25/53] Update definitions.tex

---
 content/incompleteness/introduction/definitions.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/content/incompleteness/introduction/definitions.tex b/content/incompleteness/introduction/definitions.tex
index a5683c6c..cb019794 100644
--- a/content/incompleteness/introduction/definitions.tex
+++ b/content/incompleteness/introduction/definitions.tex
@@ -16,7 +16,7 @@
 framework, and a system of axioms.  For our purposes, let us suppose
 that mathematics can be formalized in a first-order language, i.e.,
 that there is some set of !!{constant}s, !!{function}s, and
-!!{predicate}s which, together with the connectives and quatifiers of
+!!{predicate}s which, together with the connectives and quantifiers of
 first-order logic, allow us to express the claims of mathematics.
 Most people agree that such a language exists: the language of set
 theory, in which $\in$ is the only non-logical symbol.  That such a
@@ -223,7 +223,7 @@
 $y_1$, \dots, $y_n$ are all the free variables of~$!A$ and the initial
 quantifiers of~$!B$ bind the variables~$y_1$, \dots,~$y_n$.  Once we
 have extracted this~$!A$ and checked that its free variables match the
-variables bound by the universal qauntifiers at the front
+variables bound by the universal quantifiers at the front
 and~$\lforall[x]$, we go on to check that the antecedent of the
 conditional matches
 \[

From 400f15ac282314f11be63e50f1a52d711927df55 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:45:20 +0200
Subject: [PATCH 26/53] Update historical-background.tex

---
 content/incompleteness/introduction/historical-background.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/incompleteness/introduction/historical-background.tex b/content/incompleteness/introduction/historical-background.tex
index 2cd7831b..a29ef6b9 100644
--- a/content/incompleteness/introduction/historical-background.tex
+++ b/content/incompleteness/introduction/historical-background.tex
@@ -209,7 +209,7 @@
 This struck a lethal blow to Hilbert's original program. However, as
 is so often the case in mathematics, it also opened up exciting new
 avenues for research. If there is no one, all-encompassing formal
-system of mathematics, it makes sense to develop more circumscribesd
+system of mathematics, it makes sense to develop more circumscribed
 systems and investigate what can be proved in them. It also makes
 sense to develop less restricted methods of proof for establishing the
 consistency of these systems, and to find ways to measure how hard it

From 17bf893747d8fc88a046fc846f4a611c158317a6 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:45:23 +0200
Subject: [PATCH 27/53] Update overview.tex

---
 content/incompleteness/introduction/overview.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/incompleteness/introduction/overview.tex b/content/incompleteness/introduction/overview.tex
index 96922b2a..857935f6 100644
--- a/content/incompleteness/introduction/overview.tex
+++ b/content/incompleteness/introduction/overview.tex
@@ -95,6 +95,6 @@
 their own consistency statements.  The conditions required for this
 theorem to apply are a bit more stringent than just that the theory
 represents all computable functions and !!{decidable} relations, but
-we will show that $\Th{PA}$ satisifes them.
+we will show that $\Th{PA}$ satisfies them.
 
 \end{document}

From 03bb1ca7a384caa0dd0dd94287e88a853ca1770e Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:45:26 +0200
Subject: [PATCH 28/53] Update interpretability.tex

---
 .../incompleteness/theories-computability/interpretability.tex  | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/incompleteness/theories-computability/interpretability.tex b/content/incompleteness/theories-computability/interpretability.tex
index 491b1f24..bbdfbc50 100644
--- a/content/incompleteness/theories-computability/interpretability.tex
+++ b/content/incompleteness/theories-computability/interpretability.tex
@@ -8,7 +8,7 @@
 
 \olfileid{inc}{tcp}{itp}
 
-\olsection{Theories in which $\Th{Q}$ is Intepretable are Undecidable}
+\olsection{Theories in which $\Th{Q}$ is Interpretable are Undecidable}
 
 We can strengthen these results even more. Informally, an
 interpretation of a language $\Lang{L_1}$ in another language

From 2bb858b3ab1feec386fd734081ec5afa294456bd Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:45:29 +0200
Subject: [PATCH 29/53] Update natural-deduction.tex

---
 content/intuitionistic-logic/introduction/natural-deduction.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/intuitionistic-logic/introduction/natural-deduction.tex b/content/intuitionistic-logic/introduction/natural-deduction.tex
index 7dbc2ec1..a86d9dbd 100644
--- a/content/intuitionistic-logic/introduction/natural-deduction.tex
+++ b/content/intuitionistic-logic/introduction/natural-deduction.tex
@@ -246,7 +246,7 @@ \subsection{Examples of \usetoken{P}{derivation}}
 \end{proof}
 
 \begin{prob}
-  Give !!{derivation}s in intutionistic logic of the following !!{formulas}:
+  Give !!{derivation}s in intuitionistic logic of the following !!{formulas}:
   \begin{enumerate}
     \item $(\lnot !A \lor !B) \lif (!A \lif !B)$
     \item $\lnot\lnot\lnot !A \lif \lnot !A$

From 22b1a7e5e0d457139e3adabb93088dae22b2acd7 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:47:45 +0200
Subject: [PATCH 30/53] Update propositions-as-types.tex

---
 .../propositions-as-types/propositions-as-types.tex             | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/intuitionistic-logic/propositions-as-types/propositions-as-types.tex b/content/intuitionistic-logic/propositions-as-types/propositions-as-types.tex
index fe7a2791..f4fba53b 100644
--- a/content/intuitionistic-logic/propositions-as-types/propositions-as-types.tex
+++ b/content/intuitionistic-logic/propositions-as-types/propositions-as-types.tex
@@ -12,7 +12,7 @@
   Curry-Howard correspondence.  It needs more explanation and
   motivation, and there are probably errors and omissions. The proof
   of normalization should be reviewed and expanded. There are no
-  examples for the product type. Permuation and simplification
+  examples for the product type. Permutation and simplification
   conversions are not covered. It will make a lot more sense once
   there is also material on the (typed) lambda calculus which is
   basically presupposed here. Use with extreme caution.

From cb437dc48bef5d3ff73936d2b97a9b00d5528b98 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:48:46 +0200
Subject: [PATCH 31/53] Update reduction.tex

---
 .../intuitionistic-logic/propositions-as-types/reduction.tex    | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/intuitionistic-logic/propositions-as-types/reduction.tex b/content/intuitionistic-logic/propositions-as-types/reduction.tex
index e2418dd5..3154a0fa 100644
--- a/content/intuitionistic-logic/propositions-as-types/reduction.tex
+++ b/content/intuitionistic-logic/propositions-as-types/reduction.tex
@@ -141,7 +141,7 @@
 lambda calculus as if we are dealing with untyped terms.
 
 Finally, the reduction of the function type corresponds to removal of
-a detour of a $\Intro\lif$ followd by a $\Elim\lif$.
+a detour of a $\Intro\lif$ followed by a $\Elim\lif$.
 \begin{gather*}
   \bottomAlignProof
   \AxiomC{$\Discharge{!A}{u}$}

From f38f5363bad44912666a9bf7f0b88cb612217b26 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:48:49 +0200
Subject: [PATCH 32/53] Update propositions.tex

---
 content/intuitionistic-logic/semantics/propositions.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/intuitionistic-logic/semantics/propositions.tex b/content/intuitionistic-logic/semantics/propositions.tex
index e0a8e888..4e9241ed 100644
--- a/content/intuitionistic-logic/semantics/propositions.tex
+++ b/content/intuitionistic-logic/semantics/propositions.tex
@@ -1,6 +1,6 @@
 % part: intuitionistic-logic
 % chapter: semantics
-% section: propositionas
+% section: propositions
 
 \documentclass[../../../include/open-logic-section]{subfiles}
 

From e8f43760a5cc84624040c8c809f74692d0a47345 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:49:25 +0200
Subject: [PATCH 33/53] Update canonical-model.tex

---
 .../soundness-completeness/canonical-model.tex                  | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/intuitionistic-logic/soundness-completeness/canonical-model.tex b/content/intuitionistic-logic/soundness-completeness/canonical-model.tex
index f54c2743..b201b7e3 100644
--- a/content/intuitionistic-logic/soundness-completeness/canonical-model.tex
+++ b/content/intuitionistic-logic/soundness-completeness/canonical-model.tex
@@ -1,5 +1,5 @@
 % part: intuitionistic-logic
-% chapter: soundeness-completeness
+% chapter: soundness-completeness
 % section: canonical-model
 
 \documentclass[../../../include/open-logic-section]{subfiles}

From 577a7a28c49a08fa7eab1cf39f325eb89517c221 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:49:27 +0200
Subject: [PATCH 34/53] Update completeness-thm.tex

---
 .../soundness-completeness/completeness-thm.tex               | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/content/intuitionistic-logic/soundness-completeness/completeness-thm.tex b/content/intuitionistic-logic/soundness-completeness/completeness-thm.tex
index fe70390f..05eba8eb 100644
--- a/content/intuitionistic-logic/soundness-completeness/completeness-thm.tex
+++ b/content/intuitionistic-logic/soundness-completeness/completeness-thm.tex
@@ -1,5 +1,5 @@
 % part: intuitionistic-logic
-% chapter: soundeness-completeness
+% chapter: soundness-completeness
 % section: completeness-thm
 
 \documentclass[../../../include/open-logic-section]{subfiles}
@@ -36,7 +36,7 @@
 \begin{prob}
   By using the completeness theorem prove that if $\Proves !A \lor !B$ then
   $\Proves !A$ or $\Proves !B$. (Hint: Assume $\mSat/{M_1}{!A}$ and
-  $\mSat/{M_2}{!B}$ and contruct a new model $\mModel{M}$ such that
+  $\mSat/{M_2}{!B}$ and construct a new model $\mModel{M}$ such that
   $\mSat/{M}{!A \lor !B}$.)
 \end{prob}
   

From f20be69a2f39e3a6559e2adb11a1a43b79d42074 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:50:01 +0200
Subject: [PATCH 35/53] Update decidability.tex

---
 .../soundness-completeness/decidability.tex                     | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/intuitionistic-logic/soundness-completeness/decidability.tex b/content/intuitionistic-logic/soundness-completeness/decidability.tex
index c2962eb0..feee2a4d 100644
--- a/content/intuitionistic-logic/soundness-completeness/decidability.tex
+++ b/content/intuitionistic-logic/soundness-completeness/decidability.tex
@@ -1,5 +1,5 @@
 % part: intuitionistic-logic
-% chapter: soundeness-completeness
+% chapter: soundness-completeness
 % section: decidability
 
 \documentclass[../../../include/open-logic-section]{subfiles}

From 8995fbfa7bd775fcea2919be2fd95450709859b4 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:50:04 +0200
Subject: [PATCH 36/53] Update lindenbaum.tex

---
 .../intuitionistic-logic/soundness-completeness/lindenbaum.tex  | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/intuitionistic-logic/soundness-completeness/lindenbaum.tex b/content/intuitionistic-logic/soundness-completeness/lindenbaum.tex
index 218891f1..95748141 100644
--- a/content/intuitionistic-logic/soundness-completeness/lindenbaum.tex
+++ b/content/intuitionistic-logic/soundness-completeness/lindenbaum.tex
@@ -1,5 +1,5 @@
 % part: intuitionistic-logic
-% chapter: soundeness-completeness
+% chapter: soundness-completeness
 % section: lindenbaum
 
 \documentclass[../../../include/open-logic-section]{subfiles}

From 279ec4d52527bd4fcce2a84f479f1d71638467ad Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:50:08 +0200
Subject: [PATCH 37/53] Update soundness-completeness.tex

---
 .../soundness-completeness/soundness-completeness.tex           | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/intuitionistic-logic/soundness-completeness/soundness-completeness.tex b/content/intuitionistic-logic/soundness-completeness/soundness-completeness.tex
index 1b726f60..82f0b86d 100644
--- a/content/intuitionistic-logic/soundness-completeness/soundness-completeness.tex
+++ b/content/intuitionistic-logic/soundness-completeness/soundness-completeness.tex
@@ -11,7 +11,7 @@
   This chapter collects soundness and completeness results for
   propositional intuitionistic logic. It needs an introduction. The
   completeness proof makes use of facts about provability that should
-  be stated and proved explicitly somehwere.
+  be stated and proved explicitly somewhere.
 \end{editorial}
 
 \olimport{soundness-axd}

From 57b1e16cd009474fa6cd8b6fd63182edef2f00a4 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:52:29 +0200
Subject: [PATCH 38/53] Update introduction.tex

---
 content/methods/induction/introduction.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/methods/induction/introduction.tex b/content/methods/induction/introduction.tex
index aaace1ee..145133ac 100644
--- a/content/methods/induction/introduction.tex
+++ b/content/methods/induction/introduction.tex
@@ -18,7 +18,7 @@
 inference from the particular to the general.  For instance, if we
 observe many green emeralds, and nothing that we would call an emerald
 that's not green, we might conclude that all emeralds are green. This
-is an inductive inference, in that it proceeds from many particlar
+is an inductive inference, in that it proceeds from many particular
 cases (this emerald is green, that emerald is green, etc.) to a
 general claim (all emeralds are green).  \emph{Mathematical} induction
 is also an inference that concludes a general claim, but it is of a

From 48a00307ecd45a72e3edea708e41dc1f902fb2d3 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:53:06 +0200
Subject: [PATCH 39/53] Update reading-proofs.tex

---
 content/methods/proofs/reading-proofs.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/methods/proofs/reading-proofs.tex b/content/methods/proofs/reading-proofs.tex
index 3a48f5a4..4dbd6d5a 100644
--- a/content/methods/proofs/reading-proofs.tex
+++ b/content/methods/proofs/reading-proofs.tex
@@ -45,7 +45,7 @@
   \subseteq A$.''
 \end{quote}
 
-This is the first half of the proof of the identity: it estabishes
+This is the first half of the proof of the identity: it establishes
 that if an arbitrary~$z$ is !!a{element} of the left side, it is also
 !!a{element} of the right, i.e., $A \cap (A \cup B) \subseteq A$.
 Assume that $z \in A \cap (A \cup B)$. Since $z$ is an !!{element} of

From cbd6da2a96d01773444f345a1f5fedea688fcc55 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 00:53:09 +0200
Subject: [PATCH 40/53] Update using-definitions.tex

---
 content/methods/proofs/using-definitions.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/methods/proofs/using-definitions.tex b/content/methods/proofs/using-definitions.tex
index 2434b4c9..3f14dd1d 100644
--- a/content/methods/proofs/using-definitions.tex
+++ b/content/methods/proofs/using-definitions.tex
@@ -102,7 +102,7 @@
 
 \begin{prob}
 Suppose you are asked to prove that $A \cap B \neq \emptyset$. Unpack
-all the definitions occuring here, i.e., restate this in a way that
+all the definitions occurring here, i.e., restate this in a way that
 does not mention ``$\cap$'', ``='', or ``$\emptyset$''.
 \end{prob}
 

From ec363316faf55b6059c1a51175972959aeb94c9d Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 01:02:13 +0200
Subject: [PATCH 41/53] Update methods.tex

---
 content/methods/methods.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/content/methods/methods.tex b/content/methods/methods.tex
index f85c64ea..79969df9 100644
--- a/content/methods/methods.tex
+++ b/content/methods/methods.tex
@@ -8,10 +8,10 @@
 
 \begin{editorial}
   This part covers general and methodological material, especially
-  explanations of various proof methods a non-methematics student may
+  explanations of various proof methods a non-mathematics student may
   be unfamiliar with. It currently contains a chapter on how to write
   proofs, and a chapter on induction, but additional sections for
-  thos, exercises, and a chapter on mathematical terminology is also
+  those, exercises, and a chapter on mathematical terminology is also
   planned.
 \end{editorial}
 

From 98013398343d3e30de9c763f4c60a29862eb103a Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 18 May 2023 01:02:58 +0200
Subject: [PATCH 42/53] Update dlo.tex

---
 content/model-theory/basics/dlo.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/content/model-theory/basics/dlo.tex b/content/model-theory/basics/dlo.tex
index b9f5c5dd..339a1de7 100644
--- a/content/model-theory/basics/dlo.tex
+++ b/content/model-theory/basics/dlo.tex
@@ -11,7 +11,7 @@ \section{Dense Linear Orders}
 
 \begin{defn}
   A \emph{dense linear ordering without endpoints} is !!a{structure}
-  $\Struct{M}$ for the !!{language} containg a single 2-place
+  $\Struct{M}$ for the !!{language} containing a single 2-place
   !!{predicate}~$<$ satisfying the following sentences:
   \begin{enumerate}
   \item $\lforall[x][\lnot x < x]$;
@@ -39,7 +39,7 @@ \section{Dense Linear Orders}
   Back-and-Forth property.  Then $\Struct{M_1} \iso[p] \Struct{M_2}$,
   and the theorem follows by \olref[pis]{thm:p-isom1}.
 
-  To show $\PIso{I}$ satisifes the Forth property, let $p \in
+  To show $\PIso{I}$ satisfies the Forth property, let $p \in
   \PIso{I}$ and let $p(a_i) = b_i$ for $i = 1$, \dots,~$n$, and
   without loss of generality suppose $a_1 <_1 a_2 <_1 \cdots <_1
   a_n$. Given $a \in \Domain{M_1}$, find $b \in \Domain{M_2}$ as

From 8733dac92a5fef8c73edab3ef2087d2e545f3fa1 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Fri, 19 May 2023 01:28:23 +0200
Subject: [PATCH 43/53] Update introduction.tex

---
 content/model-theory/models-of-arithmetic/introduction.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/model-theory/models-of-arithmetic/introduction.tex b/content/model-theory/models-of-arithmetic/introduction.tex
index d52cb4cf..54aaf885 100644
--- a/content/model-theory/models-of-arithmetic/introduction.tex
+++ b/content/model-theory/models-of-arithmetic/introduction.tex
@@ -13,7 +13,7 @@ \section{Introduction}
 !!{structure}~$\Struct{N}$ with $\Domain{N} = \Nat$ in which
 $\Obj{0}$, $\prime$, $+$, $\times$, and $<$ are interpreted as you
 would expect. That is, $\Obj{0}$ is $0$, $\prime$ is the successor
-function, $+$ is interpeted as addition and $\times$ as multiplication
+function, $+$ is interpreted as addition and $\times$ as multiplication
 of the numbers in~$\Nat$. Specifically,
 \begin{align*}
   \Assign{\Obj{0}}{N} & = 0\\

From 1d2d5e3eaea78b433f5f83bac7f765474471d69a Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Fri, 19 May 2023 01:28:26 +0200
Subject: [PATCH 44/53] Update models-of-q.tex

---
 content/model-theory/models-of-arithmetic/models-of-q.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/content/model-theory/models-of-arithmetic/models-of-q.tex b/content/model-theory/models-of-arithmetic/models-of-q.tex
index 223076d3..8092d1e2 100644
--- a/content/model-theory/models-of-arithmetic/models-of-q.tex
+++ b/content/model-theory/models-of-arithmetic/models-of-q.tex
@@ -120,7 +120,7 @@ \section{Models of $\Th{Q}$}
 
 \begin{prob}
 Prove that $\Struct{K}$ from \olref[mod][mar][mdq]{ex:model-K-of-Q}
-satisifies the remaining axioms of~$\Th{Q}$,
+satisfies the remaining axioms of~$\Th{Q}$,
 \begin{align*}
   & \lforall[x][\eq[(x \times \Obj 0)][\Obj 0]] \tag{$!Q_6$}\\
   & \lforall[x][\lforall[y][\eq[(x \times y')][((x \times y) + x)]]] \tag{$!Q_7$}\\
@@ -176,7 +176,7 @@ \section{Models of $\Th{Q}$}
 \begin{prob}
 Expand $\Struct{L}$ of \olref[mod][mar][mdq]{ex:model-L-of-Q} to
 include $\nstimes$ and $\nsless$ that interpret~$\times$ and $<$. Show
-that your structure satisifies the remaining axioms of~$\Th{Q}$,
+that your structure satisfies the remaining axioms of~$\Th{Q}$,
 \begin{align*}
 & \lforall[x][\eq[(x \times \Obj 0)][\Obj 0]] \tag{$!Q_6$}\\ &
   \lforall[x][\lforall[y][\eq[(x \times y')][((x \times y) + x)]]]

From 9125129e60765af96103cd8cb35ac8b3ff95f3c4 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Fri, 19 May 2023 01:28:29 +0200
Subject: [PATCH 45/53] Update euclidean-filtrations.tex

---
 .../normal-modal-logic/filtrations/euclidean-filtrations.tex    | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/normal-modal-logic/filtrations/euclidean-filtrations.tex b/content/normal-modal-logic/filtrations/euclidean-filtrations.tex
index f765d544..162b2e26 100644
--- a/content/normal-modal-logic/filtrations/euclidean-filtrations.tex
+++ b/content/normal-modal-logic/filtrations/euclidean-filtrations.tex
@@ -85,7 +85,7 @@
   \ollabel{fig:ser-eucl2}
 \end{figure}
 
-In particular, to obtain a euclidean flitration it is not enough to
+In particular, to obtain a euclidean filtration it is not enough to
 consider filtrations through arbitrary $\Gamma$'s closed under
 sub-!!{formula}s. Instead we need to consider sets $\Gamma$ that are
 \emph{modally closed} (see \olref[pre]{defn:modallyclosed}). Such sets

From 3143a1dd637ff588d843c4196aa1485dfe14363b Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Fri, 19 May 2023 01:28:32 +0200
Subject: [PATCH 46/53] Update introduction.tex

---
 content/normal-modal-logic/tableaux/introduction.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/normal-modal-logic/tableaux/introduction.tex b/content/normal-modal-logic/tableaux/introduction.tex
index a136c0ba..49f4ef29 100644
--- a/content/normal-modal-logic/tableaux/introduction.tex
+++ b/content/normal-modal-logic/tableaux/introduction.tex
@@ -25,7 +25,7 @@
 applied. When a branch contains both $\sFmla{\True}{!A}$ and
 $\sFmla{\False}{!A}$, we say the branch is \emph{closed}. If every
 branch in !!a{tableau} is closed, the entire !!{tableau} is closed. A
-closed !!{tableau} consititues !!a{derivation} that shows that the set
+closed !!{tableau} constitutes !!a{derivation} that shows that the set
 of !!{signed formula}s which were used to begin the !!{tableau} are
 unsatisfiable.  This can be used to define a $\Proves$ relation:
 $\Gamma \Proves !A$ iff there is some finite set~$\Gamma_0 = \{!B_1,

From ff59e3e4837d1acf01a3ae6b8628db6015524cda Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Fri, 19 May 2023 01:28:34 +0200
Subject: [PATCH 47/53] Update reference.tex

---
 content/reference/reference.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/reference/reference.tex b/content/reference/reference.tex
index e7ecd8f1..723a9ca3 100644
--- a/content/reference/reference.tex
+++ b/content/reference/reference.tex
@@ -1,4 +1,4 @@
-% Part: refeence
+% Part: reference
 
 \documentclass[../../include/open-logic-part]{subfiles}
 

From fa8e553b2167791f8fc6195ec8e2a44b9d8e6af1 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Fri, 19 May 2023 01:28:37 +0200
Subject: [PATCH 48/53] Update loewenheim-skolem.tex

---
 content/second-order-logic/metatheory/loewenheim-skolem.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/second-order-logic/metatheory/loewenheim-skolem.tex b/content/second-order-logic/metatheory/loewenheim-skolem.tex
index 51bac444..1669d085 100644
--- a/content/second-order-logic/metatheory/loewenheim-skolem.tex
+++ b/content/second-order-logic/metatheory/loewenheim-skolem.tex
@@ -13,7 +13,7 @@
 \begin{explain}
 The (Downward) L\"owenheim-Skolem Theorem states that every set of
 !!{sentence}s with an infinite model has !!a{enumerable} model.  It,
-too, is a consequence of the completeneness theorem: the proof of
+too, is a consequence of the completeness theorem: the proof of
 completeness generates a model for any consistent set of
 !!{sentence}s, and that model is !!{enumerable}.  There is also an
 Upward L\"owenheim-Skolem Theorem, which guarantees that if a set of

From 2054a718043781e349e626d4278da9cfc0bb0d34 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Fri, 19 May 2023 01:28:40 +0200
Subject: [PATCH 49/53] Update language-of-sol.tex

---
 .../syntax-and-semantics/language-of-sol.tex                  | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/content/second-order-logic/syntax-and-semantics/language-of-sol.tex b/content/second-order-logic/syntax-and-semantics/language-of-sol.tex
index d6da15ea..1f43aaf2 100644
--- a/content/second-order-logic/syntax-and-semantics/language-of-sol.tex
+++ b/content/second-order-logic/syntax-and-semantics/language-of-sol.tex
@@ -16,8 +16,8 @@
 \emph{!!{function}s}.  From them, together with logical connectives,
 quantifiers, and punctuation symbols such as parentheses and commas,
 \emph{terms} and \emph{!!{formula}s} are formed.  The difference is
-that in addition to varaibles for objects, second-order logic also
-contains varaibles for relations and functions, and allows
+that in addition to variables for objects, second-order logic also
+contains variables for relations and functions, and allows
 quantification over them. So the logical symbols of second-order logic
 are those of first-order logic, plus:
 

From 776bd7767683d378e78a190461a6d37bffe135db Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Fri, 19 May 2023 01:28:42 +0200
Subject: [PATCH 50/53] Update countablechoice.tex

---
 content/set-theory/choice/countablechoice.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/set-theory/choice/countablechoice.tex b/content/set-theory/choice/countablechoice.tex
index 195d2a2d..86774305 100644
--- a/content/set-theory/choice/countablechoice.tex
+++ b/content/set-theory/choice/countablechoice.tex
@@ -139,7 +139,7 @@
 \end{ex}
 
 The moral is that Countable Choice was used repeatedly, without much
-awareness of its users. The philosophicaly question is: How could we
+awareness of its users. The philosophical question is: How could we
 \emph{justify} Countable Choice? 
 
 An attempt at an intuitive justification might invoke an appeal to a

From 2073f5b0df9e6e31ecb97be222a0f52d0f49c0f6 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Fri, 19 May 2023 01:28:45 +0200
Subject: [PATCH 51/53] Update vitali.tex

---
 content/set-theory/choice/vitali.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/set-theory/choice/vitali.tex b/content/set-theory/choice/vitali.tex
index 04fe9f9a..35e8e53b 100644
--- a/content/set-theory/choice/vitali.tex
+++ b/content/set-theory/choice/vitali.tex
@@ -25,7 +25,7 @@
 set-theoretic aspects of the proof of Vitali's Paradox and the
 Banach-Tarski Paradox are very similar. The essential difference
 between the results is just that Banach-Tarski considers a
-\emph{finite} decomposition, whereas Vitali's Paradox onsiders a
+\emph{finite} decomposition, whereas Vitali's Paradox considers a
 \emph{countably infinite} decomposition.  As \citet{Weston2003}
 puts it, Vitali's Paradox ``is certainly not nearly as striking as the
 Banach--Tarski paradox, but it does illustrate that geometric

From 30311957bece7857c9f607d4416066bd9a28c503 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Fri, 19 May 2023 01:28:48 +0200
Subject: [PATCH 52/53] Update extrinsic.tex

---
 content/set-theory/replacement/extrinsic.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/set-theory/replacement/extrinsic.tex b/content/set-theory/replacement/extrinsic.tex
index a6645b55..53a34922 100644
--- a/content/set-theory/replacement/extrinsic.tex
+++ b/content/set-theory/replacement/extrinsic.tex
@@ -68,7 +68,7 @@
 perhaps more fundamental than the first.) Boolos does not just point
 out that Replacement has many desirable consequences. He also states
 that Replacement has ``(apparently) no undesirable'' consequences. But
-this paranthetical caveat, ``apparently,'' is surely absolutely
+this parenthetical caveat, ``apparently,'' is surely absolutely
 crucial.
 
 Recall how we ended up here: Na\"ive Comprehension ran into

From d625798c926429a8486ea741c8ab18943682ff46 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Fri, 19 May 2023 01:28:53 +0200
Subject: [PATCH 53/53] Update reflections.tex

---
 .../sets-functions-relations/arithmetization/reflections.tex    | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/content/sets-functions-relations/arithmetization/reflections.tex b/content/sets-functions-relations/arithmetization/reflections.tex
index ccd7aff8..394aa8ef 100644
--- a/content/sets-functions-relations/arithmetization/reflections.tex
+++ b/content/sets-functions-relations/arithmetization/reflections.tex
@@ -101,7 +101,7 @@
 philosophical significance would require some additional
 \emph{philosophical} argument.
 
-%Additonally: for the entire duration of this chapter, we have treated
+%Additionally: for the entire duration of this chapter, we have treated
 %the natural numbers as simply \emph{given} to us. But what can we do
 %with them? That is the subject matter for the next chapter.