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.

learn more… | top users | synonyms

21
votes
13answers
2k views

Are there any good nonconstructive “existential metatheorems”?

Are there any good examples of theorems in reasonably expressive theories (like Peano arithmetic) for which it is substantially easier to prove (in a metatheory) that a proof exists than it is ...
11
votes
4answers
1k views

How fast can the base-bumping function in Goodstein's theorem grow?

In the usual presentation of Goodstein's theorem, the base is bumped up by the "add 1" function. Does the theorem still hold when we replace this function by a fast-growing one (e.g. Ackermann or busy ...
6
votes
3answers
1k 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 ...
7
votes
1answer
229 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 ...
1
vote
1answer
125 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 ...
0
votes
0answers
81 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 ...
11
votes
0answers
486 views

What is known about the reverse mathematics of algebraic number fields?

I know work on the reverse mathematics of countable algebraic field extensions including Galois theory, notably including Dorais, Hirst, and Shafer http://arxiv.org/pdf/1209.4944v2.pdf. But algebraic ...
3
votes
0answers
332 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
1answer
153 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 ...
9
votes
2answers
265 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 ...
12
votes
2answers
587 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 ...
25
votes
1answer
2k views

Community experiences writing Lamport's structured proofs

About two years ago, I came across this paper by Lamport http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-how-to-write.pdf on writing proofs hierarchically. It changed how I wrote ...
6
votes
1answer
194 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 ...
5
votes
0answers
165 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. ...
7
votes
7answers
385 views

Strength of Bishop style constructive mathematics vs $\mathsf{RCA}_0$

