---
title: "Failure of Higher-Order Truth within Intuitionistic Propositional Logic"
authors:
  - "Yiqi Xu"
  - "Lingyuan Ye"
year: 2026
venue: "arXiv:math.CT"
arxiv: "2608.26874"
doi: null
source: "https://arxiv.org/abs/2608.26874"
topics:
  - "curiosity"
  - "maths-foundations"
seed_rank: 1651
seed_batch: "curiosity-2026-09-09"
reviewed: "2026-09-09"
pool: "maths-foundations"
relevance_score: 9
lineage: topos-logic
cites:
  - title: "Failure of Higher-Order Truth within Intuitionistic Propositional Logic"
    url: "https://arxiv.org/abs/2608.26874"
    year: 2026
    arxiv: "2608.26874"
    doi: null
see:
  - "1614-another-counterexample-to-the-nerves-of-steel-conjecture"
---

# Failure of Higher-Order Truth within Intuitionistic Propositional Logic

## One-sentence takeaway

The free Heyting algebra on two generators cannot appear as the lattice of subterminal objects of any elementary topos — higher-order truth fails inside IPL.

## Why it's lovely

Why you might love this: every topos has a Heyting algebra of truth values (subterminals), so you might hope every Heyting algebra arises that way. Xu–Ye kill that hope: the free Heyting algebra on ≥2 generators is not a topos truth-value lattice. A sharp negative companion to last cycle's Nerves-of-Steel counterexample energy.

## Key ideas

- Subterminal objects of an elementary topos form a Heyting algebra (the truth values).
- Question: can every Heyting algebra arise this way?
- No: free Heyting on two (hence ≥2) generators cannot.
- Separates pure IPL algebra from higher-order / topos logic.

## Caveats

Existence obstruction only; does not classify which Heyting algebras do arise. Companion reading: localic / Esakia shelf from earlier Curiosity.

## Links

- arXiv abs: https://arxiv.org/abs/2608.26874
- PDF: https://arxiv.org/pdf/2608.26874.pdf