Skip to content

Commit c735002

Browse files
committed
typose reported by Julia
1 parent 07cc392 commit c735002

2 files changed

Lines changed: 12 additions & 11 deletions

File tree

first-order-logic/syntax-and-semantics/extensionality.tex

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -27,8 +27,8 @@
2727
\begin{prop}[Extensionality]
2828
Let $!A$ be a sentence, and $\Struct M$ and $\Struct M'$ be !!{structure}s.
2929
If $\Assign{c}{M} = \Assign{c}{M'}$, $\Assign{R}{M}=\Assign{R}{M'}$, and
30-
$\Assign{f}{M} = \Assign{f}{M'}$ for every !!{constant} $c$, relation
31-
symbol $R$, and !!{function} $f$ occurring in $!A$, then $\Sat{M}{!A}$
30+
$\Assign{f}{M} = \Assign{f}{M'}$ for every !!{constant}~$c$, relation
31+
symbol~$R$, and !!{function} $f$ occurring in~$!A$, then $\Sat{M}{!A}$
3232
iff $\Sat{M'}{!A}$.
3333
\end{prop}
3434

@@ -37,8 +37,8 @@
3737

3838
\begin{prop}\ollabel{prop:ext-terms}
3939
Let $\Struct M$ be a !!{structure}, $t$ and $t'$ terms, and $s$ a
40-
variable assignment. Let $s' \sim_x s$ be the $x$-variant of $s$ given
41-
by~$s'(x) = \Value{t}{M}[s]$. Then $\Value{\Subst{t}{t'}{x}}{M}[s] =
40+
variable assignment. Let $s' \sim_x s$ be the $x$-variant of~$s$ given
41+
by~$s'(x) = \Value{t'}{M}[s]$. Then $\Value{\Subst{t}{t'}{x}}{M}[s] =
4242
\Value{t}{M}[s']$.
4343
\end{prop}
4444

@@ -50,7 +50,7 @@
5050

5151
\item If $t$ is a variable other than~$x$, say, $t \ident y$, then
5252
$\Subst{t}{t'}{x} = y$, and $\Value{y}{M}[s] = \Value{y}{M}[s']$
53-
since $s' \sim_x s'$.
53+
since $s' \sim_x s$.
5454

5555
\item If $t \ident x$, then $\Subst{t}{t'}{x} = t'$. But
5656
$\Value{x}{M}[s'] = \Value{t'}{M}[s]$ by definition of~$s'$.

first-order-logic/syntax-and-semantics/semantic-notions.tex

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -64,18 +64,19 @@
6464
\end{prop}
6565

6666
\begin{proof}
67-
For the forward direction, let $\Gamma$ entail $!A$ and suppose to the
67+
For the forward direction, suppose $\Gamma \Entails !A$ and suppose to the
6868
contrary that there is a !!{structure} $\Struct M$ so that $\Sat{M}{\Gamma
6969
\cup \{ \lnot !A \}}$. Since $\Sat{M}{\Gamma}$ and $\Gamma \Entails
7070
!A$, $\Sat{M}{!A}$. Also, since $\Sat{M}{\Gamma\cup \{ \lnot !A \}}$,
7171
$\Sat{M}{\lnot !A}$, so we have both $\Sat{M}{!A}$ and $\Sat/{M}{!A}$,
7272
a contradiction. Hence, there can be no such !!{structure} $\Struct M$, so
7373
$\Gamma \cup \{ !A \}$ is unsatisfiable.
7474

75-
For the reverse direction, let $\Gamma \cup \{ \lnot !A \}$. So for
76-
every !!{structure} $\Struct M$, either $\Sat/{M}{\Gamma}$ or
77-
$\Sat{M}{!A}$. Hence, for every !!{structure} $\Struct M$ with
78-
$\Sat{M}{\Gamma}$, $\Sat{M}{!A}$, so $\Gamma \Entails !A$.
75+
For the reverse direction, suppose $\Gamma \cup \{ \lnot !A \}$ is
76+
unsatisfiable. So for every !!{structure} $\Struct M$, either
77+
$\Sat/{M}{\Gamma}$ or $\Sat{M}{!A}$. Hence, for every !!{structure}
78+
$\Struct M$ with $\Sat{M}{\Gamma}$, $\Sat{M}{!A}$, so $\Gamma \Entails
79+
!A$.
7980
\end{proof}
8081

8182
\begin{prob}
@@ -98,7 +99,7 @@
9899
Suppose that $\Gamma \subseteq \Gamma'$ and $\Gamma \Entails !A$. Let
99100
$\Struct M$ be such that $\Sat{M}{\Gamma'}$; then $\Sat{M}{\Gamma}$,
100101
and since $\Gamma \Entails !A$, we get that $\Sat{M}{!A}$. Hence,
101-
whenever $\Sat{M}{\Gamma}$, $\Sat{M}{!A}$, so $\Gamma' \Entails !A$.
102+
whenever $\Sat{M}{\Gamma'}$, $\Sat{M}{!A}$, so $\Gamma' \Entails !A$.
102103
\end{proof}
103104

104105

0 commit comments

Comments
 (0)