typos, capitalization of section headers

Author: rzach

first-order-logic/completeness/introduction.tex

@@ -26,7 +26,7 @@
 !!{derivation} that shows $\Gamma \Proves !A$ is finite and so can
 only use finitely many of the !!{sentence}s in~$\Gamma$, it follows by
 the completeness theorem that if $!A$ is a consequence of $\Gamma$, it
-is a consequence of already a finite subset of~$\Gamma$.  This is
+is already a consequence of a finite subset of~$\Gamma$.  This is
 called \emph{compactness}.  Equivalently, if every finite subset of
 $\Gamma$ is consistent, then $\Gamma$ itself must be consistent.  It
 also follows from \emph{the proof of} the completeness theorem that

first-order-logic/models-theories/expressing-props-of-structures.tex

@@ -8,7 +8,7 @@
 
 \olfileid{fol}{mat}{exs} 
 
-\olsection{Expressing properties of \printtoken{s}{structure}}
+\olsection{Expressing Properties of \printtoken{P}{structure}}
 
 \begin{explain}
 It is very often useful and important to express conditions on

first-order-logic/models-theories/expressing-relations.tex

@@ -8,8 +8,8 @@
 
 \olfileid{fol}{mat}{exr} 
 
-\olsection{Expressing relations in \article{structure}
-  \printtoken{s}{structure}}
+\olsection{Expressing Relations in \article{structure}
+  \printtoken{S}{structure}}
 
 \begin{explain}
 One main use !!{formula}s can be put to is to express properties and

first-order-logic/models-theories/set-theory.tex

@@ -8,7 +8,7 @@
 
 \olfileid{fol}{mat}{set} 
 
-\olsection{The theory of sets}
+\olsection{The Theory of Sets}
 
 Almost all of mathematics can be developed in the theory of sets.
 Developing mathematics in this theory involves a number of things.

first-order-logic/models-theories/size-of-structures.tex

@@ -8,7 +8,7 @@
 
 \olfileid{fol}{mat}{siz} 
 
-\olsection{Expressing the size of \printtoken{p}{structure}}
+\olsection{Expressing the Size of \printtoken{P}{structure}}
 
 \begin{explain}
 There are some properties of structures we can express even without

first-order-logic/models-theories/theories.tex

@@ -8,7 +8,7 @@
 
 \olfileid{fol}{mat}{the} 
 
-\olsection{Examples of first-order theories}
+\olsection{Examples of First-Order Theories}
 
 \begin{ex}
 The theory of strict linear orders in the language~$\Lang L_<$ is

first-order-logic/sequent-calculus/identity.tex

@@ -8,7 +8,7 @@
 
 \olfileid{fol}{seq}{ide}
 
-\olsection{\usetoken{P}{derivation} with \usetoken{s}{identity}}
+\olsection{\usetoken{P}{derivation} with \usetoken{S}{identity}}
 
 !!^{derivation}s with the !!{identity} require additional inference rules.
 

first-order-logic/sequent-calculus/proof-theoretic-notions.tex

@@ -26,7 +26,7 @@
 !A$ if it is not.
 \end{defn}
 
-\begin{defn}[Provability]
+\begin{defn}[!!^{derivability}]
 A sentence $!A$ is \emph{!!{derivable} from} a set of
 sentences~$\Gamma$, $\Gamma \Proves[\Log{LK}] !A$, if there is a
 finite subset~$\Gamma_0 \subseteq \Gamma$ such that $\Log{LK}$

first-order-logic/sequent-calculus/proving-things.tex

@@ -78,7 +78,7 @@
 \RightLabel{$\lif$ right} \UnaryInf$ \lnot !A \lor !B \fCenter !A \lif !B $
 \end{prooftree}
 Remember that we are trying to wind our way up to initial sequents; we
-seem to be pretty close! The right branch is just one weakening away
+seem to be pretty close!{} The right branch is just one weakening away
 from an initial sequent and then it is done:
 \begin{prooftree}
 \AxiomC{}
@@ -252,7 +252,7 @@
 rule. Since this rule is not subject to the eigenvariable restriction,
 we're in the clear. Remember, we want to try and obtain an initial
 sequent (of the form $!A(a) \Sequent !A(a)$), so we should choose $a$
-as our argument for $F$ when we apply the rule.
+as our argument for $!A$ when we apply the rule.
 \begin{prooftree}
 \Axiom$!A(a) \fCenter !A(a)$
 \RightLabel{$\lforall$ left} 
@@ -267,7 +267,7 @@
 It is important, especially when dealing with quantifiers, to double
 check at this point that the eigenvariable condition has not been
 violated. Since the only rule we applied that is subject to the
-eigenvariable condition was $\exists$ left, and the eigenvariable $a$
+eigenvariable condition was $\exists$ left, and the eigenvariable~$a$
 does not occur in its lower sequent (the end-sequent), this is a
 correct derivation.
 \end{ex}

first-order-logic/sequent-calculus/rules-and-proofs.tex

@@ -211,10 +211,10 @@
 In $\lexists$ right and $\lforall$ left there are no restrictions, and
 the term~$t$ can be anything, so we do not have to worry about any
 conditions.  However, because the $t$ may appear elsewhere in the
-sequent, the values of~$t$ for which the sequent is satisfied is
+sequent, the values of~$t$ for which the sequent is satisfied are
 constrained. On the other hand, in the $\lexists$ left and $\lforall$
 right rules, the eigenvariable condition requires that $a$ does not
-occur anywhere else in the sequent. Thus, if the upper seqeunt is
+occur anywhere else in the sequent. Thus, if the upper sequent is
 valid, the truth values of the formulas other than $!A(a)$ are
 independent of~$a$.
 \end{explain}