Here is a proof of $\Sigma^2_1$ absolulteness. arxiv.org/abs/1005.4193 Farah has another paper show this using a saturated ideal instead of the extender algebra: mathscinet.ams.org/mathscinet-getitem?mr=2322360

@AndrejBauer About your example of the homotopical circle, I am pushed to ask, what do you mean by “all”? What do you mean by “map”, and is it synonymous with “function”? We clearly do different kinds of math, but this example doesn’t seem to jive with “classical” or “ordinary” math from my humble perspective.

@AndrejBauer Sorry for the naive question, but aren't you just forgetting to specify the topology in the set-theoretic construction of the circle? You can't ask about homeomorphisms regarding a bare collection of points.

I had a thought on this. What if at each stage you add a stationary set that is almost contained in every set from some measure on κ? If κ remains strongly compact, then the nonstationary ideal restricted to this set can be extended to a measure in the extension. Then repeat. At limit stages try to show that the special stationary sets you add at each stage have stationary intersection. Starting from an indestructible supercompact, I think this can be done with iterated Levy collapses and the limit stage claim should hold at small cofinalities. I’m not sure if this helps with your goal.

Let me see if I understand correctly. It looks like we can give a more direct argument and skip the topological considerations. Just define the ideal $I$ as in your last line, or alternatively, against any countable sequence $u_n$ such that $u_n$ is a uniform ultrafilter on $\omega_1$ concentrating on $X_n$, where the $X_n$ form a partition of $\omega_1$. The we can just map $[A]_I \mapsto [\{ n : A \in u_n \} ]_{\mathrm{fin}}$ and verify directly that this is a boolean isomorphism. Or am I missing some subtlety?

@ZuhairAl-Johar Yes. Let $\phi$ be the equality relation. For all collections $F$ of pairwise disjoint sets, replace each member $f \in F$ with $f \times F$ to meet the cardinality requirement. A choice function for this family gets a choice function for the original one.

@WillBrian I gave a sketch of the proof in our seminar recently. ucloud.univie.ac.at/index.php/s/f89ENYQLkdg4BNo

What about mathematical phone calls??

A set theory with Choice that permits incomparable cardinalities just seems to be missing an axiom.