Gödel algebras free over finite distributive lattices

Gödel algebras form the locally finite variety of Heyting algebras satisfying the prelinearity axiom (x→y)∨(y→x)=⊤. In 1969, Horn proved that a Heyting algebra is a Gödel algebra if and only if its set of prime filters partially ordered by reverse inclusion–i.e. its prime spectrum–is a forest. Our main result characterizes Gödel algebras that are free over some finite distributive lattice by an intrisic property of their spectral forest.