Okay, this is what I suspected after thinking about it for a bit, but like earthwormchuck it is not clear to me in what sense we are “really” talking about running Turing machines for a nonstandard number of steps here… the interpretation I had in mind in the case of an ultrapower of the standard model is more direct: namely, running a Turing machine for the nonstandard number of steps (a1, a2, a3, …) ought to mean considering the sequence of states of the Turing machine after steps a1, a2, a3, … as an element of the ultrapower of the set of possible states of the Turing machine (in other words, after nonstandard times, the Turing machine may be in nonstandard states). It is not clear to me whether we have such an interpretation in general.
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.
WIth that interpretation, you couldn’t have a halt at a nonstandard time without halting at some standard time, right? If it were halted at some nonstandard time, it would be halted at almost all the standard times in that nonstandard time (here “almost all” is with respect to the chosen ultrafilter), and hence in particular at some standard time.
(Add here standard note for readers unused to infinity that it can be made perfectly sensible to talk about Turing machines running infinitely long and beyond but this has nothing to do with what’s being talked about here.)
Okay, this is what I suspected after thinking about it for a bit, but like earthwormchuck it is not clear to me in what sense we are “really” talking about running Turing machines for a nonstandard number of steps here… the interpretation I had in mind in the case of an ultrapower of the standard model is more direct: namely, running a Turing machine for the nonstandard number of steps (a1, a2, a3, …) ought to mean considering the sequence of states of the Turing machine after steps a1, a2, a3, … as an element of the ultrapower of the set of possible states of the Turing machine (in other words, after nonstandard times, the Turing machine may be in nonstandard states). It is not clear to me whether we have such an interpretation in general.
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.
WIth that interpretation, you couldn’t have a halt at a nonstandard time without halting at some standard time, right? If it were halted at some nonstandard time, it would be halted at almost all the standard times in that nonstandard time (here “almost all” is with respect to the chosen ultrafilter), and hence in particular at some standard time.
(Add here standard note for readers unused to infinity that it can be made perfectly sensible to talk about Turing machines running infinitely long and beyond but this has nothing to do with what’s being talked about here.)
Ah. Right. Somehow I totally forgot about Łoś′s theorem.