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 $\...
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 ...
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 (...
Community wiki
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 "...
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....
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 ...
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 ...
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 ...
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 ...
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 ...
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. $\...
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 ...
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 ...
Only top scored, non community-wiki answers of a minimum length are eligible
Related Tags
reverse-math × 166lo.logic × 134
computability-theory × 39
proof-theory × 26
set-theory × 23
theories-of-arithmetic × 22
reference-request × 18
constructive-mathematics × 14
model-theory × 10
descriptive-set-theory × 10
foundations × 9
axiom-of-choice × 7
soft-question × 5
nonstandard-analysis × 5
nt.number-theory × 4
co.combinatorics × 4
real-analysis × 4
gn.general-topology × 4
computational-complexity × 4
mathematical-philosophy × 4
metamathematics × 4
ordinal-analysis × 4
large-cardinals × 3
ac.commutative-algebra × 2
ca.classical-analysis-and-odes × 2