[FOM] relation between PA,ZFC,complexity theory

[vznuri@earthlink.net]

hi all. researcher F.Doria has been looking
into unprovability of P=?NP w.r.t. PA and ZFC over
many years now, whom Ive been in longtime correspondence with.

I'm going to sketch this out haphazardly. (due to not a full
understanding of my own). 

his approach involves creating a counterexample function
to P==NP in this sense. imagine listing out all the TMs
via some numbering that solve SAT. if P!=NP, and one confines
the list to only the P-time TMs, then there exists a number for 
which the TM must give the wrong answer.

FD has shown in some sense this counterexample function
grows very rapidly. possibly as fast or faster than the
busy beaver function. this is important, because we can
show that proving the growth of fast growing functions 
involves undecidability. 

and hence, leverage to show that
P=?NP may be independent of PA or even ZFC. seems plausible
to me. (and more really good/solid evidence for how hard P=?NP
problem may be, along with key results such as
e.g. Baker-Gill-Solovay 75, and also Razborov-Rudich, Natural Proofs)


my question. this seems to hint to a deep relationship between
the speed of growth of a function and the complexity of the
proof system required to prove it. (I have another nice
link on this for the goodstein sequence if there is interest).
does anyone know of good references on this? it seems to
me to be a very cutting edge of inquiry yet still very murky.

it apparently ties in research in logic theory to complexity
theory and is some kind of deep bridge theorem. my logic
theory background is very weak. I wish I could find a reference
something along the lines, "logic theory for complexity theorists".

in particular, I would like to know something like this.
if the function grows at speed [x] or less, it is provable
in PA. if the function grows at speed y, (y>x) or less, it
is provable in ZFC.

what are nice ways or "litmus tests"
of looking at what is provable in PA versus what is provable
in ZFC? especially, formulations that would be intuitive to a
complexity theorist.

if there is interest there is an unusual paper by bendavid & halevi
that I can look up & post the ref. its the closest of
any work Ive found of anyone else relating to FDs directions.
FD has seen it and told me that its influenced his thinking.