Delphi.science

Failure of Higher-Order Truth within Intuitionistic Propositional Logic

Yiqi Xu, Lingyuan Ye

arXivarxiv/2608.26874Aug 27, 2026math.CTscore 0

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 show that the free Heyting algebra on two generators, hence also on N generators for every N greater than 2, 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.

SourceJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/arxiv/2608.26874
curl -X POST /api/v1/records/arxiv/2608.26874/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2608.26874/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'