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

**10**

votes

**1**answer

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

**4**

votes

**2**answers

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

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

**3**

votes

**0**answers

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

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

**7**

votes

**0**answers

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

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

**0**answers

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

**6**

votes

**1**answer

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

**7**

votes

**0**answers

278 views

### Fragments of Morse—Kelley set theory

Morse—Kelley set theory (hereafter MK) is the impredicative counterpart of von Neumann—Bernays—Gödel set theory (NBG), where formulas containing class quantifiers are permitted in the comprehension ...

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

**3**

votes

**2**answers

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

**5**

votes

**0**answers

96 views

### Strength of claims about extensions of partial preorders and orders to linear ones

Consider these two axioms:
Every partial order extends to a linear order.
Every partial preorder (reflexive and transitive relation) extends to a linear preorder while preserving strict orderings: ...

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

**4**

votes

**4**answers

386 views

### Strength of some claims about finitely additive measures on infinite sets?

Assume ZF. Consider the claim:
(1) For any infinite set $\Omega$, there is a finitely additive probability measure $\mu:2^\Omega\to[0,1]$ with $\mu(A) = 0$ whenever $|A|<|\Omega|$.
Then (1) is ...

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

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

**2**answers

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

**3**

votes

**1**answer

184 views

### Reverse mathematics, Ramsey theorem and mass problem

If we look at reverse mathematics statements as mass problems, considering the class of solutions of an instance, it is known that Weak König's lemma has a maximal instance in the sense that there is ...

**16**

votes

**2**answers

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

**4**

votes

**1**answer

183 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

657 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?

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

**5**

votes

**6**answers

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

**5**

votes

**1**answer

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

**4**

votes

**1**answer

98 views

### About infinite subset of halting probability and 1-random set

Let $\Omega$ be the halting probability (see (http://en.wikipedia.org/wiki/Chaitin's_constant) and R. Downey, and D. Hirschfeldt (2010), Algorithmic Randomness and Complexity for reference). If A is ...

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

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

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

**2**

votes

**1**answer

201 views

### $\Sigma_1^0-COH$?

In reverse mathematics, $COH$ is a statement that there is a cohesive set for any uniform array of sets. Here uniform array of sets means that there exists a set $B$ such that $x\in B_e ...

**0**

votes

**0**answers

269 views

### Definitions for Oddness

In the thread Even Xor Odd Infinities I defined odd models of Modular Arithmetic (MA) as models satisfying the axioms of MA and two first order statements. Even XOR Odd Infinities?
$O1) \forall x(x=0 ...

**7**

votes

**5**answers

843 views

### Understanding the nature and structure of proofs; Reverse Mathematics and Proof Theory. Prerequisites? Good introductory texts?

I'm still studying maths at undergraduate level, but intend to continue exploring topics in pure maths after I have graduated, so am thinking already about what directions I'd like to persue now, (as ...

**4**

votes

**2**answers

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

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

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

**11**

votes

**1**answer

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

**2**

votes

**0**answers

204 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

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

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

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

**1**

vote

**4**answers

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

**10**

votes

**3**answers

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

**3**

votes

**1**answer

625 views

### Soundness Theorem in reverse mathematics

STPL := soundness theorem for predicate logic
(see this)
When trying to figure out the strength of the STPL in reverse mathematics, I managed to convince myself of the following:
a) ACA0 has a ...