= 27d567bc2d48d9f40e9ccc20ea370b15)
Perplexed comments on Exponentiation goes wrong first - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (81)
The model is unique within any given model of set theory, but isn't there more than one model of set theory? Or, to ask the same question in different terms, isn't there more than one second-order logic?
If you believe in second-order logic then you believe there's only one second-order logic.
I don't understand this statement, please explain.
I guess it means that one can have a privileged platonic model for second-order logic, just like for natural numbers. The analogy would go, "If you believe in natural numbers, then you believe that there is only one notion of natural numbers". There are other models, but this is the one you really want to think about (even if you don't know what it is). Normatively objective, introspectively inaccessible. You just test consequences of formal theories against your intuition.
Seeing as Eliezer called himself an "infinite set atheist" before, I'd be surprised to see him subscribe to such strong platonism now - e.g. thinking that the continuum hypothesis has a definite truth value "out there somewhere". So I guess he meant something else, but I can't figure out what.
It is a theorem of second order Peano arithmetic that all models are uniquely isomorphic. Note that Eliezer does not say that he believes in second order logic, but only makes a conditional statement. The problem with second order logic is that it refers to the undefined term "property." Properties are pretty close to sets, so if one believes that this term is sensible, one seems to believe in a preferred model of set theory. One could talk about second-order logic only relative to a first order theory of set theory, but then one only has a relative uniqueness statement.
Eliezer seems to have brought up second-order arithmetic not because he thinks it's a good idea, but because he thinks Nelson is using it. In fact, Nelson is nervous about set theory, so he interprets induction not for arbitrary properties, but only for formulas of the language. Then induction becomes a first-order axiom scheme and Gödel says that there are many models.
Platonism refers to the inference system component of the human decision problem, while the notion of things being real refers to the outcome (reality) concept (defined with respect to this inference system). People could turn out being able to reason about infinite, but without the infinite being real (i.e. reality being infinite). Infinite could, for example, help to model uncertainty about the world.
"Uniqueness" of the natural numbers means that for any two models of the axioms, there is an isomorphism between them that preserves the successor function and identity of zero. "Uniqueness" for second order logic would be similar, though I am less familiar with the formalization, so I won't list all the things the isomorphism should preserve.
If you manage to find axioms that capture your intuitive notion. The idea is, even if induction fails, there is still a "unique" notion of natural numbers, it just isn't adequately described using induction. When you are presented with a convincing argument for a given axiomatic definition not capturing your concept, you just find what assumptions led to the disagreement and change them to obtain a better description.
I'm not sure whether to interpret that as a novel form of other-optimization, or as an ironic take on the idea that if one believes in arithmetic ( or set theory, for that matter) one also believes that the subject matter is unique.
In any case, my personal favorite higher order logic is the internal language of the free topos, which is, in fact, unique up to isomorphism. But far from universally accepted.
That doesn't even have a model of PA in it!