FOM: Comments and queries on Friedman's last 3 posts

[Joe Shipman]

Long Walks:

What I like about this is the nonelementary growth of something that is
so easy to picture geometrically.  The idea of a walk
with steps of length <=3 in Z^3 is about as intuitive as you can get
(though it would be REALLY nice if the length could be reduced to <2,
which would be equivalent to requiring steps which didn't change any
coordinate by more than 1).

What is the growth rate w.r.t. x of the longest non-outward walk from
(x,x,x) using steps of Euclidean length <2?

As the dimension goes up this gets harder to picture and one might as
well go to the n(k) function to get incomprehensible growth.


Q-systems and Proof-Theoretic Ordinals:

This is the most accessible representation I've ever seen of a
significant portion of the large cardinal "scale".  It is not quite
"ordinary mathematics" but the concept of definability is about as
ingratiating to non-logicians as a logical concept can be.

It's too bad that you can't bootstrap these results.  You have several
results of the form

"Con(ZFC+kappa_i) implies Thereexists a Q-system satisfying i implies
Con(ZFC+lambda_i )"

where kappa_i<lambda_i, but the intervals (kappa_i,lambda_i) don't
overlap enough that you can combine these to get a result of the form

"Con(ZFC + something small) implies Thereexist Q-systems satisfying
1,2,...,i implies Con(ZFC+something big)".


Predicatively Infeasible Integers:

By far the nicest thing here is the connection between long sequences
and labeled trees, so that n(3) can be transformed into an impredicative
integer by changing "unary" to "binary".  Once you have the picture of
long sequences from {0,1,2} and the embeddability criterion, it is easy
to imagine the sequences bifurcating into trees.

Harvey, what is your best upper bound for n(3)?

-- JS