Borel Determinacy from Proofs

Borel Determinacy is a theorem on infinite game theory proved by D. A. Martin [Borel Determinacy. Annals of Mathematics 102 (1975), pp. 363-371]. It asserts that a very large family of two-player perfect-information, zero-sum games are determined, in the sense that one of the players always has a winning strategy. The proof of the theorem was very difficult to find, because a meta-mathematical result of H. M. Friedman [Higher Set Theory and Mathematical Practice. Annals of Mathematical Logic 3 (1971), pp. 325-357] asserts that any proof of Borel Determinacy must use crucial use of all the axioms of set theory. Partly because of these stringent limitations, no other proof of Borel Determinacy is known. The purpose of this project is to search for a new proof of Borel Determinacy using the methods of Proof Theory by proving a strong form of Gentzens Cut-Elimination Theorem.