The Lattice of Congruences of a Finite Line Frame

Abstract

Let $\mathbf{F}=⟨F,R⟩$ be a finite Kripke frame. A congruence of $\mathbf{F}$ is a bisimulation of $\mathbf{F}$ that is also an equivalence relation on F. The set of all congruences of $\mathbf{F}$ is a lattice under the inclusion ordering. In this article we investigate this lattice in the case that $\mathbf{F}$ is a finite line frame. We give concrete descriptions of the join and meet of two congruences with a nontrivial upper bound. Through these descriptions we show that for every nontrivial congruence $\rho$, the interval $[\mathrm{I}{\mathrm{d}}_{\mathrm{F}},\rho ]$ embeds into the lattice of divisors of a suitable positive integer. We also prove that any two congruences with a nontrivial upper bound permute.

arXiv comment31 pages, 11 figures. Expanded intro, conclusions rewritten. New, less geometrical, proofs of Lemma 19 and (former) Lemma 34