Yeah, there’s a little non-obvious trick to talking about properties of Turing machines in the language of arithmetic, which is essential to understanding this.
The first thing you do is to use a little number theory to define a bijection between natural numbers and finite lists of natural numbers. Next, you define a way to encode the status of a Turing machine at one point in time as a list of numbers (giving the current state and the contents of the tapes); with your bijection, you can encode the status at one point in time as a single number. Now, you encode execution histories as finite lists of status numbers, which your bijection maps to a single number. You can write “n denotes a valid execution history that ends in a halting state” (i.e., n is a list of valid statuses, with the first one being a start status, the last one being a halting status, and each intermediate one being the uniquely determined correct successor to the previous one). After doing all this work, you can write a formula in the language of arithmetic saying “the Turing machine m halts on input i”, by simply saying “there is an n which denotes a valid execution history of machine m, starting at input i and ending in a halting state”.
Now consider an execution history consisting of a “finite” list of nonstandard length.
you can write a formula in the language of arithmetic saying “the Turing machine m halts on input i”
You get a formula which is true of the standard numbers m and i if and only if the m’th Turing machine halts on input i. Is there really any meaningful sense in which this formula is still talking about Turing machines when you substitute elements of some non-standard model?
You get a formula which is true of the standard numbers m and i if and only if the m’th Turing machine halts on input i. Is there really any meaningful sense in which this formula is still talking about Turing machines when you substitute elements of some non-standard model?
In a sense, no. Eliezer’s point is this: Given the actual Turing machine with number m = 4 = SSSS0 and input i = 2 = SS0, you can substitute these in to get a closed formula φ whose meaning is “the Turing machine SSSS0 halts on input SS0”. The actual formula is something like, “There is a number e such that e denotes a valid execution history for machine SSSS0 on input SS0 that ends in a halting state.” In the standard model, talking about the standard numbers, this formula is true iff the machine actually halts on that input. But in first-order logic, you cannot pinpoint the standard model, and so it can happen that formula φ is false in the standard model, but true in some nonstandard model. If you use second-order logic (and believe its standard semantics, not its Henkin semantics), formula φ is valid, i.e. true in every model, if and only if machine 4 really halts on input 2.
Okay. This is exactly what I thought it should be, but the way Eliezer phrased things made me wonder if I was missing something. Thanks for clarifying.
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.)
Yeah, there’s a little non-obvious trick to talking about properties of Turing machines in the language of arithmetic, which is essential to understanding this.
The first thing you do is to use a little number theory to define a bijection between natural numbers and finite lists of natural numbers. Next, you define a way to encode the status of a Turing machine at one point in time as a list of numbers (giving the current state and the contents of the tapes); with your bijection, you can encode the status at one point in time as a single number. Now, you encode execution histories as finite lists of status numbers, which your bijection maps to a single number. You can write “n denotes a valid execution history that ends in a halting state” (i.e., n is a list of valid statuses, with the first one being a start status, the last one being a halting status, and each intermediate one being the uniquely determined correct successor to the previous one). After doing all this work, you can write a formula in the language of arithmetic saying “the Turing machine m halts on input i”, by simply saying “there is an n which denotes a valid execution history of machine m, starting at input i and ending in a halting state”.
Now consider an execution history consisting of a “finite” list of nonstandard length.
You get a formula which is true of the standard numbers m and i if and only if the m’th Turing machine halts on input i. Is there really any meaningful sense in which this formula is still talking about Turing machines when you substitute elements of some non-standard model?
In a sense, no. Eliezer’s point is this: Given the actual Turing machine with number m = 4 = SSSS0 and input i = 2 = SS0, you can substitute these in to get a closed formula φ whose meaning is “the Turing machine SSSS0 halts on input SS0”. The actual formula is something like, “There is a number e such that e denotes a valid execution history for machine SSSS0 on input SS0 that ends in a halting state.” In the standard model, talking about the standard numbers, this formula is true iff the machine actually halts on that input. But in first-order logic, you cannot pinpoint the standard model, and so it can happen that formula φ is false in the standard model, but true in some nonstandard model. If you use second-order logic (and believe its standard semantics, not its Henkin semantics), formula φ is valid, i.e. true in every model, if and only if machine 4 really halts on input 2.
Okay. This is exactly what I thought it should be, but the way Eliezer phrased things made me wonder if I was missing something. Thanks for clarifying.
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.