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

**8**

votes

**0**answers

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

**7**

votes

**0**answers

143 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

301 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

301 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

209 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

370 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

360 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

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

**0**

votes

**0**answers

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