**5**

votes

**1**answer

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

**11**

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

**9**

votes

**0**answers

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

**8**

votes

**0**answers

359 views

### What is known about the reverse mathematics of algebraic number fields?

I know work on the reverse mathematics of countable algebraic field extensions including Galois theory, notably including Dorais, Hirst, and Shafer http://arxiv.org/pdf/1209.4944v2.pdf. But algebraic ...

**7**

votes

**0**answers

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

**7**

votes

**0**answers

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

**7**

votes

**0**answers

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

**3**

votes

**0**answers

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

**2**

votes

**0**answers

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

**1**

vote

**0**answers

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

**0**

votes

**0**answers

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