Sahlqvist Correspondence Theory For Second-Order Propositional Modal Logic

Sahlqvist Correspondence Theory forSecond-Order Propositional Modal Logic(Short Paper)Zhiguang ZhaoTaishan University, China1IntroductionSecond-Order Propositional Modal Logic (SOMPL). Modal logic with propositional 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 satisfiability problem is not decidable, and indeed not even analytical. In Kaminski andTiomkin [12], the authors showed that the expressive power for SOMPL whosemodalities are S4.2 or weaker is the same as second-order predicate logic. However, not every second-order formula is equivalent to an SOMPL-formula, sinceSOMPL-formulas are preserved under generated submodels (see van Benthem[16]). In ten Cate [15], the author proved the analogues of the van BenthemRosen theorem (on the model level) and Goldblatt-Thomason theorem (on theframe level) for SOMPL. Therefore, a natural question is: on the frame level, canwe find a natural fragment of SOPML-formulas such that each formula in thisfragment 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] concernsthe 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 firstorder correspondents and are canonical, i.e. their validity are closed under takingcanonical extensions. In the present paper, we identify the Sahlqvist formulas ofSOMPL, which cover and properly extend the Sahlqvist fragment in basic modallogic. 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 SOMPLSahlqvist formula q( p(p 3p q) q) is not canonical, which is in contrastto the basic modal logic setting where each Sahlqvist formula is canonical. Thepresent paper use the same methodology as [6, 3]. The Sahlqvist fragment ofSOPML is defined in a step-by-step way, and we give an algorithm ALBASOPML(Ackermann Lemma Based Algorithm) which can successfully reduce Sahlqvistformulas in SOPML to first-order formulas and is sound with respect to Kripkesemantics.Copyright 2021 for this paper by its authors. Use permitted under CreativeCommons License Attribution 4.0 International (CC BY 4.0).

Sahlqvist-type Correspondence Theory for SOPML22.1113PreliminariesLanguage and semanticsIn the present paper we consider the unimodal language. Given a set Prop ofpropositional variables, the second-order propositional modal formulas are defined as follows:ϕ :: p ϕ ϕ ϕ ϕ ϕ ϕ ϕ 2ϕ 3ϕ pϕ pϕwhere p Prop. We use the boldface notation p to denote a set of propositional variables and use ϕ( p) to indicate that the propositional variables occurin ϕ are all in p . We say that an occurrence of a propositional variable p in aformula ϕ 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 definedas follows:Definition 1. A Kripke frame is a pair F (W, R) where W 6 is the domainof F, the accessibility relation R is a binary relation on W . A Kripke model isa pair M (F, V ) where V : Prop P (W ) is a valuation on F. VXp denote avaluation which is the same as V except that VXp (p) X W .Now the satisfaction relation can be defined as follows: given any Kripkemodel M (W, R, V ), any w W , the basic and Boolean cases are standard,and for modalities and propositional quantifiers,M, wM, wM, wM, w2ϕ iff for any v such that Rwv, M, v ϕ;3ϕ iff there exists v such that Rwv and M, v ϕ; pϕ iff for all X W , (W, R, VXp ), 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 ofSahlqvist SOPML formulas, we will need the following expanded modal languagewhich 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-lookingbox and diamond respectively, i and i are nominal quantifiers, and l is a binarymodality. We call a formula pure if it does not contain propositional variables orpropositional quantifiers (it can contain nominals, nominal quantifiers and thebinary modality l).The interpretation of the expanded modal language is given as follows: For avaluation V , it is defined as V : Prop Nom P (W ) such that V (i) is a singletonfor all i Nom. The additional satisfaction clauses are given as follows (here Vvidenote a valuation which is the same as V except that Vvi (i) {v} W .):

