OpenLogicProject/OpenLogic

Confusing paragraph in SLC section 15.9

marethyu opened this issue · 4 comments

I have issues trying to understand what is written here:

capture1

(There is a typo: $T(M,e)$ should be $T(M,w)$.)

I understand it is trying to present a counterexample to the claim: "if $T(M,w)\land E(M,w)$ has a finite model, then the machine $M$ halts on input $w$." I expect the construction of a structure $M'$ with a finite domain that satisfies $M'\models T(M,w)\land E(M,w)$ but the machine $M$ does not halt. The finite model $M'$ introduced in the previous paragraph does not appear to satisfy $T(M,w)\land E(M,w)$, and, since the machine $M$ does not halt, there is no finite model for $E(M,w)$ (?). This makes the antecedent "$T(M,w)\land E(M,w)$ has a finite model" false. The consequent "the machine $M$ halts on input $w$" is also false. So, the example presented in the paragraph does not disprove the claim...

Also, it is not clear what $\overline{n+l} refers to.

Good catch! $\mathbf{M}'$ is indeed not a counterexample. But this is (I hope!): Suppose $k$ is least such that the machine after $k$ steps goes into the described infinite loop where it stays in the same state and doesn't move the head. Let $n$ be the larger of $k$ and the length of $w$. The configurations after $n$, $n+1$, $n+2$, etc. (i.e., $n+l$ for any $l \in \mathbb{N}$) steps are all identical.

Take $|\mathbf{M}''| = \lbrace 0, \dots, n, \infty\rbrace$, the interpretations of $\prime$ and $<$ are as in $\mathbf{M}'$ for anything up to $n$ and $\infty' = \infty$ and $\infty < \infty$. Note that $\infty$ is not the value of any $\overline{n+l}$ for $l \in \mathbb{N}$, so it's a "non-standard" value. Suppose $\delta(q,\sigma)$ is undefined. Let the interpretations of $Q_q$ and $S_\sigma$ be as before for arguments $\le n$ but let's add $\langle \infty,\infty\rangle$ to $Q_q^{\mathbf{M}''}$ and $S_\sigma^{\mathbf{M}''}$. Now both $T(M,w)$ and $E(M,w)$ are true in $\mathbf{M}''$, $\mathbf{M}''$ is finite, but the machine doesn't halt.

Does that (a) make sense (how much explanation would you want?) and (b) does it work (as far as you can tell)?

I see, thanks Dr. Zach. This example might work. I think it is simpler if you instead introduce a halting state $h$ that is unreachable. Then add $\langle\infty,\infty\rangle$ to $Q_h^{\mathbf M''}$. Then, $\mathbf M''\models\exists x\exists y Q_h(x,y)$, i.e. $\mathbf M''\models E(M,w)$ holds as well.

Thanks again! (\Lambda is the empty sequence)

(You forgot to fix the typo in problem 15.10.)