Questions tagged [reverse-math]
The general enterprise of calibrating the strength of classical mathematical theorems in terms of the axioms, typically of set existence, needed to prove them; originated in its modern form in the 1970s by H. Friedman and S. G. Simpson (see R.A. Shore, "Reverse Mathematics: The Playground of Logic", 2010).
166
questions
17
votes
2
answers
918
views
Reverse mathematics of Cousin's lemma
This paper by Normann and Sanders apparently caused a stir in the reverse mathematics community when it came out a couple years ago. It says that Cousin's lemma, which is an extension of the Heine-...
- 1,117
12
votes
1
answer
456
views
How to understand the interface of the consistency strength hierarchy, reverse mathematics, and proof-theoretic ordinal analysis?
I am aware of three major "hierarchies" of mathematical theories, but I don't know how to relate these hierarchies to one another. Here are the hierarchies I have in mind:
Consistency strength. My ...
- 61.5k
2
votes
1
answer
181
views
Detecting comprehension topologically
This question basically follows this earlier question of mine but shifting from standard systems of nonstandard models of $PA$ to $\omega$-models of $RCA_0$. For $X$ a Turing ideal we get the map $c_X$...
- 19.1k
7
votes
1
answer
380
views
Every complex number has a square root via LLPO without weak countable choice
Is it possible to prove that every complex number has a square root using analytic LLPO, but avoiding Weak Countable Choice or Excluded Middle? Unique Choice is allowed.
(Analytic LLPO is the ...
- 4,843
1
vote
2
answers
259
views
The "higher topology" of countable Scott sets
Fix some computable bijection $b$ between $\omega$ and $2^{<\omega}$. For $r\in 2^\omega$, let $$[r]=\{f\in 2^\omega: \forall\sigma\prec f(b^{-1}(\sigma)\in r)\}$$ be the closed subset of Cantor ...
- 19.1k
7
votes
0
answers
307
views
$0^\#$ in weak theories vs large cardinals in $L$
To better understand the transition from large cardinal axioms consistent with the constructible universe $L$ to large cardinal axioms transcending $L$, I am looking for natural equiconsistencies ...
- 6,112
6
votes
2
answers
739
views
Uncountability of the real numbers from LLPO without countable choice
Does there exist a proof of the uncountability of the real numbers that uses analytic LLPO (the statement that any real number $x$ satisfies either $x \leq 0$ or $x \geq 0$) but avoids Excluded Middle ...
- 4,843
10
votes
1
answer
488
views
Examples of proofs using induction or recursion on a big recursive ordinal
There are many proofs use induction or recursion on $\omega$, or on an arbitary (may be uncountable) ordinal. Are there some good examples of proofs which use a big but computable ordinal?
The ...
- 475
5
votes
0
answers
237
views
An axiom that shows that the real numbers are weakly countable?
Is there a model of Intuitionistic Higher-Order Logic in which the following axiom is true?
Covering Axiom: Any true statement of the form $\forall x \in A, \exists y \in B, \phi(x,y)$ gives rise to ...
- 4,843
5
votes
1
answer
551
views
BISH: If a function is pointwise positive, is its infimum positive?
Let $f:[0,1] \to \mathbb R$ be a uniformly continuous function such that each value of $f(x)$ is greater than zero. Is its infimum greater than zero in BISH?
I believe that it is indeed the case if ...
- 4,843
13
votes
2
answers
2k
views
Why is weak Kőnig's lemma weaker than Kőnig's lemma?
Kőnig's lemma states that any finitely-branching tree with infinitely many nodes contains an infinite path. Weak Kőnig's lemma states the same thing about binary trees.
It's known that these are not ...
- 12.2k
4
votes
0
answers
252
views
Proof theory and subsystems of second-order arithmetic: in particular the reverse mathematics of Godel's system $T$
While doing some research on reverse mathematics, I came across the following document under the address, http://www.andrew.cmu.edu/user/avigad/Talks/survey1.pdf:
Proof theory and Subsystems of ...
- 6,024
20
votes
2
answers
2k
views
Is it possible to constructively prove that every quaternion has a square root?
Is it possible to constructively prove that every $q \in \mathbb H$ has some $r$ such that $r^2 = q$? The difficulty here is that $q$ might be a negative scalar, in which case there might be "too many"...
- 4,843
8
votes
1
answer
551
views
Proof-theoretic ordinals: inevitable consistency?
There are various different notions of the proof-theoretic ordinal of a theory; most of these are "notation-dependent" in that they're only nontrivial once we restrict attention to a class of "natural"...
- 19.1k
5
votes
1
answer
332
views
Why restrict to $\Sigma_1^0$ formulas in $RCA_0$ induction?
I recently asked this question over on math.se, warmly welcomed by crickets. I hope it's appropriate here.
I'm reading Stillwell's Reverse Mathematics, and the induction axiom was just introduced.
...
- 585
6
votes
2
answers
689
views
Cases where multiple induction steps are provably required
I am looking for references for theorems of the form:
1) Any proof of theorem $X$ requires $n$ applications of induction axioms
and especially
2) Any proof of theorem $X$ requires $n$ nested ...
- 335
14
votes
0
answers
595
views
Reverse Mathematics of Euclid's theorem
Euclid's theorem that there are infinitely many prime numbers has multiple proofs, ranging from Euclid's original theorem that constructs a new prime from a finite list of such, to Euler's proof that ...
- 33.9k
9
votes
1
answer
693
views
van der Waerden's theorem in Reverse Mathematics
What is known about weak systems of axiomata that allow one to prove van der Waerden's theorem?
van der Waerden's theorem can be used to show that there are infinitely many primes (see below). Is ...
- 93
13
votes
1
answer
580
views
reverse mathematics of the Lebesgue measurability of analytic sets
Can the fact that all analytic sets are Lebesgue measurable be proven in $Z_2$, or in some weak subsystem such as $\Pi^1_1\text{-CA}_0$? Conversely, can certain set existence axioms be derived from ...
- 2,090
5
votes
4
answers
1k
views
How can you formalize the metamathematics conventionally used to state Godel’s theorem?
Gödel’s incompleteness theorem states that for any sufficiently strong formal system $T$ there exists a statement $G$ such that if $T$ is consistent, then $G$ is true but not provable in $T$. But I’m ...
- 4,529
5
votes
0
answers
144
views
Does comprehension for formulas in the analytical hierarchy imply comprehension for all formulas in second-order arithmetic?
The proof that all formulas of second-order arithmetic are $\Pi^1_n$ for some $n$ (i.e. can be written with a bloc of second-order quantifiers followed by an arithmetical formula) uses the axiom of ...
- 2,090
11
votes
2
answers
423
views
Are all generalized Scott sets realized as generalized standard systems?
Below, I've focused on PA when lots of other theories would do. If replacing PA with a different theory leads to a more answerable question, feel free to do so.
The standard system of a nonstandard ...
- 19.1k
6
votes
1
answer
286
views
Am I counting quantifiers correctly?
I think this is right but I want to check. The theory $\mathsf{WKL}^*_0$ is conservative over EFA for $\Pi^0_2$ sentences. And the first order part of $\mathsf{WKL}^*_0$ is axiomatized by EFA plus ...
- 10.8k
3
votes
0
answers
257
views
Are there amenable groups without explicit Folner sets?
This is essentially a follow-up to this previous discussion on how, in the absence of choice, the "invariant mean" and "Folner set" characterizations of amenability are no longer equivalent. Recently ...
- 578
3
votes
1
answer
110
views
If one adds an inductive subset to a model of $ACA_0$, do we always get a new model of $ACA_0$?
Suppose $(M, \mathcal X) \models ACA_0$. Recall that a subset $A \subseteq M$ is $inductive$ over $M$ if $M$ satisfies all instances of induction in the expanded language with a predicate for $A$. ...
- 1,832
17
votes
1
answer
2k
views
What is known about the relationship between Fermat's last theorem and Peano Arithmetic?
As far as I know, whether Fermat's Last Theorem is provable in Peano Arithmetic is an open problem. What is known about this problem?
In particular, what is known about the arithmetic systems $PA + \...
- 5,821
4
votes
0
answers
165
views
A forcing which can build weird models of $\neg$ADS
There is a class of forcing notions I've been playing around with recently. They have a couple nice properties, and all have the same theme, but I've found them difficult to analyze beyond the basics. ...
- 19.1k
60
votes
8
answers
9k
views
What does it mean to suspect that two conjectures are logically equivalent?
Here's a familiar conversation:
Me: Do you think Conjecture A and Conjecture B are equivalent?
Friend: Yes, because I think they're both true.
Me: [eye roll] You know what I mean...
Does there ...
- 7,573
2
votes
0
answers
78
views
Is there a connection between the subsystems of second-order arithmetic and computational complexity?
The "big five subsystems of second-order arithmetic" in reverse arithmetic reveal the stratification of the structure of mathematics. What if any is the connection of these strata with complexity ...
user37691
5
votes
1
answer
290
views
A game with boldface strength
This is a problem which has been bothering me for a while now; it doesn't seem inherently too hard, but I haven't been able to make any real headway, so I'm putting it out in the open since at this ...
- 19.1k
3
votes
2
answers
738
views
Is any Cauchy sequence for completion of rational semicomputable?
For the definition of a semicomputable real, see An Introduction to Kolmogorov Complexity and its Applications by Li and Vitanyi (1997). In fact, it is not true that every Cauchy sequence for ...
- 3,000
6
votes
1
answer
271
views
Bounded-width Konig's lemma in reverse math
We define $\mathsf{BWKL}$ as follows:
Every infinite binary tree of bounded width has an infinite path.
This obviously follows from $\mathsf{WKL}$. Is this principle true in $\mathsf{RCA}_0$? If not, ...
- 256
7
votes
1
answer
329
views
Axiomatizations of arithmetical parts of theories
For common theories that talk about something more general than first-order arithmetic (e.g. set theories and subsystems of second-order arithmetic), are there nice axiomatizations of their arithmetic ...
- 2,090
1
vote
1
answer
315
views
How does $RCA_0$ achieve weak completeness?
Few days ago I asked about $WKL_0$ and the role of binary trees to provide for completeness for first order theories, and the question was nicely answered by Joel David Hamkins: Does $WKL_0$ plus CON(...
- 3,292
2
votes
1
answer
139
views
Does $WKL_0$ plus CON(PA+X) give a binary tree model of PA+X?
In the context of reverse mathematics $WKL_0$ is considered equivalent to Gödel's completeness theorem over $RCA_0$. Does this mean that e.g. $WKL_0$ plus the consistency statement CON(PA+X) gives a ...
- 3,292
3
votes
1
answer
372
views
Forcing in Second-Order Arithmetic
If I understand correctly, Stephen Simpson, in his book Subsystems of Second Order Arithmetic, deems second-order arithmetic as a two-sorted first-order theory. If this is correct, then it seems ...
- 6,024
95
votes
5
answers
8k
views
Is there a database for tracking the dependencies of mathematical theorems?
Given a proof for a result, one could denote the proof as a node on a graph, and then draw arrows to the node from axioms and previous results that the proof uses, and then draw arrows from the node ...
- 2,622
2
votes
1
answer
307
views
Is there a model of ZF+ACC where transfer fails for the definable hyperreals?
In 2003 Kanovei and Shelah constructed a definable hyperreal field. The ultrapower used exploits a fairly large index set so that it is clear that the usual proof of Los and transfer does not go ...
- 15.2k
3
votes
0
answers
168
views
Circular reasoning in proof of bounded comprehension
Theorems II.3.7 and II.3.9 in Simpson's Subsystems of Second-Order Arithmetic appear to be circular. Specifically, theorem II.3.7 seems to make implicit use of theorem II.3.9.
[Theorem II.3.9 is the ...
- 31
2
votes
1
answer
254
views
Transfer with minimal choice
Let FUF postulate the existence of a Free UltraFilter on $\mathbb{N}$ and ACC the axiom of countable choice. Consider the superstructure on $\mathbb{R}$ and its inclusion in the bounded ultrapower. ...
- 15.2k
12
votes
2
answers
467
views
Can noncomputable sets be distinguishable in $RCA_0$?
Say that a set $X\subseteq\omega$ is distinguishable if there is some Turing machine $\Phi_e$ which, when given two sets exactly one of which is $X$, can determine which set is $X$. Formally, $X$ is ...
- 19.1k
38
votes
2
answers
5k
views
Why is this new result such a big deal?
This popular article reports a recent result in reverse mathematics, showing that a certain theorem in Ramsey theory is provable from RCA$_0$, the base theory in SOSOA. Then there are a bunch of ...
- 381
5
votes
1
answer
406
views
Constructive compactness for countable models?
The compactness theorem for countable (Tarski?) models is equivalent to the weak König's lemma by a result of H. Friedman and others as noted here, in the context of classical logic. The weak König's ...
- 15.2k
1
vote
2
answers
286
views
Compactness for countable models?
How and where is it proved that WKL$_0$ proves the compactness theorem for countable models? (This is a follow-up to a comment of F. Dorais.)
- 15.2k
6
votes
1
answer
349
views
Are there first order theories of interest to an algebraist or at least a model theorist of large cardinal consistency strength?
I am wondering if there are some first order theories of algebraic structures or structures of interest to model theorists of large cardinal consistency strength or at least unexpectedly high ...
- 27.8k
4
votes
1
answer
322
views
Proving moduli of uniform continuity in RCA_0
Simpson's Subsystems of Second Order Arithmetic (pp. 134ff.) uses RCA$_0$ to prove various theorems of analysis for all continuous functions with a suitable modulus of uniform continuity. And he ...
- 10.8k
9
votes
1
answer
376
views
Proof-theoretic ordinals after liberalizing induction to $RCA_0$
This is kind of a follow-up to this question.
For a class $\Gamma$ of second-order formulas (here either $\Sigma_n^0$ or $\Sigma_n^1$), let $X\Gamma$ be a formal theory consisting of $RCA_0$ together ...
- 27.4k
4
votes
2
answers
201
views
What can be achieved by liberalizing induction for $RCA_0$?
$RCA_0$ has $\Delta_0$-comprehension and $\Sigma_1$ induction. Let $X\Sigma_{n}$ be $RCA_0$ plus $\Sigma_n$-induction and let $X\Sigma_{\omega}$-induction be $RCA_0$ plus the full induction schema.
...
- 3,292
6
votes
1
answer
175
views
Does $WKL_0$ provide more comprehension than $RCA_0$?
$WKL_0$ extends $RCA_0$ with the statement that any infinite subset of the infinite binary tree has an infinite branch. Does $WKL_0$ Prove that there are sets which are not proven to exist by the $\...
- 3,292
5
votes
1
answer
594
views
What are key $\Sigma^0_2$ or $\Pi^0_3$ theorems?
I am researching a logical system that is limited to $\Pi^0_2$ sentences and I am busy to prove that FOL + PA is a conservative extension of that system. Meaning that with $\Sigma^0_n$ sentences (that ...
- 1,659