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

365
questions

1
vote

0
answers

77
views

### Realizing arithmetic hierarchy in algebraic number theory

Is it possible to realize arithmetic hierarchy in algebraic number theory?
For example, consider a $\Pi^0_4$ statement of the form $\forall x \exists y \forall z \exists w \phi(x,y,z,w)=0$ where $\phi$...

23
votes

0
answers

535
views

### Which proofs of the fundamental theorem of algebra are "essentially the same" vs. "essentially different"?

The classic MO thread Ways to prove the fundamental theorem of algebra contains $60$ proofs of FTA, and I'm sure there are many more in the literature. It would be nice to have some way to organize ...

1
vote

1
answer

196
views

### Minimal Turing machines associated to math statements

It is known that some famous Number Theoretic problems are equivalent to halting of specific Turing machines:
Goldbach conjecture holds iff a 47 state TM halts
Lagarias' formulation of Riemann ...

16
votes

1
answer

978
views

### Proving that ZF is Artemov-consistent

As discussed in another MO question, Sergei Artemov has proposed that the standard formalization Con(PA) of "PA is consistent" is flawed, and has proposed a different way to formalize "...

-6
votes

1
answer

413
views

### Is it true AI achieves silver-medal standard solving IMO problems (2024UK)? [closed]

I am always interested in the development of AI within mathematics, particularly in number theory. I read on this website that AI has achieved a silver-medal level in solving IMO problems, which has ...

8
votes

0
answers

147
views

### Is there a substructure-preservation result for FOL in finite model theory?

It's well-known$^*$ that the Los-Tarski theorem ("Every substructure-preserved sentence is equivalent to a $\forall^*$-sentence") fails for $\mathsf{FOL}$ in the finite setting: we can find ...

5
votes

0
answers

94
views

### Computational view of subsystems of second-order arithmetic

If System T "corresponds" to full first-order arithmetic, and System F (λ2) corresponds to full second-order arithmetic, what type systems would be associated with weaker fragments, ...

6
votes

0
answers

278
views

### Bounding proofs of transfinite induction

Let $\phi$ be a "reasonable" formula in the language of first-order arithmetic expressing some amount of transfinite induction along a given (index for a) computable linear order; my default ...

4
votes

0
answers

97
views

### Computational complexity of arithmetic sentences over classical theories

Below, I use the term "tracker" rather than "realizer" since I'm not requiring the relevant objects to be computable.
Define the relation "$f$ tracks $\varphi$" for $f:\...

4
votes

1
answer

171
views

### Further research on relevant realizability etc

I just read Dunn's 1979 paper Relevant Robinson's Arithmetic, and the end especially caught my interest. Following the surprising role of constant functions in collapsing "relevant Q with zero&...

1
vote

0
answers

99
views

### Effortless automated proofs for "simple" formulae?

From small cases to all of them. This is in the spirit of 15 theorem see https://en.wikipedia.org/wiki/15_and_290_theorems
EXAMPLE : Suppose you have the following problem: P(a)
For any fixed non ...

4
votes

0
answers

160
views

### In finite model theory, is "invariant FOL with $\varepsilon$-operator" unavoidably second-order?

Throughout, all structures are finite.
Say that a class of finite structures $\mathbb{K}$ is $\mathsf{FOL}_\varepsilon^\text{inv}$-elementary iff it is the class of finite models of a sentence in the ...

3
votes

1
answer

122
views

### $\Pi^0_1$ sentences modulo "schematic entailment"

Let $\mathfrak{P}$ be the preorder of $\Delta^0_0$ (= only bounded quantifiers) formulas with one free variable in the language of arithmetic, under the relation $\alpha(x)\le\beta(x)$ iff there is a ...

4
votes

1
answer

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

4
votes

1
answer

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

5
votes

0
answers

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

1
vote

1
answer

187
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$? ...

6
votes

0
answers

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

4
votes

0
answers

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

2
votes

0
answers

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

1
vote

2
answers

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

15
votes

5
answers

3k
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 ...

6
votes

2
answers

1k
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. ...

6
votes

1
answer

250
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

218
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

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

7
votes

0
answers

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

6
votes

0
answers

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

-2
votes

1
answer

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

23
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

276
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) ...

9
votes

0
answers

199
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

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

7
votes

1
answer

332
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

113
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

622
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

166
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

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

5
votes

1
answer

359
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

325
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

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

6
votes

1
answer

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

14
votes

1
answer

671
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

206
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

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

33
votes

2
answers

2k
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

201
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

326
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

104
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, ...