>Let GCH stand for the generalized continuum hypothesis.No need to consider the generalized one for you question, but okay.
>In ZFC, is the proposition "GCH or not GCH" true?Yes, because the logic underlying ZFC typically adopts the law of excluded middle, which makes "P or not(P) true for any P. (The axiom of regularity in its standard form, as well as the axiom of choice, both also imply the law for all propositions about sets, although there are weaker alternatives.)
>so intuitively it's neither true nor falseIt's not provable in the formal framework of ZFC. It's not provable because the ZFC axioms aren't restrictive enough and, in turn, there are classes U of sets that fulfill ZFC while provably not fulfilling (G)CH.
ZFC is just one of many set theories and no strong set theory can be categorical in the sense that there's only one model
https://en.wikipedia.org/wiki/Categorical_theoryThe truth of (G)CH is just not captured by that particular theory - don't overstate that.
>But wouldn't the proposition being false contradict LEM?It's not false in ZFC, so what do you mean? Again, the unprovability is w.r.t. ZFC.
You may as well add G(CH) as an axiom to ZFC.
>neither GCH nor "not GCH" is true, so the proposition "not GCH and not not GCH" would be trueGCH is not provable (provably true) in ZFC. This doesn't mean not GCH" is provable:
The unprovability of those statements A is not established by showing that are absurd (i.e. it's not like "not A" is proven). Instead, one looks at different miniature models (call em M1 and M2) of ZFC that, respectively, fulfill and not fulfil A (while fulfilling all ZFC-axioms). As a result, if you were to prove or disprove A (disprove, say), then one of the models (M1, say) would have lied to you - which would mean ZFC is inconsistent.
The issue is, again, that ZFC doesn't actually characterize sets to the point.