Benja comments on Logical Pinpointing - Less Wrong

62 Post author: Eliezer_Yudkowsky 02 November 2012 03:33PM

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

Comments (338)

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

Comment author: Eliezer_Yudkowsky 25 October 2012 03:08:33AM 16 points [-]

Mainstream status:

The presentation of the natural numbers is meant to be standard, including the (well-known and proven) idea that it requires second-order logic to pin them down. There's some further controversy about second-order logic which will be discussed in a later post.

I've seen some (old) arguments about the meaning of axiomatizing which did not resolve in the answer, "Because otherwise you can't talk about numbers as opposed to something else," so AFAIK it's theoretically possible that I'm the first to spell out that idea in exactly that way, but it's an obvious-enough idea and there's been enough debate by philosophically inclined mathematicians that I would be genuinely surprised to find this was the case.

On the other hand, I've surely never seen a general account of meaningfulness which puts logical pinpointing alongside causal link-tracing to delineate two different kinds of correspondence within correspondence theories of truth. To whatever extent any of this is a standard position, it's not nearly widely-known enough or explicitly taught in those terms to general mathematicians outside model theory and mathematical logic, just like the standard position on "proof". Nor does any of it appear in the S. E. P. entry on meaning.

Comment author: Benja 01 November 2012 05:06:34PM 9 points [-]

Very nice post!

Bug: Higher-order logic (a standard term) means "infinite-order logic" (not a standard term), not "logic of order greater 1" (also not a standard term). (For whatever reason, neither the Wikipedia nor the SEP entry seem to come out and say this, but every reference I can remember used the terms like that, and the usage in SEP seems to imply it too, e.g. "This second-order expressibility of the power-set operation permits the simulation of higher-order logic within second order.")