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.

Filter by
Sorted by
Tagged with
7 votes
0 answers
461 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. ...
Payam Seraji's user avatar
6 votes
2 answers
2k 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 θ ...
user3757091's user avatar
6 votes
1 answer
545 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$ ...
Payam Seraji's user avatar
12 votes
1 answer
966 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 ...
Colin McLarty's user avatar
20 votes
1 answer
2k 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 ...
Dávid Natingga's user avatar
2 votes
1 answer
113 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 ...
rsharma's user avatar
  • 123
2 votes
2 answers
754 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 ...
Colin McLarty's user avatar
7 votes
1 answer
545 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 ...
Colin McLarty's user avatar
16 votes
2 answers
1k 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 ...
Mohammad Golshani's user avatar
9 votes
2 answers
450 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 ...
Colin McLarty's user avatar
14 votes
1 answer
1k 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 ...
Wojowu's user avatar
  • 27.4k
12 votes
1 answer
737 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 ...
Wojowu's user avatar
  • 27.4k
15 votes
2 answers
1k views

Decidability of decidability

The questions I'm going to ask are non formal because they concern decidability of decidability, and I couldn't find any references on that after some quick searches. I hope that this thread is still "...
sure's user avatar
  • 438
1 vote
2 answers
710 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 ...
Rafał Gruszczyński's user avatar
16 votes
1 answer
2k 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 ...
Trent's user avatar
  • 999
8 votes
2 answers
522 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 ...
Eliezer Yudkowsky's user avatar
9 votes
1 answer
601 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 ...
Dave Albert's user avatar
4 votes
1 answer
134 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 ...
Per Alexandersson's user avatar
10 votes
2 answers
786 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: Theorem. A ...
Ian Agol's user avatar
  • 66.8k
17 votes
4 answers
2k 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 ...
14 votes
1 answer
1k 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 ...
Zhen Lin's user avatar
  • 14.9k
4 votes
1 answer
330 views

Gödel's speed up theorem and Matiyasevich polynomials

Unless I am sadly mistaken, there should exist a polynomial $ P\in\mathbb Z[X_1,X_2,\dots, X_n]$ coding for the speed-up theorem (for, say, ZFC), i.e. having the following properties : 1) P has an ...
Feldmann Denis's user avatar
3 votes
2 answers
746 views

notable inductive proofs relating to fractals

what are notable/ prominent inductive proofs relating to fractals? the motivation for this question is: fractals are very difficult mathematical objects to work with, and many problems/questions ...
vzn's user avatar
  • 529
4 votes
0 answers
104 views

$n$th order arithmetic with predicates for orders

Two papers I have looked at lately axiomatize $n$-th order arithmetic in a single sorted language with predicates $Z_1,\dots,Z_n$ and axioms like $\forall x(Z_1(x)\vee\dots\vee Z_n(x))$ to say ...
Colin McLarty's user avatar
7 votes
1 answer
647 views

Does the totality of Ackermann's function prove the consistency of $\Sigma_1$-induction?

It is well known that Ackermann's function is not primitive recursive. Therefore, the theories of primitive recursive arithmetic (PRA) and of $\Sigma_1$-induction ($I\Sigma_1$) cannot prove the ...
alexod's user avatar
  • 757
31 votes
2 answers
906 views

Why is there no connection between fast-growing functions and complex analysis

I found myself wondering the other day whether the fast-growing functions from natural to naturals that are studied by people like proof theorists are the restriction to the naturals of analytic ...
Thomas Forster's user avatar
2 votes
1 answer
812 views

what are the proof-theoretic ordinals of second-order arithmetic and ZFC? [duplicate]

are they still smaller than omega-1-CK?what are the notations of them?
huhao's user avatar
  • 21
16 votes
1 answer
558 views

Nontrivial upper bounds on proof-theoretic ordinals of strong theories: do we have any?

Motivated by Consistency of Analysis (second order arithmetic) and Proof-Theoretic Ordinal of ZFC or Consistent ZFC Extensions?, I have the following question: Are there any examples of strong ...
Noah Schweber's user avatar
13 votes
3 answers
2k views

Consistency of Analysis (second order arithmetic)

Is there a proof of the consistency of Analysis (second order arithmetic), which is similar to Gentzen's proof of the consistency of arithmetic? Update: Which (different) methods can be used to ...
Mohammad Golshani's user avatar
12 votes
4 answers
2k views

Are there non-diagonal proofs for Cantor's continuum and Godel's incompletness theorems?

There is a formal definition for the notion of a formal proof. Question 1. Is there any formal definition for the notion of a diagonal formal proof? Consider the following theorems both proved by ...
user47544's user avatar
  • 141
10 votes
1 answer
444 views

Reverse mathematics of meromorphic functions on Riemann surfaces

Various sources touch briefly on the reverse mathematics of measure theory and complex analysis. But I have found none on the uniformization theorem for Riemann surfaces or the existence of non-...
Colin McLarty's user avatar
7 votes
0 answers
248 views

When is a reduction not a reduction?

Every mathematician understands the concept of reducing a complicated problem to a simpler problem. "Without loss of generality, we may assume…" However, I've noticed that some kinds of "...
Timothy Chow's user avatar
  • 78.1k
2 votes
1 answer
227 views

A question about consistent fragments of formalized mathematical theories with Natural Deduction

Ref to : Sara Negri & Jan von Plato, Structural Proof Theory (2001). In Ch.6 : Structural Proof Analysis of Axiomatic Theories [page 126-on], they give a method of adding axioms to sequent ...
Mauro ALLEGRANZA's user avatar
4 votes
0 answers
118 views

Stabilization of recursive approximation in $PA^-+I\Sigma_1^0$

