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.