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.
352
questions
11
votes
1
answer
592
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
907
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
718
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
329
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
692
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
251
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 $...
4
votes
0
answers
283
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
175
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
421
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
191
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 ...
15
votes
1
answer
357
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 ...
5
votes
1
answer
360
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 ...
3
votes
0
answers
538
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" ...
17
votes
2
answers
1k
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
3
answers
572
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 \; ...
7
votes
1
answer
387
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 \...
10
votes
2
answers
2k
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, ...
9
votes
3
answers
701
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
62
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
140
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
3k
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
101
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 ...
8
votes
1
answer
719
views
Why relative consistency results by forcing arguments are provable in finitistic metatheory
It is claimed in many textbooks that relative consistency results, such as $\text{Con}(\text{ZFC})\rightarrow\text{Con}(\text{ZFC}+2^{\aleph_0}\geq\aleph_2)$, are provable in the finitistic metatheory....
40
votes
4
answers
7k
views
Did Euler prove theorems by example?
In his 2014 book, Giovanni Ferraro writes at beginning of chapter 1, section 1 on page 7:
Capitolo I
Esempi e metodi dimostrativi
Introduzione
In The Calculus as Algebraic Analysis, Craig Fraser, ...
12
votes
4
answers
876
views
Let's keep adding once undecidable statements
This present thread is inpired by the previous thread the true reason of the incompleteness of formal systems.
I have the following intuitive idea: Gödel's second incompleteness theorem states that a ...
1
vote
1
answer
182
views
What is difference between length of proof and length of its presentation in Peano Arithmetic?
In this paper http://www.sciencedirect.com/science/article/pii/0304397584901117 page $19$ or $29$ it seems to imply there is a difference between length of proof and length of its presentation in ...
3
votes
0
answers
186
views
What is the known weakest axiom system has Löb's derivability conditions?
We know that Peano Arithmetic satisfies Löb's derivability conditions, which is required in the proof of Gödel's 2nd incompleteness theorem. Is this the best result? If not, is there any known weaker ...
3
votes
0
answers
471
views
A question about the Chaitin constant of a theory
Chaitin's famous incompleteness theorem states that for every r.e. theory $T\supseteq Q$ in the language of arithmetic, there is a constant $d_T$ such that for any $m\geq d_T$ and any $x$, $T$ can ...
1
vote
1
answer
497
views
A question on the provability predicate of Q
I am not familiar with Robinson's construction as I do not have access to his text or to precise accounts of this, but I have come to understand that the proof predicate of Robinson arithmetic is non-...
10
votes
2
answers
596
views
Bounded Arithmetic vs Complexity Theory
In this post, when I talk about bounded arithmetic theories,
I mean the theories of arithmetic according to "Logical Foundations of Proof Complexity", which capture the complexity classes between $AC^...
16
votes
2
answers
1k
views
Is there a consistent arithmetically definable extension of PA that proves its own consistency?
I asked this on stackexchange with no answer.
The negation would be the obvious generalization of Gödel's second incompleteness from r.e. extensions of PA to any arithmetically definable extension of ...
6
votes
1
answer
335
views
Adding a truth-like predicate to PA
It is well known that adding a truth predicate to arithmetic in the most natural way leads to a contradiction.
Suppose as usual that we add a one place relation T to the language of arithmetic, and ...
4
votes
0
answers
205
views
Set theory and forcing from the point of view of a formal system $G^+$ of Gentzen type
There are four papers by Vladimir Alfeevich Kuznetsov, which discuss the above titled topic:
(1) Some problems in set theory from the standpoint of a formal system G+ of Gentzen type. (Russian) Akad. ...
3
votes
0
answers
183
views
Reducing Consistency of $PA$ [closed]
By godel translation consistency of $PA$ is equivalent to consistency of $HA$.
I want to know any similar theorems for $PA$.
1.What is the minimal theory $T\subsetneq PA$ such that the proof of $PA\...
13
votes
1
answer
661
views
Intutionistic Robinson Arithmetic
By Friedman translation $HA$ and $PA$ prove the same $\Pi_2$ formulas.
Is it true for Intutionistic Robinson arithmetic(Robinson axioms with intutionistic logic) and classic Robinson arithmetic?
...
3
votes
1
answer
673
views
Why is a cut-free system consistent?
Assume that the cut-elimination theorem holds for a system $T$. Then, for any proof that makes use of the cut-rule in $T$, there is a proof that does not make use of the cut-rule. An immediate ...
4
votes
1
answer
321
views
How do I evaluate this sum for $s$ is a complex variable :$\sum_{n=1}^{\infty} \frac{(-1)^{n+1}}{n^{2s}n!}$?
This question related to this question in SE ,I would like to know how do I
evaluate this sum for $s$ is a complex variable :$$\sum_{n=1}^{\infty} \frac{(-1)^{n+1}}{n^{2s}n!}$$ .
Edit01:And I think ...
15
votes
3
answers
1k
views
Algorithmic complexity of formal proof verification?
In this question, suppose $S$ is some popular real-world automated proof system that is stronger than or equivalent to Peano Arithmetic. I would be happy with a positive answer to the following for ...
6
votes
3
answers
2k
views
Euler's constant: irrationality and proof theory
Let $\gamma$ represent Euler's constant. Is there a real number $x$ such that there is a proof within Zermelo-Fraenkel set theory (ZF) that $x$ is irrational and there is also a proof within ZF that $\...
2
votes
0
answers
118
views
A Question on Provability Logic and Co-Necessitation
The provability logic $GL$ has the characteristic axioms:
$K\hspace{15pt}\Box(\alpha\rightarrow \beta)\rightarrow(\Box\alpha\rightarrow\Box\beta)$
$L\hspace{15pt}\Box(\Box \alpha\rightarrow \alpha)\...
5
votes
2
answers
533
views
Does the notion of provably total function depend on the chosen representation?
A typical definition of "provably total function in a theory $T$" goes like this (paraphrased from Odifreddi, Classical Recursion Theory II):
A function $f : \mathbb{N}^n \to \mathbb{N}$ is ...
10
votes
0
answers
443
views
(A little bit) Beyond the E-recursive
The E-recursive functions are a particular generalization of classical recursion theory to the entire set-theoretic universe, $V$. They are defined via a schemes: see Sacks' $E$-recursive intuitions. ...
41
votes
6
answers
4k
views
Hilbert's (cancelled) 24th problem
Hilbert's 23 problems, ten of which were presented at the 1900 ICM in Paris, are too famous for any mathematician to not know. If one reads the descriptions of the problems in Hilbert's paper, one ...
13
votes
0
answers
519
views
Large cardinals arising from alternate set theories
My question is whether there are model-theoretic large cardinal axioms associated with $NFU$ - or more generally, with set theories other than $ZFC$.
Large cardinal properties generally come in one ...
9
votes
1
answer
375
views
Proof-theoretic ordinals after liberalizing induction to $RCA_0$
This is kind of a follow-up to this question.
For a class $\Gamma$ of second-order formulas (here either $\Sigma_n^0$ or $\Sigma_n^1$), let $X\Gamma$ be a formal theory consisting of $RCA_0$ together ...
5
votes
0
answers
236
views
What useful admissible rules does ZFC have beyond the deduction theorem?
I'm interested in formal proof verification, and one of the surprisingly difficult parts of this is dealing with proofs by contradiction. The issue is that the final step of such proofs is typically "...
4
votes
0
answers
154
views
Undecidability of the existential theory
Do you know if I can find the proof that the existential theory of $\mathbb{Z}$ with the structure of addition , divisibility and the relation $(\exists s \in \mathbb{Z})m=np^s$ is undecidable, ...
0
votes
2
answers
279
views
Undecidable set of problems [closed]
Is there some set of problems, for which determining if given problem is decidable or not is itself undecidable?
8
votes
1
answer
664
views
Which ordinals are proof-theoretic ordinals?
Few months ago I have posted this question on MO, but I must admit that at the time, admittedly, I had no idea on how technical proof-theoretic considerations can be. I have decided to revise this ...
0
votes
1
answer
299
views
Provability of unprovability
I have three questions (without any real background, this is just something I've been wondering about recently)
Can PA prove that PA can't prove nor disprove, say, Goodstein theorem (or any natural ...