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
On Tue, 11 Jan 2005, Prof. Peter Johnstone wrote:
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?
Yes, and the answer is yes. Algebras satisfying all of the implications true for Heyting algebras have been called "Hilbert algebras", and their local finiteness was first shown in A. Diego, "Sur les algebres de Hilbert", Gauthier-Villars, Paris, 1966, although there is also an apparently earlier article in Spanish that I have not been able to get, A. Diego, "Sobre algebras de Hilbert", Notas de Logica Mathematica 26, Instituto de Matematica, Universidad Nacional del Sur, Bahia Blanca, 1965, that may be the same, or very similar. Better bounds on the size of free Hilbert algebras and a better construction of them can be found in A. Urquhart, "Implicational formulas in intuitionistic logic", JSL 39 (4), 1974, p. 661-664. Rasiowa discusses these algebras, under the name "positive implication algebras", in her book H. Rasiowa, An algebraic approach to non-classical logics, Studies in Logic and the Foundations of Mathematics, V. 78, North-Holland, 1974, referring to Diego and proving his representation theorem that every Hilbert algebra is a subalgebra of the Hilbert algebra of open sets of a topological space (the points are the binary-intersection-irreducible filters, appropriately defined). She also refers to J. C. Abbott, "Semi-boolean algebras", Matematicki Vesnik, 4 (1967), pp. 177-198. for the theory of "implication algebras" (all the implications true in Boolean algebras). Another important reference is the technical report N. G. De Bruijn, "Exact finite models for minimal propositional calculus over a finite alphabet." TR 75-WSK-02, Technological University Eindhoven, Netherlands, Department of Mathematics, February 1975. which deals with Heyting semilattices. De Bruijn also cites Diego and Urquhart, commenting: It was only after the completion of this paper that the author learned that proofs for the finiteness of the number of classes had been given by [Diego, Urquhart]. Both authors showed the finiteness for the case without conjunction, but the finiteness of the case with conjunction is a simple consequence. The present approach is very different; as a matter of fact our treatment shows that it is profitable to study the case of implication plus conjunction, since this reveals so much more of the structure. De Bruijn shows that free finitely generated Heyting semilattices are finite topological spaces (thus Kripke models), and he displays the cases n = 1,2,3 explicitly (with 1, 5, and 61 points), and calculates their cardinalities: |HS(1)| = 2 |HS(2)| = 18 |HS(3)| = 623,662,965,552,330 The general case is handled by a recursive construction. He says, of the sequence of cardinalities, a_1, a_2, a_3, ..., that "It can be expected that log a_(n+1) is of the order of a_n", so their sizes, though finite, become incomprehensible quite quickly. -- Todd Wilson A smile is not an individual Computer Science Department product; it is a co-product. California State University, Fresno -- Thich Nhat Hanh 12-Jan-2005 12:21:18 -0400,2592;000000000000-00000000
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
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.
I see a pattern that very strongly inclines me to the conjecture that they are all finite. Peter's poset is simply the product of three chains, 2 x 3 x 3. One rarely sees that kind of regularity in a combinatorial enumeration that blows up to infinity at some finite point. The one-generator chain being simply 2 (1 and x), the question then becomes, what's the next element in the sequence 2, 2 x 3 x 3, ...? I'd like to see one more term before going out on a limb here. :) Vaughan Pratt 12-Jan-2005 12:21:18 -0400,2004;000000000000-00000000
participants (4)
-
Peter Freyd -
Prof. Peter Johnstone -
Todd Wilson -
Vaughan Pratt