# Consistency of reflective sequences

Is it consistent that there is a measurable cardinal $$κ$$, a $$κ$$-complete normal nonprincipal ultrafilter $$U$$ on $$κ$$, and $$S∈U$$ such that for every $$T⊂S$$ with $$T∈U$$ and $$T$$ ordinal definable from $$S$$ and a countable sequence of ordinals, $$S$$ and $$T$$ satisfy the same $$Σ_2^V$$ properties with parameters in $$V_{\min(S)}$$? If so, what is the consistency strength?

Notes:
* Using $$Σ_n^V$$ ($$n>2$$) in place of $$Σ_2^V$$ properties should have a similar (but likely growing with $$n$$) consistency strength.
* A possible natural additional requirement is that for every $$S'∈U$$, there is $$T∈U$$ with $$T⊂S∩S'$$ and $$S$$ and $$T$$ satisfying the same $$Σ_2^V$$ properties with parameters in $$V_{\min(S)}$$.

The motivation for the question is (1) it is a very strong form of indiscernibility (given the axiom of choice), and (2) its role in extensions of set theory.

The axiom of choice precludes unconditional infinitary indiscernibles: $$κ \not\rightarrow (ω)^ω$$. However, it does not usually prevent definable versions of regularity properties, so the above restricts it to (essentially) definable predicates and definable subsets of $$S$$. For long enough $$S$$, both restrictions are necessary. However, our use of parameters in $$V_{\min(S)}$$ (for distinguishing but not defining $$T$$) is not a problem, or rather $$S∈U$$ is but a point in a hierarchy of notions, and stronger notions without $$V_{\min(S)}$$ give weaker notions with $$V_{\min(S)}$$.

The relevance to extensions of set theory is the following. To increase expressiveness beyond the language of set theory, we can 'choose' a cardinal $$S_0$$ with sufficiently strong reflection properties, which allows us to express statements in higher order set theory. For further expressiveness, we can choose a larger cardinal $$S_1$$ in the same manner, and iterate this indefinitely, getting (essentially) a reflective sequence $$S$$. (Reflective cardinals and reflective sequences are introduced and analyzed in my paper Reflective Cardinals (and its precursor Extending the Language of Set Theory).) We continue through $$S_ω$$ (which is above $$\lim_{n→ω} S_n$$), $$S_{ω_1}$$, $$S_{\min(S)}$$, eventually reaching a limit point of $$S$$ that is in $$S$$, and going further, $$S∈U$$ is a strong version of claiming that $$S$$ has many elements.
To axiomatize such $$S$$, we assert a strong form of symmetry and indiscernibility, and in particular that if we were stricter about putting elements into $$S$$ in a sufficiently definable manner (with symmetry allowing the use of definability from $$S$$) and still get enough elements (formalized through $$T∈U$$), then we get the same theory (with parameters that are small relative to $$\min(S)$$). We also want strong reflection properties for $$κ$$ and $$U$$, but the form in the question suffices for many basic properties of $$S$$, assuming there is no falsehood or inconsistency.

Starting with an inner model with a measurable cardinal of order 2 below $$ω_1^V$$, we can iterate it and the measurables below it until they match the elements of $$S$$ (but I have not proved that), with $$\sup(S)$$ being the resulting least measurable of order 2. Thus (assuming the above), $$(L[S],∈,S)$$ has a well-behaved theory that does not depend on $$S$$. However, the least measurable in $$K^{L[S]}$$ appears to be $$\lim_{n→ω} S_n$$, so in $$L[S]$$, $$S \setminus S_ω$$ is distinguishable from $$S$$. We would need more sets to get the symmetry in the question.