Skip to content

Commit 8d6bdb6

Browse files
beastaughrzach
authored andcommitted
Clarify atomic case reasoning in proof of local determination for firsr-order formulas.
1 parent 3fae285 commit 8d6bdb6

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

content/first-order-logic/syntax-and-semantics/assignments.tex

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -67,6 +67,8 @@
6767
\iftag{prvFalse}{$\lfalse$,}{}
6868
$\Atom{R}{t_1, \dots, t_k}$ for a $k$-place predicate $R$ and terms
6969
$t_1$, \dots,~$t_k$, or $\eq[t_1][t_2]$ for terms $t_1$ and~$t_2$.
70+
In the latter two cases, we only demonstrate the forward direction of
71+
the !!{biconditional}, since the proof of the reverse is symmetrical.
7072

7173
\begin{enumerate}
7274
\tagitem{prvTrue}{%
@@ -87,7 +89,7 @@
8789
For $i = 1$, \dots,~$k$, $\Value{t_i}{M}[s_1] =
8890
\Value{t_i}{M}[s_2]$ by \olref{prop:valindep}. So we also have
8991
$\langle \Value{t_i}{M}[s_2], \ldots, \Value{t_k}{M}[s_2] \rangle
90-
\in \Assign{R}{M}$.}
92+
\in \Assign{R}{M}$, and hence $\Sat{M}{\indfrm}[s_2]$.}
9193
\item
9294
\indcase{!A}{\eq[t_1][t_2]}{suppose $\Sat{M}{\indfrm}[s_1]$.
9395
Then $\Value{t_1}{M}[s_1] = \Value{t_2}{M}[s_1]$. So,

0 commit comments

Comments
 (0)