**17**

votes

**2**answers

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

**11**

votes

**3**answers

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

**7**

votes

**3**answers

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

**2**

votes

**0**answers

540 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

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

**4**

votes

**2**answers

140 views

### What can be achieved by liberalizing induction for $RCA_0$?

$RCA_0$ has $\Delta_0$-comprehension and $\Sigma_1$ induction. Let $X\Sigma_{n}$ be $RCA_0$ plus $\Sigma_n$-induction and let $X\Sigma_{\omega}$-induction be $RCA_0$ plus the full induction schema.
...

**29**

votes

**3**answers

3k views

### What is the reverse mathematical strength of the fundamental theorem of algebra?

Reverse mathematics (RM) is that area that tries to pin down exactly which axioms are necessary to prove theorems, given some weak base theory. Harvey Friedman has pointed out several times (on the ...

**24**

votes

**3**answers

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

**9**

votes

**2**answers

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

**7**

votes

**7**answers

385 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

331 views

### What are key $\Sigma^0_2$ or $\Pi^0_3$ theorems?

I am researching a logical system that is limited to $\Pi^0_2$ sentences and I am busy to prove that FOL + PA is a conservative extension of that system. Meaning that with $\Sigma^0_n$ sentences (that ...

**5**

votes

**2**answers

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

**5**

votes

**1**answer

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

**2**

votes

**2**answers

184 views

### Compactness for countable models?

How and where is it proved that WKL$_0$ proves the compactness theorem for countable models? (This is a follow-up to a comment of F. Dorais.)