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
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. ...
truebaran's user avatar
  • 9,040
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 ...
Z. A. K.'s user avatar
  • 271
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 ...
Spaceka13's user avatar
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 ...
ale64bit's user avatar
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 ...
Noah Schweber's user avatar
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 ...
C7X's user avatar
  • 804
-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 ...
Zuhair Al-Johar's user avatar
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) ...
Noah Schweber's user avatar
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 ...
Spencer Woolfson's user avatar
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 ...
Martin Dowd's user avatar
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 ...
Hanul Jeon's user avatar
  • 2,317
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 ...
Reflecting_Ordinal's user avatar
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 ...
Giacomo Cozzi's user avatar
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'...
hatch22's user avatar
  • 123
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 ...
Noah Schweber's user avatar
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 \...
Victor's user avatar
  • 2,036
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}$ ...
Noah Schweber's user avatar
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 ...
Sidharth Ghoshal's user avatar
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 ...
Hank Igoe's user avatar
  • 193
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 ...
Keshav Srinivasan's user avatar
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 ...
Noah Schweber's user avatar
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 $...
Martín S's user avatar
  • 421
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 ...
Dmytro Taranovsky's user avatar
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 ...
Joel David Hamkins's user avatar
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,...
Jii's user avatar
  • 301
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 ...
Max Demirdilek's user avatar
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, ...
Max Demirdilek's user avatar
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 ...
Max Demirdilek's user avatar
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 ...
SSequence's user avatar
  • 821
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 ...
Peter Gerdes's user avatar
  • 2,419
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 $\...
user avatar
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 ...
Max Demirdilek's user avatar
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 ...
Boris Dimitrov's user avatar
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 ...
Boris Dimitrov's user avatar
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 ...
Reflecting_Ordinal's user avatar
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 $\...
Noah Schweber's user avatar
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....
Noah Schweber's user avatar
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 ...
Oddly Asymmetric's user avatar
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 ...
Alwe's user avatar
  • 178
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, ...
Gro-Tsen's user avatar
  • 27.8k
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 ...
Alwe's user avatar
  • 178
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 ...
user21820's user avatar
  • 2,678
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 ...
Peter Gerdes's user avatar
  • 2,419
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 $\...
Nik Weaver's user avatar
  • 40.9k
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 :...
Trebor's user avatar
  • 770
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 ...
Frode Alfson Bjørdal's user avatar
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 ...
Rise of Kingdom's user avatar
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 ...
Not_Here's user avatar
  • 462
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 ...
Rise of Kingdom's user avatar

1
2 3 4 5
7