Yes, finitely generated Heyting semilattices are finite. My proof is recorded in the dissertation of one Samuel Johnson from the 70s. I suspect that it had many earlier proofs. My proof is as follows: For any equational theory (with a finite number of primitive operations) to show that the free algebra on n generators is finite it suffices to show that there is a (finite) upper bound on the size of subdirectly irreducible algebras on n generators. For HSLs, subdirect irreducibility is equivalent to a unique maximal element below 1. I'll denote the element M. I like to call these "local HSLs". (For examples, take any non-trivial topological space and any point x therein; identify open sets if they are locally equivalent at x, that is if their intersections with an open nhbd of x are equal; the HA of equivalent class is local -- M is named by the complement of the closure of {x}). If we remove M from a local HSL, the result is still an HSL (clearly M is not the meet of two things in the complement, and -- perhaps not quite so clearly -- M is not the result of x -> y for x and y in the complement, indeed M = x -> y iff x = 1 and y = M). Hence if a local HSL is generated by n of its elements, then its complement is necessarily generated by n-1 of its elements. Hence a a local HSL has at most K+1 elements where K is the number of elements in the free HSL on n generators. Done. 12-Jan-2005 12:21:18 -0400,1002;000000000000-00000000