Sources and background

Bellissima’s construction

Motivation

Bellissima’s universal model gives a representation of the free Heyting algebra on two generators by building the "image-finite part" of the dual space. The construction is recursive, and proceeds by layers, taking into account the structure of successors and the "colors" -- the propositional variables satisfied by each point.

Bellissima’s universal model $U (2)$ is the image-finite part part of $X_{2}$ . We begin with four maximal points, one of each colour $\emptyset$ , ${p}$ , ${q}$ , ${p, q}$ .

At each round we build a new layer of $U (2)$ as follows: pick a finite antichain $A$ from the existing model, containing at least one point from the preceding layer, and a color $C$ which is below the color of each point in this antichain; then add a point which has $A$ as its successors, and is colored $C$ .

The interactive display shows the four maximal points, and a selection of 18 points (the layers grow extremely quickly -- at the third layer several hundreds or thousands of points). The color upsets in the end are given by the points sharing the colors $p$ and $q$ .

At the end of the construction, the poset will contain a copy of each (irreducible) 2-generated Kripke model.

Details of the construction

Choose a nonempty finite antichain A in the existing model, containing a point from the preceding layer. For each colour C contained in every colour on A, add the unique point x whose immediate successors are exactly A. A singleton support requires a strict colour drop.

col(x) = C \subseteq ⋂ a\inA col(a) ↑x ∖ {x} = ↑A A = {a} \Rightarrow C ⊊ col(a)

This partial view has 18 points across four layers: all four maxima, followed by 4, 5, and 5 selected points. Every ancestor of every selected point is included, so all displayed Hasse lines are genuine covers in U(2), including lines that skip a row.

The two colour upsets are p = {x : p ∈ col(x)} and q = {x : q ∈ col(x)}.

References

Fabio Bellissima (1986)
Finitely generated free Heyting algebras.
The Journal of Symbolic Logic 51(1), 152–165.
DOI
Luck Darnière and Markus Junker (2010)
On Bellissima’s construction of the finitely generated free Heyting algebras, and beyond.
Archive for Mathematical Logic 49(7–8), 743–771.
DOI
Nick Bezhanishvili (2006)
Lattices of Intermediate and Cylindric Modal Logics.
PhD thesis, Universiteit van Amsterdam. ILLC Dissertation Series DS-2006-02. ISBN 978-90-5776-147-8.
Thesis
Ladislav Svante Rieger (1949)
On the Lattice Theory of Brouwerian Propositional Logic.
Acta Facultatis Rerum Naturalium Universitatis Carolinae, no. 189, pp. 1–40. F. Řivnáč, Prague.
Bibliographic record, reference [3]
Iwao Nishimura (1960)
On formulas of one variable in intuitionistic propositional calculus.
The Journal of Symbolic Logic 25(4), 327–331.
DOI
R. Elageili and J. K. Truss (2012)
Finitely generated free Heyting algebras: the well-founded initial segment.
The Journal of Symbolic Logic 77(4), 1291–1307.
DOI
Leo Esakia (2019)
Heyting Algebras: Duality Theory.
Trends in Logic, vol. 50. Edited by Guram Bezhanishvili and Wesley H. Holliday; translated by Anton Evseev. Springer, Cham.
DOI