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.
268
questions
8
votes
1answer
256 views
The lattice of analogues of Robinson's $Q$
This question was asked and bountied at MSE without response.
Call a sentence $\varphi$ in the language of arithmetic $Q$-like iff $\mathbb{N}\models\varphi$ and $\{\varphi\}$ is essentially ...
4
votes
1answer
228 views
How can we know the well-foundedness of $\epsilon_0$?
I think the question can be quite philosophical, but I see that $WF(\epsilon_0)$ is widely accepted as one of the attributes of the natural numbers.
Gentzen proved $Con(PA)$ with $PRA+WF(\epsilon_0)$....
0
votes
0answers
30 views
restriction of a formula with matrix inverse multiplied by a vector
I'm trying to reproduce a proof from this paper but I'm stuck in one point (Lemma 6). The general subject is bayesian model for multi-armed bandit problem solved with Thompson sampling.
I think I ...
11
votes
0answers
423 views
Where did this presentation of Godel's theorem appear?
This question was asked and bountied at MSE, with no response.
Many years ago I ran into the following proof of Godel's first incompleteness theorem
(here $T$ is an "appropriate" theory of ...
8
votes
1answer
217 views
How to understand the interface of the consistency strength hierarchy, reverse mathematics, and proof-theoretic ordinal analysis?
I am aware of three major "hierarchies" of mathematical theories, but I don't know how to relate these hierarchies to one another. Here are the hierarchies I have in mind:
Consistency strength. My ...
6
votes
2answers
329 views
Interpreting proper elementarily equivalent end extensions?
Is there a tuple of parameter-free formulas $\Phi$ and a nonstandard $M\models PA$ such that $\Phi^M\models PA$, the induced $M$-definable initial segment embedding $j_\Phi^M:M\rightarrow\Phi^M$ is ...
5
votes
0answers
119 views
$Π_2$ strength of KP
I am looking for a characterization of the $Π_2$ statements provable in KP.
Here, KP (often denoted KPω) is the Kripke-Platek set theory, including infinity and full induction on ordinals. Here is ...
7
votes
1answer
200 views
Birkhoff's completeness theorem put into practice
Birkhoff's completeness theorem (see here, Theorem 14.19) states that an equation which is true in all models of an algebraic theory can be proven in equational logic.
Question. Does the proof of ...
6
votes
0answers
206 views
$0^\#$ in weak theories vs large cardinals in $L$
To better understand the transition from large cardinal axioms consistent with the constructible universe $L$ to large cardinal axioms transcending $L$, I am looking for natural equiconsistencies ...
0
votes
0answers
32 views
Reasons for inapplicability of complete induction to tour expansion
It is known that tour expansion is a rather poor heuristic for generating short Hamilton cycles even in the planar Euclidean case. That comes as a surprise when learning of that for the first time.
...
3
votes
0answers
149 views
Elementary self-embeddings conservative over ZFC
Question: Is the following theory conservative over ZFC? And if not, what is its strength?
Language: $∈$, $j$ (unary function symbol)
Axioms:
1. ZFC (without separation and replacement for formulas ...
6
votes
1answer
270 views
“Robinson arithmetic” for (some) levels of $L$?
I'll write "$\mathcal{L}_\alpha$" for the fragment $\mathcal{L}_{\infty,\omega}\cap L_\alpha$.
Say that a countable admissible $\alpha$ is Robinsonian if there is some sentence $\varphi\in\mathcal{L}...
0
votes
0answers
317 views
Artificial intelligence simulating mathematicians (what a distopia!)
This is kind of soft and naive question, so feel free to shame on me :)
I start from the fact that, in my opinion, what humans are interested in about mathematics are things that we find deep and ...
8
votes
1answer
487 views
Gentzen's result on PA
The Wikipedia states that Gentzen proved that "in modern terms, the proof-theoretic ordinal of PA is $\varepsilon_0$." Further down, the article defines what the "proof theoretic ordinal" of a theory ...
10
votes
1answer
164 views
Is there a relation between type (maximum linearization) of a computable WQO and the ordinal strength of a theory needed to prove it?
Background:
Given a well partial order $X$ (more commonly studied with antisymmetry dropped as well-quasi-orders, but I'm going to say well partial order to make this definition simpler, obviously ...
0
votes
1answer
453 views
On provability of false statements in constructive mathematics [closed]
Lagarias "elementary" reformulation of Robin's theorem is that $$\mathrm{RH}\iff\sigma(n)\leq H_n+e^{H_n}\log(H_n)$$
holds for every $n\geq 1$, where $\sigma(n)$ is the sum of divisors function and $...
6
votes
0answers
209 views
What is proof-theoretic ordinal of weak first-order arithmetic?
According to Wikipedia(https://en.wikipedia.org/wiki/Ordinal_analysis) and nlab(https://ncatlab.org/nlab/show/ordinal+analysis), a proof-theoretic ordinal of $\mathsf{PRA}$ is $\omega^\omega$.
...
3
votes
0answers
172 views
Proof theory and subsystems of second-order arithmetic: in particular the reverse mathematics of Godel's system $T$
While doing some research on reverse mathematics, I came across the following document under the address, http://www.andrew.cmu.edu/user/avigad/Talks/survey1.pdf:
Proof theory and Subsystems of ...
3
votes
0answers
238 views
Can third-order arithmetic prove the consistency of second-order arithmetic?
I'm trying to get a deeper understanding of Buss's version of Gödel's speedup proof. In short, if we assume that $Z_0$ is first-order arithmetic, $Z_1$ is second-order arithmetic, and so on, then for $...
1
vote
1answer
303 views
What does “can almost be proven in PA” mean regarding Theorem 2 of Timothy Chow's expository article, “The Consistency of Arithmetic”?
In his expository article, "The Consistency of Arithmetic" (MSN), Prof. Chow has the following theorems:
Theorem 1. If $a_1, a_2, a_3,\dotsc$ is a sequence of ordinals and $a_i \ge a_j$ whenever $...
6
votes
0answers
264 views
Does second order ZFC conservatively extend first order ZFC?
If I replace the axiom schema of specification in ZFC by a single axiom in second order logic, and similarly do same thing for the axiom schema of replacement, is this version of "second order ZFC" ...
2
votes
0answers
135 views
Cut elimination proofs of the consistency of arithmetic
It is well known that one can use cut elimination to establish the consistency of arithmetic (though this involves assuming transfinite induction up to $\varepsilon_0$.) Most proofs, however, work ...
4
votes
1answer
291 views
Proof-theoretic ordinals: inevitable consistency?
There are various different notions of the proof-theoretic ordinal of a theory; most of these are "notation-dependent" in that they're only nontrivial once we restrict attention to a class of "natural"...
4
votes
2answers
475 views
Ordinal analysis and proofs of consistency
$\epsilon_0$ is the proof-theoretic ordinal of PA. Gentzen proved the consistency of Peano's first-order axioms for arithmetic using primitive recursive arithmetic and induction up to $\epsilon_0$.
...
19
votes
2answers
2k views
Status of proof by contradiction and excluded middle throughout the history of mathematics?
Occasionally I see the claim, that mathematics was constructive before the rise of formal logic and set theory. I'd like to understand the history better.
When did proofs by contradiction or by ...
9
votes
1answer
279 views
Computability-theoretic results relevant to realizability
This may be a very naive question which only reflects my failure at literature search, but:
Although realizability (in its original form at least) is grounded in computability, the details of ...
5
votes
0answers
170 views
Finite axiomatizability and $\mathrm{PA^{top}}$
Is $\mathrm{PA^{top}}$ finitely axiomatizable? If not, does it have a finitely axiomatizable extension (allowing new predicates but not new variable types) that has arbitrarily large finite models?
$\...
6
votes
0answers
108 views
Lambek calculus, linear logic, and linear algebra
In his 1958 paper, The Mathematics of Sentence Structure, Joachim Lambek introduced the Lambek calculus. In modern terms, it could be understood as a syntax for biclosed
monoidal categories, and he ...
7
votes
1answer
223 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 ...
3
votes
0answers
124 views
Partial well-ordering of formulas
Given a theory $T$, for arbitrary formulas $φ$ and $ψ$ that provably in $T$ denote an ordinal, set $[φ]_T < [ψ]_T$ iff provably in $T$, the ordinal denoted by $φ$ is less than the ordinal denoted ...
8
votes
1answer
205 views
Is restricting Replacement and Separation enough to make $Q+I\Sigma_n$ bi-interpretable with Set Theory?
We have the result that $\mathsf{ZFCfin}$, the usual $\mathsf{ZFC}$ axioms with the axiom of infinity replaced by its negation, is bi-interpretable with $\mathsf{PA}$, first order Peano Arithmetic. We ...
1
vote
1answer
105 views
Decidability of S2S with real numbers
Is the theory of natural numbers and functions $ℕ → ℝ$ decidable under:
- for natural numbers: $\mathrm{succ1}(n) = 2n+1$; $\mathrm{succ2}(n) = 2n+2$; equality
- for functions: pointwise addition and ...
6
votes
2answers
823 views
How can the simply typed lambda calculus be Turing-incomplete, yet stronger than second-order logic?
It is well-known that the simply typed lambda calculus is strongly normalizing (for instance, Wikipedia). Hence, it is not strong enough to be Turing-complete, as also mentioned on the Wikipedia page ...
12
votes
3answers
543 views
Infinite descending consistency chains
What are some examples of consistent theories $T_i$ (extending elementary arithmetic EA) such that for $∀i∈ℕ \,\, T_i ⊢ \mathrm{Con}(T_{i+1})$?
Such theories exist; see for example An infinitely ...
1
vote
0answers
69 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, ...
0
votes
0answers
77 views
Are the HBL derivability conditions necessary for Gödel's incompleteness theorems? (For Löb's 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, ...
0
votes
0answers
80 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, ...
1
vote
0answers
84 views
n-consistency - provability/truth of $\Sigma^0_n$ and $\Pi^0_{n+1}$ -formulas; n-consistent extensions, etc
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, ...
7
votes
1answer
380 views
van der Waerden's theorem in Reverse Mathematics
What is known about weak systems of axiomata that allow one to prove van der Waerden's theorem ?
van der Waerden's theorem can be used to show that there are infinitely many primes (see below). Is ...
4
votes
0answers
211 views
Ordinal analysis and nonrecursive ordinals
Ordinal analysis is typically described as characterizing recursive ordinals in a theory $T$, but there is a sense in which it can characterize all $T$-ordinals, even those that are nonrecursive.
...
2
votes
0answers
105 views
Lengths of proofs and quasilinear time
Length of proofs depends not only on the theory but also on its axiomatization. Once an axiomatization is fixed, typical proof systems are equivalent up to a polynomial factor. But what if we care ...
28
votes
9answers
6k views
“Strange” proofs of existence theorems [closed]
This question isn't related to any specific research. I've been thinking a bit about how existence theorems are generally proven, and I've identified three broad categories: constructive proofs, ...
18
votes
2answers
1k views
Has Apéry's proof of the irrationality of $\zeta(3)$ ever been used to prove the irrationality of other constants?
Apéry's proof of the irrationality of $\zeta(3)$ astounded contemporary mathematicians for its wealth of new ideas and techniques in proving the irrationality of a known constant. It is often the case ...
3
votes
1answer
521 views
Going beyond the strength of Peano arithmetic “without sets”
First-order arithmetic is fairly weak, as measured for example by its consistency strength. When a stronger theory is desired, it is common to work with (fragments of) second-order arithmetic or set ...
4
votes
0answers
98 views
Reasonable reference index or list of the interpretability/consistency hierarchy
In Kanamori's The Higher Infinite a diagram is included towards the end of the book which illustrates the large cardinal hierarchy by listing many large cardinal axioms and drawing their direction ...
9
votes
4answers
536 views
What would $\mathcal{P} \neq \mathcal{NP}$ tell us about some non-constructive proofs?
Let me sum up my - hopefully correct - understanding of the travelling salesman problem and complexity classes. It's about decision problems:
"[...] a decision problem is a problem that can be ...
3
votes
3answers
457 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 ...
8
votes
0answers
283 views
What metatheory proves cut elimination for Simple Type Theory?
Gaisi Takeuti's book Proof Theory proves cut elimination for Simple Type Theory (a combined result of several researchers). Thus it proves consistency of Simple Type Theory with full comprehension in ...
6
votes
1answer
196 views
Correspondence between proof-theoretic ordinals and fast growing functions?
For theories with well known proof-theoretic-ordinals, (what) is there a correspondence between their proof-theoretic-ordinal and (ordinal indexed families of?) fast growing functions provable total ...
6
votes
1answer
258 views
Am I counting quantifiers correctly?
I think this is right but I want to check. The theory $\mathsf{WKL}^*_0$ is conservative over EFA for $\Pi^0_2$ sentences. And the first order part of $\mathsf{WKL}^*_0$ is axiomatized by EFA plus ...
