All Questions
Tagged with foundations proof-theory
17 questions
22
votes
1
answer
4k
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 ...
- 711
20
votes
5
answers
2k
views
Does formalizing math require search and creativity, or is it near-mechanical?
I remember reading somewhere that it takes about a week to convert a page of math into something a proof-assistant like Isabelle or HOL Light would accept.
Is this type of conversion something that ...
17
votes
1
answer
390
views
How much can "(recursively) large ordinal axioms" prove?
In "Collapsing functions based on recursively large ordinals: A well–ordering proof for KPM", Michael Rathjen shows that certain notations for the proof-theoretic ordinals of theories, which ...
- 3,612
16
votes
2
answers
852
views
Appearance of proof relevance in "ordinary mathematics?"
I've been wondering recently what—if any—applications proof theory has to ordinary mathematics (by which I mean algebra, analysis, topology, and so on). In particular, I'd be fascinated to see a proof ...
- 177
13
votes
3
answers
2k
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 ...
- 32.1k
12
votes
3
answers
648
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 ...
- 4,587
8
votes
1
answer
301
views
Logic with "co-relations" - sources?
My question is on a seemingly-natural extension of classical logic that I've been playing around with a bit in the context of generalized recursion theory. I'm sure it's been treated extensively ...
- 21.1k
6
votes
1
answer
292
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 ...
- 4,587
5
votes
3
answers
897
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 ...
- 4,587
5
votes
1
answer
720
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 ...
- 4,587
5
votes
0
answers
243
views
What useful admissible rules does ZFC have beyond the deduction theorem?
I'm interested in formal proof verification, and one of the surprisingly difficult parts of this is dealing with proofs by contradiction. The issue is that the final step of such proofs is typically "...
- 443
3
votes
2
answers
814
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,587
3
votes
1
answer
391
views
Reference request on Gentzen's proof of the consistency of PA
I've always been interested in having a good understanding of Gentzen's proof of the consistency of arithmetic.
Being more precise, he showed that $PRA + WF(\epsilon_0) \vdash Con(PA)$.
I am ...
- 3,318
3
votes
0
answers
853
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 ...
- 4,587
2
votes
0
answers
255
views
A formal definition of a useful theorem?
Sorry if this feels a bit squishy, but I'm wondering if there is any published work trying to give a fully formal definition of the notion of a useful theorem. I mean, in mathematics we all know that ...
- 3,029
1
vote
0
answers
101
views
Questions in proof theory (PRA-provability of EA-theorems, Girards book from '87)
I've been working through a textbook, often encountering difficulties with the exercises.
On mathstackexchange, with most of them I haven't arrived yet at a satisfactory solution.
As I understand, ...
- 121
0
votes
0
answers
96
views
Shepherdson's conditions - a shortcut to the second incompleteness theorem?
I've been working through a textbook, often encountering difficulties with the exercises. On mathstackexchange, with most of them I haven't arrived yet at a satisfactory solution.
As I understand, ...
- 121