Talk:Internal set theory

Are there infinitesimals?

The lead paragraph contains the following sentence: "In particular, non-standard elements within the set of real numbers can be shown to have properties that correspond to the properties of infinitesimal and unlimited elements." The sentence is vague and probably incorrect. Could someone take a look at this? Katzmik (talk) 11:20, 21 September 2008 (UTC)

it is vague, but not incorrect. For instance, any nonstandard real number is either infinitely close to some standard real or infinitely far from every standard real

(formally: $\forall x~\lnot \operatorname {st} (x)\implies ((\exists y\forall z~\operatorname {st} (z)\implies |x-y|<|z|)\lor (\forall w\forall v(\operatorname {st} (w)\land \operatorname {st} (v))\implies |x-w|>|v|)$ where st(_) means "_ is standard )

Kaoru Itou (talk) 18:19, 22 February 2009 (UTC)

The problem is that the article conflates Nelson's rather bizarre philosophical point of view on what his theory means with the theory itself. The claim is exactly like saying that NBG set theory doesn't add anything new to the ZFC set theory for which it is a conservative extension. Well, it does. In just the same way, IST, which is a conservative extension of ZFC, has all of the theorems of ZFC including the construction of the integers and the reals within ZFC. The the nonstandard reals are therefore new. And of course, nonstandard integers are not standard integers for which you don't have enough ink and paper to write them down, as Nelson likes to suggest. Gene Ward Smith (talk) 04:56, 16 July 2012 (UTC)

Nonstandard natural numbers?

"Nevertheless, there are (many) non-standard whole numbers in any infinite subset of N"

This bullet point troubled me - I thought that nonstandard numbers were too big to fall in the naturals, and that by definition were outside of it (since a nonstandard model of the natural numbers is one nonisomorphic to N.) But maybe nonstandard models are separate from nonstandard sets or elements? If so, could someone explain how nonstandard models relate to the IST notion of standardness? Dr satsuma (talk) 14:41, 20 June 2010 (UTC)

It may be helpful to keep in mind the fact that when one talks about "N" in IST, what one means is "*N" in Robinson's theory. When one says "infinite subset of N" in IST, what one means is "internal subset of *N" in Robinson's theory. Tkuvho (talk) 14:54, 20 June 2010 (UTC)

I think they are different notions, since there are only finitely many standard natural numbers in Nelson's convention while there are infinitely many in the convention based on standard models of PA. C7XWiki (talk) 05:37, 12 September 2022 (UTC)

A model?

Suppose M is the minimal model of ZFC, all of whose elements are definable. Take an ultrapower, U, of M over some non-principal ultrafilter on ω. For any element x of M, let ι(x) be the equivalence class of the constant function on ω whose value is always x. Then ι is an elementary embedding of M into U. For y∈U, let S(y) hold whenever there is an x∈M such that y=ι(x). In other words, the standard elements of U would be just the images of the elements of M. Then it seems to me that (U,S) would be model of IST. Is that right? JRSpriggs (talk) 15:00, 23 December 2010 (UTC)

Do you have a specific purpose in mind when you start with a minimal model of ZFC rather than the "usual" model? Otherwise you seem to have summarized the ultrapower construction, which can certainly be re-worded in terms of IST. The advantage of IST is to codify as axioms certain properties that require tedious proof in the so to speak standard non-standard approach. Tkuvho (talk) 15:50, 23 December 2010 (UTC)

I was trying to confirm the claim that IST is a conservative extension of ZFC + exists a standard model of ZFC, by constructing a model of IST within the universe of ZFC. The minimal model (a set in that universe) has the property that each element is definable, thus satisfying "Any number uniquely specified by a classical formula is standard (by definition).". JRSpriggs (talk) 19:33, 23 December 2010 (UTC)

That's an interesting idea. I don't know enough about set-theoretical minimal models to comment competently. I am not sure why one would need minimal models to prove conservativeness. Apparently the existence of the ultrapower construction, together with all the tedious theorems that the properties taken as axioms in IST are indeed satisfied (particularly the "idealisation" axiom, which I don't understand fully; perhaps someone can improve on the explanation in the article), implies conservativeness. Tkuvho (talk) 19:43, 23 December 2010 (UTC)

What you seem to want to gain through working with minimal models is a particular realisation of the "standard" predicate in IST, namely that an individual will be "standard" if and only if it is definable. Is that correct? This may well be true, but I am still not sure if it is directly related to a verification of "conservativeness". Tkuvho (talk) 08:45, 24 December 2010 (UTC)

Yes, I see. If you limit yourself to just verifying the three additional axioms, then using the minimal model for M or even a countable model is not necessary. But this raises the question whether the three axioms adequately represent the intuitive notion of "standard" described in the preceding section. JRSpriggs (talk) 12:44, 24 December 2010 (UTC)

I made a comment about this at the discussion at constructions of real numbers, feel free to comment further. Tkuvho (talk) 16:32, 25 December 2010 (UTC)

Actually the comment I was referring to was at real number, not at "construction". Here is the relevant segment of the discussion there:

It's not necessary to resolve this in order to find an acceptable wording for the article. But I don't see why we need ZFC to see that the real line is a complete Archimedean ordered field; I think this is clear just from our intuition about various properties of idealized geometric lines. — Carl (CBM · talk) 22:13, 22 December 2010 (UTC)

Trovatore: I am still not sure what you are trying to say. Fine, let's call it "set theory". The traditional approach to defining the reals certainly starts with set theory. The question is, which set theory do you start with? If you don't specify the axioms, you don't know which set theory you are in. If you start with ZF, you get one kind of real field. If you start with the IST axiomatisation, you get a real field with greater ability to express intuitively appealing constructions in calculus. Carl: I think I can appreciate that your "idealized geometric line" is a ZF-based real field. On the other hand, quantum theory tells us that certain tiny lengths are inaccessible even theoretically. Similarly, the finite size of the universe tells us that certain huge sizes are inaccessible even theoretically (see the related motivational discussion at IST). My "idealized geometric line" is much closer to Nelson's than to Cantor's. Tkuvho (talk) 10:25, 23 December 2010 (UTC)

I should add that I am not really sure one can apply the ultrapower construction to the minimal model you mentioned. I am relying on naive set theory in my thinking about the ultrapower construction. One would have to check that whatever set-theoretic tools one needs to implement the ultrapower construction, are still available in the context of a minimal model. Perhaps someone could comment as to the feasibility of this. Tkuvho (talk) 15:50, 3 January 2011 (UTC)

First, I meant that the minimal model is the object of which one is taking an ultrapower. On the other hand, the ultrafilter and the resulting ultrapower model are constructed within the original set theoretic universe which contains the minimal model as a set. So they are not constrained by being inside the minimal model.

Second, if one were doing a construction inside the minimal model itself, one would still have the full power of ZFC available, since it is the minimal model of ZFC after all. JRSpriggs (talk) 06:48, 4 January 2011 (UTC)

OK. Apparently if everything is definable everything is also countable. Could you comment what happens to Cantor's diagonal argument inside the minimal model? Tkuvho (talk) 10:09, 4 January 2011 (UTC)

In the universe of sets which contains the minimal standard model, M, as an element, one can define a surjective function from a subset of ω (the Gödel numbers of formulas defining sets) onto M. However, this requires the ability to define satisfaction (Tarski's truth predicate) for M. That cannot be done within M itself because one cannot talk about subsets of M ⁿ within M. Thus M is countable but is unable to know that it is countable because the requisite bijection cannot be defined inside M. JRSpriggs (talk) 10:41, 4 January 2011 (UTC)

If we apply the ultrapower construction to M, how does the notion of "definability" go over exactly? How do we know that the imbedding of the minimal R to the resulting R* will hit precisely the definable numbers in the new system? Tkuvho (talk) 11:22, 4 January 2011 (UTC)

That is a special case of Ultraproduct#Łoś's theorem. If all the factor spaces are the same and the element selected from them is the same, then the equivalence class of the function which selects them satisfies the same formula as the element in the original model, i.e. its definition in our case. JRSpriggs (talk) 11:42, 4 January 2011 (UTC)

Why couldn't there be new definable elements in R*? Tkuvho (talk) 14:54, 4 January 2011 (UTC)

Perhaps the reason is as follows. If there were an element in such an exotic R* that satisfies a formula f(x), then the formula $(\exists x\in R*)f(x)$ is satisfied in R*. Since R* is elementarily equivalent to R by Los, it follows that there must be an x0 in R satisfying the same formula. Now I guess we need a more precise version of elementary equivalence saying that the diagonal imbedding of R in R* is compatible with the equivalence. Then x and x0 must be the same. Does that work? Tkuvho (talk) 15:06, 4 January 2011 (UTC)

Yes. The predicate f defines x in R* if and only if R* satisfies $\forall y(f(y)\leftrightarrow y=x)\,.$ In that case, one also has R* satisfies $\exists z\forall y(f(y)\leftrightarrow y=z)\,,$ and thus R also satisfies it. Thus there is a w in R such that R satisfies $\forall y(f(y)\leftrightarrow y=w)\,.$ Thus R* satisfies $\forall y(f(y)\leftrightarrow y=w)\,.$ This is only possible if x=w which is in R. JRSpriggs (talk) 17:04, 4 January 2011 (UTC)

Getting back to the original minimal model M (before ultrapowering it), given that it's a model for all of ZF in particular you can develop each "real" in M as a decimal. What kind of decimal expansions do you get for the "reals" in M"? Is it correct to say that they are precisely the decimal expansions of the standard definable reals? Then M seems to be naturally imbeddable in R. Can the same be said of all of M, i.e. the the entire minimal ZF theory gets imbedded in standard ZF? If so, why do we need existence theorems for minimal models? Apparently merely extracting everything definable from standard ZF should give such an M. Tkuvho (talk) 17:45, 4 January 2011 (UTC)

@JRSpriggs: I see no reason why your model should satisfy the standardization axiom. If A ∈ M and B is a subset of A, then B does not have to be in M unless it is definable in M, whereas the axiom only makes it definable in (U,S), with parameters from U (note that the formula may be external).

In any case, IST is a conservative extension of plain ZFC, without any extra axioms on existence of models of ZFC (as duly noted in the article). One way to show that is as follows. Assume that IST proves an internal sentence A. Then there is a finite fragment X of ZFC such that X + the three IST axioms prove A. Now work in ZFC. By the reflection principle, there is a limit ordinal α such that V_α is a model of X, and reflects A. Let κ > |V_α|, and let M be a κ-saturated elementary extension of V_α (which can be chosen as a suitable ultrapower of V_α, but there is not really a point in that). Then (M,V_α) is a model of X and Transfer (by elementarity), Idealization (by saturation), and Standardization (as V_α includes all subsets of its elements), hence M satisfies A, therefore so does V_α (by elementarity) and the universe (by reflection).—Emil J. 15:27, 6 January 2011 (UTC)

This is a bit terse for my level. Would you be willing to provide some additional clarifications? First of all, are you using the terms "external" and "internal" in the sense of nonstandard analysis, or in some other set-theoretic sense? Also, I find your use of the reflection principle a bit puzzling. Apparently all of nonstandard analysis can be done in the countable union of sets at each rank n, so that one never needs to work with classes. Would you care to comment? Tkuvho (talk) 20:12, 6 January 2011 (UTC)

To EmilJ: Yes, that was the point of my question. I wanted an explanation of how it is shown that IST is a conservative extension of ZFC. Please put it into the article. JRSpriggs (talk) 22:50, 6 January 2011 (UTC)

I don't think it is a good idea to put this into the article. The construction is fairly technical, way above the level of the rest of the article, and it relies on several nontrivial concepts from set theory and model theory. If someone is really interested in the technical details, they can find it in the literature. Speaking of which, I added a reference to Nelson's original paper. He includes a proof of the conservativity in the appendix; the proof follows the outline I wrote above, except that he (or rather Powell, who is quoted as the actual author of the result) constructs the model I denoted M explicitly as a limit of an elementary chain of suitable ultrapowers (which makes it look more complicated, but it avoids the use of model-theoretic machinery).

@Tkuvho: I added a couple of explanatory wikilinks above. Yes, I am using "external" and "internal" in the sense of nonstandard analysis (i.e., formulas of the usual language of set theory are internal, and formulas in the expanded language with the "standard" predicate are external). Nelson uses the same terminology, I have no idea why this article uses a different one (apparently, "classical" = internal). As for reflection, I am using a variant of Levy's reflection principle which says that for any finite list of sentences A₁, ..., A_n (here: A and the sentences from X) there exists an ordinal α such that $A_{i}\leftrightarrow (V_{\alpha },\in )\models A_{i}$ for every i. The idea is that instead of dealing with the full universe, we work with a set model which behaves in a sufficiently similar way, but (being a set) admits rich elementary extensions.

The least obvious part of the construction above is probably verification of the Idealization axiom schema, which goes as follows. Assume that R(f,g) is an internal formula (possibly with parameters from M) such that $(M,V_{\alpha })\models \forall ^{\operatorname {stfin} }F\,\exists g\,\forall f\in F\,R(f,g)$. This means that for any finite subset F of V_α, there is a g in M satisfying R(f,g) for all f in F. In other words, the set of formulas in one free variable $\Gamma (x)=\{R(f,x)\mid f\in V_{\alpha }\}$ is a 1-type of M (i.e., each finite subset is satisfiable in the model) with parameters from V_α and finitely many parameters from M. The total number of parameters is thus less than κ, hence by κ-saturation, Γ is satisfied in M by some element g, and this g then satisfies R(f,g) for every f in V_α.

I don't quite understand your last remark. Are you saying that one can do analysis in a nonstandard theory of hereditarily finite sets (i.e., Peano arithmetic)? I guess that's possible to some limited extent (reals, continuous functions on reals). However, I don't see what this has to do with IST, which by definition extends full ZFC.—Emil J. 14:06, 7 January 2011 (UTC)

Please give the axiom schemas as explicit formulas in this article, as is done in the article Zermelo–Fraenkel set theory. JRSpriggs (talk) 09:30, 8 January 2011 (UTC)

Done.—Emil J. 16:33, 10 January 2011 (UTC)

To EmilJ: You have improved the article quite a lot. Thank you. JRSpriggs (talk) 02:41, 11 January 2011 (UTC)

ZFC+IST

You wrote "IST includes ZFC, it's pointless to write ZFC + IST". Here IST is a bit ambiguous, as it may mean "idealisation, standardisation, transfer" rather than "internal set theory", so it is probably better to keep the somewhat redundant ZFC+IST. Incidentally, while you are at it, it may be helpful to clarify the idealisation axiom. As it currently appears it is difficult to follow. Tkuvho (talk) 16:29, 10 January 2011 (UTC)

"IST" is used consistently in this article (and elsewhere in the literature) to denote the whole theory. There is no reason to think otherwise, and writing ZFC + IST is positively confusing as it suggests that IST does not include ZFC.

As for the idealization axiom, could you be more specific?—Emil J. 16:37, 10 January 2011 (UTC)

As far as idealisation, I understand that every internal set in R is finite and I think I can even prove it, but the general statement of Idealisation is just too confusing. Perhaps some more examples would help bridge the gap? I am not talking about explaining this to others, I can't follow it myself properly. Tkuvho (talk) 16:42, 10 January 2011 (UTC)

What do you mean by an "internal set in R"? Anyway, the right-to-left implication in the statement simply says that finite standard sets have only standard elements. The important implication is the left-to-right one, and it's not that easy to explain it. Basically, it says that the collection of all standard sets can be embedded in a finite internal set, and moreover, one can take this finite set to satisfy any additional (internal) property that holds for all standard finite sets and is upwards directed (say, closed under finite unions). The axiom is actually formulated a bit differently to avoid dealing with the directedness assumptionfor whatever reasons. It is a variant of the finitization principle, which is a well-known tool in nonstandard analysis; I don't think there is a good way of understanding it other than learning how things get proved in nonstandard analysis. I'd also like to stress that I am not the right person to ask about IST, as I've never worked with this theory before (but I had some exposure to other, somewhat similar, nonstandard theories).—Emil J. 17:05, 10 January 2011 (UTC)

By "internal set in R" I meant that in Robinson's framework, if you have an internal subset of R* which happens to lie in R, then the subset is finite. This is clearly a special case of Idealisation. I am thinking about your remarks. Tkuvho (talk) 17:57, 10 January 2011 (UTC)

I see, I was confused as the descriptions in the article refer to an unrelated R. I also realized that I made the explanation unnecessarily complicated. The assumption of directedness is not really needed here. (What I confused it with was another statement, namely if (P,≤) is a standard directed partial order and an internal property holds for all standard elements of P, then it also holds for some element of P that majorizes all its standard elements. Here, P would be the class of all finite sets, which is automatically directed.)—Emil J. 18:53, 10 January 2011 (UTC)

I think I figured out what is going on. Let me formulate it in Robinson's framework. Every real entity (of any rank in the set-theoretic tower) has a natural extension A*. It also has an image $\;{}^{im}\!A\subset A^{*}$. If I understand it correctly, Idealisation says that if X is an internal subset of A* contained in ${}^{im}A$, then X is a finite subset thereof. Is that what the logical riddle is all about? Tkuvho (talk) 19:48, 10 January 2011 (UTC)

No, this sounds wrong. It's been a while since I've seen Robinson's framework, but if I understand it correctly, your statement says that every infinite internal set has a nonstandard element. That is a consequence of idealization, but it is much weaker than the axiom. Let me give another try. Idealization is a form of compactness. A topological space is compact iff the following holds:

If $\{X_{i}\mid i\in I\}$ is a collection of closed sets such that $\bigcap _{i\in J}X_{i}\neq \varnothing$ for every finite $J\subseteq I$, then $\bigcap _{i\in I}X_{i}\neq \varnothing$.

Back to IST, let ST = {x | standard(x)} be the collection of all standard sets. Then the idealization axiom states:

If $\{X_{i}\mid i\in ST\}$ is a uniform collection of internal classes such that $\bigcap _{i\in J}X_{i}\neq \varnothing$ for every finite $J\subseteq ST$, then $\bigcap _{i\in ST}X_{i}\neq \varnothing$.

Here, a collection of internal classes is uniform if there is a single formula $\phi (x,y)$ (possibly with parameters) such that $X_{i}=\{y\mid \phi (i,y)\}$ for every standard i. Pretty much the same formulation should work in Robinson's approach, with R in place of ST. It's a variant of what's called “saturation” in our nonstandard analysis article, except that there is no cardinality restriction.—Emil J. 12:30, 11 January 2011 (UTC)

What you are describing is the defining property of an enlargement. So Idealisation is an idealisation of enlargement? Wouldn't have guessed it in its intensional guise. Note that the ordinary ultrapower construction (with indices in N) is only countably saturated, so it fails the "I" test? Tkuvho (talk) 14:10, 11 January 2011 (UTC)

If you mean this definition of enlargement, then no, that's still a weaker property. First, you need a single hyperfinite set containing all standard entities in V(^*X). Second, even then you only get the idealization principle for formulas without internal parameters. To get the parameters, you'd need to iterate the enlargement construction countably many times. An ultrapower over a countable index set is indeed not enough.—Emil J. 14:45, 11 January 2011 (UTC)

It's nicely summarized in [1] (it's page 103 if the Google Books link does not work). The idealization axiom corresponds basically to polysaturation, except that it's supposed to apply to internally definable classes rather than “entities” (which I assume are elements of the model, i.e., sets here).—Emil J. 14:51, 11 January 2011 (UTC)

I see. It would be helpful to have a wiki page on enlargements and how they relate to Nelson. Tkuvho (talk) 15:00, 11 January 2011 (UTC)

At the very least the reader should be given an indication of the magnitude of the task, by listing in "increasing order", first the easily stated property that every element standard implies finite, then countable saturation, then arbitrary saturation, then the full scope of the thing. Otherwise it is hard to orient oneself. Tkuvho (talk) 15:10, 11 January 2011 (UTC)

Tell me if I have this right. The idea of idealization is to add as many external elements, y, as one can without contradicting the other axioms. Deriving a contradiction from

$\forall ^{\mathrm {st} }x\,\phi (x,y,u_{1},\dots ,u_{n})\,$

internally would mean that one would have a finite proof of 0=1 which necessarily uses only finitely many instances, that is,

$\phi (x_{k},y,u_{1},\dots ,u_{n})\,$

for k∈{0,1,2,...,j}. So we can take z={x₀,x₁,...,x_j} which gives the negation of the left hand side, i.e.

$\exists ^{\mathrm {st} }z\,(z{\text{ is finite}}\,\land \lnot \exists y\,\forall x\in z\,\phi (x,y,u_{1},\dots ,u_{n}))\,.$

OK? JRSpriggs (talk) 16:34, 11 January 2011 (UTC)

Yes, this is one way to look at it (except that the elements are internal, not external). You can construct models satisfying I by suitably iterating this construction.—Emil J. 17:29, 11 January 2011 (UTC)