You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Jencel Panic (Dec 02 2024 at 14:57):Wikipedia says that the free Heyting algebra over one generator is called a Rieger–Nishimura lattice. but I found almost no info about this object, so I came here to fill the blanks.
From the term "Free Cyclic Heyting algebra " I can derive that it is composed of all statements that are derived from a single statement plus all of the the products, coproducts and hom objects that exist. Is there something more interesting to know about it? The graphic suggests that there are exactly 2 statements at each level of implication.
Also, what is the Rieger–Nishimura ladder (which is the dual of the lattice, according to some other article)?
Kevin Carlson (Dec 02 2024 at 17:39):I have a prized possession that's a sketch of this lattice Dana Scott once drew for me after I revealed to him I hadn't realized it's infinite. But it's on my desk in Berkeley so I can't share it right now.
Kevin Carlson (Dec 02 2024 at 17:39):The sketch is quite similar to the image you sent, anyway.
Kevin Carlson (Dec 02 2024 at 17:42):But yes, this is meant to be a picture of an inductive characterization of the whole lattice; you construct new elements by ing something with indirectly below it or by ing something with something directly (diagonally) below it, and the claim is that that's everything in the lattice.
John Baez (Dec 02 2024 at 17:48):Alas, those double dollar signs for LaTeX are deactivated when they're right next to a letter.
Kevin Carlson (Dec 02 2024 at 17:48):Ugh, how many times has that happened to me...
Peter Arndt (Dec 03 2024 at 08:34):If you take the language of usual intuitionistic propositional logic and consider not valuations in all Heyting algebras, but only in the Rieger-Nishimura lattice, you get a strengthening of intuitionistic logic, its so-called 1-scheme logic. See this article, the paragraph after Def. 3.1.
Peter Arndt (Dec 03 2024 at 08:36):Section 2.3 also gives some hints on why to consider the ladder.
Jencel Panic (Dec 03 2024 at 10:12):@Peter Arndt Sorry didn't get any of that (:
Perhaps I should start with the original paper by Nishimura, which I found in the paper you linked:
