Observation algebras: Heyting algebra over coherence spaces

conference paper, in TbiLLC 2025

In this report, we introduce observation algebras, constructed by considering the downclosed subsets of a coherence space ordered by reverse inclusion. These may be interpreted as specifications of sets of events via some predicates with some extra structure. We provide syntax for these algebras, as well as axiomatisations. We establish completeness of these axiomatisations in two cases: when the syntax is that of bounded distributive lattices (conjunction, disjunction, top, and bottom), and when the syntax also includes an implication operator (in the sense of Heyting algebra), but the underlying coherence space satisfies some tractability condition. We also provide a product construction to combine graphs and their axiomatisations, yielding a sound and complete composite system. This development has been fully formalised in Rocq.

@inproceedings{b25a,
    title = "Observation algebras: Heyting algebra over coherence spaces",
    author = "{Paul Brunet}",
    year = 2025,
    booktitle = "TbiLLC",
    doi = "10.48550/arXiv.2503.07130"
}

Links

	Permanent link
	Conference abstract
	Preprint on HAL
	Preprint on arXiV

Other ressources

	Rocq proof on Github
	Documentation of the proof

Related talks
	Observation algebras: Heyting algebra over coherence spaces TbiLLC in Tskaltubo, September 2025.	More