Questions tagged [proof-theory]
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.
399 questions
4
votes
3
answers
332
views
Optimal Subsystem of $\mathsf{PA}_{2}$ for Proving Existence of Set of Gödel Codes of True Arithmetic
Let $\mathcal{N}$ denote the standard model of first-order Peano arithmetic, $\mathsf{PA}$, and let true arithmetic, $\mathsf{Th}(\mathcal{N})$, be the set of sentences in $\mathsf{L}_{\mathsf{PA}}$ ...
- 51
13
votes
1
answer
356
views
How far does Cantor-Bendixson rank counting let us build computable isomorphisms between ordinals?
This is tangentially related to this old question of mine.
Say that a clean well-ordering is a computable well-ordering $\triangleleft$ of $\mathbb{N}$ such that the following additional data is ...
- 19k
2
votes
1
answer
321
views
Is there a second incompleteness theorem for Rosser-provability?
In question What are the adequacy conditions for Rosser Provability? I asked for the adequacy conditions for Rosser-provability ($\rho$) as compared with the Hilbert-Bernays-Löb derivability ...
- 4,168
3
votes
0
answers
161
views
Proof-theoretic strength of subsystems of Kripke-Platek set theory
We know that the $\mathsf{KP}$ set theory with Infinity (and its variants with and without Urelemenets) has impredicative strength, i.e. its proof-theoretic ordinal is Bachmann-Howard (same as $\...
- 31
3
votes
0
answers
286
views
Using dilators to formalize the intuitions about the size of small uncomputable ordinals
The least recursively inaccessible ordinal $I$, is, intuitively, the supremum of the ordinals that come from "recursively" iterating the function $\alpha\mapsto\omega^{CK}_\alpha$. For an ...
- 1,812
11
votes
0
answers
317
views
Girard's alternate proof-theoretic ordinals
In his review of Girard's book Proof theory and logical complexity, volume 1, Pfeiffer writes the following:
In the second volume the author will present an assignment of ordinals to theories, which ...
- 19k
10
votes
0
answers
631
views
Simple true $\Pi^0_1$ statements independent of weak arithmetics
I originally asked this question on Math StackExchange here, but I have copied it here as I now feel it is more appropriate for this site.
There is an explicitly known 549-state Turing machine where, ...
- 3,069
1
vote
0
answers
216
views
For a given theory $T$, do all theorems provable in $T$ have "short" proofs using stronger theories?
Godel's speedup theorem states that for a given theory $T$ we can build specific theorems that have only very long proofs in $T$ but short ones in $T + con_T$.
What do we know about the case of all ...
- 119
6
votes
1
answer
345
views
Löb's Theorem and Large Cardinal Analogs for Second Order Arithmetic
Löb's Theorem tells us we can't consistently supplement a sufficently strong theory with the schema $$\operatorname{Prov}(\phi) \implies \phi$$ at least when $\operatorname{Prov}$ captures provability ...
- 4,069
2
votes
0
answers
100
views
A generalization of Heyting prealgebras which may fail weakening
By definition, a Heyting prealgebra is a bounded prelattice in which all Heyting implications exist. In other words, it is a set $X$ with a relation $⊢$ such that there exist operators $⊤, ⊥, ∧, ∨, ⇒$ ...
- 1,971
7
votes
0
answers
251
views
Different forms of completeness of intuitionistic propositional logic for topological semantics
I've gotten myself very confused as to what “completeness” means in the context of intuitionistic logic.
I'm aware of the following theorem (Alfred Tarski, “Der Aussagenkalkül und die Topologie”, Fund....
- 39.7k
1
vote
0
answers
135
views
Cut-elimination in a Hilbert-type system?
I have a question regarding the paper "Provably computable functions and the fast growing hierarchy" by Buchholz and Wainer (1987).
The authors perform their analysis on a Gentzen-type ...
- 1,184
6
votes
0
answers
277
views
Are there natural statements in primitive recursive arithmetic with only bounded quantifiers that are true but not provable?
Goodstein's "Recursive Number Theory" (1957) presents a "logic-free" version of primitive recursive arithmetic: all statements in the logic are equalities of expressions involving ...
- 489
5
votes
1
answer
312
views
Proof-theoretic ordinals of $\mathsf{ACA}_0$ plus $\Pi^1_n$-induction
The proof-theoretic ordinal of $\mathsf{ACA}_0$ is $\varepsilon_0$ (Simpson, Subsystems of Second Order Arithmetic, 2009, theorem IX.5.7), and the proof-theoretic ordinal of $\mathsf{ACA}$ is $\...
- 3,069
3
votes
0
answers
517
views
Who first noticed that the Löb formula holds in arithmetic?
Cross-posted to History of Science and Mathematics
(Löb, 1955) established Löb's theorem that A is derivable in arithmetic if (Bew([A]) -> A) is.
(Macintyre and Simmons 1973) in Theorem 2.1 iv), p. ...
- 4,168