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.

Metatheory. Graded modal logic decidable (EXPTIME). More expressive than basic modal. Finite model property holds. Complete axiomatization exists. Complexity: satisfiability is PSPACE for fixed n, EXPTIME with n in input. Expressively equivalent to counting in two-variable logic with counting.

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. Complexity grows with numbers. Infinite counts: ◇≥ω requires infinitary logic. Numbers in constraints can be large. Axiomatization less elegant than basic modal. Graded μ-calculus more complex. Counting approximations may suffice in practice.

© 2026 Lingenic LLC