Intuitionistic propositional logic, envisaged as the free Heyting algebra over a non-empty collection of generators P, is infinite. When P is a singleton, we obtain the well-known Rieger–Nishimura lattice. For larger P, however, the free Heyting algebra is very complex and little is known about it. Closer inspection learns that the combination of disjunction and implication causes the free Heyting algebras to become infinite. When we only consider formulae of IpL without disjunction, the corresponding algebras are finite. However, as N.G. de Bruijn already pointed out, their size grows superexponentially with the number of generators. I will report on investigations on fragments of IpL without disjunction. For the characterization of these fragments, (quasi-)exact models are used, a special kind of universal models. The presentation is based on joint work with Dick de Jongh and Lex Hendriks.
http://logcom.oxfordjournals.org/cgi/reprint/exq058?ijkey=s85AtbYEq6ckd9r&keytype=ref