Skip to main content

All Questions

Filter by
Sorted by
Tagged with
32 votes
11 answers
11k views

Is PA consistent? do we know it?

1) (By Goedel's) One can not prove, in PA, a formula that can be interpreted to express the consistency of PA. (Hopefully I said it right. Specialists correct me, please). 2) There are proofs (...
16 votes
2 answers
2k views

Could Kronecker accept a proof of Goodstein's theorem?

A famous result of Goodstein asserts that the Goodstein sequence of integers terminates. For a precise statement and a short proof, see https://en.wikipedia.org/wiki/Goodstein%27s_theorem. A well ...
Piotr Hajlasz's user avatar
12 votes
2 answers
866 views

The inconsistency of Graham Arithmetics plus $ \forall n, n < g_{64}$

As you all know, Ronald Graham just passed away. He is famous for many fabulous contributions to finite combinatorics, and much much more, but perhaps none of them is as popular as the infamous ...
Mirco A. Mannucci's user avatar
10 votes
1 answer
350 views

An internalized version of Tennenbaum's Theorem

Tennenbaum's celebrated 1959 theorem (see here for a reference) is certainly one of the key theorems in mathematical logic. Not so much for its proof, but because it helps "isolating" $N$ ...
Mirco A. Mannucci's user avatar
9 votes
1 answer
1k views

Does Nelson try to prove PA inconsistent directly?

Edward Nelson is known for his serious attempts to show that Peano axioms, and sometimes even weaker theories, are inconsistent. I wasn't able to find Nelson's papers anywhere, so I wanted to ask a ...
Wojowu's user avatar
  • 28.2k
8 votes
3 answers
2k views

Does the Feferman-Schutte analysis give a precise characterization of Predicative Second-Order Arithmetic?

A definition is called impredicative if it involves quantification over a domain that contains the thing being defined. For instance, if you define hereditary property to be a property which applies ...
Keshav Srinivasan's user avatar
8 votes
1 answer
574 views

Iterated Gentzen: or, a Sith objection to the proof of consistency of PA

$\DeclareMathOperator\PRA{PRA}\DeclareMathOperator\WF{WF}\DeclareMathOperator\Con{Con}\DeclareMathOperator\PA{PA}$Preamble: In the year … in a galaxy far far away, a nasty Sith named Darth Dubious (...
Mirco A. Mannucci's user avatar
6 votes
2 answers
998 views

Are omega-consistent extensions of PA always consistent with each other?

The question is as in the title. In the edit history you can find my attempt to formalise the question, but that was a failure, for reasons stated clearly in the comments. Thus, my question is just: ...
N. Virgo's user avatar
  • 1,344
3 votes
1 answer
405 views

Godel 's Ladder: Undecidable PI_N sentences for N =2, 3, ......

After Godel's groundbreaking results, a plethora of $\Pi_1^0$ undecidable arithmetical sentences have been found by many authors. But what about $\Pi_n^0$ for $n=2,3,.....$ ? There are, to my ...
Mirco A. Mannucci's user avatar
3 votes
0 answers
282 views

What is the meaning and proof of Harvey Friedman’s ultrafinite incompleteness sentence?

On page 7 of his paper “Adventures in Incompleteness”, Harvey Friedman states the following: IN ANY LONG ENOUGH SEQUENCE $x_1,...,x_n$ FROM $\{1,2,3\}$, SOME $(x_i,...,x_{2i})$ IS A SUBSEQUENCE OF ...
Keshav Srinivasan's user avatar
3 votes
0 answers
301 views

What does second order set theory give us that is new?

There is a natural analogy between the theories PA and ZFC. See the linked question by Gro-Tsen here. Peano arithmetic (PA) is a first order approximation to the natural numbers. As is well known, ...
Pace Nielsen's user avatar
  • 18.7k
2 votes
1 answer
456 views

Is the statement "All numbers are counting numbers" independent of $PA$?

In his paper, "Completed versus Incomplete Infinity in Arithmetic" (which can be found here), the late Edward Nelson defines the notion of 'counting number' as follows: 0 is a counting ...
Thomas Benjamin's user avatar
1 vote
1 answer
395 views

Complete and consistent first-order theories that contain interesting phenomena

Gödel has shown that a consistent recursively axiomatizable first-order theory that can interpret Robinson arithmetic is incomplete. I think there is some sentimental value in working with a theory ...
user avatar
1 vote
0 answers
117 views

Can this type theory interpret second order arithmetic?

Language: multi-sorted first order logic with equality and membership, where for each natural $t$ there is a set $x^t$ of sort $t$. Equality "$=$" only occurs between variables of the same ...
Zuhair Al-Johar's user avatar