引理 1. For every modal formula and pointed model, in the game(M,s,ϕ) either V or F has a winning strategy.

证明. 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 ψ₁∧ψ₂. Suppose V does not have a winning strategy, then V does not have a strategy on either subgame ψ₁ or ψ₂. 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 ψ₁∨ψ₂. Suppose V does not have a winning strategy, then V does not have a strategy on both subgame ψ₁ and ψ₂. 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.

定理 2. The following two assertions are equivalent for all modal formulas and pointed models:

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 ψ₁∧ψ₂, then M,s⊨ψ₁ and M,s⊨ψ₂. 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 ψ₁∨ψ₂, then M,s⊨ψ₁ or M,s⊨ψ₂. Suppose M,s⊨ψ₁, then V just choose ψ₁ and win; likewise for ψ₂.

• 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.