# Tagged Questions

**5**

votes

**1**answer

106 views

### Attribution of an equivalence of the existence of omega-models of RCA0

There are many well-known equivalences in reverse mathematics between statements of the form "Every set is contained a countable coded $\omega$-model of $T$" and $S$, where $S, T$ are subsystems of ...

**4**

votes

**2**answers

353 views

### Reverse Math of High Sets?

Is there a standard principle in reverse math that is known to be equivalent (over $RCA_0$) to the existence of a set of high (Turing) degree? I'm interested in the general case, but would be happy to ...

**3**

votes

**0**answers

120 views

### Why is adopting Russell's Axiom of Reducibility as strong as eliminating the Ramified Hierarchy?

In order to respond to concerns of impredicativity, Bertrand Russell developed a system of ramified second-order logic, which is like regular second-order logic except the comprehension schema is ...

**7**

votes

**0**answers

270 views

### “Hard” separation results in reverse mathematics (or similar)

This is a fairly broad question. In particular, I specify 5 questions (Q1, Q2.1, Q2.2, Q3, Q4) which for me all fall under one umbrella. Since this is unreasonably broad, I'm really interested in an ...

**6**

votes

**1**answer

86 views

### Is 0' of PA degree relative to a non-low set?

Definitions:
A set $X$ is of PA degree relative to a set $Y$ if every infinite $Y$-computable binary tree has an infinite $X$-computable path.
A set $X$ is low if $X'$ is computable from ...

**10**

votes

**1**answer

273 views

### Harvey Friedman's strict reverse mathematics vs. Cook-Nguyen's V$^0$

Harvey Friedman posted several manuscripts [1] proposing a program for "strict" reverse mathematics, in the sense that the base theory should be mathematically natural and coding-free.
In them he ...

**0**

votes

**0**answers

97 views

### What references cover finitary systems of Ramified Analysis with transfinite levels?

The ramified theory of types, invented by Bertrand Russell, is a way of dealing with impredicativity by breaking the comprehension schema of second-order logic into levels. The comprehension schema ...

**1**

vote

**0**answers

191 views

### What is the role of the (formalized) omega rule in Ramified Analysis?

In the 1960's, Feferman and Schutte did groundbreaking proof-theoretic work to find out the strength of predicative systems of second-order arithmetic. They used the ramified theory of types, a ...

**3**

votes

**2**answers

216 views

### What is the proof-theoretic ordinal of Hyperarithmetical Comprehension?

As I discuss in my answer here, it seems to me that Solomon Feferman shows, on pages 10-11 of his seminal 1964 paper "Systems of Predicative Analysis", that if you consider predicative second-order ...

**4**

votes

**2**answers

337 views

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

Second-Order Arithmetic is considered impredicative, because the comprehension scheme allows formulas with bound second-order variables that range over all sets of natural numbers, including the set ...

**7**

votes

**0**answers

289 views

### What is known of the reverse math of Riemann-Roch?

I hope this is not too trivial, but I think this may be well known to someone (not me).

**3**

votes

**0**answers

342 views

### Is there a notion of “predicative given the real numbers”?

A definition is called impredicative if it involves quantification over a domain that contains the thing being defined. For instance, if you define hereditary property to be a property which applies ...

**5**

votes

**2**answers

242 views

### Does the Feferman-Schutte analysis give a precise characterization of Predicative Second-Order Arithmetic?

A definition is called impredicative if it involves quantification over a domain that contains the thing being defined. For instance, if you define hereditary property to be a property which applies ...

**4**

votes

**1**answer

182 views

### Who first proved there's an $\omega$-model of $\mathsf{WKL}_0$ in which all sets are low?

I am trying to pin down: who first proved that $\mathsf{WKL}_0$ has an $\omega$-model in which every set is of low degree? As shown in Simpson's Subsystems of Second Order Arithmetic (Theorem ...

**12**

votes

**1**answer

654 views

### Reverse mathematics of Hilbert's Theorem 90

What is known, and what is published, on the reverse mathematics of the nest of results called Hilbert's Theorem 90?

**5**

votes

**6**answers

215 views

### Strength of Bishop style constructive mathematics vs $\mathsf{RCA}_0$

