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.
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.