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

296
questions

**1**

vote

**0**answers

123 views

### A question on entailments in sequents

Suppose $\Gamma\vdash A\vee \Delta$, where as usual $\Gamma$ and $\Delta$ are thought of as sets of propositions and the turnstyle is for logical consequence, or entailment.
Given the assumption, may ...

**1**

vote

**1**answer

69 views

### Knapsack problem with capacity constraint

The traditional knapsack problem is that: given a sequence of $i$ items with positive weights $w_1,w_2,...,w_i$, positive values $v_1,v_2,...,v_i$, and a bag with capacity $B$, we want to insert items ...

**1**

vote

**0**answers

91 views

### What is the proof theoretic strength of PCF?

Godel's system $T$ means different, although equivalent, things to different people. To people working in the traditon of mathematical logic, $T$ is a quantifier-free equational theory of arithmetic ...

**1**

vote

**1**answer

81 views

### Knapsack problem with value range constraint

The traditional knapsack problem is that: given a sequence of $i$ items with positive weights $w_1,w_2,...,w_i$, positive values $v_1,v_2,...,v_i$, and a bag with capacity $B$, we want to insert items ...

**10**

votes

**3**answers

672 views

### Is there a semantics for intuitionistic logic that is meta-theoretically “self-hosting”?

One can study the standard semantics of classical propositional logic within classical logic set theory, so we can say that the semantics of classical logic is meta-theoretically "self-hosting&...

**0**

votes

**0**answers

50 views

### Computational practicality of proving a theorem by transforming into a map coloring and finding $P(3)$, where $P$ is the chromatic polynomial

So I have heard that you can transform a math statement into a map in such a way that proving the statement is true is equivalent to finding a $3$-coloring of that map.
I'm also aware that you can ...

**1**

vote

**1**answer

171 views

### Is there an example of converting a mathematical statement into a three color mapping? [closed]

https://youtu.be/5ovdoxnfFVc?t=1118
At this point, prof Wigderson says it is easy to go from a mathematical statement to a graph coloring problem. The video does not provide an example of this, and a ...

**4**

votes

**1**answer

316 views

### Uniform incomparable consistency strengths

For every true arithmetical statement $T$, there are $T$-incomparable $Π^0_1$ statements, but can we find them uniformly in $\text{Theory}(T)$?
Specifically, are there computable $A$ and $B$ such that ...

**1**

vote

**0**answers

49 views

### The relationship of deteminant of a matrix and its diagonol block matrix?

