This question is something of a follow-up to this one: Iterating Neeman's forcing
It regards the work of Itay Neeman, MR3201836.
Neeman formulates his two-type models forcing seemingly in greater generality than is actually used. He defines what it means for a quadruple $\kappa,\lambda,\mathcal S,\mathcal T$ to be appropriate for a transitive structure $K$ satisfying enough ZFC, and defines the sequences of models in $\mathcal S \cup \mathcal T$ that make up the conditions of his forcing. Let me highlight the key things relevant to my question:
- The sequences have length less than $\kappa$.
- The models in $\mathcal T$ are assumed to be ${<}\kappa$-closed. But in practice they are often assumed to be $|M|$-closed for every $M \in \mathcal S$, which is usually ${\leq} \kappa$-closed. The exception is when they are assumed internally club via $\mathcal S$-type models.
- The models in $\mathcal S$ are assumed to contain $\kappa$ but not to be ${<}\kappa$-closed. However, they can be, and Neeman notes that if they are, then the whole forcing is ${<}\kappa$-closed. But Neeman takes some effort to show that the main properties of the forcing hold without this assumption.
Now, why does he go to such pains? Question: Are there any examples in the literature, or in your own unpublished notes, of such forcing where $\kappa>\omega$, the models in $\mathcal S$ are not $\kappa$-closed, and we can show that $\kappa$ is preserved?
