proofreading

CHANGELOG.md

@@ -5,7 +5,11 @@
 - Fully accessible HTML version and SCORM packages using BookML
   ([issue 23](https://github.com/rzach/forallx-yyc/issues/23)). This
   required many changes under the hood; see the [blog post on
-  technical details](https://richardzach.org/2023/07/converting-latex-to-html-technical-notes/).
+  technical
+  details](https://richardzach.org/2023/07/converting-latex-to-html-technical-notes/).
+- Proofs now label premises by
+  PR and assumptions by AS (helps with accessibility, and makes
+  textbook match Carnap's conventions more closely).
 - New chapter 13 (Limitations of TFL) based in part on section 12.5 of
   F21 edition.
 - New chapter 35 (Properties of relations)
@@ -21,6 +25,9 @@
   variables, and added section 36.6 to explain what can go wrong if
   you're not careful with substitution ([issue
   77](https://github.com/rzach/forallx-yyc/issues/77))
+- Revisions to section 4.2 to bring it in line with the terminology of
+  chapter 3.
+- Added brief discussion of asymmetric use of “and” in section 5.2
 - Many minor revisons, fixed typos, and fixed formatting
 
 ## Changes in the Fall 2021 edition

forallx-yyc-interpretations.tex

@@ -18,7 +18,10 @@ \chapter{Extensionality}\label{s:Interpretations}
 
 \section{Symbolizing versus translating}
 
-FOL has some similar limitations. It gets beyond mere truth values, since it enables us to split up sentences into terms, predicates and quantifiers. This enables us to consider what is \emph{true of} some particular object, or of some or all objects. \emph{But that's it}.
+FOL has some similar limitations. It gets beyond mere truth values,
+since it enables us to split up sentences into terms, predicates and
+quantifiers. This enables us to consider what is \emph{true of} a
+particular object, or of some or all objects. \emph{But that's it}.
 
 To unpack this a bit, consider this symbolization key: 
 	\begin{ekey}
@@ -132,7 +135,7 @@ \section{Interpretations}
 		`$=$'), a specification of what things (in what order) the
 		predicate is to be true of.
 	\end{compactlist}
-We don't need to specify anything for`$=$', since it has a
+We don't need to specify anything for~`$=$', since it has a
 \emph{fixed} meaning, namely that of identity. Everything is identical
 to itself, and only to itself. 
 
@@ -381,7 +384,7 @@ \section{When the main logical operator is a quantifier}
 		$\metav{A}(\ldots \metav{x}\ldots\metav{x}\ldots)$.
 		\end{factoiditems}
 	}
-To be clear: all this is doing is formalizing (very pedantically) the intuitive idea expressed on the previous page. The result is a bit ugly, and the final definition might look a bit opaque. Hopefully, though, the \emph{spirit} of the idea is clear.
+To be clear: all this is doing is formalizing (very pedantically) the intuitive idea expressed above. The result is a bit ugly, and the final definition might look a bit opaque. Hopefully, though, the \emph{spirit} of the idea is clear.
 
 \practiceproblems
 \solutions
@@ -710,7 +713,7 @@ \section{Validity, entailment and satisfiability}
 
 In passing, note that we have also shown that `$\exists x(\atom{G}{x} \eif \atom{G}{a})$' does \emph{not} entail `$\exists x\, \atom{G}{x} \eif \atom{G}{a}$', i.e., that $\exists x (\atom{G}{x} \eif \atom{G}{a}) \nentails \exists x\, \atom{G}{x} \eif \atom{G}{a}$. Equally, we have shown that the sentences `$\exists x (\atom{G}{x} \eif \atom{G}{a})$' and `$\enot (\exists x\, \atom{G}{x} \eif \atom{G}{a})$' are jointly satisfiable.
 
-Let's consider a second example. Consider:
+Let's consider a second example:
 $$\forall x \exists y\, \atom{L}{x,y} \therefore \exists y \forall x\, \atom{L}{x,y}$$
 Again, we want to show that this is invalid. To do this, we must make the premises true and the conclusion false. Here is a suggestion:
 \begin{ekey}
@@ -1011,7 +1014,9 @@ \chapter{Properties of relations}\label{ch:PropRelations}
 Relations that are reflexive, transitive, and anti-symmetric are
 called \define{partial orders}. For instance, $\le$ and $\ge$ are
 partial orders. The relation `is no older than', by contrast, is
-reflexive and transitive, but not anti-symmetric.
+reflexive and transitive, but not anti-symmetric. (Two different
+people can be of the same age, and so neither is older than the
+other.)
 
 \practiceproblems
 

forallx-yyc-ml.tex

@@ -523,7 +523,7 @@ \section{A Semantics for System \mlT}
 Does that mean that these systems are a waste of time? Not at all! These systems are only unsound \emph{relative to the definition of validity we gave above}. (Or to use symbols, they are unsound relative to $\entails_\mlK$.) So when we are dealing with these stronger modal systems, we just need to modify our definition of validity to fit. This is where accessibility relations come in really handy.
 
 When we introduced the idea of an accessibility relation, we said that it could be any relation between worlds that you like: you could have it relating every world to every world, no world to any world, or anything in between. That is how we were thinking of accessibility relations in our definition of $\entails_\mlK$. But if we wanted, we could start putting some restrictions on the accessibility relation. In particular, we might insist that it has to be \emph{reflexive}:
-\[\forall wRww\]
+\[\forall w\, Rww\]
 In English: every world accesses itself. Or in terms of relative possibility: every world is possible relative to itself. If we imposed this restriction, we could introduce a new consequence relation, $\entails_\mlT$, as follows:
 \factoidbox{
 	$\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\entails_\mlT \metav{C}$ \ifeff{} there is no world in any interpretation \emph{which has a reflexive accessibility relation}, at which $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n$ are all true and $\metav{C}$ is false
@@ -608,7 +608,7 @@ \section{A Semantics for \mlSfive}
 Now, if $\enot\ebox\metav{A}$ is true at $w_1$, then $w_1$ must access some world, $w_2$, at which $\metav{A}$ is false. Equally, if $\ebox \enot\ebox \metav{A}$ is false at $w_1$, then $w_1$ must access some world, $w_3$, at which $\enot\ebox \metav{A}$ is false. Since we are now insisting that the accessibility relation is an equivalence relation, and hence symmetric, we can infer that $w_3$ accesses $w_1$. Thus, $w_3$ accesses $w_1$, and $w_1$ accesses $w_2$. Again, since we are now insisting that the accessibility relation is an equivalence relation, and hence transitive, we can infer that $w_3$ accesses $w_2$. But earlier we said that $\enot\ebox \metav{A}$ is false at $w_3$, which implies that $\metav{A}$ is true at every world which $w_3$ accesses. So $\metav{A}$ is true \emph{and} false at $w_2$. Contradiction!
 
 In the definition of $\entails_\mlSfive $, we stipulated that the accessibility relation must be an equivalence relation. But it turns out that there is another way of getting a notion of validity fit for \mlSfive. Rather than stipulating that the accessibility relation be an equivalence relation, we can instead stipulate that it be a \emph{universal} relation:
-\[\forall w_1\forall w_2Rw_1w_2\]
+\[\forall w_1\forall w_2\, Rw_1w_2\]
 In English: every world accesses every world. Or in terms of relative possibility: every world is possible relative to every world. Using this restriction on the accessibility relation, we could have defined $\entails_\mlSfive $ like this:
 \factoidbox{
 	$\metav{A}_1,\metav{A}_2, \dots \metav{A}_n\entails_\mlSfive  \metav{C}$ \ifeff{} there is no world in any interpretation \emph{which has a universal accessibility relation}, at which $\metav{A}_1,\metav{A}_2, \dots \metav{A}_n$ are all true and $\metav{C}$ is false.

forallx-yyc-preface.tex

@@ -27,7 +27,7 @@ \chapter{Preface}\label{preface}
 common in advanced texts (such as those based on the
 \href{https://openlogicproject.org/}{Open Logic Project}) where
 arguments to predicate symbols are enclosed in parentheses (i.e.,
-`$R(a,b)$' instead of `$Rab$'). Theis version of \forallx{} also uses
+`$R(a,b)$' instead of `$Rab$'). This version of \forallx{} also uses
 the standard definition of syntax for FOL which allows vacuous
 quantification, and Gentzen's original introduction and elimination
 rules for natural deduction (i.e., double negation elimination and

forallx-yyc-prooffol.tex

@@ -201,7 +201,7 @@ \section{Universal introduction}\label{s:forallIntro}
 	\end{earg}
 We might symbolize this as follows:
 $$\forall x\,\atom{O}{x,x} \therefore \forall x\,\atom{O}{x,d}$$
-But now suppose we tried to \emph{vindicate} this terrible argument with the following:
+But now suppose we tried to vindicate this terrible argument with the following:
 \begin{fitchproof}
 	\hypo{x}{\forall x\, \atom{O}{x,x}}\PR
 	\have{a}{\atom{O}{d,d}}\Ae{x}
@@ -257,8 +257,8 @@ \section{Existential elimination}\label{s:existsElim}
 Now, suppose we tried to offer a proof that vindicates this argument:
 \begin{fitchproof}
 	\hypo{f}{\atom{L}{b}}\PR
-	\hypo{nf}{\exists x\, \enot \atom{L}{x}}	
-	\open	
+	\hypo{nf}{\exists x\, \enot \atom{L}{x}}\PR
+	\open
 		\hypo{na}{\enot \atom{L}{b}}\AS
 		\have{con}{\atom{L}{b} \eand \enot \atom{L}{b}}\ai{f, na}
 	\close
@@ -433,11 +433,11 @@ \section{Quantifier rules and vacuous quantification}
 The following three proofs are missing their citations (rule and line numbers). Add them, to turn them into bona fide proofs.
 \begin{compactlist}
 \item \begin{fitchproof}
-\hypo{p1}{\forall x\exists y(\atom{R}{x,y} \eor \atom{R}{y,x})}\PR
-\hypo{p2}{\forall x\,\enot \atom{R}{m,x}}\PR
+\hypo{p1}{\forall x\exists y(\atom{R}{x,y} \eor \atom{R}{y,x})}
+\hypo{p2}{\forall x\,\enot \atom{R}{m,x}}
 \have{3}{\exists y(\atom{R}{m,y} \eor \atom{R}{y,m})}{}
 	\open
-		\hypo{a1}{\atom{R}{m,a} \eor \atom{R}{a,m}}\AS
+		\hypo{a1}{\atom{R}{m,a} \eor \atom{R}{a,m}}
 		\have{a2}{\enot \atom{R}{m,a}}{}
 		\have{a3}{\atom{R}{a,m}}{}
 		\have{a4}{\exists x\, \atom{R}{x,m}}{}
@@ -446,8 +446,8 @@ \section{Quantifier rules and vacuous quantification}
 \end{fitchproof}
 
 \item \begin{fitchproof}
-\hypo{1}{\forall x(\exists y\,\atom{L}{x,y} \eif \forall z\,\atom{L}{z,x})}\PR
-\hypo{2}{\atom{L}{a,b}}\PR
+\hypo{1}{\forall x(\exists y\,\atom{L}{x,y} \eif \forall z\,\atom{L}{z,x})}
+\hypo{2}{\atom{L}{a,b}}
 \have{3}{\exists y\,\atom{L}{a,y} \eif \forall z\atom{L}{z,a}}{}
 \have{4}{\exists y\, \atom{L}{a,y}} {}
 \have{5}{\forall z\, \atom{L}{z,a}} {}
@@ -460,11 +460,11 @@ \section{Quantifier rules and vacuous quantification}
 \end{fitchproof}
 
 \item \begin{fitchproof}
-\hypo{a}{\forall x(\atom{J}{x} \eif \atom{K}{x})}\PR
-\hypo{b}{\exists x\,\forall y\, \atom{L}{x,y}}\PR
-\hypo{c}{\forall x\, \atom{J}{x}}\PR
+\hypo{a}{\forall x(\atom{J}{x} \eif \atom{K}{x})}
+\hypo{b}{\exists x\,\forall y\, \atom{L}{x,y}}
+\hypo{c}{\forall x\, \atom{J}{x}}
 \open
-	\hypo{2}{\forall y\, \atom{L}{a,y}}\AS
+	\hypo{2}{\forall y\, \atom{L}{a,y}}
 	\have{3}{\atom{L}{a,a}}{}
 	\have{d}{\atom{J}{a}}{}
 	\have{e}{\atom{J}{a} \eif \atom{K}{a}}{}
@@ -478,7 +478,11 @@ \section{Quantifier rules and vacuous quantification}
 
 \problempart
 \label{pr.BarbaraEtc.proof1}
-In \cref{s:MoreMonadic} problem A, we considered fifteen syllogistic figures of Aristotelian logic. Provide proofs for each of the argument forms. NB: You will find it \emph{much} easier if you symbolize (for example) `No F is G' as `$\forall x (\atom{F}{x} \eif \enot \atom{G}{x})$'.
+In \hyperref[pr.BarbaraEtc]{exercise \ref*{s:MoreMonadic}A}, we
+considered fifteen syllogistic figures of Aristotelian logic. Provide
+proofs for each of the argument forms. NB: You will find it
+\emph{much} easier if you symbolize (for example) `No F is G' as
+`$\forall x (\atom{F}{x} \eif \enot \atom{G}{x})$'.
 
 \
 
@@ -909,7 +913,7 @@ \chapter{Derived rules}\label{s:DerivedFOL}
 %You will note that on line 3 I have written `for $\exists$E'. This is not technically a part of the proof. It is just a reminder---to me and to you---of why I have bothered to introduce `$\enot \atom{A}{c}$' out of the blue. You might find it helpful to add similar annotations to assumptions when performing proofs. But do not add annotations on lines other than assumptions: the proof requires its own citation, and your annotations will clutter it.
 Here is a justification of the third CQ rule:
 \begin{fitchproof}
-	\have[m]{nEna}{\exists x\, \enot \atom{A}{x}}\PR
+	\have[m]{nEna}{\exists x\, \enot \atom{A}{x}}
 	\open
 		\hypo[m+1]{Aa}{\forall x\, \atom{A}{x}}\AS
 		\open