Re: Free Heyting semilattices
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
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
participants (2)
-
Peter Freyd -
Silvio Ghilardi