Skip to main content
Search type Search syntax
Tags [tag]
Exact "words here"
Author user:1234
user:me (yours)
Score score:3 (3+)
score:0 (none)
Answers answers:3 (3+)
answers:0 (none)
isaccepted:yes
hasaccepted:no
inquestion:1234
Views views:250
Code code:"if (foo != bar)"
Sections title:apples
body:"apples oranges"
URL url:"*.example.com"
Saves in:saves
Status closed:yes
duplicate:no
migrated:no
wiki:no
Types is:question
is:answer
Exclude -[tag]
-apples
For more details on advanced search visit our help page
Results tagged with
Search options not deleted user 5017

For question in Proof Theory, where "proofs" themselves are the object of mathematical investigation. It is not to be used to request a proof of some result.

12 votes
3 answers
644 views

Has the Ramified Theory of Types been applied to NBG?

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 …
Keshav Srinivasan's user avatar
7 votes
4 answers
1k views

How can you formalize the metamathematics conventionally used to state Godel’s theorem?

Gödel’s incompleteness theorem states that for any sufficiently strong formal system $T$ there exists a statement $G$ such that if $T$ is consistent, then $G$ is true but not provable in $T$. But I’m …
Keshav Srinivasan's user avatar
6 votes
1 answer
271 views

Does $\text{ACA}_0$ + True Arithmetic prove the well-foundedness of every recursive ordinal?

As discussed in Noah Schweber's answer to What is the proof-theoretic ordinal of true arithmetic?, it is somewhat ambiguous what “the proof-theoretic ordinal of True Arithmetic” might mean. In one se …
Keshav Srinivasan's user avatar
5 votes
1 answer
710 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 ap …
Keshav Srinivasan's user avatar
5 votes
3 answers
881 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 b …
Keshav Srinivasan's user avatar
4 votes

Did Gödel prove that the Ramified Theory of Types collapses at $\omega_1$?

I was reading Feferman's original 1964 paper "Systems of Predicative Analysis", and I think I've found an answer to my question about how much second-order arithmetic you can do if you let the ramifie …
Keshav Srinivasan's user avatar
3 votes
2 answers
799 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 ar …
Keshav Srinivasan's user avatar
3 votes
0 answers
845 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 metho …
Keshav Srinivasan's user avatar