Wei_Dai comments on Open Problems Related to Solomonoff Induction - Less Wrong

27 Post author: Wei_Dai 06 June 2012 12:26AM

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

Comments (102)

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

Comment author: Wei_Dai 29 December 2012 02:34:44PM 0 points [-]

Then in second-order logic, why doesn't the sentence (ST->"All sets: Set entails S") form a truth predicate for S?

Let S="ST -> false". Then S is false in second-order logic (assuming ST is consistent), but (ST->"All sets: Set entails S") is true, because ST's model has to be bigger than any set (I think it's usually taken to be the proper class of all sets), so every set entails "Not ST".

So the new answer would be that you are welcome to hypothesize that a device prints out truths of second-order logic, for any given background second-order set theory which provides a universe of models against which those sentences are judged universally semantically true.

On input S="ST -> false", your device prints out "true", while my device prints out "false". I still want to be able to hypothesize my device. :)

Comment author: Eliezer_Yudkowsky 30 December 2012 12:55:26AM 0 points [-]

There are totally models of ZFC containing sets that are models of ZFC. See "Grothendieck universe". Is there a reason why it'd be different in second-order logic? I don't think a second-order set theory would pin down a unique model, why would it? Unless you had some axiom stating that there were no more ordinals past a certain point in which case you might be able to get a unique model. Unless I'm getting this all completely wrong, since I'm overrunning my expertise here.

So in retrospect I have to modify this for us to somehow suppose that the device is operating in a particular model of a second-order theory. And then my device prints out "true" (if it's in one of the smallest models) or the device prints out "false" (if it's in a larger model), unless the device is against the background of an ST with an upper bound imposing a unique model, in which case the device does print out "true" for ST -> false and from the outside, we think that this device is about a small collection of sets so this result is not surprising.

Then the question is whether it makes sense to imagine that the device is about the "largest relevant" model of a set theory - i.e., for any other similar devices, you think no other device will ever refer to a larger model than the current one, nor will any set theory successfully force a model larger than the current one - I think that's the point at which things get semantically interesting again.

Comment author: Wei_Dai 30 December 2012 01:57:03AM 0 points [-]

Is there a reason why it'd be different in second-order logic?

Second-order set theory is beyond my expertise too, but I'm going by this paper, which on page 8 says:

We have managed to give a formal semantics for the second-order language of set theory without expanding our ontology to include classes that are not sets. The obvious alternative is to invoke the existence of proper classes. One can then tinker with the definition of a standard model so as to allow for a model with the (proper) class of all sets as its domain and the class of all ordered-pairs x, y (for x an element of y) as its interpretation function.12 The existence of such a model is in fact all it takes to render the truth of a sentence of the language of set theory an immediate consequence of its validity.

So I was taking the "obvious alternative" of proper class of all sets to be the standard model for second order set theory. I don't quite understand the paper's own proposed model, but I don't think it's a set either.

Comment author: Eliezer_Yudkowsky 30 December 2012 02:42:11AM 0 points [-]

I'm not sure I believe in proper classes and in particular, I'm not sure there's a proper class of all sets that could be the model of a second-order theory such that you could not describe any set larger than the model, and as for pinning down that model using axioms I'm pretty sure you shouldn't be able to do that. There are analogues of the Lowenheim-Skolem theorem for sufficiently large infinities in second-order logic, I seem to recall reading.