The Lattice of Congruences of a Finite Line Frame

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

JOURNAL OF LOGIC AND COMPUTATION

OXFORD UNIV PRESS

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

0955-792X

Let F = (F, R) be a finite Kripke frame. A congruence of F is a bisimulation of F thatis also an equivalence relation on F. The set of all congruences of F is a lattice under theinclusion ordering. In this article we investigate this lattice in the case that F is a finiteline frame. We give concrete descriptions of the join and meet of two congruences witha nontrivial upper bound. Through these descriptions we show that for every nontrivialcongruence ρ, the interval [Id F , ρ] embeds into the lattice of divisors of a suitable positiveinteger. We also prove that any two congruences with a nontrivial upper bound permute.