Are you interested in quantifier depth as an indicator of difficulty? I seem to recall that many of the decision procedures get an exponential in quantifier depth. But keep in mind that Hilbert's Tenth Problem has only existential quantifiers, although they are quantifiers over the integers, and this problem is undecidable. At 01:00 PM 5/6/2006, Schroeppel, Richard wrote:
What's the maximum quantifier depth for doing everyday mathematics?
I count groups of quantifiers of the same type as 1, so that a block of variables of the shape (all x,y,z), or the statement that there's a magic square of size 3x3 (exists a,b,c,d,e,f,g,h,i) are counted as one quantifier. So I'm really talking about Alternating Quantifier Depth.
The definition of "a function f is continuous at a point x" has depth 3:
(all epsilon) (exists delta) (all y) 0 < |y-x| < delta => |f(y)-f(x)| < epsilon
and "f is continuous" is also depth 3:
(all x,epsilon) (exists delta) (all y) etc. etc.
The theorem that "the sum of continuous functions is continuous" is depth 5:
(all f,g) (exists h) (all x,epsilon) (exists delta) (all y) h(x) = f(x)+g(x) And { 0 < |y-x| < delta => ... }
So it looks like routine math might use a maximum depth of 8 or so. Presumably there are a few specialties that go much deeper. (?) Evaluating a game tree is an example.
Rich