Graded Modal Logic

Origin. Fine (1972) and Goble (1970) introduced graded modalities. Extends modal logic with counting. ◇≥n φ: "at least n accessible worlds satisfy φ." Useful for cardinality constraints. Applications in description logics and database queries.

Models. Counting accessible worlds. Standard modal: ◇φ means at least one accessible φ-world. Graded: ◇≥n φ means at least n accessible φ-worlds. Expresses majority, uniqueness, cardinality bounds. Strictly more expressive than basic modal logic.

Formalism.

Graded operators:

◇≥n φ: at least n R-successors satisfy φ
◇>n φ: more than n (= ◇≥(n+1))
◇≤n φ: at most n (= ¬◇≥(n+1))
◇=n φ: exactly n (= ◇≥n φ ∧ ◇≤n φ)

Semantics: M, w ⊨ ◇≥n φ iff |{v : wRv ∧ M, v ⊨ φ}| ≥ n

Special cases:

◇≥1 φ = ◇φ (standard diamond)
□φ = ¬◇≥1 ¬φ (standard box)
◇≤0 φ = □¬φ (no successors satisfy)
◇≥1 φ ∧ ◇≤1 φ = ◇=1 φ (unique successor)

Axioms:

◇≥0 φ (at least zero: tautology)
◇≥(n+1) φ → ◇≥n φ (monotonicity)
◇≥n (φ ∨ ψ) → ◇≥n φ ∨ ◇≥1 ψ (distribution)
Counting interaction axioms

In description logic (qualified number restrictions): ≥n R.C: at least n R-fillers satisfying C. ∃R.C = ≥1 R.C

Symbols.

Symbol	Unicode	Name	Meaning
◇≥n	—	At least n	Counting diamond
◇≤n	—	At most n	Upper bound on successors
◇=n	—	Exactly n	Exact count
◇	U+25C7	White diamond	Standard possibility, ◇≥1
□	U+25A1	White square / Box	Standard necessity, ¬◇≥1¬
≥	U+2265	Greater-than or equal to	Lower bound on the count
≤	U+2264	Less-than or equal to	Upper bound on the count
⊨	U+22A8	Satisfaction	Truth at a world in a model
¬	U+00AC	Not sign	Negation
∧	U+2227	Logical and	Conjunction
∨	U+2228	Logical or	Disjunction
→	U+2192	Rightwards arrow	Material implication
⊤	U+22A4	Down tack	Verum; ◇≥2⊤ counts successors outright
ω	U+03C9	Greek small omega	Infinite grade, outside the language
φ, ψ	U+03C6, U+03C8	Phi, psi	Schematic formulas
R	—	Accessibility relation	Successor relation, a role in description logic
n	—	Grade	Numeral bounding the count
\|S\|	—	Cardinality	Size of the successor set
≥n R.C	—	Qualified number restriction	Description-logic form of ◇≥n

Metatheory. Fine (1972) gave a complete axiomatization of the graded extension of K and established its finite model property; the models can require exponentially many successors, so that property alone yields no elementary decision procedure. Tobies (2001) settled the complexity: satisfiability is PSPACE-complete even when the grades are written in binary, refuting the expectation that succinct numerals push the problem to EXPTIME, so counting costs nothing over K. Under the standard translation graded modal logic lands inside the two-variable fragment with counting quantifiers, which Grädel, Otto and Rosen (1997) proved decidable, and de Rijke (2000) supplied the matching characterization theorem: graded modal logic is exactly the fragment of first-order logic invariant under counting bisimulation, the refinement whose back-and-forth clauses match successors injectively. The gain in expressive power over K is real rather than notational, since ◇≥2⊤ is not equivalent to any basic modal formula — no ordinary bisimulation distinguishes a world with one successor from a world with two. The graded μ-calculus is still EXPTIME-complete (Kupferman, Sattler and Vardi, 2002), no worse than the plain μ-calculus.

Applies to. Description logics (number restrictions in OWL). Database queries (cardinality constraints). Social choice theory (majority). Quantitative requirements. Resource bounds. Voting and preferences. Multi-agent systems (counting agents).

Limitations. Counting reaches exactly one step: the operators bound the number of immediate R-successors, so nothing can be said about how many worlds in the model as a whole, or along a path, satisfy a formula, and global counting requires the universal modality or nominals. The grades are numerals compared against fixed constants, so a cardinality comparison between two successor sets — more φ-successors than ψ-successors — is not expressible and needs a Presburger extension, and infinite grades such as ◇≥ω fall outside the language entirely. Counting bisimulation is a ceiling of the same kind as ordinary bisimulation: irreflexivity, well-foundedness and the identity of a world stay undefinable, so grading adds cardinality and nothing else. Combination is where the failure is sharp — number restrictions applied to transitive relations make the resulting description logic undecidable, which is why SHIQ forbids them.