Rich writes: << What's the maximum quantifier depth for doing everyday mathematics? . . . 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.

...

The theorem T(n): "For every finite perfect information 2-player game of maximum length n, one player has a strategy" has the following proof ***for each n***, in which F1, S3, etc., mean the First player's 1st play, the Second player's 3rd play, etc. ~[(all F1) (exist S1) (all F2) (exist S2) . . . (all Fn) (exist Sn) such that S wins] <=> (exist F1) (all S1) (exist F2) (all S2) . . . (exist Fn) (all Sn) such that F wins. This is depth 2n, of course. Is there a way to prove the obvious fact: (all n) T(n) within the same elementary logic system (set theory?) by, say, induction? In any case, is it true that the theorem (all n) T(n) requires arbitrarily high depth? Or is there a more direct proof of (all n) T(n) ? --Dan