Second order logic, in first order set-theory: what gives?

https://www.lesswrong.com/posts/DavM6jKpPMk9Hr3PK/second-order-logic-in-first-order-set-theory-what-gives

With thanks to Paul Christiano

My previous post left one important issue unresolved. Second order logic needed to make use of set theory in order to work its magic, pin down a single copy of the reals and natural numbers, and so on. But set theory is a first order theory, with all the problems that this brings—multiple models, of uncontrollable sizes. How can these two facts be reconciled?

Quite simply, it turns out: for any given model of set theory, the uniqueness proofs still work. Hence the proper statement is:

Often, different models of set theory will have the same model of the reals inside them; but not always. Countable models of set theory, for instance, will have a countable model of the reals. So models of the reals can be divided into three categories:

And similarly for the natural numbers.

Comment

https://www.lesswrong.com/posts/DavM6jKpPMk9Hr3PK/second-order-logic-in-first-order-set-theory-what-gives?commentId=sqHYt8puraHNd3b72

The standard model of the reals, the unique field that obeys the second order axioms inside standard models of set theory...

(Emphasis added.)

Are there such things as "standard models of set theory"? This page from a book on model theory says that there is no standard model. The closest things, it says, are something called "natural models". I only glanced at it, but the notion of "natural model" appears to be a second-order concept that depends on the set theory with which you started.

Comment

https://www.lesswrong.com/posts/DavM6jKpPMk9Hr3PK/second-order-logic-in-first-order-set-theory-what-gives?commentId=frTyK3Jy5qnYhTtaD

Yes, I’m not sure about this myself. But people do seem to feel that some models of set theory are non-standard (eg countable models), and that there is a standard model of the reals. I get the impression that some models of set theory are "standardler" than others...

https://www.lesswrong.com/posts/DavM6jKpPMk9Hr3PK/second-order-logic-in-first-order-set-theory-what-gives?commentId=ZNs8hKDhLmiBeWFfM

If you believe that there’s a unique standard model of the reals, you must also believe that the continuum hypothesis has a definite truth value. Some people don’t believe that.

Comment

https://www.lesswrong.com/posts/DavM6jKpPMk9Hr3PK/second-order-logic-in-first-order-set-theory-what-gives?commentId=K6auxqqvQN9xBQ4qv

I don’t think that’s true. You may not believe that the set of functions is unique (in which case the notion of sets in bijection is no longer unique).

https://www.lesswrong.com/posts/DavM6jKpPMk9Hr3PK/second-order-logic-in-first-order-set-theory-what-gives?commentId=6T6TNNr8y3PDDXWpM

What exactly are you denying when you deny that the continuum hypothesis has a definite truth value? After all it’s very easy to prove "CH is either true or false" in whatever formal system you prefer, with some notable but unpopular exceptions.

Comment

I’m not completely sure of that myself, but consider this analogy. Let PA+X be a formal system that consists of the axioms of PA plus a new axiom that introduces a new symbol X and simply says "X is an integer", without saying anything more about X. Then it’s easy to prove "X is either even or odd" in PA+X, but it would be wrong to say that PA+X has a unique distinguished "standard model" that pins down the parity of X. So my statement about CH is more of a statement about our intuitions possibly misfiring when they say a formal system must have a unique standard model.

Comment

Are you comfortable rejecting the idea that PA has a "standard model"?

https://www.lesswrong.com/posts/DavM6jKpPMk9Hr3PK/second-order-logic-in-first-order-set-theory-what-gives?commentId=GupLmECTboFe6ADjN

Hmm. I don’t have the time just now, but this sequence really feels like it’s crying out for a cartoon interpretation with smiley faces and speech bubbles. What do people think?

Comment

https://www.lesswrong.com/posts/DavM6jKpPMk9Hr3PK/second-order-logic-in-first-order-set-theory-what-gives?commentId=kiRJRyyb2gkAWAZgN

Sounds like a cool idea! Though I wouldn’t call it a "sequence" :-)

https://www.lesswrong.com/posts/DavM6jKpPMk9Hr3PK/second-order-logic-in-first-order-set-theory-what-gives?commentId=tAaXwcmJaynqTbbz6

Often, different models of set theory will have the same model of the reals inside them

This sounds fishy.

Comment

https://www.lesswrong.com/posts/DavM6jKpPMk9Hr3PK/second-order-logic-in-first-order-set-theory-what-gives?commentId=4P6ePMhNPWZitjW26

If you have a model of ZFC, you can make another model by adding some large cardinals on top, and the reals will stay the same. Or am I missing something?

Comment

The predicate "is a real number" is absolute for transitive models of ZFC in the sense that if M and N are such models with M contained in N, then for every element x of M, the two models agree on whether x is a real number. But it can certainly happen than N has more real numbers than M; they just have to lie completely outside of M.

Example 1: If M is countable with respect to N, then obviously M doesn’t contain all of N’s reals.

Example 2 (perhaps more relevant to what you asked): Under mild large cardinal assumptions (existence of a measurable cardinal is sufficient), there exists a real number 0# (zero-sharp) which encodes the shortcomings of Gödel’s Constructible Universe L. In particular 0# lies outside of L, so L does not contain all the reals.

Thus if you started with L and insisted on adding a measurable cardinal on top, you would have to also add more reals as well.

Comment

Oh. Thanks.

Are there any examples of different models of ZFC that contain the same reals?

Comment

Well, models can have the same reals by fiat. If I cut off an existing model below an inaccessible, I certainly haven’t changed the reals. Alternately I could restrict to the constructible closure of the reals L(R), which satisfies ZF but generally fails Choice (you don’t expect to have a well-ordering of the reals in this model).

I think, though, that Stuart_Armstrong’s statement

Often, different models of set theory will have the same model of the reals inside them

is mistaken, or at least misguided. Models of set theory and their corresponding sets of reals are extremely pliable, especially by the method of forcing (Cohen proved CH can consistently fail by just cramming tons of reals into an existing model without changing the ordinal values of that model’s Alephs), and I think it’s naive to hope for anything like One True Real Line.

Comment

Thanks for that elucidation.

Thank you for helping me fill my stupid gap in understanding!

https://www.lesswrong.com/posts/DavM6jKpPMk9Hr3PK/second-order-logic-in-first-order-set-theory-what-gives?commentId=wLuiGQpirdnyCyzeA

Set theory has countable models? Countable according to who, or according to what system?

I’ve grappled with model theory in the past, but only long enough to convince myself that my interpretation of Godel and Lob held water. Poizat seems to say that set theory need not have a countable model unless the language has (at most) countably many symbols; now in practice this is always true, but for set theory we keep pretending that it isn’t.

Comment

https://www.lesswrong.com/posts/DavM6jKpPMk9Hr3PK/second-order-logic-in-first-order-set-theory-what-gives?commentId=eymsiLwjQtj4hbYwT

ZFC amounts to a binary relation "is an element of", satisfying some axioms. A countable model of ZFC is a binary relation on the integers 1,2,3,… satisfying the axioms. According to set theory such a relation exists, for instance this is a consequence of the Lowenheim-Skolem theorem. This relation is not computable.

https://www.lesswrong.com/posts/DavM6jKpPMk9Hr3PK/second-order-logic-in-first-order-set-theory-what-gives?commentId=4F7BEsYZeCH5J8udo

According to ZFC + "ZFC has models."