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