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

341
questions

3
votes

1
answer

250
views

### MIP*=RE theorem and its impact on logic and proof theory

In the monumental paper MIP*=RE five authors, Zhengfeng Ji, Anand Natarajan, Thomas Vidick, John Wright, and Henry Yuen, managed to show that two complexity classes: RE and MIP* do in fact coincide. ...

2
votes

0
answers

110
views

### Existence property for second-order propositional logic

Consider the intuitionistic second-order propositional calculus (SOL) formulated in the full $\wedge,\vee,\rightarrow,\bot,\top,\forall,\exists$ language.
Question: Assume that $\Gamma$ and $\Psi$ are ...

6
votes

1
answer

150
views

### Consistency in pure type systems

Summary
My question is about how (i) a certain presentation of pure type systems in the $\lambda$-cube, bears on (ii) a standard definition of consistency in pure type systems. In short, I'm ...

1
vote

0
answers

501
views

### Possible cardinalities of the sets tautologically implied by minimal sets

Question
Consider the set $V$ of all unordered 3-clauses $(l_1, l_2, l_3)$, where $l_i$ is a literal (i.e. a variable $x$ or its negation $\neg x$), and no clause contains two literals having the same ...

7
votes

0
answers

90
views

### How tightly are decidability and "induction-completeness" linked?

It is known that there are a number of expansions of the structure $\mathfrak{N}:=(\mathbb{N};+)$ which are decidable (= have computable theories); one such example is the expansion by a predicate ...

5
votes

0
answers

79
views

### Iterated $\Pi^1_1$-reflection and non-Gandiness underrepresented in ordinal analyses?

This is a copy of Math StackExchange question #4395977, which I felt was more appropriate for MathOverflow.
The admissible ordinals $\alpha$ s.t. the supremum of $\alpha$-recursive well-orderings is ...

-2
votes

1
answer

179
views

### Can we have consistent theories stating opposing provability statements that are non-standardly coded?

I want to coin a notion of "strong provability", to be defined as:
$S$ is strongly provable in $T$ if and only if there is a Gödel code of its proof in $T$ that is strictly smaller than any ...

22
votes

4
answers

3k
views

### Brute force open problems in graph theory

Usually, a graph theoretic problem asks whether some class of graphs $C$ possesses a quality $P$. For example, $C$ is the class of all graphs and $P$ is the reconstructability property in Kelly-Ulam ...

5
votes

2
answers

245
views

### Is the usual enumeration of $\mathsf{PA}$ "minimal for consistency strength"?

This question is about a technical imprecision which is easily avoidable but whose details I'd like to understand better. When we refer to "the consistency strength of $\mathsf{PA}$" (say) ...

8
votes

0
answers

173
views

### Is there an Arithmetized Completeness theorem for intuitionistic theories?

For classical theories, Henkin's completeness proof can be arithmetized. This leads to the result that for classical theories $T$ and $S$ if $\sigma$ is a formula enumerating $S$ in $T$ then $S \leq T ...

0
votes

0
answers

299
views

### A question regarding an unprovability proof

Let LA denote polynomial time arithmetic, Con_LA the equation stating the
consistency of LA, LAJ the system LA+Con_LA, and E2A double exponential time
arithmetic.
A manuscript of mine provides a proof ...

7
votes

1
answer

309
views

### Does Mostowski's collapsing lemma prove $\Delta_0$-transfinite recursion?

Let $\mathsf{T}$ be the theory comprising Extensionality, Foundation (stating every set has an $\in$-minimal element), Pairing, Infinity, Union, $\Delta_0$-Separation, and the closure under ...

1
vote

0
answers

92
views

### Is there an error in W. Buchholz's paper "A simplified version of local predicativity"?

I want to self-learn proof theory. It seems that the operator controlled derivation method is important in this field, and the paper in the title is the first paper that uses this method.
So I'm ...

6
votes

3
answers

547
views

### Is the union of two conservative extensions of a theory conservative?

Background/Motivation
A theory T over a signature(language) Σ is a set of formulae over Σ. These formulae are called the non-logical axioms of T.
To talk about what is provable in T we can agree on ...

2
votes

1
answer

156
views

### How can Kőnig's Lemma be expressed in Monadic Second-Order Logic of 2 Successors?

