# 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

**14**

votes

**1**answer

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

**8**

votes

**1**answer

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

**2**

votes

**1**answer

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$...

**5**

votes

**1**answer

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

**1**

vote

**2**answers

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

**6**

votes

**0**answers

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

**5**

votes

**2**answers

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

**10**

votes

**1**answer

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

**4**

votes

**0**answers

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

**5**

votes

**1**answer

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

**13**

votes

**2**answers

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

**3**

votes

**0**answers

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

**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**

votes

**1**answer

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"...

**4**

votes

**1**answer

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

**6**

votes

**2**answers

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

**10**

votes

**0**answers

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

**7**

votes

**1**answer

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

**13**

votes

**1**answer

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

**3**

votes

**3**answers

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

**4**

votes

**0**answers

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

**11**

votes

**2**answers

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

**6**

votes

**1**answer

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

**3**

votes

**0**answers

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

**3**

votes

**1**answer

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$. ...

**12**

votes

**1**answer

1k 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 + \...

**4**

votes

**0**answers

152 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. ...

**54**

votes

**8**answers

7k 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 ...

**2**

votes

**0**answers

70 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 ...

**5**

votes

**1**answer

242 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 ...

**2**

votes

**2**answers

527 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 ...

**6**

votes

**1**answer

217 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, ...

**7**

votes

**1**answer

245 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 ...

**1**

vote

**1**answer

210 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(...

**2**

votes

**1**answer

104 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 ...

**1**

vote

**1**answer

220 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 ...

**88**

votes

**5**answers

6k 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**

votes

**1**answer

250 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 ...

**2**

votes

**0**answers

146 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 ...

**2**

votes

**1**answer

203 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. ...

**12**

votes

**2**answers

374 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 ...

**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 ...

**5**

votes

**1**answer

361 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 ...

**2**

votes

**2**answers

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

**6**

votes

**1**answer

320 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 ...

**4**

votes

**1**answer

153 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 ...

**9**

votes

**1**answer

347 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 ...

**4**

votes

**2**answers

176 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.
...

**6**

votes

**1**answer

140 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 $\...

**5**

votes

**1**answer

473 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 ...