The lattice of congruences of a finite line frame
Carlos Areces, Miguel A. Campercholi, Daniel Penazzi, Pedro Sánchez Terraf · Journal of Logic and Computation · 2017
Let F = F, R be a finite Kripke frame.A congruence of F is a bisimulation of F that is also an equivalence relation on F. The set of all congruences of F is a lattice under the inclusion ordering.In this article we investigate this lattice in the case that 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 ρ, the interval [Id F , ρ] embeds into the lattice of divisors of a suitable positive integer.We also prove that any two congruences with a nontrivial upper bound permute.