I am trying to prove an inequality that :
$$
\operatorname{det} \Sigma_{V \mathrm{~V}}<\prod i \operatorname{det}\left(\Sigma_{V_{i} V_{i}}\right)
$$
Where
$$
\Sigma_{V V}=\left[\begin{array}{ccc}
\...

**0**

votes

**0**answers

129 views

### What are the handy, go-to methods of proving consistency of a proof system?

Suppose you face a proof system portraying some notion or knowledge that you haven't encountered, or others haven't studied before. What would be your first attempts to examine the consistency of the ...

**8**

votes

**0**answers

161 views

### Reverse mathematics of Noetherian rings over $\mathbb{Q}$

Take the Hilbert Basis Theorem over the rational numbers in this form in the language of Second Order Arithmetic: For every $n\in N$ every ideal of the polynomial ring $\mathbb{Q}[x_1,\dots,x_n]$ is ...

**8**

votes

**1**answer

276 views

### Reference request: proof-theoretic strength of $\mathsf{KP}$ with recursively large ordinals and $\mathsf{CZF}$ with large set axioms

Large set axioms are notions corresponding to large cardinals on constructive set theories like $\mathsf{IZF}$ or $\mathsf{CZF}$. The notion of inaccessible sets, Mahlo sets, and 2-strong sets ...

**3**

votes

**0**answers

228 views

### Is $\mathsf{R}$ axiomatizable by finitely many schemes?

Recall that $\mathsf{R}$ is the theory of arithmetic consisting of the quantifier-free theory of $(\mathbb{N};+,\times,0,1,<)$ together with, for each $k\in\mathbb{N}$, the sentence $$\forall x[(\...

**7**

votes

**2**answers

212 views

### Incompleteness theorems for theories with omega-rule

Recall that the omega-rule is an infinitary rule of inference that allows one to deduce $\forall x A(x)$ from $A(0), A(1), \dots$. It's known that adjoining PA (or even Q) with the omega-rule results ...

**4**

votes

**0**answers

105 views

### Edge contraction-like graph operation

Previously asked on MSE.
Given a simple graph $G=(V,E)$ and an edge $uv\in E$, the contraction of $uv$ refers to the replacement of the vertices $u$ and $v$ with a new vertex $w$ such that the edges ...

**5**

votes

**0**answers

178 views

### Does $\mathsf{Q}$ have any interesting provably recursive functions?

This question was asked and bountied at MSE without success.
For an appropriate theory $T$, say that an $n$-ary $T$-provably recursive function is a $\Sigma_1$ formula $\varphi$ with $n+1$ free ...

**63**

votes

**3**answers

6k views

### Replication crisis in mathematics

Lately, I have been learning about the replication crisis, see How Fraud, Bias, Negligence, and Hype Undermine the Search for Truth (good YouTube video) — by Michael Shermer and Stuart Ritchie. ...

**4**

votes

**0**answers

180 views

### PA, provably total function, Gödel's T

If I am not mistaken, the provably total functions of $PA$ are exactly those definable in terms of the functionals of higher type $T$, as introduced by Gödel in his 1958 Dialectica paper.
In ...

**2**

votes

**0**answers

250 views

### Theorems with many proofs

Q. What are the characteristics of theorems that seem to invite (or possess) several or even many distinct proofs?
What I have in mind are examples such as these:
Proofs that there are infinitely ...

**4**

votes

**1**answer

129 views

### Information density of proofs?

I am a CS person so please excuse the hand-waving.
Given a set of machine-represented proofs, each different (but not necessarily proving a different thing), what sort of information-theoretic ...

**9**

votes

**1**answer

244 views

### Concrete examples of statements not provable in PRA + $\epsilon_0$-induction that are provable in PA?

It is well-known that $\mathbf{PRA}$ plus $\epsilon_0$-induction on bounded formulas cannot prove all $\mathbf{PA}$ theorems (essentially because $I\Sigma_1$ plus $\epsilon_0$-induction on bounded ...

**4**

votes

**0**answers

150 views

### The Return of Graham Arithmetics: adding induction up to $g_{64}$

In my previous question The inconsistency of Graham Arithmetics plus $ \forall n, n < g_{64}$, I introduced an extension of Robinson Arithmetics with the recursive definition of Tetraction, a small ...

**14**

votes

**2**answers

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

**1**

vote

**1**answer

261 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**

votes

**1**answer

221 views

### Model of PA with false $\Sigma^0_1$ sentence but no false Con sentence?

This is probably a really basic result that I'm forgetting but if $M \models \text{PA}$ and $M \models \phi$ for some $\Sigma^0_1$ sentence $\phi$ such that $\mathbb{N} \models \lnot \phi$ does it ...

**1**

vote

**0**answers

121 views

### Checking existence of proofs of fixed length

This question is a continuation of a related previous question (check here).
Let $\mathcal{L}$ be a recursive first-order theory with the Hilbert-Ackerman's proof calculus, and such that the ...

**5**

votes

**1**answer

206 views

### Computational complexity of proof verification

Let $\mathcal{L}$ be a recursive first-order theory, with a deductive system $\Xi$ (for instance, Hilbert-Ackerman proof system). Let $\phi$ be a formula and let $l=(\psi_1, \ldots, \psi_n=\phi)$ be a ...

**2**

votes

**1**answer

113 views

### Constructivity of two problems on a standard simplex?

Maximizing a hyperplane $\sum_i a_ix_i$ where $a_i\in\mathbb R$ and each $a_i$ are fixed and non-negative and $x_i$ are variables over a standard simplex $\sum_i x_i\leq 1$ with $0\leq x_i$ always ...

**8**

votes

**1**answer

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

**6**

votes

**1**answer

294 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

33 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

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

**9**

votes

**1**answer

277 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

354 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

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

**8**

votes

**1**answer

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

**7**

votes

**0**answers

251 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

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

**7**

votes

**1**answer

375 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

350 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

519 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

186 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

471 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

234 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

192 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

370 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

313 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

292 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

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