@inbook{Buchi1990,
    Abstract = {To have recognized the fundamental role that quantifiers play, is one of Frege's contributions to mathematics. Elimination of quantifiers, however, was not invented by logicians. In fact, it is easily the most important thing that happens in any mathematical proof. Investigation would probably reveal a direct relation between the usefulness of a theorem, and its ability to simplify quantifications. (The same goes for notions, e.g., continuous everywhere versus uniformly continuous). In particular, (what some call) infinity lemmas, or (what others call) combinatorial lemmas, turn out to be simple instructions for replacing bad combinations (∀∃) by more manageable ones (∃∀). Here is a list of examples:(1)Axiom of choice: (1){\$}{\$}{\backslash}left( {\{}{\backslash}forall x{\}} {\backslash}right){\backslash}left( {\{}{\backslash}exists y{\}} {\backslash}right)Rxy. {\backslash}equiv .{\backslash}left( {\{}{\backslash}exists f{\}} {\backslash}right){\backslash}left( {\{}{\backslash}forall x{\}} {\backslash}right)Rxfx{\$}{\$}(2)Infinity lemma (compactness): (1){\$}{\$}{\backslash}left( {\{}{\backslash}forall x{\}} {\backslash}right){\backslash}left( {\{}{\{}{\}}{\\_}{\backslash}exists {\backslash}overline {\{}Zx{\}} {\}} {\backslash}right){\backslash}left( {\{}{\backslash}forall t{\}} {\backslash}right){\{}{\}}^xM{\backslash}left( {\{}{\backslash}overline X t,{\backslash}overline Z t{\}} {\backslash}right). {\backslash}equiv {\backslash}left( {\{}{\{}{\}}{\\_}{\backslash}exists Z{\}} {\backslash}right){\backslash}left( {\{}{\backslash}forall t{\}} {\backslash}right)M{\backslash}left( {\{}{\backslash}overline X t,{\backslash}overline Z t{\}} {\backslash}right){\$}{\$}(3)Ramsey's lemma: (1){\$}{\$}{\{}{\backslash}left( {\{}{\{}{\}}{\\_}{\backslash}forall Z{\}} {\backslash}right)^{\{}{\backslash}inf {\}}{\}}{\backslash}left( {\{}{\{}{\}}{\\_}{\{}{\backslash}exists y{\}}{\}} {\backslash}right){\{}{\backslash}left( {\{}{\{}{\}}{\\_}{\{}{\backslash}exists x{\}}{\}} {\backslash}right)^y{\}}{\backslash}left[ {\{}Z{\{}x{\\_}A{\}}Z{\{}y{\\_}A{\}}{\backslash}overline R xy{\}} {\backslash}right]. {\backslash}supset .{\{}{\backslash}left( {\{}{\{}{\}}{\\_}{\backslash}exists Z{\}} {\backslash}right)^{\{}{\backslash}inf {\}}{\}}{\backslash}left( {\{}{\backslash}forall y{\}} {\backslash}right){\{}{\backslash}left( {\{}{\backslash}forall x{\}} {\backslash}right)^y{\}}{\backslash}left[ {\{}Z{\{}x{\\_}A{\}}Zy {\backslash}supset Rxy{\}} {\backslash}right]{\$}{\$}Why, in the course of a proof, is the right side ∃∀ more desirable? Having arrived at (∃x)(∀y)Sxy, I will simply say ``let b be one of these x, and so (∀y)Sby''. Such and ``existentiation'' permanently eliminates a quantifier.},
    Address = {New York, NY},
    Author = {Buchi, J. Richard},
    BookTitle = {The Collected Works of J. Richard B{\"u}chi},
    Editor = {Mac Lane, Saunders and Siefkes, Dirk},
    File = {Using Determinancy of Games to Eliminate Quantifiers - 978-1-4613-8928-6\_32.pdf},
    ISBN = {978-1-4613-8928-6},
    Pages = {581--592},
    Publisher = {Springer New York},
    Title = {Using Determinancy of Games to Eliminate Quantifiers},
    URL = {https://doi.org/10.1007/978-1-4613-8928-6\_32},
    Year = {1990},
    bdsk-url-1 = {https://doi.org/10.1007/978-1-4613-8928-6\_32},
    date-added = {2022-10-18 16:14:58 +0200},
    date-modified = {2022-10-18 16:14:58 +0200},
    doi = {10.1007/978-1-4613-8928-6_32}
}