I'm going to ask a quite vague question, since the borderline between theoretical computer science and math is not always easy to distinguish.
QUESTION: Are you aware of any interesting result in CS which is either independent of ZFC (i.e. standard set theory), or that was originally proven in ZFC (+ some other axiom) and only later proven in ZFC alorne?
I'm asking because I'm close to finish my PhD thesis, and my main result (the determinacy of a class of games which are used to give "game semantics" to a probabilistic modal $\mu$-calculus) is at the moment proven in ZFC extended with other Axioms (namely the negation of the Continuum hypothesis $\neg CH $ and, Martin's Axiom $MA$).
So the setting is clearly Computer Science (the modal $\mu$-calculus is a temporal logic, and I'm extending it to work with probabilistic systems).
I would like to cite in my thesis other examples (if you are aware of any) of this kind.
Thank you in advance,