114Zhiguang ZhaoM, wM, wM, wM, wM, wM, wiiff V (i) {w}; ϕiff for any v such that Rvw, M, v ϕ; ϕiff there exists v such that Rvw and M, v ϕ; iϕiff for all v W , (W, R, Vvi ), w ϕ; iϕiff there exists v W such that (W, R, Vvi ), 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 naturalway.2.2Inequalities and complex inequalitiesWe 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 expandedmodal language. We define complex inequalities as follows:Comp :: Ineq Comp & Comp Comp Comp pComp pComp iComp iCompHere 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 ofpointed models (M, w). The semantics of complex inequalities is defined as follows:– An inequality is interpreted as follows:(W, R, V )(for all w W, if (W, R, V ), w– (W, R, V )– (W, R, V )Comp2 );– (W, R, V )– (W, R, V )Comp;– (W, R, V )– (W, R, V )2.3ϕ ψ iffϕ, then (W, R, V ), wψ);Comp1 &Comp2 iff (W, R, V ) Comp1 and (W, R, V ) Comp2 ;Comp1 Comp2 iff ((W, R, V )Comp1 implies (W, R, V ) pComp iff for all X W , (W, R, VXp ) Comp; pComp iff there exists an X W such that (W, R, VXp ) iComp iff for all v W , (W, R, Vvi ) Comp; iComp iff there exists an v W such that (W, R, Vvi )Comp.Standard translationIn the correspondence language which is second-order due to the existence ofpropositional quantifiers in SOPML, we have a binary predicate symbol R corresponding to the binary relation, a set of constant symbols i correspondingto each nominal i, a set of unary predicate symbols P corresponding to eachpropositional variable p.Definition 2. The standard translation of the expanded SOPML language isdefined as follows (for the basic and Boolean case, it is standard):

Sahlqvist-type Correspondence Theory for SOPML––––––––––115STx (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 SOPMLformula ϕ,M, w ϕ iff M STx (ϕ)[x : w].For inequalities and complex inequalities, the standard translation is givenin 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 complexinequality Comp,M Ineq iff M ST (Ineq);M3Comp iff M ST (Comp).Sahlqvist formulas in second-order propositional modallogicIn this section, we define Sahlqvist formulas of second-order propositional modallogic step by step.We first define (quantifier-free) positive formulas POS( p) whose propositonalvariables are among p :POS( p) :: p 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 positiveconsequent part in Sahlqvist formulas in basic modal logic, which are goingto receive minimal valuations. The reason why we do not allow propositionalquantifiers in positive formulas is that we want the formula after receiving theminimal valuations to be translated into a first-order formula, while propositionalquantifiers will make it second-order.

1163.1Zhiguang ZhaoThe Π1 -fragment: Sahlqvist formulas in basic modal logicWe define the Π1 -Sahlqvist antecedent Sahl1 ( p) whose propositonal variables areamong p :Sahl1 ( p) :: 2n p POS( p) Sahl1 ( p) Sahl1 ( p) 3Sahl1 ( p)where p is in p .Then the Π1 -Sahlqvist formulas are defined as p(Sahl1 ( p) POS( p)). Indeed, Sahlqvist formulas1 in the basic modal logic setting can be treated asuniversally quantified by propositional quantifiers which bind all occurrences ofpropositional variables, so in this sense the Π1 -Sahlqvist formulas can be takenas the Sahlqvist formulas in basic modal logic.3.2The Π2 -fragmentWe 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 propositionalvariables: q is to receive minimal valuations for q from somewhere else, and p isused 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) :: Sahl1 ( p) q(Sahl1 ( q) PIA( q, p )) Sahl2 ( p) Sahl2 ( p) 3Sahl2 ( p)Then Π2 -Sahlqvist formulas are defined as p(Sahl2 ( p) POS( p)).It is easy to see that formulas of the form p(Sahl1 ( p) q(Sahl1 ( q) PIA( q, p )) POS( p)) are in the Π2 -hierarchy.3.3The Πn -fragmentNow for the Πn -fragment, assume that we have already defined Πn 1 -Sahlqvistantecedents Sahln 1 ( p) and Πn 1 -Sahlqvist formulas p(Sahln 1 ( p) POS( p)),then we can define Πn -Sahlqvist antecedents as follows:Sahln ( p) :: Sahln 1 ( p) q(Sahln 1 ( q) PIA( q, p )) Sahln ( p) Sahln ( p) 3Sahln ( p)Then Πn -Sahlqvist formulas are defined as p(Sahln ( p) POS( p)).1In [1, Chapter 3], what we call Sahlqvist formulas are called Sahlqvist implications.

Sahlqvist-type Correspondence Theory for SOPML4117The Algorithm ALBASOMPLIn the present section, we define the correspondence algorithm ALBASOMPL forsecond-order propositional modal logic, in the style of [4, 5]. The algorithm receives a Πn -Sahlqvist formula p(Sahln ( p) POS( p)) as input and goes in threestages.1. Preprocessing and first approximation:The algorithm receives a Πn -Sahlqvist formula p(Sahln ( p) POS( p)) asinput, and then apply the rewriting rule: p(Sahln ( p) POS( p)) p(Sahln ( p) POS( p))Then apply the first-approximation rule: p(Sahln ( p) POS( 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 inwhich p occurs either in the form ϕ p where ϕ is pure or in the formj 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 occurin the whole complex inequality before applying the rule.(c) The residuation rules:α 2β(Res 2) α βα β γ(Res )α β γ