# 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
Filter by
Sorted by
Tagged with
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 ...
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 ...
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 ...
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 ...
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&...
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 ...
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 ...
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 ...
49 views

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 ...
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 ...
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 ...
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. ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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)$....
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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. ...
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 ...
375 views

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$. ...
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 ...
370 views

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