• If ϕ is atomic formula p, then either pV or pV. 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, φ).

• If ϕ is atomic formula p, then pV. 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.