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.

**2**

votes

**0**answers

52 views

### Lengths of proofs and quasilinear time

Length of proofs depends not only on the theory but also on its axiomatization. Once an axiomatization is fixed, typical proof systems are equivalent up to a polynomial factor. But what if we care ...

**26**

votes

**9**answers

4k views

### “Strange” proofs of existence theorems [on hold]

This question isn't related to any specific research. I've been thinking a bit about how existence theorems are generally proven, and I've identified three broad categories: constructive proofs, ...

**18**

votes

**2**answers

833 views

### Has Apéry's proof of the irrationality of $\zeta(3)$ ever been used to prove the irrationality of other constants?

Apéry's proof of the irrationality of $\zeta(3)$ astounded contemporary mathematicians for its wealth of new ideas and techniques in proving the irrationality of a known constant. It is often the case ...

**3**

votes

**1**answer

365 views

### Going beyond the strength of Peano arithmetic “without sets”

First-order arithmetic is fairly weak, as measured for example by its consistency strength. When a stronger theory is desired, it is common to work with (fragments of) second-order arithmetic or set ...

**3**

votes

**0**answers

57 views

### Reasonable reference index or list of the interpretability/consistency hierarchy

In Kanamori's The Higher Infinite a diagram is included towards the end of the book which illustrates the large cardinal hierarchy by listing many large cardinal axioms and drawing their direction ...

**7**

votes

**4**answers

456 views

### What would $\mathcal{P} \neq \mathcal{NP}$ tell us about some non-constructive proofs?

Let me sum up my - hopefully correct - understanding of the travelling salesman problem and complexity classes. It's about decision problems:
"[...] a decision problem is a problem that can be ...

**3**

votes

**3**answers

306 views

### How can you formalize the metamathematics conventionally used to state Godel’s theorem?

Gödel’s incompleteness theorem states that for any sufficiently strong formal system $T$ there exists a statement $G$ such that if $T$ is consistent, then $G$ is true but not provable in $T$. But I’m ...

**8**

votes

**0**answers

199 views

### What metatheory proves cut elimination for Simple Type Theory?

Gaisi Takeuti's book Proof Theory proves cut elimination for Simple Type Theory (a combined result of several researchers). Thus it proves consistency of Simple Type Theory with full comprehension in ...

**6**

votes

**1**answer

150 views

### Correspondence between proof-theoretic ordinals and fast growing functions?

For theories with well known proof-theoretic-ordinals, (what) is there a correspondence between their proof-theoretic-ordinal and (ordinal indexed families of?) fast growing functions provable total ...

**6**

votes

**1**answer

225 views

### Am I counting quantifiers correctly?

I think this is right but I want to check. The theory $\mathsf{WKL}^*_0$ is conservative over EFA for $\Pi^0_2$ sentences. And the first order part of $\mathsf{WKL}^*_0$ is axiomatized by EFA plus ...

**2**

votes

**0**answers

48 views

### Substructural shuffling: can we avoid a modal collapse in a certain Intuitionistic modal logic via making the logic linear?

Consider Propositional Lax Logic ($PLL$)
https://www.uni-bamberg.de/fileadmin/uni/fakultaeten/wiai_professuren/grundlagen_informatik/papersMM/pll.pdf
The Hilbert system of $PLL$ takes as axiom ...

**2**

votes

**1**answer

151 views

### Can we avoid the modal collapse in a certain Intuitionistic modal logic by abandoning ¬◯⊥ but retaining the law of the excluded middle?

Consider Propositional Lax Logic ($PLL$)
https://www.uni-bamberg.de/fileadmin/uni/fakultaeten/wiai_professuren/grundlagen_informatik/papersMM/pll.pdf
The Hilbert system of $PLL$ takes as axiom ...

**2**

votes

**1**answer

126 views

### Modal collapse upon addition of the law of the excluded middle to an Intuitionistic modal logic

Consider Propositional Lax Logic ($PLL$)
https://www.uni-bamberg.de/fileadmin/uni/fakultaeten/wiai_professuren/grundlagen_informatik/papersMM/pll.pdf
The Hilbert system of $PLL$ takes as axiom ...

**6**

votes

**1**answer

315 views

### What is this property exhibited by some logical systems?

I'm migrating this question from MSE to MO, as in the span of five months, it received 6 upvotes but no answers. If my language needs to be fine-tuned in any way, constructive suggestions and guidance ...

**1**

vote

**1**answer

133 views

### Is Calculus of Constructions type inhabitance semi-decideable?

I'm wondering if type inhabitance for the calculus of constructions is semi-decideable. I know the following:
System F inhabitance and, correspondingly, second-order unification are semi-decideable
...

**7**

votes

**1**answer

191 views

### Independent/Easy fraction of sentences over PA

