Are there known statements in $V_{ω+ω}$ independent through forcing after $\mathrm{Col}(ω,<κ_1)*\mathrm{Col}(κ_1,<κ_2)*\mathrm{Col}(κ_2,<κ_3)*...$ where $κ_1<κ_2<κ_3<...$ are supercompact?
If no, what if we start with $\mathrm{Col}(ω_1,<κ_1)$ instead? If yes, can we get an independence in $V_{ω+2}$?
Notes:
- Note that the forcing is an iteration rather than a product.
- Extension: It is unclear how to best continue past $ω_ω$, but the simplest choice is to ignore singular cardinals, and collapse above the regular cardinals, using Easton support for the iteration.
- Other collapses: There are other collapsing notions besides $\mathrm{Col}$, and I will accept an answer for the symmetric generic collapse (it is natural; not sure if it is equivalent here since after collapsing $κ_n$, the next step absorbs $\mathrm{Add}(κ_n,1)$).
- Clarification: For this question, "independent through forcing" means that there is a generic extension $V[G]$ such that the truth depends on whether the collapse is performed in $V$ or in $V[G]$ (with $κ_1,κ_2,...$ still supercompact in $V[G]$, or using different supercompact cardinals). As supercompactness is not $Σ^V_2$, we allow class forcing with every set in $V[G]$ set-generic over $V$; or we could simply require $κ_1,κ_2,...$ to be supercompact up to the same inaccessible. Being consistently independent through forcing (with $V$ having enough supercompacts) also works for an answer. There is also the possibility that formally there are independent statements, but practically they are about as rare as arithmetical incompleteness of ZFC + supercompact.
Motivation
The set theoretical universe $V$ can be 'scrambled' by forcing. Large cardinal axioms offer symmetry, but mostly only at the scale of the large cardinals. Generic collapses can often unscramble the effects of forcing, perhaps giving us a precise approximation of the true $V$, and a natural canonical nonrestrictive theory of uncountable sets, without the pervasive incompleteness of ZFC.
The above iteration corresponds to first maximizing the reals up to a sufficiently closed and symmetric point, then proceeding with sets of reals, sets of sets of reals, and so on; and it is the simplest forcing implementing this maximization idea. After $\mathrm{Col}(ω,<\text{inaccessible})$, due to symmetry, $\mathrm{HOD}(ℝ)$ sets of reals are measurable, have Baire property, and perfect subset property. And $\mathrm{Col}(ω_n,<\text{inaccessible})$ gives certain symmetry properties for $\mathrm{OD}(\mathrm{Ord}^{ω_n})$ subsets of $P(ω_n)$.
I chose supercompactness as it is the level where the complexity of the large cardinal structure above $κ$ matches the complexity of $V$ above $κ$. A weak extender model for supercompactness must approximate $V$ (In search of Ultimate-L by Hugh Woodin). Moreover, there are indications (modulo iterability) that large cardinal axioms below supercompactness have canonical models with all reals $Δ^2_2$ in a countable ordinal, and presumably too weak to 'capture' third order arithmetic. Also, with just inaccessibles, I suspect the various square principles will be independent after the collapses even if supercompacts exist in $V$.
There are certain similarities between supercompactness and symmetry properties we want $ω_n$ to have; and consistency proofs of some forcing axioms (conjectured to be equiconsistent with supercompact) end up collapsing a supercompact to be $ω_2$. As for starting with $\mathrm{Col}(ω_1,<κ_1)$, the possibility is that large cardinal axioms themselves provide enough closure for countable sets, with natural forcing independences restricted to the uncountable.
It is also possible that some forcings leave traces that survive the generic collapses. A stationary subset of $κ_n$ will remain stationary in the extension due to $κ_n\text{-c.c}$ of the collapse through $κ_n$, and $κ_n$-closure of the remainder, but with the supercompactness, I do not know whether we can exploit this.
