**23**

votes

**0**answers

869 views

### Godel on recursion-theoretic hierarchies

At the end of his excellent article, "The Emergence of Descriptive Set Theory" (http://math.bu.edu/people/aki/2.pdf), Kanamori writes:
"Another mathematical eternal return: Toward the end of his ...

**12**

votes

**0**answers

280 views

### How to measure the strength of Zermelo over bounded Zermelo?

Bounded Zermelo is Zermelo set theory with only bounded separation. It has the same strength as simple type theory or MacLane set theory or ETCS. It is a finitely axiomatized fragment of Zermelo, so ...

**9**

votes

**0**answers

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

**8**

votes

**0**answers

322 views

### What is known about the reverse mathematics of algebraic number fields?

I know work on the reverse mathematics of countable algebraic field extensions including Galois theory, notably including Dorais, Hirst, and Shafer http://arxiv.org/pdf/1209.4944v2.pdf. But algebraic ...

**8**

votes

**0**answers

321 views

### Can second order arithmetic make $\aleph_1^L$ countable?

Simpson's book Subsystems of Second Order Arithmetic shows $Z_2$ can interpret some fragments of ZF strong enough to give good theories of constructible sets and formalize statements like "there is a ...

**7**

votes

**0**answers

250 views

### Godel's second incompleteness theorem for non-r.e. theories

R. Jeroslow in this paper proves that a non-recursively enumerable theory whose set of theorems is $\Delta_2$-definable may prove consistency of itself
but it can not prove 2-consistency of itself.
...

**7**

votes

**0**answers

188 views

### When is a reduction not a reduction?

Every mathematician understands the concept of reducing a complicated problem to a simpler problem. "Without loss of generality, we may assume…" However, I've noticed that some kinds of ...

**6**

votes

**0**answers

129 views

### cut-elimination for infinitary logic

Takeuti (1987, 223) deduces a cut-elimination theorem for infinitary logic from the corresponding soundness-and-completeness theorems. However, is there a way to adapt the basic Gentzen-style ...

**4**

votes

**0**answers

78 views

### $n$th order arithmetic with predicates for orders

Two papers I have looked at lately axiomatize $n$-th order arithmetic in a single sorted language with predicates $Z_1,\dots,Z_n$ and axioms like $\forall x(Z_1(x)\vee\dots\vee Z_n(x))$ to say ...

**4**

votes

**0**answers

91 views

### Stabilization of recursive approximation in $PA^-+I\Sigma_1^0$

Over any model M of $PA^-+I\Sigma_1^0$. Suppose $A\in [T]$ where $T$ is a $\Delta_2^0$-tree and $A$ is one isolated path. Further, $A$ is regular, i.e. $\forall n A\upharpoonright n$ has a code in ...

**3**

votes

**0**answers

229 views

### The substitution theorem in first order logic (finitely many variables)

We consider the language ${\cal L}=\{\in\}$ with an arbitrary set of variables $V$. Specifically we define ${\bf P}(V)$ as the free algebra of type $\{\bot,\to\}\cup\{\forall x:x\in V\}$ (with the ...

**3**

votes

**0**answers

120 views

### Why the choice of pairing function in Subsystems of Second Order Arithmetic?

Simpson's book uses a pairing function $\langle i,j\rangle = (i+j)^2+j$. Is that choice of function simply unimportant, or does it have expository advantages over the Cantor pairing, or does it have ...

**2**

votes

**0**answers

71 views

### Seeking name for an order raising operator in Higher Order Arithmetic.

Any class $X$ of order $j$ in HOA is in bijection with the order $j+1$ class built up from singletons $\{x\}$ of natural numbers $x$ just the way that $X$ is built up from the numbers $x$. And of ...

**1**

vote

**0**answers

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

**1**

vote

**0**answers

167 views

### Has the Ramified Theory of Types been applied to Predicative Set Theories?

Questions of predicativity are well-studied in the context of arithmetic. We have a base theory, first-order Peano arithmetic. Some people, like Edward Nelson (in chapter 1 of his book) and Charles ...

**0**

votes

**0**answers

184 views

### subformula property (anchored proofs)

Hello,
I would like to ask for some explanation on some property of propositional sequent calculus.
The sequent calculus that I use here follows that of Stephen Cook, in "Logical Foundations of ...

**0**

votes

**0**answers

132 views

### Implications of complex solutions of Matiyasevich / Chaitin diophantine polynomials.

This is a shot in the dark: In twf:202, an isomorphism $T\cong T^{7}$ between binary trees $T$ and seven tuples of binary trees T^{7} is mentioned. The argument for this isomorphism starts with the ...