Let $S(n)$ be the set of all sentences over PA of length at most $n$ (counting the quantifier symbols, boolean connectives, arithmetic operations and constants, and counting each variable as length $1$...

**8**

votes

**0**answers

194 views

### Unprovable integer identity involving exponentiation

I was thinking about Tarski's problem, and was wondering what happens if we have a theory $T$ with two sorts $N,Z$ with intended interpretations $\def\nn{\mathbb{N}}$$\def\zz{\mathbb{Z}}$$\nn,\zz$ ...

**5**

votes

**2**answers

533 views

### What things does ZFC not know if it knows?

The statement "ZFC $\vdash 0=1$" is independent of ZFC due to Goedel's second incompleteness theorem. That got me wondering, for what other statements $\phi$ is "ZFC $\vdash \phi$" independent of ZFC?
...

**50**

votes

**8**answers

7k views

### What does it mean to suspect that two conjectures are logically equivalent?

Here's a familiar conversation:
Me: Do you think Conjecture A and Conjecture B are equivalent?
Friend: Yes, because I think they're both true.
Me: [eye roll] You know what I mean...
Does there ...

**6**

votes

**1**answer

309 views

### Is ZFC+(negation of a large cardinal axiom) arithmetically sound?

My knowledge in set theory is very limited, so I apologize if this question is naive or trivial:
Let $A$ to be a large cardinal axiom. $T=ZFC+\neg A$ is a consistent theory. My question is:
Question ...

**8**

votes

**2**answers

351 views

### cut-elimination provable in PRA

What is the standard reference for the provability of the cut-elimination theorem in PRA?
Update: Rasmus Blanck has offered a reference for a system other than Gentzen's $\mathfrak L \mathfrak K$. ...

**7**

votes

**1**answer

328 views

### Is there good reference for proof complexity?

I am asking if there are some good or standard references for proof complexity theory? I didn't find references when I search in internet. Thanks!

**1**

vote

**0**answers

73 views

### Question Regarding Hierarchies of Functions

The more precise statement of this question is partly inspired by the question Extensions of fast-growing hierarchy. However, I didn't want to derail the original question (since the OP may have ...

**6**

votes

**1**answer

200 views

### Provability in $S^1_2$

What are some examples of natural true statements of the form $∀n φ(n)$ ($φ$ is a polynomial time computation/test) that are unprovable in $S^1_2$?
Examples may be unconditional or dependent on ...

**9**

votes

**2**answers

537 views

### Adding nonconstructive disjunction to intuitionistic logic

In constructive mathematics, under realizability interpretations, we can define nonconstructive disjunction $A⅋B$ as follows:
A witness for $A⅋B$ gives a candidate witness for $A$ and a candidate ...

**6**

votes

**0**answers

139 views

### $Π^0_1$ Proof Ordinals

Natural theories extending EFA (exponential/elementary function arithmetic) are well-ordered by $Π^0_1$ provability, and we would like a formal definition of the well-ordering that is robust yet as ...

**9**

votes

**1**answer

196 views

### Complexity of induction formulas in proof theoretic ordinals

According to The Art of Ordinal Analysis, the proof theoretic ordinal of a theory $T$ is the least ordinal $\alpha$ such that:
$${\bf ERA}+TI(\alpha,ECP)\vdash Con(T)$$
In above definition, $ECP$ ...

**9**

votes

**1**answer

349 views

### Cut-free proofs in ZFC

If a statement $P$ has a ZFC proof of length $n$, must it also have a cut-free ZFC proof of length polynomial in $n$?
By a cut-free ZFC proof, I mean a proof in sequent calculus without cut rule of ...

**7**

votes

**3**answers

526 views

### Notable examples of syntactic proofs whose existence is guaranteed by completeness, but having been found later than a semantic proof?

Question.
What are examples (preferably documented and explicitly commented on from this perspective in the literature, preferably in an article dedicated to this aspect alone) of the following well-...

**12**

votes

**5**answers

587 views

### Asymmetric $A \iff B$ proofs

When proving that conditions $A$ and $B$ are equivalent, it is often an arbitrary choice whether to first prove $A\implies B$ or $B\implies A$. Are there examples where the second implication uses the ...

**7**

votes

**1**answer

217 views

### Axiomatizations of arithmetical parts of theories

For common theories that talk about something more general than first-order arithmetic (e.g. set theories and subsystems of second-order arithmetic), are there nice axiomatizations of their arithmetic ...

**5**

votes

**4**answers

459 views

### Mathematical induction vis-a-vis primes

One of the most used proof-techniques is mathematical induction, and one of the oldest subjects is the study of prime numbers. Thanks to Euclid, we can consider the primes as a infinite monotone ...

**7**

votes

**1**answer

197 views

### Weird analogy between quadratic forms and formal systems

A fundamental connection between provability and consistency for formal systems is that, if $Q$ is a formal system and $A$ is a sentence in the language of $S$, then
$Q$ proves $A$ if and only if $...

**0**

votes

**0**answers

197 views

### Is it believed that the Baillie-PSW test is (un)likely to be deterministic?

Given that the Baillie-PSW primality test is currently (as of 2017) the 'state-of-the-art' test for whether large integers are prime, I'm interested in knowing more about the consensus of ...

**4**

votes

**0**answers

230 views

### the strength of saying “each sentence of true arithmetic has a recursive proof”

Let $PA_{\omega}$ be just like $PA$ except that $PA_{\omega}$-proofs can use any number of applications of the recursive $\omega$-rule.
The recursive $\omega$-rule allows the following:
For each ...

**1**

vote

**0**answers

148 views

### Is there a Carnap-Gödel style account of the undecidability of the Halting Problem?

The proof of Gödel's incompleteness theorem can be streamlined by means of the Carnap-Gödel diagonal lemma and the ensuing fixed point theorem $\vdash_S G\leftrightarrow\lnot\Pi\ulcorner G\urcorner$ ...

**4**

votes

**1**answer

187 views

### $f_{\epsilon_0}$ and provably total functions in $PA$

A total recursive function $f(x)$ is provably total in $PA$ if there's some formula $\phi(x,y)$ such that
$f(x)=y \iff PA\vdash \phi(x,y)$ and
$PA\vdash \forall x \exists y \phi(x,y)$
I know (not in ...

**2**

votes

**0**answers

172 views

### $P=NP$ and provability of family of propositional formulas

Let $\mathcal{L}'=\{+,\cdot,0,S,=,<,||,\#,R\}$ be the lanugage of bounded arithmetic with a $k$-ary relation $R$.
For every bounded sentence $\phi({\bf\bar{n}})$ in $\mathcal{L}'$ define ...

**11**

votes

**0**answers

185 views

### How much can “(recursively) large ordinal axioms” prove?

In "Collapsing functions based on recursively large ordinals: A well–ordering proof for KPM", Michael Rathjen shows that certain notations for the proof-theoretic ordinals of theories, which ...

**4**

votes

**1**answer

180 views

### The difference between KP+Inf+Pow and Z

I'd like to clarify some details about the theories Z (= Zermelo set theory) and KP+=KP+Infinity+Powerset (KP is Kripke-Platek set theory).
In this paper (M1), Mathias claims that Z+KP is consistent ...

**2**

votes

**0**answers

289 views

### When must one strengthen one's induction hypothesis?

My questions are about the phenomenon that in order to prove a fact $\forall x \phi(x)$ by induction, sometimes straightforward induction "does not work" and instead one "must" use a "stronger" ...

**15**

votes

**2**answers

869 views

### Who first proved that we can prove that we prove things we prove?

Sorry about the title, I couldn't resist.
It's a classic fact that, not only does $PA$ prove every true $\Sigma_1$ sentence, but $PA$ proves that $PA$ proves every true $\Sigma_1$ sentence! In ...

**9**

votes

**2**answers

318 views

### Admissibility of Harrop's rule, computationally

It is obvious that the following formula is not a theorem of
intuitionistic propositional calculus (IPC).
$$
(\neg A \; \to \; B \vee C) \;\; \to \;\;
((\neg A \; \to \; B) \vee (\neg A \; \to \; ...

**6**

votes

**1**answer

232 views

### Pure first order logic formulations of Markov's principle

Markov's principle is a statement of constructive arithmetic that allows classical reasoning on formulas of the shape $\exists x P$ when $P$ is a recursive predicate:
$\neg \neg \exists x P \to \...

**5**

votes

**2**answers

634 views

### What exactly is a judgement?

Before formulating my question, let me briefly sum up what I know about the topic (feel free to correct me if something I claimed is false!). This is for you good to see what my state of knowledge is, ...

**7**

votes

**3**answers

409 views

### What is the definition of computational content?

I am interested in type theory and proof theory. I have read a lot of papers and books that use the term "computational content" (For example: https://scholar.google.com/scholar?hl=en&q=%...

**3**

votes

**0**answers

54 views

### Equational theory for resolution proof system

Is there any equational theory $T$ like $PV$ with following properties:
If $T\vdash f=g$ for terms $f$ and $g$, translation of $f=g$ to propositional formulas has polynomial resolution proof.(like $...

**1**

vote

**0**answers

119 views

### eliminating contraction

I'd like to better understand the role of the contraction rule in Gentzen's $\mathsf{LK}$. I would like to have an example of a derivable sequent that is no longer derivable if the contraction rule is ...

**8**

votes

**4**answers

2k views

### The Halting Problem and Church's Thesis

In the opening chapters of Hartley Rogers, Jr.'s book Theory of Recursive Functions and Effective Computability, the proofs of the unsolvability of the halting problem and related unsolvability ...

**5**

votes

**0**answers

62 views

### Medium Growing Hierarchy

I want to bound some functions using the fast-growing hierarchy, but for accounting reasons it looks like it's going to be easier to deal with a modified hierarchy that grows at "$1/\omega$-th" the ...