Authors
Yde Venema
Date (dd-mm-yyyy)
2007
Title
A modal distributive law
Publication Year
2007
Number of pages
1
Publisher
Springer Verlag
ISBN
9783540734437
Document type
Conference contribution
Abstract

In our talk we consider the coalgebraic, or cover modality ∇ which, in modal logic, goes back to the work of Fine on normal forms. The connective, taking a set of formulas as its argument, can be defined in terms of the usual box and diamond operators: ∇Φ:=□∨ΦΛ∧◇Φ where ◇Φ denotes the set {◇φ | φ ∈ Φ}. Conversely, the standard modalities can be defined in terms of the cover modality, from which it follows that we may equivalently base our modal language on ∇ as a primitive symbol: ◇φ ≡ ∇ {φ, ⊤} □φ ≡ ∇ ø ∨ ∇{φ}. The main purpose of the talk is to underline the fundamental importance of the following equivalence, which we call a distributive law since it shows how conjunctions distribute over nabla's (and disjunctions): ∇Φ Λ ∇ Φ′ ≡ ∨ Z∈ΦbowtieΦ′ ∇{φ Λ φ′ | (φ,φ′) ∈ Z}. Here Φ bowtie Φ′ denotes the set of relations R ⊆ Φ × Φ′ that are full in the sense that for all φ ∈ Φ there is a φ′ ∈ Φ′ with (φ,φ′) ∈ R, and vice versa. As an important corollary of (1) and the equidefinability of ∇ and {□, ◇}, every modal formula can be rewritten into a distributive normal form in which the only conjunctions are of the form ∧ P Λ ∇Φ, where P is a set of literals, i.e., proposition letters and negations of proposition letters. We then move on to some consequences of this fact. First we show that formulas in distributive normal form allow a direct, inductive definition of uniform interpolants. And second, we briefly review the work of Janin and Walukiewicz on automata for the modal μ-calculus (which is where the notion of distributive normal form stems from). Finally, we turn to some of our recent work in this area. We discuss our axiomatization of (positive) modal logic based on the cover modality, and, time permitting, sketch its connection with the Vietoris construction in topology. We finish with putting the cover modality into the wider, coalgebraic perspective, introduced by Moss, and discuss the meaning of the associated distributive law in this more general setting.

URL
go to publisher's site
Permalink
https://hdl.handle.net/11245.1/a9affdfc-05eb-4227-8985-a0b523e53b13