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.
5
votes
1answer
279 views
van der Waerden's theorem in Reverse Mathematics
What is known about weak systems of axiomata that allow one to prove van der Waerden's theorem ?
van der Waerden's theorem can be used to show that there are infinitely many primes (see below). Is ...
4
votes
0answers
137 views
Ordinal analysis and nonrecursive ordinals
Ordinal analysis is typically described as characterizing recursive ordinals in a theory $T$, but there is a sense in which it can characterize all $T$-ordinals, even those that are nonrecursive.
...
2
votes
0answers
91 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
5k views
“Strange” proofs of existence theorems [closed]
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
890 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
402 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
72 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 ...
8
votes
4answers
473 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
317 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
212 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
154 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
228 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
156 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
128 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
318 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
138 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
539 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
314 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$. ...
8
votes
1answer
388 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
207 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
545 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 ...
7
votes
0answers
150 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
200 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$ ...
11
votes
1answer
367 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
541 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
592 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
218 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
462 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
199 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
213 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
232 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
196 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
174 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
189 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
188 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
297 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
873 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
324 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
241 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
657 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, ...
8
votes
3answers
420 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
123 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 ...
