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 ...
- 1,525
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 $\...
- 101
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 ...
- 213
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 ...
- 442
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 ...
- 442
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 $\...
- 21.7k
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....
- 21.7k
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 ...
- 173
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 ...
- 178
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, ...
- 21.7k
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 ...
- 178
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,576
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 ...
- 1,525
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 $\...
- 37.2k
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{ ...
- 417
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 :...
- 417
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 ...
- 2,844
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 ...
- 442
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&...
- 153
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 ...
- 101
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 ...
- 4,061
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}
\...
- 11
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 ...
- 505
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 ...
- 10.2k
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 ...
- 1,577
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[(\...
- 21.7k
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 ...
- 615
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 ...
- 141
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 ...
- 21.7k
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 ...
- 141
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 ...
- 153
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 ...
- 169
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 ...
- 7,061
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 ...
- 157
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 ...
- 1,713
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,525
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 ...
- 1,713
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 ...
- 1,713
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 ...
- 1,708
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 ...
- 21.7k
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)$....
- 161
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 ...
- 1
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 ...
- 21.7k
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 ...
- 49.2k