JasonGross comments on Second-Order Logic: The Controversy - LessWrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (188)
Supposing that physics is computable, this isn't necessarily true. For example, if physics is computable in type-theory (or any language with non-standard models), then the non-standard-ness propagates not just to your physics, but to the individuals living in that physics which are trying to model it. Consider the non-standard model of the calculus of inductive constructions (approximately, Martin-Löf type theory) in which types are pointed sets, and functions are functions between sets which preserve the distinguished point. Then any representation of a person in space-time you can construct in this model (of the computation running physics) will have a distinguished point. Since any function to or from such a person-located-in-space-time must preserve this point, I'm pretty sure no information can propagate from the the person at the non-standard time to the person at any standard time. So even if you expect to observe the turing machine to halt whenever you find yourself in a non-standard model, you should also expect to not be able to tell that it's non-standard except when you're actively noticing its non-standardness. Furthermore, since functions must preserve the point, you should expect (provably) that for all times T, the turing machine should not be halted at time T (because the function mapping times T to statements must map the non-standard point of T to the non-standard (and trivial) statement).
For a more eloquent explanation of how non-standard models are unavoidable, and often useful, see The Elements of an Inductive Type.