# 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

**1**answer

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

**1**answer

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

**0**answers

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

**0**answers

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

**1**answer

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

**2**answers

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

**0**answers

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

**1**answer

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

**0**answers

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

**0**answers

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

**0**answers

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

**1**answer

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

**0**answers

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

**1**answer

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

**1**answer

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

**1**answer

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

**0**answers

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

**0**answers

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

**0**answers

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

**1**answer

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

**0**answers

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

**0**answers

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

**1**answer

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

**2**answers

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

**2**answers

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

**1**answer

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

**0**answers

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

**0**answers

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

**1**answer

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

**0**answers

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

**1**answer

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

**1**answer

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

**2**answers

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

**3**answers

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

**0**answers

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

**0**answers

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

**0**answers

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

**0**answers

84 views

### n-consistency - provability/truth of $\Sigma^0_n$ and $\Pi^0_{n+1}$ -formulas; n-consistent extensions, etc

**7**

votes

**1**answer

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

**0**answers

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

**0**answers

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

**9**answers

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

**2**answers

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

**1**answer

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

**0**answers

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

**4**answers

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

**3**answers

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

**0**answers

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

**1**answer

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

**1**answer

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