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

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}$ ...
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 ...
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 ...
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 ...
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 ...
192 views

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