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.)
The answer is yes, it is Diego-McKay theorem: semilattices with implication (usually called Brouwerian semilattices) are a locally finite variety; in other words, there are only finitely many intuitionistically non-equivalent propositional formulas built up from finitely many propositional letters, conjunction and implication. For a quick algebraic proof of this fact, see p.107 in P. Kohler "Brouwerian semilattices", Trans. Amer. Math. Soc., vol. 268, n.1, (1981), pp.103-126 The same paper describes a duality for finite brouwerian semilattices and gives some cardinality information on p.118 for n-generated free algebras (bounds are very large: on 3 generators there are 623, 662, 965, 552, 330 elements !!!!! ). silvio ghilardi Silvio Ghilardi Professor in Logic Dipartimento di Scienze dell'Informazione Università degli Studi di Milano via Comelico 39 20135 Milano, Italy e-mail: ghilardi@dsi.unimi.it tel: +39/0250316217 fax:+39/0250316373 web-page: http://homes.dsi.unimi.it/~ghilardi/ 12-Jan-2005 12:21:18 -0400,1744;000000000000-00000000