JasonGross comments on Second-Order Logic: The Controversy - Less Wrong

24 Post author: Eliezer_Yudkowsky 04 January 2013 07:51PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (188)

You are viewing a single comment's thread.

Comment author: JasonGross 21 October 2013 06:46:34AM *  3 points [-]

Screw set theory. I live in the physical universe where when you run a Turing machine, and keep watching forever in the physical universe, you never experience a time where that Turing machine outputs a proof of the inconsistency of Peano Arithmetic. Furthermore, I live in a universe where space is actually composed of a real field and space is actually infinitely divisible and contains all the points between A and B, rather than space only containing a denumerable number of points whose existence can be proven from the first-order axiomatization of the real numbers. So to talk about physics - forget about mathematics - I've got to use second-order logic.

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.