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. ...
- 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 ...
- 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 ...
- 63
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 ...
- 11
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 ...
- 18.2k
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 ...
- 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 ...
- 7,891
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) ...
- 18.2k
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 ...
- 481
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 ...
- 131
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 ...
- 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 ...
- 1,276
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'...
- 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 ...
- 18.2k
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 \...
- 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}$ ...
- 18.2k
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 ...
- 1,968
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 ...
- 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 ...
- 4,471
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 ...
- 18.2k
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 $...
- 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 ...
- 5,742
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 ...
- 216k
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,...
- 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 ...
- 510
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, ...
- 510
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 ...
- 510
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 ...
- 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 ...
- 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 $\...
user158501
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 ...
- 510
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 ...
- 482
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 ...
- 482
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 ...
- 1,276
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 $\...
- 18.2k
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....
- 18.2k
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 ...
- 295
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 ...
- 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, ...
- 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 ...
- 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 ...
- 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 ...
- 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 $\...
- 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 :...
- 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 ...
- 3,044
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 ...
- 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 ...