Skip to content

Commit

Permalink
Clarify atomic case reasoning in proof of local determination for fir…
Browse files Browse the repository at this point in the history
…sr-order formulas.
  • Loading branch information
beastaugh authored and rzach committed Dec 1, 2024
1 parent fc8a66d commit 6891b66
Showing 1 changed file with 3 additions and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,8 @@
\iftag{prvFalse}{$\lfalse$,}{}
$\Atom{R}{t_1, \dots, t_k}$ for a $k$-place predicate $R$ and terms
$t_1$, \dots,~$t_k$, or $\eq[t_1][t_2]$ for terms $t_1$ and~$t_2$.
In the latter two cases, we only demonstrate the forward direction of
the !!{biconditional}, since the proof of the reverse is symmetrical.

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

0 comments on commit 6891b66

Please sign in to comment.