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