Linear Christmas

@user267839

Finally, no need to be dogmatic or fiercely loyal to one position throughout time. Some malleability can be useful, and one position more useful in one exercise than another.

If you want to judge "betterness", the universe is a good judge. But if you do not want to harshly? judge models against one another, a multiverse view can help.

In conclusion, you arrive at oxymora or seeming paradoxes because (i) you seem to be dissatisfied with the purely "$x$ is smallest inductive set" is a well-formed formula, which is provable in ZFC approach. From the philosophical side, (ii) you are at the same time comparing two different models of ZFC, attempting to judge which is "better" but not completely following through with this judgment.

(b) You might be interested in the multiverse (pluralist) view on set theory, recently popuralised by J. D. Hamkins, see, e.g., arxiv.org/pdf/1108.4223.

(a) The (classic) universe view is that there is only one true set of integers (up to isomorphism). Various strange models of set theory might think that what they have is (a representative of the class of) the true set of integers, but these models might be said to be mistaken from the point of view of the universe. The "universe" is the jury, the arbiter.

(2) Thinking in terms of philosophical positions:

(1) Consider transitive epsilon-models of ZFC (or even Z – P). Then $x = \omega$ is absolute between such models. Finiteness ("$x$ is finite") is also absolute for transitive epsilon-models of ZFC. So this particular problem no longer occurs.

Solutions:

You say "it is dangerous to talk about the set of integers" because different models of ZFC will (think to) have a set of integers of various seemingly conflicting properties.

So there is some association between the results that present themself and the philosophy of the cameraman, sort of speak. With this association in mind and positing the existence of a subjective meter stick on types of result one considers interesting or useful or worthy, one may loosely judge the various positions at a given point in time. Regardless of the fact that they are equivalent in the sense explained previously. There is no need to be loyal to one position only.

Nevertheless, there are ways in which the philosophical positions differ. Namely that they have unlike consequences for our psychology. This psychological effect manifests in the behaviour of the mathematician: what results are considered important to study, which topics even come to mind to study, which results seem intuitive, which proofs are inspired, etc, etc. So the output and ways of thinking will be different.

Various philosophical positions on ZFC and mathematics in general usually respect what I have said before. In that we can always resort to syntactical proofs in ZFC if necessary, and that for actually writing and verifying the proof (without additional meaning given) the various positions are equivalent.

This formula is derivable. You can define auxiliary shorthand using $\omega$ for convenience, with the express understanding that this shorthand is either (1) actually expanded out in a formal proof; (2) proven in a minimal metatheory way to behave in certain ways (proven by expanding out in a formal proof), and then used in these certain ways (because this use has been justified beforehand); or (3) definitionally expanded and proven to behave as intended.

"$x$ is smallest inductive set" is a specific well-formed formula (up to some renaming of individual variables in the language of ZFC), and that's it.

Perhaps we are now discussing different matters, so my response might be of limited use. The emphasis I made was that "$x$ is the smallest inductive set" is a well-formed formula in the language of ZFC. Really, the formula says that "$x$ has the inductive property and amongst such $x$ has the property of being smallest". There is no "is a set" predicate in the language. So all this talk about models and different natural number sets is irrelevant, at least when doing formal proofs with ZFC.

It is best to ask Alex what exactly he meant. We, of course, can talk about the set of natural numbers as the smallest inductive set in ZFC (in fragments, such as ZFC minus Inf we'd need an alternative formula). And if we call these "external naturals" then via the defining formula we can indeed talk about the unique ω.

Further, you cannot extend ZFC with the axiom that $\exists x: \varphi(x) \wedge |x| > |\omega|$. This would be a syntactically inconsistent system to begin with.

@user267839 Yes, ZFC derives derivable objects which very commonly are formulae. The point is not that you need to start fixing models to talk about sets. The point is that the talk about sets is "just in your head", a helpful but removable fictional narrative to make sense of what you are doing. Whether you take the further truly platonistic view is up to you, not really crucial (you could pretend to be platonistic, you could pretend to be playing a game, be a formalist etc). But depending on the situation, the narrative can also help to come up with results which otherwise'd be hidden.

@user267839 (The platonic model of ZFC, I denote this by U (or V), is not a set model, it is a proper class model. In the context of ZFC, it is actually a syntactic conceptual shorthand for the formula $x = x$. One can analogously view other definable-with-parameters classes within ZFC, but there can be further classes if you consider some true class theory. But this is beside the point here, I think.)

In terms of ZFC, which is a formal syntactic theory, with its alphabet, formula definition, derivable objects (can be formulae but need not be), proofs and so on, "exists unique minimal inductive set" is a well-formed formula which can be proven from the axioms using the rules of inference. The word "set" there is superfluous. It is the useful narrative we tell ourselves that ZFC is talking about sets, not part of the formal language. There is no "x is a set" predicate; the formal deductions don't use "is a set" anywhere; we humans informally interpret ZFC as talking about sets.

(2/2) for $\varphi^{(M, E)}$ the same unique existence, more precicely $\exists ! x E M : \varphi^{(M, E)}$ which is the aforementioned relativization. Denote this unique set by $\omega^{(M, E)}$. Elements of this set are the "internal naturals of (M, E)". We (tend to) view our "external naturals" from $\omega$ as the true naturals, insofar as ZFC "truly" describes "(a subset of) the Platonistic world of sets", if there is such a thing.

@user267839 I hope not to misrepresent Alex's words. External-internal are relative terms. As I read his answer, the external-internal distinction takes place within ZFC. Namely, define "the set of natural numbers" to be any set that is a minimal inductive set (there's a formula $\varphi$ which says "minimal inductive"). Then ZFC proves there's exactly one set $\omega$ satisfying $\varphi$ whose elements are the "external naturals". If you have a (partial) model $(M, E)$ of ZFC, you may relativize a formula to this model (this is a syntactic process). Then ZFC proves ... (1/2)