This question came out of this other MO question of mine. My question is Is there a formal comparison between $\mathsf{RCA}_0$ and $\mathsf{BISH}$ (Bishop style constructive mathematics as used ...
3
votes
0answers
154 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 ...
11
votes
1answer
297 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? ...
1
vote
1answer
152 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 ...
9
votes
4answers
3k views

What does it mean to 'discharge assumptions or premises'?

When constructing proofs using natural deduction what does it mean to say that an assumption or premise is discharged? In what circumstances would I want to, or need to, use such a mechanism? The ...
11
votes
3answers
403 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 ...
3
votes
1answer
220 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 ...
12
votes
4answers
3k views

Bourbaki's epsilon-calculus notation

Bourbaki used a very very strange notation for the epsilon-calculus consisting of $\tau$s and $\blacksquare$. In fact, that box should not be filled in, but for some reason, I can't produce a \Box. ...
2
votes
0answers
70 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 ...
4
votes
2answers
160 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 ...
9
votes
0answers
226 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 ...
35
votes
4answers
2k 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 ...
11
votes
0answers
312 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
0answers
157 views

From interpolation to separation

Lusin's separation theorem states that, if $A$ and $B$ are disjoint analytic subsets of a Polish space, then there is a Borel set $X$ separating them ($A\subseteq X$, $B\cap X=\emptyset$). Craig's ...
4
votes
0answers
103 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
0answers
113 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
2answers
149 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?
6
votes
1answer
319 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 ...
-2
votes
1answer
90 views

Reconciling undecidability of FOL with Soundness and Completeness of Hilbert Proof Systems [closed]

I am reading Logic and Declarative Languages by Michael Downward, where he describes Hilbert's Proof System for First Order Logic and states that it is both sound and complete, he then adds that: ...
16
votes
1answer
707 views

Goodstein's theorem without transfinite induction

Goodstein's theorem is an example of a theorem that is not provable from first order arithmetic. All proofs of the theorem seem to deploy transfinite induction and I've wondered if one could prove the ...
0
votes
1answer
231 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 ...
7
votes
0answers
390 views

Godel's second incompleteness theorem for non-r.e. theories

R. Jeroslow in this paper proves that a non-recursively enumerable theory whose set of theorems is $\Delta_2$-definable may prove consistency of itself but it can not prove 2-consistency of itself. ...
6
votes
2answers
1k views

What defines a “short proof”?

I would like to know what the definition of a short proof is. In Lance Fortnow’s article “The Status of the P Versus NP Problem”, Communications of the ACM, Vol. 52 No. 9, he says, If a formula θ ...
5
votes
4answers
5k views

About the proof of the proposition “there exists irrational numbers a, b such that a^b is rational”

What does the classical proof of the proposition "there exists irrational numbers a, b such that $a^b$ is rational" want to reveal? I know it has something to do with the difference between classical ...
4
votes
1answer
224 views

Generalizing a result of Kreisel on $\omega$-consistency

In (reference)The following result is attributed to Kreisel: Lemma1(Kreisel) If $T$ is an $\omega$-consistent theory in the language of arithmetic and $\pi$ is a true $\Pi_1$ sentence, then $T+\pi$ ...
56
votes
29answers
6k views

Can infinity shorten proofs a lot?

I've just been asked for a good example of a situation in maths where using infinity can greatly shorten an argument. The person who wants the example wants it as part of a presentation to the general ...
19
votes
6answers
3k views

Writing “Semi-Formal” Proofs

I am very interested in proofs. I have taken an undergraduate course called "Logic and Set Theory" which I found very interesting, but ultimately unsatisfying. My biggest disappointment has to do ...
12
votes
6answers
2k views

Deduction theorem

Is there an axiomatic system where the deduction theorem does not hold?
13
votes
1answer
570 views

Can ZFC prove it cannot derive an inconsistency in $n$ steps?

Let $Con(\mathtt{ZFC}, n)$ denote the statement "$\mathtt{ZFC}$ cannot prove the contradiction within $n$ steps (or better within $n$ symbols) within a given proof system (say a natural deduction to ...
2
votes
1answer
87 views

Notion of strongness in cut rule [closed]

I've read somewhere that the cut rule in sequent calculus $$\frac{A \vdash \mathbf{C}, B \qquad A',\mathbf{C} \vdash B'}{A,A' \vdash B,B'} (\text{cut})$$ states that the $\mathbf{C}$ on the right is ...
1
vote
2answers
343 views

What is the consistency strength of a standard model of ZF versus a transitive model?

A standard model of ZF need not be transitive, of course, and Joel David Hamkins' answer to Large cardinal axioms and Grothendieck universes gives Tarski sets as an interesting example. I should ...
6
votes
1answer
238 views

Higher order arithmetic and fragments of ZFC

Zbierski "Models for Higher Order Arithmetics" (BULL. DE L'ACAD. POLONAISE DES SCIENCES Serie des sciences math., astr. et phys. - Vol. XIX, No. 7, 1971) defines ZF$_n$ as ZFC with the power set axiom ...
12
votes
1answer
826 views

Von Neumann's consistency proof

In the paper Zur Hilbertschen Beweistheorie, John Von Neumann has proposed a consistency proof for a fragment of first-order arithmetic (the fragment without induction and with the successor axioms ...
9
votes
2answers
299 views

When was Bounded Zermelo set theory first formulated?

Bounded Zermelo set theory, and many variants named for MacLane in some way, are used in equiconsistency proofs for Simple Theory of Types plus infinity, and for the Elementary Theory of the Category ...
8
votes
1answer
288 views

Which ordinals can be proof-theoretic ordinals of a reasonable theory?

When talking to a friend recently he asked a question - are there any reasonable first-order theories which have proof theoretic ordinal equal to small or large Veblen ordinal? I have then extended ...
9
votes
2answers
407 views

Peano arithmetic vs. fast-growing hierarchy with pathological fundamental sequences

Fundamental sequence for a countable limit ordinal $\alpha$ is an increasing sequence $\{\alpha[i]\}$ of ordinals of length $\omega$ such that $\lim_{i\rightarrow\omega}\alpha[i]=\alpha$. There are ...