Over any model M of $PA^-+I\Sigma_1^0$. Suppose $A\in [T]$ where $T$ is a $\Delta_2^0$-tree and $A$ is one isolated path. Further, $A$ is regular, i.e. $\forall n A\upharpoonright n$ has a code in $M$....
Jing Zhang's user avatar
  • 3,138
2 votes
3 answers
575 views

Show that Z2 is not conservative over PA

It is well-known that $\mathsf{ACA}_0$ is a conservative extension of PA. I assume this theorem gets a lot of attention because $\mathsf{Z}_2$ is not conservative over PA. Thus there ought to be first-...
A.C.'s user avatar
  • 39
6 votes
1 answer
501 views

Is Kolmogorov complexity (KC) relevant for proof theory? [closed]

Note. The title was modified. Previous title was "Every theorem t has a proof no more complex than~|t|. Is this right?" The question ("Is Kolmogorov complexity (KC) relevant for proof theory?") ...
Armando Matos's user avatar
12 votes
1 answer
875 views

What is the proof-theoretic ordinal of PA + Con(PA), PA + Con(PA + Con(PA)) etc., and why?

I seem to remember having read that the proof-theoretic ordinal (sup of ordinals the theory can prove well-ordered) of $\mathsf{PA} + \mathsf{Con}(\mathsf{PA})$ is the same as that of $\mathsf{PA}$, ...
Benya's user avatar
  • 141
2 votes
1 answer
330 views

Elementary proof of bounds on factor polynomials

The question Getting a bound on the coefficients of the factor polynomial got very nice answers on Gelfond's theorem. But for work on proof theory of arithmetic I want a proof in arithmetic. The ...
Colin McLarty's user avatar
9 votes
0 answers
523 views

"Hard" separation results in reverse mathematics (or similar)

This is a fairly broad question. In particular, I specify 5 questions (Q1, Q2.1, Q2.2, Q3, Q4) which for me all fall under one umbrella. Since this is unreasonably broad, I'm really interested in an ...
Noah Schweber's user avatar
7 votes
0 answers
248 views

cut-elimination for infinitary logic

Takeuti (1987, 223) deduces a cut-elimination theorem for infinitary logic from the corresponding soundness-and-completeness theorems. However, is there a way to adapt the basic Gentzen-style ...
mmw's user avatar
  • 171
3 votes
0 answers
821 views

What is the role of the (formalized) omega rule in Ramified Analysis?

In the 1960's, Feferman and Schutte did groundbreaking proof-theoretic work to find out the strength of predicative systems of second-order arithmetic. They used the ramified theory of types, a ...
Keshav Srinivasan's user avatar
3 votes
2 answers
764 views

What is the proof-theoretic ordinal of Hyperarithmetical Comprehension?

As I discuss in my answer here, it seems to me that Solomon Feferman shows, on pages 10-11 of his seminal 1964 paper "Systems of Predicative Analysis", that if you consider predicative second-order ...
Keshav Srinivasan's user avatar
11 votes
3 answers
625 views

Has the Ramified Theory of Types been applied to NBG?

Questions of predicativity are well-studied in the context of arithmetic. We have a base theory, first-order Peano arithmetic. Some people, like Edward Nelson (in chapter 1 of his book) and Charles ...
Keshav Srinivasan's user avatar
5 votes
3 answers
832 views

Did Gödel prove that the Ramified Theory of Types collapses at $\omega_1$?

Second-Order Arithmetic is considered impredicative, because the comprehension scheme allows formulas with bound second-order variables that range over all sets of natural numbers, including the set ...
Keshav Srinivasan's user avatar
5 votes
1 answer
686 views

Can the Burgess-Hazen analysis of Predicative Arithmetic be extended to Transfinite Types?

Around page 300 of his book "Mathematical Thought and its Objects", Charles Parsons discusses the work of Edward Nelson, who believes that mathematical induction is impredicative, because it can be ...
Keshav Srinivasan's user avatar
0 votes
1 answer
771 views

Is there any danger far from home? (Edited & Revised Version) [closed]

The notion of formal proof is defined by finite sequences ($<\omega$ - sequences) of sentences. In some sense if a sentence $\sigma$ is (finitely) provable from the theory $T$ it is very "near" to ...
user avatar
0 votes
1 answer
243 views

Does this algorithm terminate in all scenarios?

Let $x \in \mathbb{R}^p$ denote a $p$-dimensional data point (a vector). I have two sets $A = \{x_1, \dots, x_n\}$ and $B = \{x_{n+1}, \dots, x_{n+m}\}$, so $|A| = n$, and $|B| = m$. Given $k \in \...
shna's user avatar
  • 123
22 votes
2 answers
2k views

Deep theorems and long proofs

I ran across this discussion by Daniel Shanks, "Is the quadratic reciprocity law a deep theorem?." Solved and Unsolved Problems in Number Theory. Vol. 297. AMS, 2001. p.64ff. which made me ...
Joseph O'Rourke's user avatar
4 votes
1 answer
535 views

the choice of representing formulas and Gödel's second incompleteness theorem

In Rautenberg's book (A Concise Introduction to Mathematical Logic, Universitext, Springer 2006), Gödel's second incompleteness theorem is stated: Theorem 3.2 (Second incompleteness theorem). PA ...
user40921's user avatar
  • 143
22 votes
1 answer
3k views

Proof-Theoretic Ordinal of ZFC or Consistent ZFC Extensions?

Let the proof theoretic ordinal $\alpha$ of a theory $T$ be the least recursive ordinal such that $T$ does not prove that $\alpha$ is well-founded. This ordinal is intended to quantify in some sense ...
user40919's user avatar
  • 701

1
4
5
6 7 8