Ok—as I replied to earthwormchuck, I think Eliezer isn’t saying at all that there is a useful way in which these nonstandard execution histories are “really” talking about Turing machines, he’s saying the exact opposite: they aren’t talking about Turing machines, which is bad if you want to talk about Turing machines, since it means that first-order logic doesn’t suffice for expressing exactly what it is you do want to talk about.
Ok—as I replied to earthwormchuck, I think Eliezer isn’t saying at all that there is a useful way in which these nonstandard execution histories are “really” talking about Turing machines, he’s saying the exact opposite: they aren’t talking about Turing machines, which is bad if you want to talk about Turing machines, since it means that first-order logic doesn’t suffice for expressing exactly what it is you do want to talk about.