OpenLogicProject · rzach · May 22, 2023 · May 17, 2023 · May 17, 2023 · May 17, 2023
diff --git 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.''

diff --git 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}

diff --git 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)

diff --git 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}
 

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

diff --git 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

diff --git 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

diff --git 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

diff --git 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

diff --git 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

diff --git 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

diff --git 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}

diff --git 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}

diff --git 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}

diff --git 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
 \[

diff --git 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

diff --git 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}
diff --git 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

diff --git 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$

diff --git 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.

diff --git 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}$}

diff --git 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}
 

diff --git 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}

diff --git 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}
 

diff --git 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}

diff --git 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}

diff --git 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}

diff --git 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

diff --git 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}
 

diff --git 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

diff --git 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}
 

diff --git 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

diff --git 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\\

diff --git 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)]]]

diff --git 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

diff --git 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,

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

diff --git 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