[FOM] feasible numbers (WAS: n(3) < Graham's number < n(4) < TREE[3])

[hendrik@topoi.pooq.com]

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[3]. 

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 
same thing.

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 
    idea "feasible"?

    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