[FOM] feasible numbers (WAS: n(3) < Graham's number < n(4) < TREE)
hendrik at topoi.pooq.com
Thu Mar 30 10:13:29 EST 2006
On Wed, Mar 29, 2006 at 07:52:30PM -0500, Harvey Friedman wrote:
> So this is certainly bigger than the lower bound that I state for n(3) >
> A_7198(158386). In fact, I know an upper bound for n(3) of, if I memory is
> not failing me, AA(5), which is certainly smaller than Graham's number.
> However, n(4) > AA...A(1), where there are A(L) A's. Here L >= 187196.
> So n(4) >> Graham's number.
> PS: n(1) = 3, n(2) = 11. n(4) is too puny to even think about mentioning
> against TREE.
All this reminds me very strongly of ordinal notations and the difficulty of
comparing them as if we're dealing with the feasible/finitist version of the
What would be, by analogy, a natural-number notation? We usually use decimal,
which has the nice property of denseness -- that if there is a feasible notation
for n, then there is also a feasible notation for every smaller natural number.
We could use Church numerals. These, unfortunately, leave it undecidable
whether we have a numeral, but do provide us with some very large numbers. I
suspect the Graham number, for example, would have a moderately short expression
as a Church numeral.
Perhape Church numerals of simple type (N->N)->(N->N). These are decidable.
Do we get more feasible numerals if we use higher type theories? Or just
simpler proofs that some of them are feasible?
Should we require a natural-number notation to have a recursive comparison
operation? Or a feasible one?
I suppose some of the the wider questions here are,
What precise concepts are suitable as a precise analogue of the intuitive
Do we neet do have a feasible mindset, a feasible logic, a feasible
metalogic to talk meaningfully about feasibility, much as we need a
constructive mindset to make sense of constructivism?
I've once seen someone prove something was constructive by contradiction.
The proof started with the sentence, "Suppose this was not constructive."
Are we having trouble reasoning about feasibility because we are
starting from an infeasible mindset?
-- hendrik boom
More information about the FOM