22 votes

What notable theorems cannot be automatically proven without choice using Shoenfield absoluteness?

$\text{ZF}+ \text{AC}_{\omega}$ is not $\Sigma^1_4$-conservative over ZF and ZF + DC is not $\Sigma^1_4$-conservative over $\text{ZF}+ \text{AC}_{\omega}.$ An example of the former: the sentence $\...
Elliot Glazer's user avatar
13 votes
Accepted

Is "All hyperreal fields $C(\mathbb{R})/M$ are isomorphic" independent of ZFC+$\lnot$CH?

In On ultra powers of Boolean algebras (Topology Proceedings 9 (1984) 269-291) Alan Dow proved (Corollary 2.3) that $\neg\mathsf{CH}$ implies there are two fields of the form $C(\mathbb{N})/M$ that ...
KP Hart's user avatar
  • 9,795
11 votes

What notable theorems cannot be automatically proven without choice using Shoenfield absoluteness?

This is sort of an anti-answer, which I've accordingly made CW, but here goes: Whether $\mathsf{ZFC}$ is projectively conservative over $\mathsf{ZF}$ seems open; see Joel's answer from a while ago (...
11 votes
Accepted

How much determinacy do you need for second order arithmetic to be as strong as ZFC?

Because ZFC proves soundness of $\text{Z}_2$, no consistent finite extension of $\text{Z}_2$ proves all second order arithmetic statements that are provable in ZFC (for example, the statement "...
Dmytro Taranovsky's user avatar
10 votes

Set-theoretical reverse mathematics of the reals

TL;DR: A most basic property of $\mathbb{R}$ is that it is not countable, which is surprisingly hard to prove (namely far beyond the Big Five you mention), as explored in [1, 2, 3]. The longer version....
Sam Sanders's user avatar
  • 3,901
7 votes
Accepted

Strength of Borel determinacy

I don't know why you would want to work with $\mathrm{ZC}^{-}$, this is not a theory I would recommend to do math in. But as long as you only care about second order number theory, there is really no ...
Andreas Lietz's user avatar
6 votes
Accepted

Proving finiteness in Reverse Mathematics

Here's a proof that $\mathsf{ACA}_0$ suffices for the analogous statement over $2^\mathbb{N}$ instead of $\mathbb{R}$, where codes for closed sets are viewed as subtrees of $2^{<\mathbb{N}}$; it's ...
Noah Schweber's user avatar
6 votes

Trading Choice for Comprehension (or Replacement)

Most of the examples I know can be found in [1,2] and are joint work with Dag Normann. The prettiest examples we have are perhaps the following: Let RCA$_0^\omega$ be Kohlenbach's base theory of RM ...
Sam Sanders's user avatar
  • 3,901
6 votes

Trading Choice for Comprehension (or Replacement)

In second-order number theory, one typically presumes induction on the numbers for the classes of numbers that are available. And so comprehension gives you more classes, hence more induction, but ...
Joel David Hamkins's user avatar
6 votes
Accepted

Proof of global Peano existence theorem in ZF?

First of all, as Holo mentioned in the comments, it's already known that the pure existential statement of the Peano existence theorem can be shown in $\mathsf{WKL}_0$, which is significantly weaker ...
James Hanson's user avatar
  • 10.3k
6 votes
Accepted

How much of second-order arithmetic do you need for $\mathbf{\Sigma}^1_1$-determinacy to give you countable transitive models of $\mathsf{ZFC}$?

$\mathsf{RCA}_0 + \mathbf{\Sigma}^1_1\text{-Det}$ suffices to get sharps for all reals (and thus ctm of ZFC and more). With boldface determinacy principles, we can bootstrap the background theory. $\...
Dmytro Taranovsky's user avatar
4 votes

Kleene normal form theorem for r.e. relations proven in arithmetical theories

The usual formal systems in which one can carry out basic recursion-theoretic constructions and theorems such as the ones you are asking about are $\mathrm{I}\Sigma_1$ (a fragment of $\mathrm{PA}$ in ...
Ali Enayat's user avatar
3 votes

Did Gödel prove that the Ramified Theory of Types collapses at $\omega_1$?

I realize this is an old question, but in case this is still of interest: if I correctly understand that you are talking about the ramified analytical hierarchy, namely the one in which each next ...
Gro-Tsen's user avatar
  • 29.8k

Only top scored, non community-wiki answers of a minimum length are eligible