**1**

vote

**0**answers

18 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 ...

**3**

votes

**0**answers

52 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 ...

**-2**

votes

**0**answers

9 views

### Can someone explain the reasoning behind Cantor's diagonal argument? [migrated]

I'm taking a class that's covering cardinalities, and I was introduced to Cantor's diagonal argument today, and I'm having trouble following the logic. The theorem states, "If s[1], s[2], … , s[n], … ...

**4**

votes

**0**answers

92 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

**2**answers

126 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?

**4**

votes

**1**answer

229 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

**1**answer

76 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

**1**answer

672 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

**1**answer

214 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

**0**answers

347 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

**2**answers

948 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

**4**answers

4k 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

**1**answer

197 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$ ...

**55**

votes

**29**answers

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

**6**answers

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

**6**answers

2k views

**8**

votes

**0**answers

352 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

**1**answer

507 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

**1**answer

81 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

**2**answers

304 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

**1**answer

205 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

**1**answer

787 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

**2**answers

286 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 ...

**7**

votes

**1**answer

239 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 ...

**7**

votes

**2**answers

349 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 ...

**1**

vote

**2**answers

292 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 ...

**62**

votes

**16**answers

5k views

### When are two proofs of the same theorem really different proofs

Many well-known theorems have lots of "different" proofs. Often new proofs of a theorem arise surprisingly from other branches of mathematics than the theorem itself.
When are two proofs really the ...

**10**

votes

**1**answer

287 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 ...

**12**

votes

**1**answer

685 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 ...

**11**

votes

**4**answers

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 ...

**6**

votes

**2**answers

203 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

**1**answer

318 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

**1**answer

108 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

**2**answers

357 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

**1**answer

305 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 ...

**12**

votes

**1**answer

406 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

**1**answer

173 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 ...

**0**

votes

**1**answer

173 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

**0**answers

85 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 ...

**24**

votes

**2**answers

519 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

**1**answer

227 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?

**24**

votes

**15**answers

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

**3**answers

763 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

**1**answer

224 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 ...

**11**

votes

**4**answers

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 ...

**8**

votes

**0**answers

326 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 ...

**7**

votes

**0**answers

193 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

**3**answers

612 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

**1**answer

127 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

**0**answers

95 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 ...