(3/2) Whether this mission to pin down THE naturals can succeed, is a different question, and may be impossible depending on the background and criteria for "succeeding".

(2/2) An analogous question: Is the formal theory of first-order logic contradiction-free? It's provable that it is, in a sense. Its proof (formulated in Platonistic logic) shows that if there were a syntactic contradiction in FOL, then there'd be a contradiction in Platonistic logic which is in turn assumed absurd. How do we really know that there's no contradiction in Platonistic logic? Point being that there are no free lunches, you need to make clear what you consider to be "THE natural numbers" first and only then can you hope to reason about whether your theory is talking about them.

@user267839 If by "formula" you mean well-formed formula, then I do not understand why you chose scenario 3 to ask about formulae referring to natural numbers. Are you asking about if we have a formal theory (either a formal metatheory, or formal object theory) and if it seems that the language allows us to talk about natural numbers (via constant symbols or otherwise), how to know for sure (in a very strong sense of sure) that the formal theory is referring to THE natural numbers? If this is the case, we never really know. (1/2)

@spaceisdarkgreen About why "encoding entailment could be the problem". It would be the source of the problem if, for instance, we could also encode "is class model". Is that not correct? So I guess I just extended that intuition :)

@spaceisdarkgreen I have heard whispers... that for any proof that uses at least one instance of the replacement schema, there is an alternative proof which uses exactly one instance of replacement. But that is not enough either.

Thank you for the reference. Unless I missed it, it just is absent in the registry of symbols in the back of the book.

@spaceisdarkgreen Notice that I put \vDash (not \Vdash), that should be the correct symbol? Or is there some small difference here? You're right that \models would be better semantically, for that I apologise. I used detexify which yielded \vDash, so looked no further.

That's all I meant to say, I guess.

Any existence and uniqueness proof attached to a definition will work for M in ZFC+, just in relativised form, because whatever axioms are used for the proof are there in ZFC+ in relatived form.

@spaceisdarkgreen The "obstacle" part was replying to your comment "You can always relativize relations, since thats just a formula. But to define a constant or a function there is always an existence and uniqueness proof that goes along with the definition. Like for instance when you write P(omega)^M you're assuming that M satisfies enough axioms to carry out the definition of P(omega)."

c) the word "model" really-really does not have the connotations I thought it did.

b) a similar non-closedness thing but having to do with expressing "is a model of" or some related theorem in the background;

a) maybe the proof of the reflection principle is not "closed wrt any finite part of ZFC", always requiring something not from a chosen finite list to prove itself;

I do see some ways out of this conundrum:

For if we take a large enough finite part of ZFC, capable in particular of proving the reflection principle for itself, and expressing "is a model (of some set of sentences)", then this finite part of ZFC would prove its own consistency.

The possibility of expressing, in the language of ZFC, statements such as "is a model of ZFC" or even expressing "is a model of some specified finite part of ZFC"... sound off alarms in my head a little bit.

@spaceisdarkgreen Hmm... I did not find the entails symbol $\vDash$ in the registry of his newer set theory book. In the older one (Set theory and independence proofs), there is, of course, a lot of talk about transitive models but I could not find discussions on “transitive model axiom” or such.

I thought about Chang&Keisler's book (Model theory), but it seems not to have a table of contents... :)

On a related note, is there a book discussing this "transitive model axiom"?

(I'll be back in less than a day)

I am thinking about some things at the moment, so feel free not to respond just yet (but you may, if you'd like)

And we should get an existence-uniqueness proof of the relativised concept...

@spaceisdarkgreen By this, I was trying to understand why the existence and uniqueness proofs were an obstacle here. After all, any existence-and-uniqueness proof is relativisable to M in ZFC+.

@spaceisdarkgreen So it will include some sort of coding of these concepts in PA, and then carrying this coding over inside ZFC by means of $\omega$?

Is that correct?

So you must be saying, essentially, that the problem is the following: Even if (a) the definition of the concept is absolute, and (2) the ex. and uniq. proof may be done in relativised form, a subpart of the proof is not absolute.

But if there is an existence and uniqueness proof of a constant / function, then that can always be completed as relativised to M, in ZFC+