Does anyone know of any work on the question: is the free Heyting semilattice (i.e. the free cartesian closed poset) on a finite set of generators always finite? Or, to put an equivalent question in terms more familiar to logicians: is the Lindenbaum algebra for the pure implicational calculus, with a finite number of primitive propositions, always finite? (Note that the two questions are equivalent, though not the same: although we have the operation of conjunction (= meet) as well as implication in a Heyting semilattice, any Heyting-semilattice term is expressible as a finite conjunction of terms involving only implication.) Of course, free Heyting algebras are wildly infinite; but the wildness seems to derive from the (lack of) interaction between disjunction and implication, so things ought to be better-behaved if you leave out the operation of disjunction. I have explicitly calculated the free Heyting semilattice on two generators: it turns out to have 18 elements, which is a lot smaller than I'd expected. (Even more bizarrely, it turns out to be self-dual as a poset: I append its Hasse diagram below, for anyone who's interested.) However, it seems fairly clear that the corresponding calculation with three generators is too large to be done by hand, and I can't see any "pattern" emerging from the two-generator one which might indicate why they should all be finite. It seems quite likely that someone has considered the problem before; so I'd be very grateful for any pointers to relevant literature. Peter Johnstone Here is the Hasse diagram for the free Heytng semilattice on {x,y}. Conventions: implication is denoted by juxtaposition, and binds more strongly than conjunction (denoted &). Iterated implications are associated from left to right -- that is, pqr denotes ((p => q) => r) -- unless otherwise parenthesized. (Interestingly, with these conventions there is only one element whose description requires the use of parentheses: it may be equivalently described as xy(yxx), xy(yxy), yx(xyx) or yx(xyy).) 1 /|\ / | \ / | \ / | \ / | \ / | \ yxyy xy(yxx) xyxx /|\ / \ /|\ / | \ / \ / | \ / | \/ \/ | \ / | /\ /\ | \ / | / \ / \ | \ / |/ \ / \| \ yx xyy yxyy&xyxx yxx xy |\ / \ /|\ / \ /| | \ / \ / | \ / \ / | | \/ \/ | \/ \/ | | /\ /\ | /\ /\ | | / \ / \ | / \ / \ | |/ \ / \|/ \ / \| xyx xyyx xyy&yxx yxxy yxy \ |\ / \ /| / \ | \ / \ / | / \ | \/ \/ | / \ | /\ /\ | / \ | / \ / \ | / \|/ \ / \|/ x xy&yx y \ | / \ | / \ | / \ | / \ | / \|/ x&y 11-Jan-2005 13:05:23 -0400,3879;000000000001-00000000