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

12
votes
5answers
1k views

Deduction theorem

Is there an axiomatic system where the deduction theorem does not hold?
12
votes
1answer
472 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 ...
10
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 ...
5
votes
2answers
149 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 ...
4
votes
1answer
273 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 ...
3
votes
1answer
99 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
285 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 ...
6
votes
1answer
237 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 ...
11
votes
1answer
330 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 ...
4
votes
1answer
143 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 ...
-1
votes
1answer
132 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 ...
4
votes
0answers
76 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 ...
23
votes
2answers
461 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 ...
2
votes
1answer
152 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?
23
votes
15answers
4k views

What's a magical theorem in logic?

Some theorems are magical: their hypotheses are easy to meet, and when invoked (as lemmas) in the midst of an otherwise routine proof, they deliver the desired conclusion more or less ...
8
votes
3answers
595 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 ...
12
votes
1answer
194 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 ...
9
votes
4answers
1k 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
161 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 ...
7
votes
0answers
310 views

Can second order arithmetic make $\aleph_1^L$ countable?

Simpson's book Subsystems of Second Order Arithmetic shows $Z_2$ can interpret some fragments of ZF strong enough to give good theories of constructible sets and formalize statements like "there is a ...
6
votes
0answers
166 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 ...
2
votes
3answers
380 views

Existential instantiation in Hilbert-style deduction systems

In some deduction systems there is a rule* that given $\exists x (\phi(x))$, we can infer $\phi(y)$, where $y$ is a fresh variable (i.e., one we haven't yet mentioned in this context). Call this rule ...
1
vote
1answer
114 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 ...
0
votes
0answers
106 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
85 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
336 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
280 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
0answers
303 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 ...
8
votes
1answer
260 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}$, ...
1
vote
0answers
277 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 ...
2
votes
1answer
222 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 ...
4
votes
1answer
231 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 ...
4
votes
2answers
366 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 ...
6
votes
0answers
114 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 ...
10
votes
1answer
466 views

Left-bracketed Ackermann function also not primitive recursive?

The original Ackermann function $\varphi\colon \mathbb{N}\times\mathbb{N}\times\mathbb{N}_0\to \mathbb{N}$ as defined in [1] was invented to prove that there is a function that is recursive but not ...
3
votes
2answers
247 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
158 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 ...
17
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 ...
0
votes
1answer
656 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
203 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
802 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 ...
20
votes
0answers
800 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 ...
5
votes
1answer
219 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 ...
11
votes
1answer
389 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 ...
12
votes
1answer
240 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 ...
1
vote
2answers
268 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 ...
8
votes
2answers
832 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 ...
3
votes
0answers
196 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 ...
8
votes
6answers
21k views

Difference between a 'calculus' and an 'algebra'

What is really the conceptual difference between a calculus and an algebra. Eg. Is SKI combinator calculus really a calculus? A friend claims that free variables are fundamental for a calculus, and ...
9
votes
2answers
240 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 ...