# 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).

116 questions
Filter by
Sorted by
Tagged with
324 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-...
221 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 ...
153 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$...
218 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 ...
210 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 ...
208 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 ...
492 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 ...
369 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 ...
174 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 ...
362 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 ...
1k 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 ...
172 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 ...
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"...
293 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"...
157 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. ...
426 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 ...
428 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 ...
380 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 ...
416 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 ...
459 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 ...
120 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 ...
303 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 ...
258 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 ...
158 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 ...
87 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$. ...
### 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 ...