The lattice of congruences of a finite line frame

ARECES, CARLOS; CAMPERCHOLI, MIGUEL; PENAZZI, DANIEL; SÁNCHEZ TERRAF, PEDRO

JOURNAL OF LOGIC AND COMPUTATION

OXFORD UNIV PRESS

Lugar: Oxford; Año: 2017 vol. 27 p. 2653 - 2688

0955-792X

Let F 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 non-trivial upper bound. Through these descriptions we show that for every non-trivial congruence R, the interval [0,R] embeds into the lattice of divisors of a suitable positive integer. We also prove that any two congruences with a non-trivial upper bound permute.