**11**

votes

**1**answer

728 views

### Proof-Theoretic Ordinal of ZFC or Consistent ZFC Extensions?

Let the proof theoretic ordinal $\alpha$ of a theory $T$ be the least recursive ordinal such that $T$ does not prove that $\alpha$ is well-founded. This ordinal is intended to quantify in some sense ...

**12**

votes

**1**answer

322 views

### What metatheory proves $\mathsf{ACA}_0$ conservative over PA?

Simpson's book shows $\mathsf{ACA}_0$ is conservative over $\mathsf{PA}$ in the natural way by model theory using definable subsets. Of course, $\mathsf{ACA}_0$ being conservative over PA is ...

**4**

votes

**1**answer

316 views

### Can the Burgess-Hazen analysis of Predicative Arithmetic be extended to Transfinite Types?

Around page 300 of his book "Mathematical Thought and its Objects", Charles Parsons discusses the work of Edward Nelson, who believes that mathematical induction is impredicative, because it can be ...

**64**

votes

**16**answers

5k views

### When are two proofs of the same theorem really different proofs

Many well-known theorems have lots of "different" proofs. Often new proofs of a theorem arise surprisingly from other branches of mathematics than the theorem itself.
When are two proofs really the ...

**29**

votes

**3**answers

3k views

### Feit-Thompson Theorem: The Odd Order Paper

For reference, the Feit-Thompson Theorem states that every finite group of odd order is necessarily solvable. Equivalently, the theorem states that there exist no non-abelian finite simple groups of ...

**14**

votes

**2**answers

2k views

### Clarification of Gödel's second incompleteness theorem

I am sorry for the following question, because the actual answer to this question is in the beautiful works of Feferman and Jeroslow, but, unfortunately, I havn't any time to go into that specific ...

**9**

votes

**3**answers

858 views

### Consistency of Analysis (second order arithmetic)

Is there a proof of the consistency of Analysis (second order arithmetic), which is similar to Gentzen's proof of the consistency of arithmetic?
Update:
Which (different) methods can be used to ...

**11**

votes

**3**answers

769 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

2k views

### Independence of PA implies independence of PA union all true $\Pi_1$ statements

Prove that if a statement is independent of Peano Arithmetic (PA), then it's also independent of PA$_1$, where PA$_1$ is the union of the set of axioms in PA and the set of all true $\Pi_1$ ...

**3**

votes

**1**answer

558 views

### Feferman's extensional and intensional applications of the method of arithmetization

At the very beginning of Feferman's Arithmetization of metamathematics in a general setting it can be read:
The method of arithmetization, as developed by Gödel[10], exploits the possibility of ...

**1**

vote

**0**answers

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

**26**

votes

**15**answers

5k views

### What's a magical theorem in logic?

Some theorems are magical: their hypotheses are easy to meet, and when invoked (as lemmas) in the midst of an otherwise routine proof, they deliver the desired conclusion more or less ...

**24**

votes

**2**answers

534 views

### Why is there no connection between fast-growing functions and complex analysis

I found myself wondering the other day whether the fast-growing functions from natural to naturals that are studied by people like proof theorists are the restriction to the naturals of analytic ...

**20**

votes

**2**answers

933 views

### Deep theorems and long proofs

I ran across this discussion by Daniel Shanks,
"Is the quadratic reciprocity law a deep theorem?."
Solved and Unsolved Problems in Number Theory. Vol. 297. AMS, 2001. p.64ff.
which made me ...

**14**

votes

**1**answer

1k views

### Proof theoretic ordinal

In Ordinal Analysis, Proof-theoretic Ordinal of a theory is thought as measure of a consistency strength and computational power.
Is it always the case? I. e. are there some general results about ...

**10**

votes

**1**answer

355 views

### What is the proof-theoretic ordinal of PA + Con(PA), PA + Con(PA + Con(PA)) etc., and why?

I seem to remember having read that the proof-theoretic ordinal (sup of ordinals the theory can prove well-ordered) of $\mathsf{PA} + \mathsf{Con}(\mathsf{PA})$ is the same as that of $\mathsf{PA}$, ...

**7**

votes

**3**answers

2k views

### Most general formulation of Gödel's incompleteness theorems

Modern statements of Gödel's incompleteness theorems are usually in terms of first-order predicate logic. However, I've often read the claim that they extend to arbitrary formal systems that can prove ...

**9**

votes

**2**answers

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

**16**

votes

**1**answer

690 views

### Goodstein's theorem without transfinite induction

Goodstein's theorem is an example of a theorem that is not provable from first order arithmetic. All proofs of the theorem seem to deploy transfinite induction and I've wondered if one could prove the ...

**6**

votes

**1**answer

320 views

### Essential incompleteness via diophantine formulas?

Work in the first order language of number theory, consisting of the symbols $\mathbf{0}$, $\mathbf{S}$, $\boldsymbol{+}$, and $\boldsymbol{\cdot}$, and let $Q$ denote Robinson's arithmetic.
By a ...

**5**

votes

**4**answers

5k views

### About the proof of the proposition “there exists irrational numbers a, b such that a^b is rational”

What does the classical proof of the proposition "there exists irrational numbers a, b such that $a^b$ is rational" want to reveal? I know it has something to do with the difference between classical ...

**4**

votes

**1**answer

304 views

### ERA, PRA, PA, transfinite induction and equivalences

I'm quite sure I don't understand very well the links between proof theoretical ordinals of theories, the axioms of transfinite induction and the objects a theory can prove to exist.
For instance I'm ...

**8**

votes

**1**answer

267 views

### Which ordinals can be proof-theoretic ordinals of a reasonable theory?

When talking to a friend recently he asked a question - are there any reasonable first-order theories which have proof theoretic ordinal equal to small or large Veblen ordinal? I have then extended ...

**7**

votes

**7**answers

370 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

**2**answers

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

**2**

votes

**1**answer

252 views

### what are the proof-theoretic ordinals of second-order arithmetic and ZFC? [duplicate]

are they still smaller than omega-1-CK?what are the notations of them?

**1**

vote

**2**answers

291 views

### Embedding of consistent subset in first order logic (finitely many variables)

I am looking at FOL with no equality, no constant, no function symbol and the unique binary predicate $\in$ with variables in arbitrary sets $V$ or $W$. Specifically we define ${\bf P}(V)$ as the free ...