引理
证明. Perform induction on ϕ.
If ϕ is atomic formula p, then either p∈V or p∉V. Thus either V or F has a winning strategy.
If ϕ is ψ_{1}∧ψ_{2}. Suppose V does not have a winning strategy, then V does not have a strategy on either subgame ψ_{1} or ψ_{2}. By induction, F has strategy on one of these two subgames, so F can just choose this subgame and is able to win. Then F would have a strategy on ϕ.
If ϕ is ψ_{1}∨ψ_{2}. Suppose V does not have a winning strategy, then V does not have a strategy on both subgame ψ_{1} and ψ_{2}. By induction, F has strategy on both of these two subgames. Thus, no matter what V chooses, F will win.
If ϕ is □ψ. Suppose V does not have a winning strategy, then for some t such that Rst, V does not have winning strategy in t. By induction, F has strategy on t. So F just chooses t and is able to win.
If ϕ is ⋄ψ. Suppose V does not have a winning strategy, then for all t such that Rst, V does not have winning strategy in t. By induction, F has strategy on all such t. Thus no matter what V chooses, F is able to win.
If ϕ is ¬ψ. Suppose V does not have a winning strategy, then after switch, F does not have a strategy on ψ. By induction, after switch V has a strategy, that is, F has a strategy before switch.
定理
1. φ is true in M at s.
2. V has a winning strategy in game(M, s, φ).
证明. We perform induction on the structure of ϕ:
If ϕ is atomic formula p, then p∈V. Thus V wins.
If ϕ is ψ_{1}∧ψ_{2}, then M,s⊨ψ_{1} and M,s⊨ψ_{2}. By induction, V has winning strategy in both sub-games. Thus, no matter what F chooses at the first step, V could win.
If ϕ is ψ_{1}∨ψ_{2}, then M,s⊨ψ_{1} or M,s⊨ψ_{2}. Suppose M,s⊨ψ_{1}, then V just choose ψ_{1} and win; likewise for ψ_{2}.
If ϕ is □ψ, then for all t such that Rst then M,t⊨ψ, and V has winning strategy in every t. Thus no matter what F chooses at the first step, V could win.
If ϕ is ⋄ψ, then there is a t such that Rst and M,t⊨ψ. V just choose this t and wins.
If ϕ is ¬ψ, then M,s⊭ψ. So V does not have winning strategy for ψ. After switch, F will be V, and he will not have a winning strategy. Then V will have a winning strategy by Lemma 1.