[FOM] Finite trees and Goodstein's Theorem

[Rupert Swarbrick]

Hello all,

I am an undergraduate and writing a project/essay centred on Goodstein's
Theorem that is supposed to be intelligible to other 2nd year students.

The plan of the essay was to talk a little about formal systems, then
prove Goodstein's theorem in normal naive maths and finally talk a bit
about the Paris and Kirby result: the idea of what it means for the
result to be independent of PA, rather than talking about model theory
properly.

Anyway. My original plan was to prove Goodstein's theorem by:
1) describing the natural finite rooted tree that goes with each term
2) defining an ordering on these trees
3) show that the sequence of trees corresponding to the Goodstein
sequence was decreasing
4) show that the ordering was a well-ordering on that sequence.
5) use the restricted ordinal theorem that I proved in previous section

So I thought this worked before I found a gaping hole in my proof of
part 4. Then I managed to find the article:

How to Well Order Finite Trees
by Herman Ruge Jervell
www.ml.kva.se/preprints/meta/JervellMon_Jun_11_10_58_31.rdf.html

Now, this goes about proving that one can well-order the set of finite
trees and does so by talking about whether a tree is accessible. Once he
has proven that all trees are accessible, he then proves that the
ordering is a well-ordering.

Clearly this is exactly the opposite way around from what I was hoping
to do.

So my questions are:

- Is there any way of proving that an ordering on the finite trees in
this situation is a well-ordering without using Jervell's method. I am
of course considering a significantly smaller set than he was - I don't
know if that will help.

- If not, can anyone give me a mathematical/proof theoretic reason that
this can't be done? I realise that step 4 would have to be the bit where
you leave PA, so maybe there isn't a good way to do it from this direction?

Note that I'm an undergraduate so, although I'm really interested by the
subject and willing to learn, I may not know about a result in the field
that makes the answer to these questions obvious!

Thank you very much for your time reading such a long question!

Rupert Swarbrick





-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 370 bytes
Desc: OpenPGP digital signature
Url : /pipermail/fom/attachments/20070414/b3975e5d/signature.bin