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.'' 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} 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) 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} 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} 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 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 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 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 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 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 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} 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} 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} 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 \[ 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 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} 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 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$ 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. 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}$} 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} 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} 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} 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} 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} 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} 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 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} 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 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} 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 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\\ 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)]]] 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 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, 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} 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 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: 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 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 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 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. 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} 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 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 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} 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} 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 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 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}) \] 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. 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}