eli_sennesh comments on Completeness, incompleteness, and what it all means: first versus second order logic - Less Wrong

45 Post author: Stuart_Armstrong 16 January 2012 05:38PM

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

Comments (38)

You are viewing a single comment's thread. Show more comments above.

Comment author: cousin_it 23 January 2012 02:54:46PM *  2 points [-]

If the human and the computer are using the same formal system, then sure. But how does a human arrive at the belief that some formal system, e.g. PA, is "really" talking about the integers, and some other system, e.g. PA+¬Con(PA), isn't? Can we formalize the reasoning that leads us to such conclusions? Pointing out that PA can be embedded in some larger formal system, e.g. ZFC, doesn't seem to be a good answer because that larger formal system will need to be justified in turn, leading to an infinite regress. And anyway humans don't seem to be born with a belief in ZFC, so something else must be going on.

Comment author: [deleted] 07 September 2015 08:23:42PM *  0 points [-]

But how does a human arrive at the belief that some formal system, e.g. PA, is "really" talking about the integers, and some other system, e.g. PA+¬Con(PA), isn't? Can we formalize the reasoning that leads us to such conclusions?

Well, human beings are abductive and computational reasoners anyway. I think our mental representation of the natural numbers is much closer to being the domain-theoretic definition of the natural numbers as the least fixed point of a finite set of constructors.

Note how least fixed-points and abductive, computational reasoning fit together: a sensible complexity prior over computational models is going to assign the most probability mass to the simplest model, which is going to be the least-fixed-point model, which is the standard model (because nonstandard naturals will require additional bits of information to specify their constructors).

A similar procedure, but with a coinductive (greatest-fixed-point) definition that involves naturals as parameters to the data constructors, will give you the real numbers.