Since we're on the subject, say that a Heyting semi-lattice (sometimes Hilbert algebra) is LINEAR if it satisfies the further equation: ((x -> y) -> z) ^ ((y -> x) -> z) = z The prime examples are totally ordered sets (where, necessarily, x -> y = if y < x then y else 1). One may prove that every linear HSL is isomorphic to a subalgebra of a cartesian product of totally ordered HSLs. One may then prove that every linear HSL is, in fact, a Heyting algebra: the join operation is constructible as: ((x -> y) -> y) ^ ((y -> x) -> x) The proof is easy: first verify that this term yields the join of x and y in any totally ordered HSL; second realize that it therefore necessarily satisfies the axioms for a join operation (with respect to the given meet operation) in every totally ordered HSL; third note that the representation theorem says that such must be the case in every linear HSL. There's a nice converse: a variety of HSLs all of whose members are Heyting algebras is necessarily a variety of linear HSLs. (And it's not hard to find all such varieties.) Anyway, it is possible to count the number of elements in free linear HSLs. You can find the following on Neil Sloane's Encyclopedia of Integer Sequences: ID Number: A067765 URL: http://www.research.att.com/projects/OEIS?Anum=A067765 Sequence: 1,2,18,370386,143436460933743129632865858558642 Name: Order of linear Heyting semi-lattice on n points. References P. J. Freyd, On the size of Heyting semi-lattices, preprint, 2002. Formula: a(0)=1; for n>0, a(n) = product((1+a(r))^binomial(n,r),r=0..n-1). Maple: A067765 := proc(n) option remember; if n=0 then 1 else mul((1+A067765(r))^binomial(n,r),r=0..n-1); fi; end; See also: Sequence in context: A059783 A066361 A007184 this_sequence A086367 A059706 A096481 Adjacent sequences: A067762 A067763 A067764 this_sequence A067766 A067767 A067768 Author(s): Peter Freyd (pjf(AT)saul.cis.upenn.edu), Feb 07 2002 Extension: The next term is too large to include. 18-Jan-2005 13:32:32 -0400,1956;000000000000-00000000