8
$\begingroup$

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?

Improve this question
$\endgroup$
1

1 Answer 1

Reset to default
9
$\begingroup$

There are no such statements $s$, at least not for a suitably formalized version of your question, using intuitionistic set theory with Peano arithmetic.

Suppose we have an arithmetical statement $\phi$, and $ZFC \vdash \phi$. By Shoenfield absoluteness, $ZF \vdash \phi$. Then by results of Friedman, $IZF \vdash \phi^{-}$, the double-negation translation of $\phi$. So $IZF + PA \vdash \phi$.

See Michael Beeson, Foundations of Constructive Mathematics (1985), chapter VIII.3. That chapter shows that this phenomenon is fairly robust to the choice of formalization.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Is seems to me that this justifies the use of LEM in the non-definite realm. $\endgroup$
    – Tastatur
    Commented Aug 13, 2016 at 13:43
  • 1
    $\begingroup$ I once heard that people discussed whether the proof of Wiles proving Fermat's last theorem relied on the Grothendieck universe axiom. Now I wonder: If we have that an arithmetical statement s is provable in ZFC + Grothendieck universe axiom, can we infer that s is provable in the semi-intuitionistic system? $\endgroup$
    – Tastatur
    Commented Aug 13, 2016 at 13:52

Not the answer you're looking for? Browse other questions tagged or ask your own question.