Preprint about theorem-proving program up on arXiv

Mohan Ganesalingam and I have just put a preprint up on arXiv entitled “A fully automatic problem solver with human-style output.” In it, we give quite a lot of detail about how the program discussed in this post works. We also talk about our general approach, and why we think it may allow us to solve problems fully automatically that are currently out of reach. (Some fairly easy — for humans — problems fall into this category.) We have also made the program’s output for our current set of test problems available. A quick look at that may be a more efficient way of getting an idea of what the program does than reading the explanation we give in the paper.

If you are interested enough to look at the preprint and find that you spot a typo or more serious error, we would of course be very grateful to be told.

Determinacy of Borel games V

This post is a kind of postscript to the previous four. It consists of miscellaneous observations that shed some light on the proof of Borel determinacy. I’m writing it mainly for my own benefit, but there seems to be no harm in posting it, just in case anyone else finds it interesting.

An attempt to lift that sort of works and sort of doesn’t

One way to get some further insight into the proof of Borel determinacy is to look at some auxiliary games that don’t work as lifts. A particularly natural candidate is this. Let be an infinite (pruned) tree, let and let be the game . Now define a game as follows. Player I plays a move of the form , where is a strategy for with first move . Player II plays a move of the form , where is a strategy for and . Thereafter, the two players must play the strategies and .

Clearly the outcome of this game is decided after the first two moves: if beats then Player I wins and otherwise Player II wins.

Determinacy of Borel games IV

To recap briefly, we have defined a notion of lifting from one game to another and embarked on a proof that every Borel game can be lifted to a clopen game. The stages of that proof are to show that every closed game can be lifted to a clopen game, and that the set of games that can be lifted is closed under countable unions. It is straightforward to show that it is also closed under taking complements, so that will prove that all Borel games can be lifted to clopen games. As we saw earlier, if a game can be lifted to a determined game, then it is itself determined. Since clopen games are determined, this will be enough.

We are in the middle of the proof that closed games can be lifted to clopen games. We have defined the game to which we will lift, and shown how to map Player I strategies for the auxiliary game to strategies for the original game . So the first thing to do in this post is to show how to map Player II strategies for to Player II strategies for .

Determinacy of Borel games III

My aim in this post (if I have enough space) is to prove that every closed game can be lifted to an open (and therefore, by continuity, which is part of the definition of lifting, clopen) game. Since I am discussing a formal proof, I shall be a little more formal with my definitions than I have been so far. Much of what I write to begin with will be repeating things I have already said in the two previous posts.

Trees and paths

Recall the definition of a pruned tree. This is an infinite rooted tree such that from every vertex there is at least one directed infinite path. (Less formally, if you are walking away from the root, you never get stuck.) Given such a tree , we write for the set of infinite directed paths in . If we are working in , then the tree we will work with has finite sequences as its vertices, with each sequence joined to its extensions . Then .