Sahlqvist Correspondence Theory for Second-Order Propositional Modal Logic (Short Paper) Zhiguang Zhao Taishan University, China 1 Introduction Second-Order Propositional Modal Logic (SOMPL). Modal logic with proposi- tional quantifiers has been considered in the literature since Kripke [13], Bull [2], Fine [8, 9], and Kaplan [7]. This language is of high complexity: its satisfia- bility problem is not decidable, and indeed not even analytical. In Kaminski and Tiomkin [12], the authors showed that the expressive power for SOMPL whose modalities are S4.2 or weaker is the same as second-order predicate logic. How- ever, not every second-order formula is equivalent to an SOMPL-formula, since SOMPL-formulas are preserved under generated submodels (see van Benthem [16]). In ten Cate [15], the author proved the analogues of the van Benthem- Rosen theorem (on the model level) and Goldblatt-Thomason theorem (on the frame level) for SOMPL. Therefore, a natural question is: on the frame level, can we find a natural fragment of SOPML-formulas such that each formula in this fragment corresponds to a first-order formula, in the sense of Sahlqvist theory (see [14, 16])? This is what we will answer in the paper. Correspondence Theory. Typically, modal correspondence theory [16] concerns the correspondence of modal formulas and first-order formulas over Kripke frames, via the tools of standard translation. Syntactic classes (e.g. Sahlqvist formulas [14], inductive formulas [11], etc.) of modal formulas are identified to have first- order correspondents and are canonical, i.e. their validity are closed under taking canonical extensions. In the present paper, we identify the Sahlqvist formulas of SOMPL, which cover and properly extend the Sahlqvist fragment in basic modal logic. We show that there is an SOMPL Sahlqvist formula which corresponds to ∀x∀y(Rxy ∧ Ryx → Rxx), which is not modally definable, and that the SOMPL Sahlqvist formula ∀q(∀p(p → 3p ∨ q) → q) is not canonical, which is in contrast to the basic modal logic setting where each Sahlqvist formula is canonical. The present paper use the same methodology as [6, 3]. The Sahlqvist fragment of SOPML is defined in a step-by-step way, and we give an algorithm ALBASOPML (Ackermann Lemma Based Algorithm) which can successfully reduce Sahlqvist formulas in SOPML to first-order formulas and is sound with respect to Kripke semantics. Copyright © 2021 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). Sahlqvist-type Correspondence Theory for SOPML 113 2 Preliminaries 2.1 Language and semantics In the present paper we consider the unimodal language. Given a set Prop of propositional variables, the second-order propositional modal formulas are de- fined as follows: ϕ ::= p | ⊥ | > | ¬ϕ | ϕ ∧ ϕ | ϕ ∨ ϕ | ϕ → ϕ | 2ϕ | 3ϕ | ∀pϕ | ∃pϕ where p ∈ Prop. We use the boldface notation p~ to denote a set of proposi- tional variables and use ϕ(~p) to indicate that the propositional variables occur in ϕ are all in p~. We say that an occurrence of a propositional variable p in a formula ϕ is positive (resp. negative) if it is in the scope of an even (resp. odd) number of negations (here α → β is regarded as ¬α ∨ β). The semantics of the second-order propositional modal formulas are defined as follows: Definition 1. A Kripke frame is a pair F = (W, R) where W 6= ∅ is the domain of F, the accessibility relation R is a binary relation on W . A Kripke model is a pair M = (F, V ) where V : Prop → P (W ) is a valuation on F. VXp denote a valuation which is the same as V except that VXp (p) = X ⊆ W . Now the satisfaction relation can be defined as follows: given any Kripke model M = (W, R, V ), any w ∈ W , the basic and Boolean cases are standard, and for modalities and propositional quantifiers, M, w 2ϕ iff for any v such that Rwv, M, v ϕ; M, w 3ϕ iff there exists v such that Rwv and M, v ϕ; M, w ∀pϕ iff for all X ⊆ W , (W, R, VXp ), w ϕ; M, w ∃pϕ iff there exists X ⊆ W such that (W, R, VXp ), w ϕ. In order to use the algorithm to compute the first-order correspondents of Sahlqvist SOPML formulas, we will need the following expanded modal language which is defined as follows: ϕ ::= p | i | ⊥ | > | ¬ϕ | ϕ ∧ ϕ | ϕ ∨ ϕ | ϕ → ϕ | 2ϕ | 3ϕ | ϕ | ♦ϕ | ∀pϕ | ∃pϕ | ∀iϕ | ∃iϕ | l(ϕ, ϕ) where p ∈ Prop, i ∈ Nom is a nominal,  and ♦ are the backward-looking box and diamond respectively, ∀i and ∃i are nominal quantifiers, and l is a binary modality. We call a formula pure if it does not contain propositional variables or propositional quantifiers (it can contain nominals, nominal quantifiers and the binary modality l). The interpretation of the expanded modal language is given as follows: For a valuation V , it is defined as V : Prop∪Nom → P (W ) such that V (i) is a singleton for all i ∈ Nom. The additional satisfaction clauses are given as follows (here Vvi denote a valuation which is the same as V except that Vvi (i) = {v} ⊆ W .): 114 Zhiguang Zhao M, w i iff V (i) = {w}; M, w ϕ iff for any v such that Rvw, M, v ϕ; M, w ♦ϕ iff there exists v such that Rvw and M, v ϕ; M, w ∀iϕ iff for all v ∈ W , (W, R, Vvi ), w ϕ; M, w ∃iϕ iff there exists v ∈ W such that (W, R, Vvi ), w ϕ; M, w l(ϕ, ψ) iff for all v ∈ W (if M, v ϕ, then M, v ψ). We can extend V to a map from the set of formulas to P (W ) in the natural way. 2.2 Inequalities and complex inequalities We will find it convenient to use the inequality notation ϕ ≤ ψ where ϕ and ψ are formulas. We use Ineq to denote the set of all inequalities in the expanded modal language. We define complex inequalities as follows: Comp ::= Ineq | Comp & Comp | Comp ⇒ Comp | ∀pComp | ∃pComp | ∀iComp | ∃iComp Here we assume that the quantifiers have a higher precedence than &, and & is higher than ⇒. Complex inequalities are interpreted in models M = (W, R, V ) instead of pointed models (M, w). The semantics of complex inequalities is defined as fol- lows: – An inequality is interpreted as follows: (W, R, V ) ϕ ≤ ψ iff (for all w ∈ W, if (W, R, V ), w ϕ, then (W, R, V ), w ψ); – (W, R, V ) Comp1 &Comp2 iff (W, R, V ) Comp1 and (W, R, V ) Comp2 ; – (W, R, V ) Comp1 ⇒ Comp2 iff ((W, R, V ) Comp1 implies (W, R, V ) Comp2 ); – (W, R, V ) ∀pComp iff for all X ⊆ W , (W, R, VXp ) Comp; – (W, R, V ) ∃pComp iff there exists an X ⊆ W such that (W, R, VXp ) Comp; – (W, R, V ) ∀iComp iff for all v ∈ W , (W, R, Vvi ) Comp; – (W, R, V ) ∃iComp iff there exists an v ∈ W such that (W, R, Vvi ) Comp. 2.3 Standard translation In the correspondence language which is second-order due to the existence of propositional quantifiers in SOPML, we have a binary predicate symbol R cor- responding to the binary relation, a set of constant symbols i corresponding to each nominal i, a set of unary predicate symbols P corresponding to each propositional variable p. Definition 2. The standard translation of the expanded SOPML language is defined as follows (for the basic and Boolean case, it is standard): Sahlqvist-type Correspondence Theory for SOPML 115 – STx (i) := x = i; – STx (2ϕ) := ∀y(Rxy → STy (ϕ)); – STx (3ϕ) := ∃y(Rxy ∧ STy (ϕ)); – STx (ϕ) := ∀y(Ryx → STy (ϕ)); – STx (♦ϕ) := ∃y(Ryx ∧ STy (ϕ)); – STx (∀pϕ) := ∀P STx (ϕ); – STx (∃pϕ) := ∃P STx (ϕ); – STx (∀iϕ) := ∀iSTx (ϕ); – STx (∃iϕ) := ∃iSTx (ϕ); – STx (l(ϕ, ψ)) := ∀y(STy (ϕ) → STy (ψ)). The following proposition states that this translation is correct: Proposition 1. For any Kripke model M, any w ∈ W and any expanded SOPML formula ϕ, M, w ϕ iff M  STx (ϕ)[x := w]. For inequalities and complex inequalities, the standard translation is given in a global way: Definition 3. – ST (ϕ ≤ ψ) := ∀x(STx (ϕ) → STx (ψ)); – ST (Comp1 & Comp2 ) = ST (Comp1 ) ∧ ST (Comp2 ); – ST (Comp1 ⇒ Comp2 ) = ST (Comp1 ) → ST (Comp2 ); – ST (∀p(Comp)) := ∀P (ST (Comp)); – ST (∃p(Comp)) := ∃P (ST (Comp)); – ST (∀i(Comp)) := ∀i(ST (Comp)); – ST (∃i(Comp)) := ∃i(ST (Comp)). Proposition 2. For any Kripke model M, any inequality Ineq, any complex inequality Comp, M Ineq iff M  ST (Ineq); M Comp iff M  ST (Comp). 3 Sahlqvist formulas in second-order propositional modal logic In this section, we define Sahlqvist formulas of second-order propositional modal logic step by step. We first define (quantifier-free) positive formulas POS(~ p) whose propositonal variables are among p~: p) ::= p | ⊥ | > | POS(~ POS(~ p) ∧ POS(~ p) | POS(~ p) ∨ POS(~ p) | 2POS(~ p) | 3POS(~ p) where p is in p~. These positive formulas have similar roles to the positive consequent part in Sahlqvist formulas in basic modal logic, which are going to receive minimal valuations. The reason why we do not allow propositional quantifiers in positive formulas is that we want the formula after receiving the minimal valuations to be translated into a first-order formula, while propositional quantifiers will make it second-order. 116 Zhiguang Zhao 3.1 The Π1 -fragment: Sahlqvist formulas in basic modal logic We define the Π1 -Sahlqvist antecedent Sahl1 (~ p) whose propositonal variables are among p~: p) ::= 2n p | ⊥ | > | ¬POS(~ Sahl1 (~ p) | Sahl1 (~ p) ∧ Sahl1 (~ p) | 3Sahl1 (~ p) where p is in p~. Then the Π1 -Sahlqvist formulas are defined as ∀~ p) → POS(~ p(Sahl1 (~ p)). In- deed, Sahlqvist formulas1 in the basic modal logic setting can be treated as universally quantified by propositional quantifiers which bind all occurrences of propositional variables, so in this sense the Π1 -Sahlqvist formulas can be taken as the Sahlqvist formulas in basic modal logic. 3.2 The Π2 -fragment We define the PIA formula PIA(~q, p~) as follows: PIA(~q, p~) ::= p | 2PIA(~q, p~) | PIA(~q, p~) ∧ PIA(~q, p~) | POS(~q) ∨ PIA(~q, p~) where p is in p~. Here the PIA formula has two bunches of propositional variables: ~q is to receive minimal valuations for ~q from somewhere else, and p~ is used to compute minimalVvaluations for p~. Then it is easy to see that PIA(~q, p~) is equivalent to the form 2(POS(~q) ∨ 2(POS(~q) ∨ . . . p)), where p is in p~. Now we can define Π2 -Sahlqvist antecedents as follows: Sahl2 (~ p) | ∀~q(Sahl1 (~q) → PIA(~q, p~)) | Sahl2 (~ p) ::= Sahl1 (~ p) ∧ Sahl2 (~ p) | 3Sahl2 (~ p) Then Π2 -Sahlqvist formulas are defined as ∀~ p) → POS(~ p(Sahl2 (~ p)). It is easy to see that formulas of the form ∀~ p) ∧ ∀~q(Sahl1 (~q) → p(Sahl1 (~ PIA(~q, p~)) → POS(~ p)) are in the Π2 -hierarchy. 3.3 The Πn -fragment Now for the Πn -fragment, assume that we have already defined Πn−1 -Sahlqvist p) and Πn−1 -Sahlqvist formulas ∀~ antecedents Sahln−1 (~ p) → POS(~ p(Sahln−1 (~ p)), then we can define Πn -Sahlqvist antecedents as follows: Sahln (~ p) | ∀~q(Sahln−1 (~q) → PIA(~q, p~)) | Sahln (~ p) ::= Sahln−1 (~ p) | 3Sahln (~ p)∧Sahln (~ p) Then Πn -Sahlqvist formulas are defined as ∀~ p) → POS(~ p(Sahln (~ p)). 1 In [1, Chapter 3], what we call Sahlqvist formulas are called Sahlqvist implications. Sahlqvist-type Correspondence Theory for SOPML 117 4 The Algorithm ALBASOMPL In the present section, we define the correspondence algorithm ALBASOMPL for second-order propositional modal logic, in the style of [4, 5]. The algorithm re- ceives a Πn -Sahlqvist formula ∀~ p) → POS(~ p(Sahln (~ p)) as input and goes in three stages. 1. Preprocessing and first approximation: The algorithm receives a Πn -Sahlqvist formula ∀~ p) → POS(~ p(Sahln (~ p)) as input, and then apply the rewriting rule: ∀~ p) → POS(~ p(Sahln (~ p)) ∀~ p) ≤ POS(~ p(Sahln (~ p)) Then apply the first-approximation rule: ∀~ p) ≤ POS(~ p(Sahln (~ p)) ∀~ p∀i0 (i0 ≤ Sahln (~ p) ⇒ i0 ≤ POS(~ p)) 2. The reduction stage: In this stage, we aim at reducing i ≤ Sahln (~ p) to a complex inequality in which p occurs either in the form ϕ ≤ p where ϕ is pure or in the form j ≤ ¬POS(~ p). (a) The commutativity rule and the associativity rule for &; (b) The rules for nominals: i. Splitting rule: i≤α∧β (Spl − N om) i≤α&i≤β ii. Separation rule: i≤α→β (Sep − N om) i≤α ⇒ i≤β iii. Quantifier rule: i ≤ ∀qα (Quant − N om) ∀q(i ≤ α) iv. Approximation rule: i ≤ 3α (Approx − N om) ∃j(j ≤ α & i ≤ 3j) The nominals introduced by the approximation rule must not occur in the whole complex inequality before applying the rule. (c) The residuation rules: α ≤ 2β α≤β∨γ (Res − 2) (Res − ∨) ♦α ≤ β α ∧ ¬β ≤ γ 118 Zhiguang Zhao (d) The splitting rule: α≤β∧γ (Splitting) α≤β &α≤γ (e) The quantifier rules: ∃j(Comp1 ) & Comp2 ∃j(Comp1 ) ⇒ Comp2 (Scope − &) (Scope− ⇒) ∃j(Comp1 & Comp2 ) ∀j(Comp1 ⇒ Comp2 ) where Comp2 does not have free occurrences of j. ∀q∀p(Comp) ∀i∀p(Comp) (Ex − pq) (Ex − pi) ∀p∀q(Comp) ∀p∀i(Comp) ∀p∀i(Comp) ∀i∀j(Comp) (Ex − ip) (Ex − ji) ∀i∀p(Comp) ∀j∀i(Comp) ∀p(Comp1 ⇒ (Comp2 &Comp3 )) (Spl − Quant − p) ∀p(Comp1 ⇒ Comp2 ) & ∀p(Comp1 ⇒ Comp3 ) ∀i(Comp1 ⇒ (Comp2 &Comp3 )) (Spl − Quant − i) ∀i(Comp1 ⇒ Comp2 ) & ∀i(Comp1 ⇒ Comp3 ) (f) The Ackermann rule: In this step, we compute the minimal valuation for propositional vari- ables and use the Ackermann rule to eliminate all the propositional vari- ables. ∀q(α1 ≤ β1 & . . . &αn ≤ βn & ψ1 ≤ q& . . . &ψm ≤ q ⇒ α ≤ β) W W W W W W α1 [ ψ/q] ≤ β1 [ ψ/q]& . . . &αn [ ψ/q] ≤ βn [ ψ/q] ⇒ α[ ψ/q] ≤ β[ ψ/q] where: i. ϕ[θ/p] W means uniformly replace occurrences of p in ϕ by θ; ii. ψ = ψ1 ∨ . . . ∨ ψm ; iii. Each αi is positive, and each βi negative in q, for 1 ≤ i ≤ n; iv. α is negative in q and β is positive in q; v. Each ψi is pure (therefore q does not occur in ψi ). (g) The packing rule: ∀i(α1 ≤ β1 & . . . &αn ≤ βn ⇒ α ≤ β) ∃i(l(α1 , β1 ) ∧ . . . ∧ l(αn , βn ) ∧ α) ≤ β where β does not contain occurrences of i. 3. Output: By the execution of the algorithm, we can guarantee that given a Πn -Sahlqvist formula as input, we can rewrite it into a pure complex inequality. Then we use standard translation to translate it into a first-order formula. Sahlqvist-type Correspondence Theory for SOPML 119 Theorem 1 (Soundness and Success). – If ALBASOPML runs successfully on an input Πn -Sahlqvist formula ∀~ p) → p(Sahln (~ POS(~p)) and outputs a first-order formula FO(∀~ p) → POS(~ p(Sahln (~ p))), then for any Kripke frame F = (W, R), F ∀~ p(Sahln (~ p)) iff F |= FO(∀~ p) → POS(~ p) → POS(~ p(Sahln (~ p))). – There is an algorithm such that for any Πn -Sahlqvist formula ϕ, it can be transformed into an equivalent first-order formula. 5 Examples We give three examples of Π2 -Sahlqvist formulas to show how the ALBASOPML algorithm works: Example 1. ∀p(32p ∧ ∀q(32q → 2(2q ∨ 2p)) → 232p) ∀p∀i(i ≤ 32p ∧ ∀q(32q → 2(2q ∨ 2p)) ⇒ i ≤ 232p) ∀p∀i(i ≤ 32p & i ≤ ∀q(32q → 2(2q ∨ 2p)) ⇒ i ≤ 232p) ∀p∀i(i ≤ 32p & ∀q(i ≤ 32q → 2(2q ∨ 2p)) ⇒ i ≤ 232p) ∀p∀i(i ≤ 32p & ∀q(i ≤ 32q ⇒ i ≤ 2(2q ∨ 2p)) ⇒ i ≤ 232p) ∀p∀i(i ≤ 32p & ∀q∀j(i ≤ 3j & j ≤ 2q ⇒ i ≤ 2(2q ∨ 2p)) ⇒ i ≤ 232p) ∀p∀i(i ≤ 32p & ∀q∀j(i ≤ 3j & ♦j ≤ q ⇒ i ≤ 2(2q ∨ 2p)) ⇒ i ≤ 232p) ∀p∀i(i ≤ 32p & ∀j(i ≤ 3j ⇒ i ≤ 2(2♦j ∨ 2p)) ⇒ i ≤ 232p) ∀p∀i(i ≤ 32p & ∀j(i ≤ 3j ⇒ ♦i ≤ 2♦j ∨ 2p) ⇒ i ≤ 232p) ∀p∀i(i ≤ 32p & ∀j(i ≤ 3j ⇒ ♦i ∧ ¬2♦j ≤ 2p) ⇒ i ≤ 232p) ∀p∀i(i ≤ 32p & ∀j(i ≤ 3j ⇒ ♦(♦i ∧ ¬2♦j) ≤ p) ⇒ i ≤ 232p) ∀p∀i(i ≤ 32p & ∀j(l(i, 3j) ∧ ♦(♦i ∧ ¬2♦j) ≤ p) ⇒ i ≤ 232p) ∀p∀i(i ≤ 32p & ∃j(l(i, 3j) ∧ ♦(♦i ∧ ¬2♦j)) ≤ p ⇒ i ≤ 232p) now denote ∃j(l(i, 3j) ∧ ♦(♦i ∧ ¬2♦j)) as ϕ, then ∀p∀i(i ≤ 32p & ϕ ≤ p ⇒ i ≤ 232p) ∀p∀i∀k(i ≤ 3k & k ≤ 2p & ϕ ≤ p ⇒ i ≤ 232p) ∀p∀i∀k(i ≤ 3k & ♦k ≤ p & ϕ ≤ p ⇒ i ≤ 232p) ∀i∀k(i ≤ 3k ⇒ i ≤ 232(♦k ∨ ϕ)) Then we can use standard translation to get its first-order correspondence. Example 2. The following example resembles the irreflexivity rule of Gabbay [10]: ∀q(∀p(p → 3p ∨ q) → q) ∀q∀i(i ≤ ∀p(p → 3p ∨ q) ⇒ i ≤ q) ∀q∀i(∀p(i ≤ p → 3p ∨ q) ⇒ i ≤ q) ∀q∀i(∀p(i ≤ p ⇒ i ≤ 3p ∨ q) ⇒ i ≤ q) ∀q∀i(i ≤ 3i ∨ q ⇒ i ≤ q) 120 Zhiguang Zhao ∀q∀i(i ∧ ¬3i ≤ q ⇒ i ≤ q) ∀i(i ≤ i ∧ ¬3i) ∀i(i ≤ ¬3i) ∀x¬Rxx. By [1, Example 2.58], the irreflexive property is not preserved under taking ultrafilter extensions, which means that the validity of ∀q(∀p(p → 3p ∨ q) → q) is not preserved under taking canonical extensions, which means that ∀q(∀p(p → 3p ∨ q) → q) is not canonical. Example 3. The following example is not equivalent to any Sahlqvist formula in the basic modal language: ∀p(2p ∧ ∀q(q → 33q ∨ p) → p) ∀p∀i(i ≤ 2p ∧ ∀q(q → 33q ∨ p) ⇒ i ≤ p) ∀p∀i(i ≤ 2p & i ≤ ∀q(q → 33q ∨ p) ⇒ i ≤ p) ∀p∀i(♦i ≤ p & i ≤ ∀q(q → 33q ∨ p) ⇒ i ≤ p) ∀p∀i(♦i ≤ p & ∀q(i ≤ q → 33q ∨ p) ⇒ i ≤ p) ∀p∀i(♦i ≤ p & ∀q(i ≤ q ⇒ i ≤ 33q ∨ p) ⇒ i ≤ p) ∀p∀i(♦i ≤ p & i ≤ 33i ∨ p ⇒ i ≤ p) ∀p∀i(♦i ≤ p & i ∧ ¬33i ≤ p ⇒ i ≤ p) ∀p∀i(♦i ∨ (i ∧ ¬33i) ≤ p ⇒ i ≤ p) ∀i(i ≤ ♦i ∨ (i ∧ ¬33i)) ∀i(i ≤ ♦i or i ≤ i ∧ ¬33i) ∀i(i ≤ ♦i or i ≤ ¬33i) ∀i(i ≤ 33i → ♦i) ∀x∀y(Rxy ∧ Ryx → Rxx) One can show that this property is not modally definable: Consider F1 = (W1 , R1 ) where W1 is the set of all integers, R1 = {(x, x + 1) | x ∈ W1 }, F2 = (W2 , R2 ) where W2 = {w0 , w1 }, R2 = {(w0 , w1 ), (w1 , w0 )}, then F2 is a bounded morphic image of F1 , F1  ∀x∀y(Rxy ∧ Ryx → Rxx), while F2 2 ∀x∀y(Rxy ∧ Ryx → Rxx). References 1. P. Blackburn, M. de Rijke, and Y. Venema. Modal logic, volume 53 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. 2. R. A. Bull. On modal logic with propositional quantifiers. The Journal of Symbolic Logic, 34(2):257–263, 1969. 3. W. Conradie, S. Ghilardi, and A. Palmigiano. Unified correspondence. In A. Baltag and S. Smets, editors, Johan van Benthem on Logic and Information Dynamics, volume 5 of Outstanding Contributions to Logic, pages 933–975. Springer Interna- tional Publishing, 2014. 4. W. Conradie, V. Goranko, and D. Vakarelov. Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA. Logical Methods in Computer Science, 2:1–26, 2006. Sahlqvist-type Correspondence Theory for SOPML 121 5. W. Conradie and A. Palmigiano. Algorithmic correspondence and canonicity for distributive modal logic. Annals of Pure and Applied Logic, 163(3):338 – 376, 2012. 6. W. Conradie, A. Palmigiano, and S. Sourabh. Algebraic modal correspondence: Sahlqvist and beyond. Journal of Logical and Algebraic Methods in Programming, 91:60–84, 2017. 7. D.Kaplan. S5 with quantifiable propositional variables. Journal of Symbolic Logic, 35:355, 1970. 8. K. Fine. For some proposition and so many possible worlds. PhD thesis, University of Warwick, 1969. 9. K. Fine. Propositional quantifiers in modal logic. Theoria, 36(3):336–346, 1970. 10. D. M. Gabbay. An irreflexivity lemma with applications to axiomatizations of conditions on tense frames. In Aspects of philosophical logic, pages 67–89. Springer, 1981. 11. V. Goranko and D. Vakarelov. Elementary canonical formulae: Extending Sahlqvist’s theorem. Annals of Pure and Applied Logic, 141(1-2):180–217, 2006. 12. M. Kaminski and M. Tiomkin. The expressive power of second-order propositional modal logic. Notre Dame Journal of Formal Logic, 37(1):35–43, 1996. 13. S. A. Kripke. A completeness theorem in modal logic. Journal of Symbolic Logic, 24(1):1–14, 1959. 14. H. Sahlqvist. Completeness and correspondence in the first and second order semantics for modal logic. In Studies in Logic and the Foundations of Mathematics, volume 82, pages 110–143. 1975. 15. B. ten Cate. Expressivity of second order propositional modal logic. Journal of Philosophical Logic, 35(2):209–223, 2006. 16. J. van Benthem. Modal logic and classical logic. Bibliopolis, 1983.