Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

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
0answers
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
9answers
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
2answers
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
1answer
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
0answers
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
4answers
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
3answers
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
0answers
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
1answer
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
1answer
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
0answers
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
1answer
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
1answer
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
1answer
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
1answer
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
1answer
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
0answers
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
2answers
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
8answers
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
1answer
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
2answers
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
1answer
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
0answers
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
1answer
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
2answers
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
0answers
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
1answer
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
1answer
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
3answers
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
5answers
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
1answer
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
4answers
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
1answer
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
0answers
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
0answers
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
0answers
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
1answer
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
0answers
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
0answers
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
1answer
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
0answers
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
2answers
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
2answers
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
1answer
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
2answers
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
3answers
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
0answers
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
0answers
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
4answers
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
0answers
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 ...