# Tagged Questions

The general enterprise of calibrating the strength of classical mathematical theorems in terms of the axioms, typically of set existence, needed to prove them; originated in its modern form in the 1970s by H. Friedman and S. G. Simpson (see R.A. Shore, "Reverse Mathematics: The Playground of Logic", ...

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 ...
785 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 ...
463 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 ...
879 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 ...
144 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. ...
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 ...
1k views

445 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 ...
### 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 ...
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.)