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
0answers
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
1answer
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
0answers
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
1answer
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
3answers
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
0answers
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
1answer
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
1answer
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
0answers
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
0answers
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
0answers
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
1answer
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
0answers
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
2answers
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
0answers
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
0answers
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
3answers
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
0answers
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
0answers
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
1answer
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
1answer
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
0answers
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
2answers
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
1answer
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
1answer
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
0answers
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
1answer
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
1answer
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
1answer
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
1answer
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
0answers
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
0answers
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
1answer
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
2answers
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
0answers
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
1answer
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
0answers
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
0answers
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
0answers
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
1answer
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
0answers
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
1answer
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
1answer
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
1answer
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
0answers
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
0answers
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
0answers
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
1answer
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
0answers
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
0answers
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 ...
