Has an inner model theory been developed on the basis of indiscernibles rather than measures? Is there a reasonable formalization at the level of overlapping extenders?
Fine-structural models beyond $L$ are traditionally built using ultrafilters/extenders, which encode (sufficiently) elementary embeddings. However, in some ways, indiscernibles are more natural than ultrafilters, and they may provide a different perspective. For an analogy, at the level of Woodin cardinals, properties of canonical inner models closely interrelate with properties of sets of reals under determinacy, and going back and forth between the two enhances our understanding of both. Below is what I know.
It appears that under large cardinal assumptions, there is a natural hierarchy of indiscernible-based canonical inner models $M$. Here are some examples, along with (proved or conjectured) large cardinal strength of $K^M$:
$L[Card]$ — proper class of measurables ($Card$ is the class of cardinals).
$L[Reg]$ — measures of order zero ($Reg$ can be the class of regular uncountable cardinals).
$L[\mathrm{cf}]$ — measures of higher orders with $o(κ)≤κ$ (see the question Complexity of L[cf]).
$L[λκ.o(κ)]$ — perhaps just below a strong cardinal ($o$ is Mitchell order (ignoring extenders); $κ∈Ord$).
Stable Core (introduced by Sy-David Friedman) — around "Ord is Woodin" (and stronger for enriched stable cores). One version of the Stable Core is $(L[S],∈,S)$ where $S=\{(n,α,β): n>1 ∧ V_α ≺_{Σ_n} V_β\}$.
What kind of hierarchy is this?
In each case, the predicate (such as $Card$ for $L[Card]$) acts analogously to the extender sequence (for full extenders in a fine-structural model). And given a stronger model $(L[S],∈,S)$ and a weaker model $(L[S'],∈,S')$ (even with $S'$ semantically unrelated to $S$), it appears that $∃α \, \mathrm{Theory}(L[S'],∈) = \mathrm{Theory}(L_α[S],∈)$. $M$ appears to have traditional large cardinals below measurables, but apparently no measurables despite many measurables in the core model $K^M$: In place of measures, we get sequences of indiscernibles.
To understand $M$, we can analyze $K^M$, and perhaps show that $M$ is a limit of generic extensions of $K^M$ using some generalization of Prikry forcing.
Or perhaps we can do fine structure on $M$ directly. $0^\#$ can be represented by the set of the first $ω$ Silver indiscernibles (indexed at its supremum), and similarly with other measures. Soundness essentially corresponds to not skipping any indiscernibles (like omitting the first Silver indiscernible) in indexed sequences that become discernible at some stage in the model construction.
Regarding which sequences of indiscernibles to include in $M$, here is a possible answer for total extenders and below a strong cardinal. To build $M=(L[S],∈,S)$, let $N$ be a fine-structural inner model below a strong cardinal. Iterate $N$ using the standard linear normal nondropping iteration such that:
* At any point we can mark the extender before applying it, recording its current critical point.
* For limit stages, use the least available extender that has not been marked cofinally often. For successor stages, use the least available extender.
* When an extender has been marked a limit number of times, add the set of all its markings to $S$. (Whether this is correct (or is a good convention) is unclear.) $S$ is initially empty.
* End when we run out of extenders (or choose to truncate earlier).
Notes:
- 'Normal' requires the extender index to increase each time.
- I think the procedure can be generalized to iteration trees, but there are complications such as switching of branches, and multiple extenders used with the same critical point.
- For partial extenders (only needed for fine structure), the process is similar, but (for soundness) we always mark the extender to avoid skipping indiscernibles.
- Different choices of $S$ can give different models $M$, but (unless we truncate) the theory of $M$ for a given $N$ should be independent of $S$. Furthermore, for many $N$, regardless of $S$ (and unless we truncate), $K^M$ should be the last iterate of $N$.
