  We study finitely generated free Heyting algebras from a topological and from
a model theoretic point of view. We review Bellissima's representation of the
finitely generated free Heyting algebra; we prove that it yields an embedding
in the profinite completion, which is also the completion with respect to a
naturally defined metric. We give an algebraic interpretation of the Kripke
model used by Bellissima as the principal ideal sprectrum and show it to be
first order interpretable in the Heyting algebra, from which several model
theoretic and algebraic properties are derived. For example we prove that a
free finitely generated Heyting algebra has only one set of free generators,
which is definable in it. As a consequence its automorphism group is the
permutation group over its generators.
