=Paper=
{{Paper
|id=Vol-3009/short3
|storemode=property
|title=Sahlqvist-type Correspondence Theory for Second-Order Propositional Modal Logic (Short Paper)
|pdfUrl=https://ceur-ws.org/Vol-3009/short3.pdf
|volume=Vol-3009
|authors=Zhiguang Zhao
|dblpUrl=https://dblp.org/rec/conf/kr/Zhao21
}}
==Sahlqvist-type Correspondence Theory for Second-Order Propositional Modal Logic (Short Paper)==
https://ceur-ws.org/Vol-3009/short3.pdf
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.