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

5
votes
1answer
193 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....
10
votes
4answers
433 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
1answer
128 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
83 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
0answers
333 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
154 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-...
9
votes
2answers
271 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^...
12
votes
2answers
596 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
1answer
195 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
166 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
0answers
155 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
302 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
156 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 ...
3
votes
1answer
225 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 ...
11
votes
3answers
412 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
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 $\...
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 \alpha)\...
4
votes
2answers
165 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
227 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 http://www.math.harvard.edu/~...
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
315 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 ...
7
votes
1answer
253 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 ...
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
114 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
150 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
325 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
92 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: "...
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
394 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 θ ...
4
votes
1answer
228 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$ ...
11
votes
0answers
494 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 ...
13
votes
1answer
575 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
91 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
300 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 ...
9
votes
2answers
412 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 ...
8
votes
1answer
291 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 ...
1
vote
2answers
330 views

An interpretation of not-Con(PA)

Edit After Andreas Blass answer below and comments below the original post I have changed it to accommodate posters' remarks. I hope it is clear and makes more sense now. Let $\mathrm{PA}$ be the ...
12
votes
1answer
821 views

Time in Girard's Geometry of Interaction

Jean-Yves Girard writes at the end of his paper "Towards a Geometry of Interaction", page 105, that we have three intuitions about the nature of time: time is logic modulo the order of rules, time ...
6
votes
2answers
230 views

Models of PRA/EFA with induction on $X$ but not $\omega^X$

As I currently understand it, induction on formulas containing $N+1$ first-order quantifiers is required to prove the well-ordering of the ordinal $(\omega \uparrow\uparrow N) < \epsilon_0$, that ...
6
votes
1answer
374 views

Essential incompleteness via diophantine formulas?

Work in the first order language of number theory, consisting of the symbols $\mathbf{0}$, $\mathbf{S}$, $\boldsymbol{+}$, and $\boldsymbol{\cdot}$, and let $Q$ denote Robinson's arithmetic. By a ...
4
votes
1answer
113 views

Results where complexity bounds implies finite number of test cases

We have all been there, when a formula works for the first 30 parameters, but it is not sufficient for a proof. My question is where one can actually just check a finite number of cases, to conclude ...
7
votes
2answers
399 views

Proof complexity of two directions of equivalency?

This question is not precise, but I believe has a precise formulation. Consider a mathematical theorem which gives an equivalency between two conditions. As an extreme example: \begin{theorem} A ...
11
votes
4answers
1k views

Does formalizing math require search and creativity, or is it near-mechanical?

I remember reading somewhere that it takes about a week to convert a page of math into something a proof-assistant like Isabelle or HOL Light would accept. Is this type of conversion something that ...
12
votes
1answer
454 views

Is it possible for a theorem to be constructive only in a non-constructive metatheory?

There are several theorems in category-theoretic logic which say something like, "any proposition in X logic that is provable in topos logic assuming (the law of excluded middle and) the axiom of ...