Solomon Feferman (1928 – 2016) hold that statements of arithmetic are definite, while "higher-order" notions (such as the set of all subsets of $\mathbb N$) are vague, and questions about them might not be objectively answered. He proposed a formal system of mathematics (or, if you will, of set theory) that allowed to apply the law of excluded middle to arithmetical statements, but not to statements which included vague concepts. That is, in the definite realm we may reason in classical logic, while in the less definite realm one only can use intuitionistic logic (let me call this "semi-intuitionistic"). See the thread Is platonism regarding arithmetic consistent with the multiverse view in set theory? for a discussion on that view.

In his paper Is the continuum hypothesis a definite mathematical problem?, Feferman has a section called "3. A proposed logical framework for what’s definite (and what’s not)". There he discusses formal systems that are "semi-intuitionistic" in the sense that these systems somehow distinguish between "definite" and "vague" statements and depending on which of these two types a statement has, one might apply the law of excluded middle to it or not.

In this present question I don't want to fix a particular "semi-intuitionistic" formal systems, I just note that it is possible to formalize this idea.

*Question*. Is it possible that there are definite, arithmetical statements that are provable in classical logic + ZFC, but not in such a semi-intuitionistic version of set theory?

My motivation of this question are my philosophical thoughts on ZFC and my objection that there might be statements provable in ZFC, but for which this proof isn't satisfying in the sense that it applies classical logic to non-definite statements. In my opinion, these proofs should be treated with caution, since I don't believe in the definiteness of general set theoretic statements.

One may critise that my question is vague, for those of you who do, let me put my questions in other words:

*Are there any results known which demonstrate for a semi-intuitionstic formal system $K$ that there is a definite statement $s$ not provable in this systems, but which is provable in ZFC + classical logic?*