Polyadic Modal Logic

Origin. Jónsson and Tarski, "Boolean Algebras with Operators" (1951), already worked with operators of arbitrary finite arity and proved the representation theorem at that generality. Goldblatt, "Varieties of Complex Algebras" (1989), and Venema's dissertation Many-Dimensional Modal Logic (1992) developed the modal side, and Blackburn, de Rijke and Venema, Modal Logic (2001), made the arbitrary modal similarity type the default setting rather than a generalization of the unary case.

Models. A modal similarity type is a set of operators together with an arity function. An n-ary diamond is interpreted by an (n+1)-ary accessibility relation R ⊆ W^{n+1}, so R(w, v₁, ..., vₙ) relates a world to an n-tuple of worlds. Unary modal logic is the case n = 1. Temporal Until, Lewis conditionals presented relationally, arrow logic's composition operator, and the relation-algebraic reducts of products and fusions are all instances.

Formalism.

n-ary modal operator: ◇ₙ(φ₁, ..., φₙ): n-ary diamond □ₙ(φ₁, ..., φₙ): n-ary box

Semantics: w ⊨ ◇ₙ(φ₁,...,φₙ) iff ∃v₁...vₙ. R(w,v₁,...,vₙ) ∧ v₁⊨φ₁ ∧ ... ∧ vₙ⊨φₙ

Duality: □ₙ(φ₁,...,φₙ) = ¬◇ₙ(¬φ₁,...,¬φₙ) Generalized De Morgan. Truth condition is universal-disjunctive, not universal-conjunctive: w ⊨ □ₙ(φ₁,...,φₙ) iff ∀v₁...vₙ. R(w,v₁,...,vₙ) → (v₁⊨φ₁ ∨ ... ∨ vₙ⊨φₙ). Often written ▽ rather than □ₙ to mark the difference.

Normality: ◇ₙ is normal in each argument: distributes over ∨ coordinatewise; ◇ₙ(...,⊥,...) = ⊥. Minimal polyadic logic K_τ: normality axioms for each operator.

Standard translation: ST_x(◇ₙ(φ⃗)) = ∃y₁...∃yₙ (Rxy₁...yₙ ∧ ⋀ᵢ ST_{yᵢ}(φᵢ)). Lands in the guarded fragment of first-order logic: every quantifier block is guarded by the atom Rxy₁...yₙ.

Algebraic semantics: Boolean algebras with n-ary normal additive operators. Complex algebra of a frame; canonical extension. Jónsson–Tarski representation holds at every arity.

Binary modality examples: ◇₂(φ,ψ): both accessible Conditional: ψ ⇒ φ as □₂(¬ψ,φ) Until: φ U ψ as binary temporal.

Correspondence: n-ary frame conditions. More expressive than unary. Captures complex dependencies.

Composition: Product: ◇₁◇₂ as ◇₂ Fusion: ◇₁ + ◇₂ Polyadic unifies.

Arrow logic: Binary modality. Composition of transitions. Applications to processes.

Symbols.

Metatheory. Sahlqvist's theorem is not restricted to unary operators: it holds for arbitrary modal similarity types, so any polyadic axiom in Sahlqvist form is canonical and defines an elementary class of (n+1)-ary frames. The Goldblatt–Thomason theorem likewise generalizes, characterizing the modally definable classes of polyadic frames as those closed under bounded morphic images, generated subframes and disjoint unions and reflecting ultrafilter extensions. Bisimulation generalizes to (n+1)-ary back-and-forth clauses, and van Benthem's characterization survives: the polyadic modal language is the bisimulation-invariant fragment of first-order logic over the corresponding signature. The standard translation lands inside the guarded fragment, shown decidable by Andréka, van Benthem and Németi (1998), which explains why the minimal polyadic logic of any finite similarity type has the finite model property and is decidable, with satisfiability PSPACE-complete as for K. Jónsson–Tarski duality holds at every arity, so complex algebras and canonical extensions behave as in the unary case.

Applies to. Arrow logic. Process composition. Complex accessibility. Unified modal framework.

Limitations. The n-ary box's truth condition is universal over tuples but disjunctive across coordinates, so it does not distribute over conjunction argumentwise and the normal forms, filtration arguments and modal-depth induction familiar from unary logic do not transfer unchanged. Decidability is fragile once frame conditions are imposed: arrow logic over square frames is undecidable, since it is a notational variant of the equational theory of representable relation algebras, which Tarski showed undecidable and Monk (1964) showed not finitely axiomatizable. Products behave the same way — S5 × S5 is decidable but S5 × S5 × S5 is not, so a third dimension destroys the property. Polyadic operators also do not in general reduce to unary ones, so results proved for a specific similarity type give no information about others, and each new arity requires its own completeness and complexity analysis.

© 2026 Lingenic LLC