CLASS TEST #4								           11-4-05

For each of the following formulae prove its validity or invalidity in finite and infinite models:

(i)	Gφ→◊φ
(ii)	Pφ→◊φ

(i) is invalid in finite models with end of time. Let M be such a model and let tf be the final time. Let φ be false at all indeces. For all w, Gφ will be true at <w,tf> but not ◊φ, since none of the indeces is a φ-index, that is an index at which  φ is true.

(ii), on the other hand, is valid. Let M be an arbitrary model. Pφ cannot be true with respect to M at any index without φ being true at some index, and the existence of a single φ-index guarantees that ◊φ is true at all indeces. Hence there can be no model in which at some index Pφ is true but not ◊φ.

Note how a single model suffices to establish invalidity, but all models need to be considered – hence the mention of “an arbitrary model” –  to prove validity. Note also how compact the proofs can be, without any mention of g’s whatsoever.