[FOM] Defining embedding dimensions

[joeshipman@aol.com]

Nash proved that any Riemannian manifold of dimension n can be 
isometrically embedded in Euclidean space of dimension at most  m=f(n), 
where the function f was improved by later researchers.

My questions are,

1) Can the "best possible" function f be defined in Peano Arithmetic? 
Currently established upper and lower bounds for f represent 
ZFC-theorems, and one can imagine a situation where there exist n and m 
such that ZFC does not settle the question whether dimension m suffices 
to isometrically embed all n-dimensional Riemannian manifolds; even in 
that case ZFC still defines the function f(n) but PA may not. (On the 
other hand, if ZFC settles all such questions about individual values 
of f(n) then one can define f in PA in terms of ZFC-proofs.)

2) Is there an analogous theorem to Nash's embedding theorem for 
Einstein/Kahler type metrics, and what are the best known bounds on the 
dimension in that case?

-- JS