[math-fun] quantifier depth
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
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.
Is it? For definiteness, let's take a model where a game is defined as a tree with numbers at the leaves; player 1 wants to end up at a maximal leaf, player 2 at a minimal one. Let's assume that every downward path through the tree terminates. "The value of G is x" == "the value of G is >= x and the value of G is <= x". The value of G is >= x" == "there exists a strategy A such that for every strategy B, G terminates at a node of value >= x when player 1 plays A and player 2 plays B". Strategies are partial functions from nodes to nodes where f(n) is always a child of n. "G terminates at node n when p1 plays A and p2 plays B" == "there exists a set S of nodes such that for every node m m is in S iff either m is the start node or m's parent is in S and either A(parent)=m or B(parent)=m; and n is a leaf and in S". (We need some mild technical assumptions to make this work.) Thus, "the value of G is x" becomes (implementing trees as functions node -> parent) (exists A) (forall B) (exists S) (forall m,n) [m in S <=> (m = start(G) or G(m) in S and A(G(m))=m or B(G(m))=m] and [[n in S and (forall p) not G(p)=n] => value(n) >= x] together with a similar thing for the <= inequality. We might need another level or two to cash out some of the details I've left sketchy there, but I don't see how we'd need more than 8. If you want to implement "evaluating a game tree" *explicitly* with one level of quantifiers per level searched then of course you need unbounded depth, but why do that? -- g
participants (2)
-
Gareth McCaughan -
Schroeppel, Richard