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
200 views

Are there atoms in the lattice of intermediate logics?

A few days ago I stumbled upon this question on MS. The question is: Does the lattice of intermediate logics have an atom, i.e. an element that is strictly stronger than IPC but not strictly stronger ...
Navid's user avatar
  • 31
4 votes
1 answer
102 views

Does this hierarchy of fragments of $I \Sigma_1$ collapse?

Does anyone know whether the following hierarchy of fragments of $\mathrm{I} \Sigma_1$ (or rather $\mathrm{I} \Pi_1$) collapses or not? Let $\Sigma^b_n$ denote formulas in the language of arithmetic ...
Lukas Holter Melgaard's user avatar
5 votes
0 answers
143 views

Higher-order equivalence of ordinals

I wonder which ordinals are second-order equivalent, and similarly for other logical equivalences. Let the signature be fixed and include only <. For concreteness, let us first ask for the first ...
Alexey Slizkov's user avatar
1 vote
1 answer
173 views

Gödel coding and the function $z(x)$

The function $z(x)$ that associates to each formula $\alpha$ of $P$ its Gödel number $z(\alpha)$ is external to the system. How then can expressions in which $z(x)$ be involved be expressed in $P$? ...
Speltzu's user avatar
  • 169
6 votes
0 answers
100 views

Is PA interpretable in PRA + TI(<epsilon_0)?

By Gentzen's consistency proof, we know that PA has the same consistency strength as PRA + TI(<epsilon_0). Question: is PA interpretable in PRA + TI(<epsilon_0)? For simplicity, let us assume ...
Stephen Mackereth's user avatar
4 votes
0 answers
141 views

Can this theory of dyadic rationals prove that multiplying by three is the same as summing thrice?

(This question arose from a discussion with Jade Vanadium about a theory of dyadic rationals.) Let $T$ be the 2-sorted FOL theory with sorts $ℕ,ℚ$ and constant-symbols $0,1$ and binary function-...
user21820's user avatar
  • 2,734
2 votes
0 answers
74 views

Is monotonicity redundant in this definition of Tarskian logics?

Given a logic over a language $L$, which has a consequence relation $\vdash$. This logic is Tarskian if for every $\Gamma \cup \Delta \cup {\alpha} \subseteq L$: If $\alpha \in \Gamma$, then $\Gamma \...
NJay's user avatar
  • 21
1 vote
2 answers
83 views

Hardness of a Hybrid problem combining knapsack and scheduling

I am trying to prove whether the following problem is NP-hard or not: Items with a certain length arrive in a fixed sequence and must be assigned to one of two containers which are constrained in ...
Christian's user avatar
14 votes
5 answers
2k views

How is it possible for PA+¬Con(PA) to be consistent?

I'm having some trouble understanding how a certain first-order theory isn't just straight-up inconsistent. Let $PA$ be the axioms of (first-order) Peano arithmetic and let $C$ be the following ...
E8 Heterotic's user avatar
5 votes
2 answers
646 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,140
6 votes
1 answer
231 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
  • 596
6 votes
1 answer
174 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
1k 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
102 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
6 votes
0 answers
146 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. Note on terminology: "admissible", "$(^+)$-stable", and "$\Pi^1_1$-...
C7X's user avatar
  • 1,186
-2 votes
1 answer
188 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
262 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
190 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
302 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
327 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,774
1 vote
0 answers
104 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
597 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
161 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
170 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
353 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,076
8 votes
1 answer
306 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
916 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
6 votes
1 answer
224 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
652 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
198 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
119 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
175 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
321 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
103 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
135 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
296 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
  • 861
2 votes
0 answers
231 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,551
1 vote
0 answers
88 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
198 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
149 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
185 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
141 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
465 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
7 votes
1 answer
342 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
539 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
188 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
447 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
  • 29.8k

1
2 3 4 5
8