Failure of Higher-Order Truth within Intuitionistic Propositional Logic
resolvedconfidence 70%
VibeMathed reports this item as resolved. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Precise statement
We answer the question whether all Heyting algebras can appear as the lattice of subterminal objects of an elementary topos in the negative. Concretely, we have shown that the free Heyting algebra on two generators cannot be such a Heyting algebra. The mathematical results in this document were obtained with the help of ChatGPT 5.6 Sol, although the document itself was written entirely by us and we take full responsibility for its contents.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement
fidelity, correctness, priority, or novelty.
What AI did
ChatGPT 5.6 Sol
The whole disclosure is one sentence of the abstract: "The mathematical results in this document were obtained with the help of ChatGPT 5.6 Sol, although the document itself was written entirely by us and we take full responsibility for its contents." There is no acknowledgements section and no other mention of a model in the paper.
That sentence does credit the mathematics rather than tooling, which is what puts this in scope: it says the results were obtained with the model's help, not that a model wrote code or checked prose. But it identifies no lemma, construction or step, and a disclosure this general takes the lower tier, so the entry records AI-assisted rather than co-developed. If a later version attributes the obstruction term, the higher-order formula, or their identification to the model, the tier should move up.
Unreviewed: an arXiv preprint one day old (v1, 27 August 2026, math.CT), unrefereed, with no formalization, and the argument runs through Bellissima's representation and higher-order internal logic, none of which was checked here. Verified on 28 August 2026: the paper exists at arXiv:2608.26874 with this title and both authors; the statement and the negative answer are its abstract; the target is described in its introduction as "a long-standing problem in categorical logic" with Pitts cited for a recent summary and a related positive result of Awodey et al. cited alongside; and the proof strategy is as the entry describes it, constructing $A\in\mathcal O_\uparrow(K_2)\setminus F_2$ and deriving a contradiction from its definability as a global proposition. The single AI sentence in the abstract is the paper's only mention of a model.
The paper proves that not every Heyting algebra can occur as the lattice of subterminal objects of an elementary topos. Specifically, the free Heyting algebra $F_2$ on two generators cannot occur.
Using Bellissima’s representation $F_2\hookrightarrow\mathcal O_\uparrow(K_2)$, the authors construct an upward-closed subset $A\subseteq K_2$ with $A\notin F_2$. They show that if some elementary topos $\mathcal E$ satisfied $\operatorname{Sub}_{\mathcal E}(1)\cong F_2$, then higher-order internal logic would make $A$ definable as a global proposition, forcing $A$ to correspond to an element of $F_2$, a contradiction.
Thus no elementary topos has subterminal lattice isomorphic to $F_2$, disproving the claim that every Heyting algebra can arise this way. The paper does not classify which Heyting algebras are realizable.
Known method families
argument (source-reported)
Source-reported tools: argument.
Independent: unknown · difference confidence: 0
What remains uncertain
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.
VibeMath has not independently verified the mathematical claim.
AI-attempt independence and training-data exposure are unknown unless explicitly documented.
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.