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.
12
votes
1answer
153 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 ...
6
votes
3answers
445 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 ...
-6
votes
0answers
66 views
Prove: If x is a natural, then 3 divides x OR 3 divides x+1 OR 3 divides x+2 [closed]
I believe the title is pretty self explanatory. This is a very simple problem which I cannot seem to prove.
"x is natural => (3|x) OR (3|x+1) OR (3|x+2)"
I can of course think through it very ...
9
votes
4answers
951 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 ...
9
votes
0answers
116 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 ...
6
votes
0answers
141 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 ...
1
vote
1answer
93 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 ...
4
votes
0answers
73 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 ...
2
votes
3answers
319 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 ...
5
votes
1answer
256 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?") ...
8
votes
1answer
219 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}$, ...
2
votes
1answer
214 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 ...
7
votes
0answers
263 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 ...
0
votes
0answers
95 views
What references cover finitary systems of Ramified Analysis with transfinite levels?
The ramified theory of types, invented by Bertrand Russell, is a way of dealing with impredicativity by breaking the comprehension schema of second-order logic into levels. The comprehension schema ...
4
votes
0answers
105 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 ...
1
vote
0answers
173 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 ...
3
votes
2answers
206 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 ...
1
vote
0answers
138 views
Has the Ramified Theory of Types been applied to Predicative Set Theories?
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 ...
4
votes
2answers
335 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 ...
4
votes
1answer
189 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 ...
0
votes
1answer
635 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 ...
1
vote
1answer
193 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 ...
17
votes
2answers
753 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 ...
6
votes
1answer
200 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 ...
10
votes
1answer
209 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 ...
9
votes
2answers
233 views
Cut elimination algorithms
Gentzen's Hauptsatz in first order logic includes an algorithm taking any proof in the sequent calculus with cut rule, and delivering a proof without cut rule (and with the subformula property). So ...
3
votes
0answers
176 views
The substitution theorem in first order logic (finitely many variables)
We consider the language ${\cal L}=\{\in\}$ with an arbitrary set of variables $V$. Specifically we define ${\bf P}(V)$ as the free algebra of type $\{\bot,\to\}\cup\{\forall x:x\in V\}$ (with the ...
2
votes
1answer
327 views
Hilbert style axiomatic proof or sequent Calculus?
I am puzzling with the question which of the two proof systems (Hilbert style axiomatic proofs or substructural Sequent Calculi) is the most discriminatory?
With discriminatory I mean is which proof ...
8
votes
1answer
181 views
The Hasse Minkowski theorem in Peano arithmetic
Harvey Friedman's "Concrete Mathematical Incompleteness" at http://www.math.osu.edu/~friedman.8/pdf/0.Intro061311.pdf cites the Hasse Minkowski theorem saying quadratic forms over a number field are ...
1
vote
1answer
225 views
Ordinal Exponentiation in Genzen's Sequent Calculus
For Genzen's sequent calculus with PA axioms, why is the proof-theoretic ordinal $\epsilon_0$? This seems to hinge on what exactly it means for the level of a cut or CJ inference figure to be higher ...
5
votes
1answer
387 views
Axiomatization of first order logic (finitely many variables)
Standard textbooks in mathematical logic will assume an infinite supply of variables. Their axiomatization of first order logic will typically contain an axiom of the form $\forall ...
1
vote
2answers
253 views
Embedding of consistent subset in first order logic (finitely many variables)
I am looking at FOL with no equality, no constant, no function symbol and the unique binary predicate $\in$ with variables in arbitrary sets $V$ or $W$. Specifically we define ${\bf P}(V)$ as the free ...
12
votes
1answer
649 views
Reverse mathematics of Hilbert's Theorem 90
What is known, and what is published, on the reverse mathematics of the nest of results called Hilbert's Theorem 90?
5
votes
6answers
214 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 ...
14
votes
1answer
492 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 ...
1
vote
3answers
254 views
Is there an recursively axiomatized system with infinitely many proofs for some propositions or a proposition [closed]
Is there any recursively axiomized system with infinitely many proofs for some propositions or a proposition? So we will have at least one proposition which is deduced from the recursively axiomatic ...
10
votes
4answers
823 views
5
votes
1answer
202 views
Is the equivalence between a $\Sigma^0_1$ and a $\Pi^0_1$ formula defining the same recursive set provable in a sufficiently strong arithmetic ?
Let $A$ be a recursive set. $A$ is recursively enumerable, so $A$ may be defined by a $\Sigma^0_1$ formula, i.e. by $\exists \overrightarrow{a} \phi (\overrightarrow{a}, n)$, where $\phi$ contains no ...
11
votes
1answer
386 views
Does any lower bound on proofs of FLT improve Shepherdson 1965?
In 1965 Shepherdson proved that FLT is independent of the fragment of PA that uses only open induction and signature $0,S,+\times$. Indeed $2x+1\neq 2y$ is independent of that fragment. Schmerl ...
7
votes
2answers
724 views
When does $ZFC \vdash\ ' ZFC \vdash \varphi\ '$ imply $ZFC \vdash \varphi$?
Being a new member, I am not yet sure whether my question will be taken as a research level question (and thus, appropriate for MO). However, I have seen similar questions on MO, couple of which led ...
12
votes
1answer
210 views
What metatheory proves $\mathsf{ACA}_0$ conservative over PA?
Simpson's book shows $\mathsf{ACA}_0$ is conservative over $\mathsf{PA}$ in the natural way by model theory using definable subsets. Of course, $\mathsf{ACA}_0$ being conservative over PA is ...
0
votes
0answers
76 views
Beatty proof adaptation ?
If $m$ and $n$ are coprime integers, prove that each of these $m+n-2$ fractions: $$\frac{m+n}{m},\frac{2(m+n)}{m},\frac{3(m+n)}{m},...,\frac{(m-1)(m+n)}{m},$$ ...
5
votes
1answer
177 views
Interpretability and consistency strength
I have heard there is some fairly recent result showing that whenever theories $T$ and $T'$ have the same consistency strength, then each can interpret the other. I suppose it refers to first order ...
9
votes
2answers
372 views
Reverse mathematics below RCA
I'm sure this is a fairly basic question, but I can't seem to find a solid answer:
My primary question is: Is there a reasonably nice subsystem of second-order arithmetic corresponding essentially to ...
20
votes
0answers
764 views
Godel on recursion-theoretic hierarchies
At the end of his excellent article, "The Emergence of Descriptive Set Theory" (http://math.bu.edu/people/aki/2.pdf), Kanamori writes:
"Another mathematical eternal return: Toward the end of his ...
4
votes
1answer
201 views
ERA, PRA, PA, transfinite induction and equivalences
I'm quite sure I don't understand very well the links between proof theoretical ordinals of theories, the axioms of transfinite induction and the objects a theory can prove to exist.
For instance I'm ...
4
votes
1answer
164 views
Notation for upperbound power sets.
There is a standard notation $\mathrm{ZF}[n]$ for Zermelo Fraenkel set theory with the power set axiom restricted to saying the set of natural numbers has $n$ successive power sets ...
12
votes
1answer
519 views
Does Taranovsky's system of ordinal notations make sense?
Dmytro Taranovsky has a Web page on which he claims to define a system of ordinal notations strong enough to provide an ordinal analysis of full second-order arithmetic. I think (perhaps unjustly) ...
7
votes
5answers
790 views
Understanding the nature and structure of proofs; Reverse Mathematics and Proof Theory. Prerequisites? Good introductory texts?
I'm still studying maths at undergraduate level, but intend to continue exploring topics in pure maths after I have graduated, so am thinking already about what directions I'd like to persue now, (as ...
2
votes
1answer
273 views
Sequent calculus: is there a complete linear reasoning (i.e., no trees)?
In Gentzen's sequent calculus, a formal proof is described by a tree, with each node representing the sequent obtained from the child(ren) by applying a given inference rule.
If no inference rule has ...
