First, let me remark that the particular way that you've posed the question has several problematic issues of formalization. One issue, noted by François, Andres and Andreas, is that it doesn't make sense to speak about proving an assertion with an ordinal parameter (one would instead want to speak of definitions of particular ordinals). Another issue is that for all we know, we may be living in a universe with ZFC + $\neg\text{Con}(\text{ZFC})$, and in this universe everything is provable, so even if we are able to resolve the first issue nevertheless the sets $S$ and $S'$ will be empty, since everything is provable.
So let me propose a more semantic, alternative version of the question, which to my of thinking gets at the issue in which I believe you are interested.
Question. If $\alpha$ is an ordinal and the continuum $2^{\aleph_0}$ can be $\aleph_\alpha$ in a forcing extension of the universe, then can the continuum be $\aleph_\alpha$ in a forcing extension of the universe in which also the OPP holds?
The answer is yes, and so in this sense the OPP imposes no additional constraints on the value of the continuum. In this question and in the theorem below, I am speaking about possibly proper class forcing, and this is required, since if the OPP fails unboundedly often, it will require proper class forcing to force OPP again.
Theorem. If the universe $V$ satisifes ZFC, then for any ordinal $\alpha$, the following are equivalent:
- There is a forcing extension in which $2^\omega=\aleph_\alpha$.
- There is a forcing extension in which $2^\omega=\aleph_\alpha$ and the OPP holds.
- Either $\alpha$ is a successor ordinal or $\alpha$ has uncountable cofinality.
Proof. Clearly 2 implies 1, and 1 implies 3. Suppose 3 holds, and I argue for 2. Fix any ordinal $\alpha$ as in $3$. First, we may simply force the GCH by the canonical forcing of the GCH. This forcing (which may be a proper class), is countably closed and hence preserves the property of having uncountable cofinality. So $3$ still holds about $\alpha$ in the extension with GCH. We may now simply apply Easton's theorem, using an Easton function $E$ that takes $\aleph_0$ to the current $\aleph_\alpha$, and more generally which takes $\aleph_\beta$ to $\aleph_{\alpha+\beta+1}$. (But any strictly increasing Easton function will do, and there are many variations.) Note that $\alpha+\beta=\beta$ once $\alpha\cdot\omega\leq\beta$, and so this pattern is eventually the GCH pattern. By Easton's theorem, there is a further forcing extension in which $2^{\aleph_0}=\aleph_\alpha$ and the continuum function is given by $E$, which is strictly increasing, so the OPP holds. QED
In particular, for any ordinal $\alpha$ that you care to define, then you can provably force the continuum to become $\aleph_\alpha$ if and only if you can do so while also ensuring the OPP.
Notice that in the proof of the theorem, the value of $\aleph_\alpha$ may have changed, during the forcing of the GCH, since this will collapse cardinals if the GCH did not already hold. So there is another version of the question, which is about cardinals, rather than about ordinals. If we start with the GCH, then a similar conclusion can be made.
Theorem. If $V$ is a model of ZFC+GCH, then for any cardinal $\delta$ the following are equivalent:
- There is a forcing extension $V[G]$ in which the continuum is $\delta$.
- There is a forcing extension $V[G]$ in which the continuum is $\delta$ and the OPP holds.
- The cardinal $\delta$ has uncountable cofinality.
The proof is essentially the same as above. The nontrivial part is 3 implies 2, which can be achieved via Easton's theorem by using a strictly increasing Easton function $E$ with the property that $E(\aleph_0)=\aleph_\alpha$. There are many choices of such $E$, such as $E(\aleph_\beta)=\aleph_{\alpha+\beta+1}$, as above. Any such $E$ will ensure the right value for $2^{\aleph_0}$ and, because it is strictly increasing, will also achieve the OPP. In this case, since we started with the GCH, one requires only set-sized forcing.
By the way, there seems to be alternative terminology to refer to what you call the OPP. For example, in my paper, "Is the dream solution of the continuum hypothesis attainable?", I refer to the power set size axiom, denoted, PSA, and this is the same as what you call OPP. This axiom also appears in the MO question on reasonable-sounding statements that are independent of ZFC.
$\mathrm{ZFC}$
, as a subset of $\frak c$ in the following sense. From $\frak c$ eliminate any $\alpha$ for which there is a proof in$\mathrm{ZFC}$
that $\frak c$ cannot be $\aleph_\alpha$. What remains is $S$. This seems to me to be as definite a mathematical object as, say, the set of nonrecursive real numbers. $\endgroup$