This question came out of this other MO question of mine. My question is
Is there a formal comparison between $\mathsf{RCA}_0$ and $\mathsf{BISH}$ (Bishop style constructive mathematics as used ...

**16**

votes

**2**answers

712 views

### Prospects for reverse mathematics in Homotopy Type Theory

Reverse mathematics, as I mean here, is the study of which theorems/axioms can be used to prove other theorems/axioms over a weak base theory. Examples include
Subsystems of Second Order Arithmetic ...

**8**

votes

**2**answers

673 views

### Sperner's lemma and Tucker's lemma

In their article "A Borsuk-Ulam Equivalent that Directly Implies Sperner's Lemma" (American Mathematical Monthly, April 2013), Nyman and Su write "[W]e are unaware of a direct proof that Tucker's ...

**23**

votes

**4**answers

1k views

### In what rigorous sense are Sperner's Lemma and the Brouwer Fixed Point Theorem equivalent?

I understand that one can give a proof of each of these propositions assuming the truth of the other. But this seems a bit squishy to me, since there is a trivial sense in which any two true theorems ...

**5**

votes

**1**answer

213 views

### Is the equivalence between a $\Sigma^0_1$ and a $\Pi^0_1$ formula defining the same recursive set provable in a sufficiently strong arithmetic ?

Let $A$ be a recursive set. $A$ is recursively enumerable, so $A$ may be defined by a $\Sigma^0_1$ formula, i.e. by $\exists \overrightarrow{a} \phi (\overrightarrow{a}, n)$, where $\phi$ contains no ...

**5**

votes

**1**answer

324 views

### First order consequence of a combinatorial principle

(Base theory $RCA_0$)The principle says there exists a function g such that g dominates any X-recursive function for any X in the model.
i.e. For any $f\le_T X$, $\exists b\in M$ such that ...

**8**

votes

**1**answer

346 views

### Weakest choice principle required for Robertson-Seymour Graph Minor Theorem?

The main Robertson-Seymour Theorem states that finite graphs form a well-quasi-ordering under the graph minor relation. In other words, in every infinite set of finite graphs, there exist two graphs ...

**9**

votes

**2**answers

375 views

### Reverse mathematics below RCA

I'm sure this is a fairly basic question, but I can't seem to find a solid answer:
My primary question is: Is there a reasonably nice subsystem of second-order arithmetic corresponding essentially to ...

**2**

votes

**3**answers

317 views

### Indices of r.e. sets

The last part of the paper Located Sets and Reverse Mathematics [Journal of Symbolic Logic 65 (1999), 1451–1480] by Giusto and Simpson involves a proof as follows:
Given $A$ an effectively ...

**9**

votes

**1**answer

381 views

### New research on coding in reverse mathematics?

Coding is obviously a fundamental tool in reverse mathematics, and practitioners take care to both demonstrate the correctness of their coding mechanisms and point out their limitations. Harvey ...

**4**

votes

**2**answers

249 views

### About the well ordering of finite sequences of numbers

We order $\mathbb{N}^{<\mathbb{N}}$ as following: if $|\sigma| < |\tau|$ then $\sigma < \tau$; if they are of same length then they are ordered lexicographically. It is provable over ...

**7**

votes

**1**answer

389 views

### What is the status of Cantor-Schroder-Bernstein in Reverse Math?

I'd like to know which of the set theories in SOSOA prove what versions of Cantor-Schroder-Bernstein? For my own purposes I can use arbitrarily high quantifier complexity, but I wonder how little ...

**8**

votes

**1**answer

201 views

### Strength of $\Delta_1^0$ subset of $2^\mathbb{N}$ as finite union of specific basic open sets.

This question is to find the Reverse Mathematical strength of writing $\Delta_1^0$ (clopen) subset of $2^\mathbb{N}$ as a finite union $\bigcup_{\sigma \in F} [|\sigma|]$ where $F \subset ...

**9**

votes

**2**answers

379 views

### Z_2 versus second-order PA

These days, Peano Arithmetic ($PA$) refers to the first-order version of the axioms, where induction is only over formulas referring to natural number variables. Peano's original version of the ...

**1**

vote

**3**answers

479 views

### Applicability of Deduction theorem to Primitive recursive arithmetic [closed]

Hello. I already asked the question here. The main point is that I tried to prove in Primitive recursive arithmetic (PRA) the totality of the Ackerman function, and I found, that the single thing ...

**1**

vote

**2**answers

282 views

### How do you restrict the induction axiom in second (or higher) order logic?

Dear all,
I am interested in reverse mathematics. The theory is that most of mathematics can be expressed and proven in ACA0, that is second order logic, with the induction axiom restricted.
...

**2**

votes

**0**answers

203 views

### Non-Computational classical subterms

Assume we have a proof term of the form $(a^{A\rightarrow^c B\rightarrow^{nc} C}b^Ac^B)^C$, where $c$ is classical (that is, contains free instances of duplex negatio affirmat). The extracted term ...

**6**

votes

**2**answers

684 views

### reverse mathematics strength of “Lipschitz functions are somewhere differentiable”

What is the reverse mathematics strength of
"For all Lipschitz functions $\; f : \mathbb{R} \to \mathbb{R} \;$, $\;$ there exists a real number $x$ such that $f$ is differentiable at $x$." ?
...

**4**

votes

**3**answers

694 views

### The Reverse Mathematics of writing a set as a union?

To be more precise, a countable collection of sets $(S_n)_{n \in \mathbb{N}}$ is encoded as the row of some given set $S$, i.e. $S_n = S^{[n]}$. Futhermore, for any function from $\mathbb{N} ...

**8**

votes

**3**answers

568 views

### truth vs. provability for ordered fields

In Propositions equivalent to the completeness of the real numbers I started by asking "Can anyone point me to a reasonably comprehensive article (or book chapter) explaining which basic theorems of ...

**0**

votes

**1**answer

642 views

### Do we need more than the periods? [closed]

Reading this question, and the Wikipedia page on reverse mathematics, I wonder whether one needs more than the subfield $\mathcal{P} \subset \mathbb{C}$ of periods for applied mathematics, or indeed ...

**13**

votes

**2**answers

1k views

### Propositions equivalent to the completeness of the real numbers

Can anyone point me to a reasonably comprehensive article (or book chapter) explaining which basic theorems of calculus are equivalent to the completeness axiom of the reals and which ones aren't?
...

**11**

votes

**1**answer

524 views

### Complementation of $\omega$-regular languages in reverse mathematics

Does anyone know where Büchi's theorem that $\omega$-regular languages are closed under complementation fits into the reverse-mathematics classification scheme? That is, is it equivalent over ...

**12**

votes

**5**answers

1k views

### Consistency strength needed for applied mathematics

Given that we can never proof the consistency of a theory for the foundations of mathematics in a weaker system, one could seriously doubt whether any of the commonly used foundational frameworks (ZFC ...

**8**

votes

**4**answers

1k views

### Is finitism an extreme form of constructivism?

I hope this question is not too soft for MO.
The Wikipedia says about finitism that it is an extreme form of constructivism. See http://en.wikipedia.org/wiki/Finitism. I doubt that this is correct.
...

**10**

votes

**0**answers

1k views

### Reverse mathematics strength of identically zero polynomials are the zero polynomial

According to wikipedia, the statement "every polynomial over a countable field that is not the zero polynomial has only finitely many roots" is equivalent to RCA0 over RCA0* (which is called ERCA-0 in ...

**2**

votes

**1**answer

218 views

### Proving boundedness of continuous images of [0,1] in WKL0

I've been reading about reverse mathematics (mostly on wikipedia), and I had been thinking that I understood how to prove the equivalences to WKL0 and ACA0 mentioned in the its article. However, I ...

**1**

vote

**4**answers

831 views

### Can transfinite induction be defined as axiom scheme in FOL on bin-tree structures?

Transfinite induction requires a second order induction hypothesis. So, that can not be defined as axiom scheme in FOL.
However, if I look to Goodstein's theorem en the Hydra games, then they have to ...

**5**

votes

**2**answers

545 views

### Weakest subsystems of second order arithmetic for mathematical logic

It is known that to prove completeness of first-order logic for countable languages WKL0 is enough. But, is it the weakest subsystem where one can prove it?
What about the incompleteness theorems? Is ...

**1**

vote

**2**answers

817 views

### Can Goodstein's theorem been proven with first order PA + Constructive Omega Rule?

I am trying to understand transfinite induction and Gentzen's theories.
But I was wondering, if there is any connection with the Constructive Omega Rule (COR).
With COR I mean that if you can proof:
...

**5**

votes

**3**answers

1k views

### What is the reverse mathematics of first-order logic and propositional logic?

Suppose one tries to formalize first-order logic. How much "strength" is required to do this?
Strength can mean in various senses:
The fragment of ZFC needed to codify first-order logic.
Which ...

**10**

votes

**3**answers

711 views

### Reducing ACA₀ proof to First Order PA

According to the Wikipedia ACA0 is a conservative extension of First Order logic + PA.
http://en.wikipedia.org/wiki/Reverse_Mathematics
First of all I have a few questions about the proof:
a - What ...