**16**

votes

**2**answers

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

**10**

votes

**3**answers

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

**4**

votes

**2**answers

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

**1**

vote

**0**answers

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

**8**

votes

**2**answers

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

**19**

votes

**2**answers

989 views

### Reverse mathematics of (co)homology?

Background
Exercise 2.1.16b in Hartshorne (homework!) asks you to prove that if $0 \rightarrow F \rightarrow G \rightarrow H \rightarrow 0$ is an exact sequence of sheaves, and F is flasque, then $0 ...

**5**

votes

**1**answer

336 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

**2**answers

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