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.

Filter by
Sorted by
Tagged with
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 ...
user avatar
  • 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 $\...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
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 $\...
user avatar
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....
user avatar
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 ...
user avatar
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 ...
user avatar
  • 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, ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
  • 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 $\...
user avatar
  • 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{ ...
user avatar
  • 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 :...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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&...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
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} \...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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[(\...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
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)$....
user avatar
  • 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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 49.2k

1
2 3 4 5
7