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

312
questions

0
votes

0
answers

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

0
votes

0
answers

49
views

### If two functions are close apart can I proof the difference of their empirical loss is also small?

I am trying to understand the proof of Theorem 3 in the paper "A Universal Law of Robustness via isoperimetry" by Bubeck and Sellke.
Basically there exist atleast one $w_{L,e}$ in $\...

5
votes

0
answers

118
views

### On the correspondence between proof nets and sequents

1. Context
While trying to answer my question on the existence of a (useful) graphical calculus for star-autonomous categories, I came across the paper Natural deduction and coherence for weakly ...

3
votes

0
answers

106
views

### Can the essence of the $0^\#$ LCA be weakened to an axiom not requiring uncountable cardinals?

"$0^\#$ exists" is an informally stated large cardinal axiom that is to be understood as "there is an uncountable set of Silver indiscernibles", "every uncountable cardinal is ...

5
votes

0
answers

140
views

### What are the known large cardinal axioms for which weaker and stronger set theories "catch up"?

I will clarify what I mean by the title in the following four ways:
For which cardinals $\kappa$ do we have that ZFC-(Powerset axiom)+$\exists\kappa$ is equiconsistent with ZFC? If that is not ...

0
votes

0
answers

76
views

### How to define BHO alternatives below admissible ordinals?

Bachmann-Howard ordinal is a recursive ordinal. It's not that large compared to those proof-theoretic ordinals of stronger theories, but the definition of BHO is sufficient to illustrate how ...

10
votes

0
answers

422
views

### Which sentences are "irreducibly" self-referential over $\mathsf{PA}$?

Previously asked at MSE. Below, all sentences/formulas are in the language of arithmetic, and for simplicity we conflate numbers with numerals and sentences with Godel numbers.
Say that a sentence $\...

6
votes

1
answer

239
views

### Proving short consistency: can we do better than brute force search?

This is a minor variation of a question originally asked on MSE by user779130 and bountied by me, without success. Throughout, "length" refers to the number of symbols, not lines, in a proof....

13
votes

0
answers

497
views

### Is there a logical relationship between constructions of the reals and proof methods in real analysis?

In my elementary real analysis course three years ago, I remember noting that there seemed to be 3 main ways of proving the main theorems about continuity. There was Bolzano-Weierstrass, continuous ...

4
votes

0
answers

152
views

### Is there a simple proof of consistency of EA?

Let $\mathsf{EA}+\mathsf{CE}$ be elementary arithmetic with cut elimination theorem. Is there a simple (1-)consistency proof of $\mathsf{EA}$ over $\mathsf{EA}+\mathsf{CE}$? I think that a naïve ...

9
votes

1
answer

317
views

### Is Heyting arithmetic sufficient to prove its own (formalized) existence property?

Let $\mathsf{HA}$ denote first-order Heyting arithmetic (viꝫ., Peano axioms with unrestricted recursion scheme, in first-order intuitionistic logic). It is known (e.g., Troelstra & van Dalen, ...

4
votes

1
answer

148
views

### Are bi-embeddable dilators equal?

In Girard's $\Pi^1_2$-logic, a dilator $D$ is a endofunctor which commutes with pull-back and direct limit on $\mathrm{ON}$, the category whose objects are ordinals and morphisms are strictly ...

3
votes

1
answer

279
views

### Does ACA prove categoricity of the reals?

$\def\f#1{\text{#1}}$Does $\f{ACA}$ prove that any two internally complete ordered fields are isomorphic?
Here internal completeness is expressed roughly as "every sequence of reals with an upper ...

2
votes

1
answer

138
views

### Is adding all sentences true of terms in skolemized theory conservative?

Suppose I have a (incomplete) theory $T$ (e.g. PA) which I skolemize to get a theory $T_S$ in the expanded language. I now build $T'$ by adding to $T_S$ any sentence $(\forall x)\phi(x)$ where I can ...

5
votes

0
answers

144
views

### Ordinal strength of iterated truth theories

Consider the theory ${\rm PA}^{\mathbb{T}}$ obtained by adding a truth predicate to Peano arithmetic, applicable to sentences of the unaugmented language and satisfying the compositionality axioms $\...

0
votes

0
answers

59
views

### How is paramodulation used in practice?

This might be more suitable for CS StackExchange, but I'm not sure.
The paramodulation rule is:
$$\frac{P[t]\lor L_1\qquad r = s \lor L_2}{P[s\sigma] \lor L_1 \sigma \lor L_2\sigma}\, \sigma\textrm{ ...

6
votes

1
answer

219
views

### Criterion for the consistency of pure type systems

Pure type systems are characterized in an almost combinatorial way: a set of axioms $\star_i : \star_j$, and a set of triples $(\star_i, \star_j, \star_k)$ saying when the dependent product $\prod_{x :...

2
votes

0
answers

152
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

121
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

142
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

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

15
votes

3
answers

825
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

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

3
votes

1
answer

609
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

343
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

56
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

134
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

170
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

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

9
votes

1
answer

554
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

272
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

143
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

195
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

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

194
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

1
answer

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

5
votes

1
answer

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

10
votes

1
answer

284
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

169
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

683
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

287
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

268
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

123
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

248
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

122
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

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

5
votes

1
answer

319
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

36
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

2
answers

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

10
votes

1
answer

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