Not every Heyting algebra is the subterminal lattice of a topos
The free Heyting algebra on two generators cannot be the lattice of subterminal objects of an elementary topos, answering the question in the negative.
- Lab
- Independent
- Model
- ChatGPT 5.6 Sol
- Field
- Mathematics
- Date
- 2026-08-27
- Human collaborators
- Lingyuan Ye, Yiqi Xu
Sources
Original work
Independent commentary
What was found
The question is whether every Heyting algebra arises as the lattice of subterminal objects of an elementary topos, which would say that intuitionistic propositional logic is fully realised by higher-order truth. The answer is no, and the witness is concrete: the free Heyting algebra on two generators cannot be such a lattice.
Novelty check
The question is a clean yes-or-no about a standard construction relating Heyting algebras to elementary toposes, and the paper answers it with a specific named algebra rather than an abstract obstruction, which makes the counterexample checkable. vibemathed records no attributed poser or year, so the entry carries no year_posed rather than guessing one. No prior negative answer appears in the categorical logic literature cited.
Caveats and known objections
A short preprint, unrefereed, not formalized, with no independent check on record. Autonomy is graded ai-assisted, the weakest reading the disclosure supports, because the paper claims help rather than authorship of the ideas: the mathematical results in the document were obtained with the help of ChatGPT 5.6 Sol, although the document itself was written entirely by the authors, who take full responsibility for its contents. The disclosure does not separate which results came from the model.
Also recorded at
vibemathedfailure-of-higher-order-truth-within-intuitionistic-propositional-logic
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Author verified and AI-assisted.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded author verified for verification and ai-assisted for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Not every Heyting algebra is the subterminal lattice of a topos. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-08-27-intuitionistic-higher-order-truthBibTeX
@misc{whataifound-independent-2026-truth,
title = {Not every Heyting algebra is the subterminal lattice of a topos},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Author verified. Autonomy: AI-assisted.},
url = {https://whataifound.org/finding/2026-08-27-intuitionistic-higher-order-truth}
}