INTRODUCTION TO MODAL LOGIC 2014 HOMEWORK 4 • Deadline: October 30 — at the beginning of class. • Electronic submissions can be sent to Julia Ilin [email protected] or Giovanni Cina [email protected] • Grading is from 0 to 20 points. • Success! (1) (4pt) Show that in every reflexive and transitive frame the formula ♦♦p ↔ ♦p is valid. (2) (4pt) Show that Grzegorczyk’s formula ((p → p) → p) → p characterizes the class of frames F = (W, R) satisfying (i) R is reflexive, (ii) R is transitive and (iii) there are no infinite paths x0 Rx1 Rx2 R... such that for all i we have xi 6= xi+1 . (3) (4pt) Recall the definition of the basic temporal language (Example 1.14). Given a Kripke model M = (W, R, V ) recall that the semantics for the modalities P and H is given as follows: • M, w |= P ϕ iff there is v ∈ W such that Rvw and M, v |= ϕ, • M, w |= Hϕ iff for all v ∈ W , Rvw implies M, v |= ϕ. (a) Show that if w ∈ M and w0 ∈ M0 are bisimilar (according to Definition 2.16), then they do not necessarily satisfy the same formulas of basic temporal language. (b) Define the notion of temporal bisimulation such that temporal bisimilar worlds satisfy the same formulas of basic temporal language. Justify your solution. (4) (4pt) Consider the binary until operator U . In a model M = (W, R, V ) its truth definition reads: M, t |= U (ϕ, ψ) iff there is v such that Rtv and M, v |= ϕ, and for all u such that Rtu and Ruv: M, u |= ψ Prove that U is not definable in the basic modal language. For a hint consult 2.2.4 in Blackburn et al. 1 2 INTRODUCTION TO MODAL LOGIC 2014 HOMEWORK 4 (5) (4pt) (a) Give an example of a non-Sahlqvist formula other than the McKinsey, L¨ob or Grzegorczyk formula. (b) Use the Sahlqvist algorithm to compute the first-order correpsondents of the formulas: ♦p → p and ♦p → ♦p. Points of only one bonus exercise will count. If you attempt both we will consider the best of the two marks. (6) (4pt) (BONUS!) Show that for each modal formula ϕ we have (R, <) |= ϕ iff (Q, <) |= ϕ, where R and Q are the sets of the real numbers and of the rationals, respectively. [Hint: show that each finite linear sequence of clusters and irreflexive singletons such that • the top and bottom of the sequence are clusters, • no irreflexive singletons are adjacent. is a bounded morphic image of R and of Q. Then use Exercise 1 of the Homework 2 and the bonus exercise of Homework 2.] Compare this exercise with the bonus exercise of Homework 1 (this is not a question – just a note for you). (7) (4pt) (BONUS!) The aim of this exercise is to give an alternative proof of the finite model property of the basic modal logic. First read the section “Selecting finite model” (pages 74–77, Blackburn et al.). Now attempt Exercises 2.3.1, 2.3.2, 2.3.3, 2.3.4. In Exercise 2.3.2 neglect the case about arbitrary modal languages. Solve the exercise for the basic modal language with the modal operators and ♦.