I read the following on Wikipedia's page on Monadic Second-Order Logic of Two Successors (MS2S):
Weak S2S (WS2S) requires all sets to be finite (note that finiteness
is expressible in S2S using Kőnig'...

3
votes

0
answers

163
views

### Are "very conservative" connectives already definable?

I'm sadly an outsider to nonclassical propositional logics. All terminology below comes from Humberstone's book The Connectives, specifically section 4.2.
A new connective - a bit more precisely, a ...

5
votes

1
answer

341
views

### A possible flaw in Theorem 14.17 in Kurt Schütte's -Proof Theory-

Reading Chapter V, pages (73-97) in Proof Theory (Springer, 1977), by Kurt Schütte, I have encountered a peculiar problem which puzzles me.
On page 96, a map $\rm{Nr}:\overline{\rm{OT}}\rightarrow \...

8
votes

1
answer

276
views

### Modal logic of "mostly-satisfiability"

For $n\in\omega+1$ let $\mathsf{ZFC}_n$ be $\mathsf{ZC}$ + $\{\Sigma_k$-$\mathsf{Rep}: k<n\}$. Let $\widehat{\mathsf{ZFC}}$ be the strongest consistent theory $\mathsf{ZFC}_n$ (so if $\mathsf{ZFC}$ ...

9
votes

2
answers

898
views

### What theories are larger than the real closed field but still decidable?

It's well known that sentences about the real closed field can be decided by algorithm and the complexity of this is about $d^{2^{O(n)}}$ where $d$ is the product of the degrees of polynomials in the ...

9
votes

4
answers

2k
views

### Computational complexity theoretic incompleteness: is that a thing?

Has anyone done research in an area that I have not heard of but that I want to call "Computational complexity theoretic incompleteness", which would mean not absolute incompleteness in the ...

7
votes

1
answer

187
views

### Does $\text{ACA}_0$ + True Arithmetic prove the well-foundedness of every recursive ordinal?

As discussed in Noah Schweber's answer to What is the proof-theoretic ordinal of true arithmetic?, it is somewhat ambiguous what “the proof-theoretic ordinal of True Arithmetic” might mean. In one ...

13
votes

1
answer

638
views

### Are there different "levels" of self-referentiality in arithmetic?

Below, all sentences/formulas are first-order and in the language of arithmetic. For simplicity, we conflate numbers and numerals, and conflate sentences/formulas and their Godel numbers.
Given a ...

3
votes

0
answers

192
views

### Self-referential Quinean proof of Löb's Theorem

Given its relevance for Open-source game theory, Dr. Andrew Critch asks the following about provability logic:
We conjecture that Löb’s Theorem can be proven without the use of the
modal fixed point $...

2
votes

1
answer

104
views

### Axiomatization of S2S

What is a reasonable axiomatization of S2S?
S2S is the monadic second order theory with two successors (Wikipedia link). It has finite binary strings, operations $s→s0$ and $s→s1$ on strings, and ...

32
votes

2
answers

1k
views

### What is the logical status of the sentence combining the ideas of Löb and Rosser, "this sentence is provable before any proof of its negation"?

Logicians are familiar with the variety of self-referential sentences expressible in the language of arithmetic:
The Gödel sentence, "this sentence is not provable", which indeed is not ...

4
votes

1
answer

150
views

### Extending the class of primitive recursive functions with higher order recursion schema

I'm trying to extend the class of primitive recursive functions by extending the recursion schema over higher types.
We usually define the class of primitive recursive functions by using zero function,...

4
votes

0
answers

312
views

### Is this linearly distributive category really free?

In Natural deduction and coherence for weakly distributive categories Blute et al. claim to give a presentation of the free (non-symmetric) linearly distributive category $\operatorname{PNet_E}(C)$ on ...

2
votes

0
answers

97
views

### Empires and the net criterion

Currently, I am struggling to understand the proof of Proposition 2.5 on page 250 (page 22 in the document) of the paper Natural deduction and coherence for weakly distributive categories by Blute, ...

4
votes

0
answers

126
views

### Correctness criteria for proof nets

In their paper Natural deduction and coherence for weakly distributive categories Blute, Cockett, Seely and Trimble introduce so-called proof circuits (aka two-sided proof structures) for the positive ...

4
votes

1
answer

287
views

### Quantification over uncountable sets

If some statements below are too imprecise/peculiar, please note that this is mostly due to my own lack of knowledge/understanding. Nevertheless, I will try to phrase the actual question in a more ...

2
votes

0
answers

222
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
vote

0
answers

85
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

1
answer

191
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

136
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

178
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

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

11
votes

0
answers

457
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

320
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

531
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

179
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

407
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

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

4
votes

1
answer

322
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

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

6
votes

0
answers

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

7
votes

1
answer

320
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

177
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

177
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

172
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

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