# Tagged Questions

**7**

votes

**2**answers

286 views

### Proof complexity of two directions of equivalency?

This question is not precise, but I believe has a precise formulation.
Consider a mathematical theorem which gives an equivalency between two conditions. As an extreme example:
\begin{theorem}
A ...

**8**

votes

**0**answers

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

**0**

votes

**0**answers

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

**1**

vote

**0**answers

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

**3**

votes

**2**answers

247 views

### What is the proof-theoretic ordinal of Hyperarithmetical Comprehension?

As I discuss in my answer here, it seems to me that Solomon Feferman shows, on pages 10-11 of his seminal 1964 paper "Systems of Predicative Analysis", that if you consider predicative second-order ...

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

**12**

votes

**1**answer

669 views

### Reverse mathematics of Hilbert's Theorem 90

What is known, and what is published, on the reverse mathematics of the nest of results called Hilbert's Theorem 90?

**5**

votes

**6**answers

231 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

248 views

### Is the equivalence between a $\Sigma^0_1$ and a $\Pi^0_1$ formula defining the same recursive set provable in a sufficiently strong arithmetic ?

Let $A$ be a recursive set. $A$ is recursively enumerable, so $A$ may be defined by a $\Sigma^0_1$ formula, i.e. by $\exists \overrightarrow{a} \phi (\overrightarrow{a}, n)$, where $\phi$ contains no ...

**9**

votes

**2**answers

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

**8**

votes

**5**answers

1k views

### Understanding the nature and structure of proofs; Reverse Mathematics and Proof Theory. Prerequisites? Good introductory texts?

I'm still studying maths at undergraduate level, but intend to continue exploring topics in pure maths after I have graduated, so am thinking already about what directions I'd like to persue now, (as ...

**1**

vote

**3**answers

503 views

### Applicability of Deduction theorem to Primitive recursive arithmetic [closed]

Hello. I already asked the question here. The main point is that I tried to prove in Primitive recursive arithmetic (PRA) the totality of the Ackerman function, and I found, that the single thing ...

**6**

votes

**1**answer

279 views

### Strength of Transfinite Induction on the Difference Hierarchy

I'm wondering if a particular theory of second order arithmetic has been studied or is known to be equivalent to some other theory.
Consider the formulas generated by $\Pi^1_1$ and $\Sigma^1_1$ ...

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