Given the set of standard axioms (I’m not asking for proof of those), do we know for sure that a proof exists for all unproven theorems? For example, I believe the Goldbach Conjecture is not proven even though we “consider” it true.

Phrased another way, have we

proventhat if a mathematical statement is true, a proof of it exists? That, therefore, anything that is true can be proven, and anything that cannot be proven is not true? Or, is there a counterexample to that statement?If it hasn’t been proven either way, do we have a strong idea one way or the other? Is it generally thought that some theorems can have no proof, or not?

**Answer**

Relatively recent discoveries yield a number of so-called ‘natural

independence’ results that provide much more natural examples

of independence than does Gödel’s example based upon

the liar paradox (or other syntactic diagonalizations).

As an example of such results, I’ll sketch a simple example due

to Goodstein of a concrete number theoretic theorem whose proof

is independent of formal number theory PA (Peano Arithmetic) (following [Sim]).

Let $\,b\ge 2\,$ be a positive integer. Any nonnegative integer $n$

can be written uniquely in base $b$

$$\smash{n\, =\, c_1 b^{\large n_1} +\, \cdots + c_k b^{\large n_k}} $$

where $\,k \ge 0,\,$ and $\, 0 < c_i < b,\,$ and $\, n_1 > \ldots > n_k

\ge 0,\,$ for $\,i = 1, \ldots, k.$

For example the base $\,2\,$ representation of $\,266\,$ is

$$266 = 2^8 + 2^3 + 2$$

We may extend this by writing each of the exponents $\,n_1,\ldots,n_k\,$

in base $\,b\,$ notation, then doing the same for each of the exponents

in the resulting representations, $\ldots,\,$ until the process stops.

This yields the so-called ‘hereditary base $\,b\,$ representation of $\,n$’.

For example the hereditary base $2$ representation of $\,266\,$ is

$$\smash{266 = 2^{\large 2^{2+1}}\! + 2^{2+1} + 2} $$

Let $\,B_{\,b}(n)$ be the nonnegative integer which results if we take the

hereditary base $\,b\,$ representation of $\,n\,$ and then syntactically

replace

each $\,b\,$ by $\,b+1,\,$ i.e. $\,B_{\,b}\,$ is a base change operator

that ‘Bumps the Base’

from $\,b\,$ up to $\,b+1.\,$ For example bumping the base from $\,2\,$ to

$\,3\,$ in the prior equation yields

$$\smash{B_{2}(266) = 3^{\large 3^{3+1}}\! + 3^{3+1} + 3\quad\ \ \ }$$

Consider a sequence of integers obtained by repeatedly applying

the operation: bump the base then subtract one from the result.

For example, iteratively applying this operation to $\,266\,$ yields

$$\begin{eqnarray}

266_0 &=&\ 2^{\large 2^{2+1}}\! + 2^{2+1} + 2\\

266_1 &=&\ 3^{\large 3^{3+1}}\! + 3^{3+1} + 3 – 1\ =\ B_2(266_0) – 1 \\

~ \ &=&\ 3^{\large 3^{3+1}}\! + 3^{3+1} + 2 \\

266_2 &=&\ 4^{\large 4^{4+1}}\! + 4^{4+1} + 1\qquad\! =\ B_3(266_1) – 1 \\

266_3 &=&\ 5^{\large5^{5+1}}\! + 5^{5+1}\phantom{ + 2}\qquad\ =\ B_4(266_2) – 1 \\

