Topos representation of free Heyting algebras
Follow the latest progress by email.
Can every Heyting algebra be the lattice of subterminal objects of an elementary topos? The key test is the free Heyting algebra F₂ on two generators, with a possible obstruction extending to algebras surjecting onto it.
Why it matters and what counts as progress
Why it matters: An obstruction for the free two-generator algebra would limit the representation of abstract intuitionistic logic inside elementary topoi.
What counts as progress: Prove or obstruct such a representation for F₂ and algebras surjecting onto it, or classify an additional representable algebra family.
How the problem developed
- 27 Aug 2026 · Counterexample [1]
Yiqi Xu and Lingyuan Ye Reported that the free Heyting algebra on two generators cannot be the lattice of subterminal objects of an elementary topos; the obstruction also applies to Heyting algebras surjecting onto it.
AI contribution
Failure of Higher-Order Truth within Intuitionistic Propositional Logic
The free Heyting algebra F₂ on two generators cannot be the lattice of subterminal objects of an elementary topos. The obstruction extends to any Heyting algebra surjecting onto F₂, including free F_N for N≥2.
Sources
Website timeline
Publication dates and editorial changes.