HEXAGONbeta

Intuitionistic Compression and Optimal Verification Trees

Primarily human-written textHuman understanding: all partsmath.LO — Logic

Contributed by Zhenyu Sun ↗, Jilin Wang ↗

Version 1 / Nov 04, 2026 / CC BY 4.0

Abstract

In strict finitistic generation semantics, a formula is assertible at a generation if some stage in its verification tree forces it. We ask when assertibility agrees with intuitionistic truth on the poset of generations. The leaves of the verification trees, ordered by generation extension, form an intuitionistic Kripke model that preserves truth at every leaf, even without atomic prevalence. For a finite bundle, compression to the generations is exact if and only if each fiber of leaves has a greatest intuitionistic theory and the map selecting these theories has the back property. Compression remains exact under every restriction of the generation poset if and only if atomic prevalence holds. Conversely, consider coherent tree representations of a finite Kripke model whose atomic valuation reflects its order. Among representations with atomic prevalence, the minimum numbers of leaves and nodes over uu are h(u)h(u) and δC+∑x⪯uh(x)\delta_C+\sum_{x\preceq u}h(x), where h(x)h(x) counts saturated paths from minimal worlds to xx, and δC\delta_C is 11 if the comparability component of uu has no least element and 00 otherwise. Saturated-path trees attain both minima simultaneously. Among representations attaining the node minimum at every world, the common root labels in components without a least element determine the representation up to isomorphism over the outer frame. Allowing rooted posets in place of trees can reduce the number of nodes exponentially.

References

  1. Adam-Day, Sam; Bezhanishvili, Nick; Gabelaia, David; Marra, Vincenzo. Polyhedral Completeness of Intermediate Logics: The Nerve Criterion. The Journal of Symbolic Logic, vol. 89, no. 1, pp. 342–382. 2024DOI
  2. Bezhanishvili, Guram; Bezhanishvili, Nick; Moraschini, Tommaso; Stronkowski, Michał. Profiniteness and Representability of Spectra of Heyting Algebras. Advances in Mathematics, vol. 391, pp. 107959. 2021DOI
  3. de Groot, Jim; Pattinson, Dirk. Hennessy–Milner Properties via Topological Compactness. Information and Computation, vol. 287, pp. 104757. 2022arXivDOI
  4. Hamkins, Joel David. A Potentialist Conception of Ultrafinitism. Philosophia Mathematica. 2026arXivDOI
  5. Patterson, Anna. Bisimulation and Propositional Intuitionistic Logic. CONCUR '97: Concurrency Theory, vol. 1243, pp. 347–360. 1997DOI
  6. Statman, Richard. Intuitionistic Propositional Logic Is Polynomial-Space Complete. Theoretical Computer Science, vol. 9, pp. 67–72. 1979DOI
  7. Troelstra, Anne Sjerp; van Dalen, Dirk. Constructivism in Mathematics: An Introduction. Volume I. North-Holland, vol. 121. 1988
  8. van den Berg, Benno. A Kuroda-style jj-translation. Archive for Mathematical Logic, vol. 58, no. 5–6, pp. 627–634. 2019DOI
  9. Wright, Crispin. Strict Finitism. Synthese, vol. 51, no. 2, pp. 203–282. 1982DOI
  10. Yamada, Takahiro. Wright's Strict Finitistic Logic in the Classical Metatheory: The Propositional Case. Journal of Philosophical Logic, vol. 52, no. 4, pp. 1081–1100. 2023DOI
Show all 11 referencesShow fewer references
  1. Yamada, Takahiro. Wright's First-Order Logic of Strict Finitism. Studia Logica, vol. 113, no. 6, pp. 1615–1668. 2025DOI

Version history

  1. v1Submitted by Zhenyu SunInitial depositCurrentNov 03, 2026