266_4 &=&\ 6^{\large 6^{6+1}}\! + \color{#0a0}{6^{6+1}\! – 1} \\

~ \ &&\ \textrm{using}\quad \color{#0a0}{6^7\ -\,\ 1}\ =\ \color{#c00}{5555555}\, \textrm{ in base } 6 \\

~ \ &=&\ 6^{\large 6^{6+1}}\! + \color{#c00}5\cdot 6^6 + \color{#c00}5\cdot 6^5 + \,\cdots + \color{#c00}5\cdot 6 + \color{#c00}5 \\

266_5 &=&\ 7^{\large 7^{7+1}}\! + 5\cdot 7^7 + 5\cdot 7^5 +\, \cdots + 5\cdot 7 + 4 \\

&\vdots & \\

266_{k+1} &=& \ \qquad\quad\ \cdots\qquad\quad\ = \ B_{k+2}(266_k) – 1 \\

\end{eqnarray}$$

In general, if we start this procedure at the integer $\,n\,$ then

we obtain what is known as the *Goodstein sequence* starting at $\,n.$

More precisely, for each nonnegative integer $\,n\,$ we recursively define

a sequence of nonnegative integers $\,n_0,\, n_1,\, \ldots ,\,

n_k,\ldots\,$ by

$$\begin{eqnarray}

n_0\ &:=&\ n \\

n_{k+1}\ &:=&\

\begin{cases}

B_{k+2}(n_k) – 1 &\mbox{if }\ n_k > 0 \\

\,0 &\mbox{if }\ n_k = 0

\end{cases} \\

\end{eqnarray}$$

If we examine the above Goodstein sequence for $\,266\,$ numerically

we find that the sequence initially increases extremely rapidly:

$$\begin{eqnarray}

2^{\large 2^{2+1}}\!+2^{2+1}+2\ &\sim&\ 2^{\large 2^3} &\sim&\, 3\cdot 10^2 \\

3^{\large 3^{3+1}}\!+3^{3+1}+2\ &\sim&\ 3^{\large 3^4} &\sim&\, 4\cdot 10^{38} \\

4^{\large 4^{4+1}}\!+4^{4+1}+1\ &\sim&\ 4^{\large 4^5} &\sim&\, 3\cdot 10^{616} \\

5^{\large 5^{5+1}}\!+5^{5+1}\ \ \phantom{+ 2} \ &\sim&\ 5^{\large 5^6} &\sim&\, 3\cdot

10^{10921} \\

6^{\large 6^{6+1}}\!+5\cdot 6^{6}\quad\!+5\cdot 6^5\ \:+\cdots +5\cdot 6\ \ +5\

&\sim&\ 6^{\large 6^7} &\sim&\, 4\cdot 10^{217832} \\

7^{\large 7^{7+1}}\!+5\cdot 7^{7}\quad\!+5\cdot 7^5\ \:+\cdots +5\cdot 7\ \ +4\

&\sim&\ 7^{\large 7^8} &\sim&\, 1\cdot 10^{4871822} \\

8^{\large 8^{8+1}}\!+5\cdot 8^{8}\quad\!+5\cdot 8^5\ \: +\cdots +5\cdot 8\ \ +3\

&\sim&\ 8^{\large 8^9} &\sim&\, 2\cdot 10^{121210686} \\

9^{\large 9^{9+1}}\!+5\cdot 9^{9}\quad\!+5\cdot 9^5\ \: +\cdots +5\cdot 9\ \ +2\

&\sim&\ 9^{\large 9^{10}} &\sim&\, 5\cdot 10^{3327237896} \\

10^{\large 10^{10+1}}\!\!\!+5\cdot 10^{10}\!+5\cdot 10^5\!+\cdots +5\cdot 10+1\ &\sim&\

10^{\large 10^{11}}\!\!\!\! &\sim&\, 1\cdot 10^{100000000000} \\

\end{eqnarray}$$

Nevertheless, despite numerical first impressions, one can prove that this

sequence converges to $\,0.\,$ In other words, $\,266_k = 0\,$ for all

sufficiently large $\,k.\,$ This surprising result is due to Goodstein

$(1944)$ who actually proved the same result for *all* Goodstein

sequences:

**Goodstein’s Theorem** $\ $ For all $\,n\,$ there exists $\,k\,$ such

that $\,n_k = 0.\,$

In other words, every Goodstein sequence converges to $\,0.$

The secret underlying Goodstein’s theorem is that hereditary

expression of $\,n\,$ in base $\,b\,$ mimics an ordinal notation for

all ordinals less than epsilon nought $\,\varepsilon_0 = \omega^{\large \omega^{\omega^{\Large\cdot^{\cdot^\cdot}}}}\!\!\! =\, \sup \{ \omega,\, \omega^{\omega}\!,\, \omega^{\large \omega^{\omega}}\!,\, \omega^{\large \omega^{\omega^\omega}}\!,\, \dots\, \}$. For such

ordinals, the base bumping

operation leaves the ordinal fixed, but subtraction of

one decreases the ordinal. But these ordinals are well-ordered, which allows us to conclude that a Goodstein sequence

eventually converges to zero. Goodstein actually proved his

theorem for a general increasing base-bumping function $\,f:\Bbb N\to \Bbb

N\,$

(vs. $\,f(b)=b+1\,$ above). He proved that convergence of all such

$f$-Goodstein sequences is equivalent to transfinite induction

below $\,\epsilon_0.$

One of the primary measures of strength for a system of logic is

the size of the largest ordinal for which transfinite induction

holds. It is a classical result of Gentzen that the consistency

of PA (Peano Arithmetic, or formal number theory) can be proved

by transfinite induction on ordinals below $\,\epsilon_0.\,$ But we know

from Godel’s second incompleteness theorem that the consistency

of PA cannot be proved in PA. It follows that neither can

Goodstein’s theorem be proved in PA. Thus we have an example of

a very simple concrete number theoretical statement in PA whose

proof is nonetheless independent of PA.

Another way to see that Goodstein’s theorem cannot be proved in PA

is to note that the sequence takes too long to terminate, e.g.

$$ 4_k\,\text{ first reaches}\,\ 0\ \,\text{for }\, k\, =\,

3\cdot(2^{402653211}\!-1)\,\sim\, 10^{121210695}$$

In general, if ‘for all $\,n\,$ there exists $\,k\,$ such that $\,P(n,k)$’

is

provable, then it must be witnessed by a provably computable

choice function $\,F\!:\, $ ‘for all $\,n\!:\ P(n,F(n)).\,$’ But the

problem

is that $\,F(n)\,$ grows too rapidly to be provably computable in PA,

see [Smo] $1980$ for details.

Goodstein’s theorem was one of the first examples of so-called

‘natural independence phenomena’, which are considered by most

logicians to be more natural than the metamathematical

incompleteness results first discovered by Gödel. Other finite

combinatorial examples were discovered around the same time,

e.g. a finite form of Ramsey’s theorem, and a finite form of

Kruskal’s tree theorem, see [KiP], [Smo] and [Gal]. [Kip]

presents the Hercules vs. Hydra game, which provides an

elementary example of a finite combinatorial tree theorem

(a more graphical tree-theoretic form of Goodstein’s sequence).

Kruskal’s tree theorem plays a fundamental role in computer

science because it is one of the main tools for showing that

certain orderings on trees are well-founded. These orderings

play a crucial role in proving the termination of rewrite rules

and the correctness of the Knuth-Bendix equational completion

procedures. See [Gal] for a survey of results in this area.

See the references below for further details, especially

Smorynski’s papers. Start with Rucker’s book if you know no

logic, then move on to Smorynski’s papers, and then the others,

which are original research papers. For more recent work, see

the references cited in Gallier, especially to Friedman’s school

of ‘Reverse Mathematics’, and see [JSL].

**References**

[Gal] Gallier, Jean. What’s so special about Kruskal’s theorem and the ordinal $\Gamma_0$?

A survey of some results in proof theory,

Ann. Pure and Applied Logic, 53 (1991) 199-260.

[HFR] Harrington, L.A. et.al. (editors)

Harvey Friedman’s Research on the Foundations of Mathematics, Elsevier 1985.

[KiP] Kirby, Laurie, and Paris, Jeff.

Accessible independence results for Peano arithmetic,

*Bull. London Math. Soc.,* 14 (1982), 285-293.

[JSL] The Journal of Symbolic Logic,* v. 53, no. 2, 1988

This issue contains papers from the Symposium “Hilbert’s

Program Sixty Years Later”.

[Kol] Kolata, Gina. Does Goedel’s Theorem Matter to Mathematics?

*Science* 218 11/19/1982, 779-780; reprinted in [HFR]

[Ruc] Rucker, Rudy. Infinity and The Mind, 1995, Princeton Univ. Press.

[Sim] Simpson, Stephen G. Unprovable theorems and fast-growing functions,

*Contemporary Math.* 65 1987, 359-394.

[Smo] Smorynski, Craig. (all three articles are reprinted in [HFR])

Some rapidly growing functions, *Math. Intell.,* 2 1980, 149-154.

The Varieties of Arboreal Experience, *Math. Intell.,* 4 1982, 182-188.

“Big” News from Archimedes to Friedman, *Notices AMS,* 30 1983, 251-256.

[Spe] Spencer, Joel. Large numbers and unprovable theorems,

*Amer. Math. Monthly,* Dec 1983, 669-675.

**Attribution***Source : Link , Question Author : Jeremy , Answer Author : Bill Dubuque*