Skip to content

Commit 1d807ca

Browse files
committed
typos; fixes #402
1 parent 80b357e commit 1d807ca

File tree

4 files changed

+20
-19
lines changed

4 files changed

+20
-19
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@
1919

2020
\begin{explain}
2121
Just as we've defined a number of important semantic notions
22-
(validity, entailment, satisfiabilty), we now define corresponding
22+
(validity, entailment, satisfiability), we now define corresponding
2323
\emph{proof-theoretic notions}. These are not defined by appeal to
2424
satisfaction of !!{sentence}s in !!{structure}s, but by appeal to the
2525
!!{derivability} or !!{nonderivability} of certain sequents. It was

content/many-valued-logic/sequent-calculus/proof-theoretic-notions.tex

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@
1212

1313
\begin{explain}
1414
Just as we've defined a number of important semantic notions
15-
(validity, entailment, satisfiabilty), we now define corresponding
15+
(validity, entailment, satisfiability), we now define corresponding
1616
\emph{proof-theoretic notions}. These are not defined by appeal to
1717
satisfaction of !!{sentence}s in !!{structure}s, but by appeal to the
1818
!!{derivability} or !!{nonderivability} of certain sequents. It was

content/sets-functions-relations/relations/trees.tex

Lines changed: 17 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -24,20 +24,20 @@
2424

2525
\begin{center}
2626
\begin{tikzpicture}[nodes={draw, circle}, -]
27-
\node{r} [grow'=up]
28-
child { node {a}
29-
child { node {c} }
30-
child { node {d} }
31-
child { node {e} }
27+
\node{$r$} [grow'=up]
28+
child { node {$a$}
29+
child { node {$c$} }
30+
child { node {$d$} }
31+
child { node {$e$} }
3232
}
33-
child { node {b} };
33+
child { node {$b$} };
3434
\end{tikzpicture}
3535
\end{center}
3636

3737
The lowermost node~$r$ is the root. Every node other than $r$ has
3838
exactly one parent node immediately below it. We can think of the relation
39-
a node~$x$ stands in to a node~$y$ if $y$ can be reached from $x$ by
40-
following edges upwards as $x$ being an ancestor of~$y$.
39+
a node~$x$ stands in to a node~$y$ if $y$ can be reached from~$x$ by
40+
following edges upwards as $x$ being an \emph{ancestor} of~$y$.
4141

4242
The ancestor relation in a tree is a strict partial order. This
4343
motivates the set-theoretic definition. To state it we need two
@@ -69,13 +69,14 @@
6969
\end{prop}
7070

7171
\begin{proof}
72-
Suppose $y < x$ and $y' < x$ and $y \neq y$. Then both $\{y,
73-
y'\} \subseteq \Setabs{z}{z<x}$. Since $\Setabs{z}{z<x}$ is
74-
well-ordered by~$\le$, it has a minimal element, which obviously
75-
must be either $y$ or~$y'$. So either $y \le y'$ or $y' \le y$. We
76-
assumed that $y \neq y'$, so actually either $y < y'$ or $y' < y$.
77-
Since we assumed that $y < x$ and $y' < x$, we furthermore have that
78-
either $y < y' < x$ or $y' < y < x$. So $y$ and $y'$ cannot both be
72+
Suppose $y_1 < x$ and $y_2 < x$ and $y_1 \neq y_2$. Then $\{y_1,
73+
y_2\} \subseteq \Setabs{z}{z<x}$. Since $\Setabs{z}{z<x}$ is
74+
well-ordered by~$\le$, its subset $\{y_1, y_2\}$ has a minimal
75+
element, which obviously must be either $y_1$ or~$y_2$. So either
76+
$y_1 \le y_2$ or $y_2 \le y_1$. We assumed that $y_1 \neq y_2$, so
77+
actually either $y_1 < y_2$ or $y_2 < y_1$. Since we assumed that
78+
$y_1 < x$ and $y_2 < x$, we furthermore have that either $y_1 < y_2
79+
< x$ or $y_2 < y_1 < x$. So $y_1$ and $y_2$ cannot both be
7980
predecessors of~$x$.
8081
\end{proof}
8182

@@ -110,7 +111,7 @@
110111
Slightly more generally, the set of finite sequences of natural
111112
numbers~$\Nat^*$ with the extension relation~$\sqsubseteq$ is also a
112113
tree. It is obviously not finitely branching: every $s \in \Nat^*$ has
113-
infinitely many successurs~$sn$, one for every $n \in \Nat$. Every $A
114+
infinitely many successors~$sn$, one for every $n \in \Nat$. Every $A
114115
\subseteq \Nat^*$ which is closed under~$\sqsubseteq$ is a
115116
\emph{subtree} of~$\Nat^*$. (That is, $A$ is such that if $s \in A$
116117
and $s' \sqsubseteq s$, then also $s' \in A$.) All finite trees can be

content/sets-functions-relations/size-of-sets/pairing-alt.tex

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@
2424
\[\small
2525
\begin{array}{@{}c c c c c c c c c c c@{}}
2626
\mathbf 1 & \mathbf 2 & \mathbf 3 & \mathbf 4 & \mathbf 5 & \mathbf 6 & \mathbf 7 & \mathbf 8 & \mathbf 9 & \mathbf{10} & \dots \\ \\
27-
\tuple{0,1} & & \tuple{0,2} & & \tuple{0,3} & & \tuple{0,4} & & \tuple{0,5} & & \dots \\
27+
\tuple{0,0} & & \tuple{0,1} & & \tuple{0,2} & & \tuple{0,3} & & \tuple{0,4} & & \dots \\
2828
\end{array}
2929
\]
3030
Repeat this with pairs $\tuple{1,m}$ for the place that still remain

0 commit comments

Comments
 (0)