For Nathan Carter's MA305H class.
An Model Game is a game played between two players, the Challenger and the Defender. The game helps us understand which sentences of QL are true in a particular model. (Recall that QL is the first-order language introduced in the textbook forallx in Lurch.)
Each statement of QL is a game that can be played on any model.
The two players do not take turns. Rather, we read through the statement from left to right, and play as follows:
(The Defender can read the universal quantifier ∀x as, "No matter what my opponent chooses for x," and the existential quantifier ∃x as, "I can find an x such that...")
When there are no more quantifiers left,
it is easy to check to see if the statement is true or false,
using the model and the values the players chose.
If the sentence is true, the Defender wins; he or she
successfully defended the statement from attack.
If it is false, the Challenger wins.
\(\forall x, \exists y, greater(x,y)\)
UD: | whole numbers |
\(greater(x,y)\): | \(x\) is greater than \(y\) (that is, \(\{(0,1),(1,2),(0,2),(-1,0),\ldots\}\), an infinite list) |
The players might play this game as follows.
If a statement has only universal quantifiers in it, then the Defender never gets to play; the Challenger makes all the moves. But of course the Defender can still win, if the sentence comes out true.
Similarly, if a sentence has only existential quantifiers in it, the Challenger never gets to play, but may still win if the Defender's choices result in a false statement in the end.
If the Defender wins, that does not mean the statement is true in the model. Maybe the Challenger just played badly! Similarly, if the Challenger wins, the statement may still be true in the model. Maybe the Defender just played badly.
The statement is true in the model if the Defender has a winning strategy, that is, a procedure he or she can follow to always win. The statement is false in the model if the Challenger has a winning strategy. We will discuss in class how to describe winning strategies.