pith. sign in

arxiv: 2606.12504 · v1 · pith:WZ5NODEXnew · submitted 2026-06-10 · 💻 cs.LO

A Type Theory of Sense: Witnessed Choice in Stratified Semantic Spaces

Iman Poernomo This is my paper

Pith reviewed 2026-06-27 07:51 UTC · model grok-4.3

classification 💻 cs.LO
keywords type theoryFregean sensesemantic compositionconstructive apartnessmeasurement regimeshorn fillinghyperintensional differencedependent types
0
0 comments X

The pith

TTS replaces global canonicity in dependent type theory with regime-indexed indiscernibility and constructive apartness witnessed by measurement contexts.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces TTS as a dependent type theory in which semantic composition occurs via horn filling rather than a single global notion of canonical completion. Distinctions between possible fillers are tracked through explicit measurement regimes that introduce constructive apartness only when instrument outputs separate two warranted completions. Filler spaces become canonical if every pair of completions is observationally connected under the regime and forked otherwise. The approach yields conservativity over ordinary dependent type theory, a provenance property, and the result that no fork can arise from the empty record. A reader would care because the setup supplies a geometric reading of Fregean sense as choice of filler, reference as constraining boundary, and hyperintensional difference as measured separation while connecting to stratified spaces.

Core claim

TTS is a dependent type theory in which semantic composition is represented by horn filling and distinctions between possible completions are witnessed relative to explicit measurement regimes. TTS replaces globally canonical composition with regime-indexed indiscernibility and constructive apartness, allowing filler spaces to be classified as canonical when all completions are observationally connected and forked when two warranted completions are positively separated. Separation witnesses enter the calculus only through measurement contexts recording actual instrument outputs, yielding conservativity, provenance, and a no-fork-from-the-empty-record result. Forks persist under refinement wh

What carries the argument

Regime-indexed indiscernibility and constructive apartness entered solely through measurement contexts that record instrument outputs, with horn filling as the mechanism for semantic composition.

If this is right

  • Forks persist under refinement of measurement contexts.
  • Canonicity of a filler space may fail under refinement even when it held for a coarser regime.
  • An identification made by one regime can coexist with a separation made by another only when the regimes satisfy the paper's coexistence conditions.
  • The theory remains conservative over ordinary dependent type theory.
  • No fork arises from the empty record.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Branching patterns observed in language-model generation could be interpreted as regime-specific forks that persist across successive refinements of the measurement context.
  • The distinction between canonical and forked spaces supplies a concrete way to stratify representation spaces by layering distinct measurement regimes.
  • Hyperintensional differences could be tested empirically by encoding explicit instrument outputs as measurement contexts in semantic parsing tasks.
  • The framework's use of constructive apartness may connect to existing models of intensional equality in type theory without requiring new axioms beyond the measurement discipline.

Load-bearing premise

Measurement contexts can be formalized so that they record actual instrument outputs in a manner that automatically enforces conservativity over ordinary dependent type theory and the no-fork-from-empty property without additional stipulations.

What would settle it

Implement the no-fork-from-the-empty-record theorem in a concrete model of TTS and exhibit a measurement context together with two completions that are observationally separated yet arise from the empty record; if such a context exists the central conservativity claim fails.

Figures

Figures reproduced from arXiv: 2606.12504 by Iman Poernomo.

Figure 1
Figure 1. Figure 1: The pilot, in both readouts (300 sampled completions per boundary; cone configuration; apartness verdicts at the pullback index). (a) Sense￾margin distributions; dashed lines are the control-condition means (basin representatives in the estimator sense). The ambiguous boundary spans both basins with modes aligned to each — the fork signature; each control remains within its own basin. (b) The ε-sweep: siza… view at source ↗
Figure 2
Figure 2. Figure 2: The 2-horn (FIM) experiment: one ambiguous prefix, three suffixes, n = 200 sampled bridges per horn. Dashed lines: the disambiguated condi￾tions’ means. The neutral-suffix horn (top) is bimodal — riverside-committed mode plus a deferral mass; each disambiguating suffix (middle, bottom) collapses the bridge distribution onto its own basin: the suffix effect. discipline of directed type theory. Throughout th… view at source ↗
read the original abstract

We introduce TTS, a dependent type theory in which semantic composition is represented by horn filling and distinctions between possible completions are witnessed relative to explicit measurement regimes. TTS replaces globally canonical composition with regime-indexed indiscernibility and constructive apartness, allowing filler spaces to be classified as canonical when all completions are observationally connected and forked when two warranted completions are positively separated. Separation witnesses enter the calculus only through measurement contexts recording actual instrument outputs, yielding conservativity, provenance, and a no-fork-from-the-empty-record result. We prove that forks persist under refinement while canonicity may fail, and characterize exactly when an identification made by one regime can consistently coexist with a separation made by another. This framework supports a geometric account of Fregean sense as a choice of filler, reference as the boundary constraining that choice, and hyperintensional difference as measured apartness, while providing a falsifiable bridge to stratified representation spaces and branching behaviour in language-model generation.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper introduces TTS, a dependent type theory in which semantic composition is modeled by horn filling, with distinctions between completions witnessed via regime-indexed indiscernibility and constructive apartness relative to explicit measurement contexts. Filler spaces are classified as canonical (all completions observationally connected) or forked (two warranted completions positively separated). The work claims that separation witnesses enter only through measurement contexts recording instrument outputs, yielding conservativity over ordinary dependent type theory, a provenance result, a no-fork-from-the-empty-record theorem, persistence of forks under refinement, and exact conditions for coexistence of identifications and separations across regimes. It positions the framework as a geometric account of Fregean sense (choice of filler), reference (constraining boundary), and hyperintensional difference (measured apartness), with links to stratified representation spaces and branching in language-model generation.

Significance. If the central claims hold, the framework could supply a novel constructive type-theoretic treatment of hyperintensionality and a falsifiable bridge between semantic theory and computational generation behavior. The absence of any derivations, lemmas, or proof sketches, however, prevents evaluation of whether the measurement-context rules alone deliver the stated conservativity and no-fork properties without hidden stipulations.

major comments (1)
  1. [Abstract] Abstract (and the provenance/no-fork paragraph): the manuscript asserts conservativity over DTT, provenance, and the no-fork-from-empty-record result as automatic consequences of the measurement-context rules, yet supplies no inductive definition of those contexts, no interaction lemmas with horn filling or constructive apartness, and no proof sketches. This is load-bearing for the central claim, because the skeptic correctly identifies that an empty-record instantiation permitting a positive separation (or an implicit restriction not stated in the core calculus) would falsify both conservativity and the no-fork theorem.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the detailed reading and for identifying the need for explicit formal support of the central claims. The absence of inductive definitions and proof sketches in the submitted version is a genuine presentational gap that we will correct.

read point-by-point responses

  1. Referee: [Abstract] Abstract (and the provenance/no-fork paragraph): the manuscript asserts conservativity over DTT, provenance, and the no-fork-from-empty-record result as automatic consequences of the measurement-context rules, yet supplies no inductive definition of those contexts, no interaction lemmas with horn filling or constructive apartness, and no proof sketches. This is load-bearing for the central claim, because the skeptic correctly identifies that an empty-record instantiation permitting a positive separation (or an implicit restriction not stated in the core calculus) would falsify both conservativity and the no-fork theorem.

    Authors: We agree that the submitted manuscript states the results without supplying the required inductive definition of measurement contexts or the supporting lemmas and sketches. In the revised version we will add: (i) an inductive definition of measurement contexts (as finite records of regime-indexed instrument outputs), (ii) interaction lemmas establishing that horn-filling and constructive apartness are only affected when a context supplies an explicit witness, and (iii) proof sketches for conservativity (by induction on context size, showing that empty contexts coincide with ordinary DTT), provenance (every separation trace originates in a measurement output), and the no-fork-from-empty-record theorem (empty contexts contain no outputs, hence cannot witness a positive separation). These additions will make explicit that separations require non-empty measurement data and thereby rule out the empty-record counter-example. revision: yes

Circularity Check

0 steps flagged

No circularity; results presented as derived from measurement-context definitions

full rationale

The abstract states that separation witnesses enter only through measurement contexts recording instrument outputs, yielding conservativity, provenance, and the no-fork-from-empty result, with proofs given for persistence of forks and coexistence of identifications. No equations, fitted parameters, or self-citations appear in the provided text that would reduce these claims to their inputs by construction. The derivation is described as following from the inductive definition of the contexts and their interaction with horn-filling and apartness, making the framework self-contained against external benchmarks with no load-bearing reductions visible.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review supplies no explicit free parameters, axioms, or invented entities; the central claims rest on the unelaborated assumption that measurement contexts can be added to dependent type theory while preserving the listed meta-theoretic properties.

pith-pipeline@v0.9.1-grok · 5689 in / 1359 out tokens · 21684 ms · 2026-06-27T07:51:27.587807+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

51 extracted references · 1 canonical work pages

  1. [1]

    Altenkirch, C

    T. Altenkirch, C. McBride, W. Swierstra. Observational equality, now!Pro- ceedings of the ACM Workshop on Programming Languages meets Program Verification (PLPV), pp. 57–68, 2007

    2007

  2. [2]

    Annenkov, P

    D. Annenkov, P. Capriotti, N. Kraus, C. Sattler. Two-level type theory and applications.Mathematical Structures in Computer Science33(8):688–743,

  3. [3]

    Arnold, F

    J. Arnold, F. Holtorf, F. Schäfer, N. Lörch. Phase transitions in the output dis- tribution of large language models.Advances in Neural Information Processing Systems 37 (NeurIPS), 2024. arXiv:2405.17088

    arXiv 2024

  4. [4]

    Asher.Lexical Meaning in Context: A Web of Words

    N. Asher.Lexical Meaning in Context: A Web of Words. Cambridge University Press, 2011

    2011

  5. [5]

    A is B” fail to learn “B is A

    L. Berglund, M. Tong, M. Kaufmann, M. Balesni, A. Cooper Stickland, T. Ko- rbak, O. Evans. The reversal curse: LLMs trained on “A is B” fail to learn “B is A”. arXiv:2309.12288, 2023

    arXiv 2023

  6. [6]

    Bavarian, H

    M. Bavarian, H. Jun, N. Tezak, J. Schulman, C. McLeavey, J. Tworek, M. Chen. Efficient training of language models to fill in the middle. arXiv:2207.14255, 2022

    Pith/arXiv arXiv 2022

  7. [7]

    S. Ayhan. What is the meaning of proofs? A Fregean distinction in proof- theoretic semantics.Journal of Philosophical Logic50:571–591, 2021

    2021

  8. [8]

    S. Ayhan. Meaning and identity of proofs in a bilateralist setting: a two- sorted typed lambda-calculus for proofs and refutations.Journal of Logic and Computation35(2):exae014, 2025

    2025

  9. [9]

    E. M. Bender, A. Koller. Climbing towards NLU: on meaning, form, and understanding in the age of data.Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics (ACL), pp. 5185–5198, 2020

    2020

  10. [10]

    arXiv:2006.16450

    B.Bentzen.Sense, reference, andcomputation.Perspectiva Filosófica47(2):179– 203, 2020. arXiv:2006.16450

    arXiv 2020

  11. [11]

    Bigelow, A

    E. Bigelow, A. Holtzman, H. Tanaka, T. Ullman. Forking paths in neural text generation.International Conference on Learning Representations (ICLR),

  12. [12]

    Bishop, D

    E. Bishop, D. Bridges.Constructive Analysis. Grundlehren der mathematischen Wissenschaften 279, Springer, 1985

    1985

  13. [13]

    Chatzikyriakidis, Z

    S. Chatzikyriakidis, Z. Luo.Formal Semantics in Modern Type Theories. ISTE/Wiley, 2020. 55

    2020

  14. [14]

    Coecke, M

    B. Coecke, M. Sadrzadeh, S. Clark. Mathematical foundations for a com- positional distributional model of meaning.Linguistic Analysis36:345–384, 2010

    2010

  15. [15]

    Corfield.Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy

    D. Corfield.Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy. Oxford University Press, 2020

    2020

  16. [16]

    M. Duží, B. Jespersen, P. Materna.Procedural Semantics for Hyperintensional Logic. Springer, 2010

    2010

  17. [17]

    Donahue, M

    C. Donahue, M. Lee, P. Liang. Enabling language models to fill in the blanks. Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics (ACL), 2020

    2020

  18. [18]

    K. Fine. A theory of truthmaker content I: conjunction, disjunction and negation.Journal of Philosophical Logic46:625–674, 2017

    2017

  19. [19]

    G. Frege. Über Sinn und Bedeutung.Zeitschrift für Philosophie und philosophis- che Kritik100:25–50, 1892

  20. [20]

    Gratzer, J

    D. Gratzer, J. Weinberger, U. Buchholtz. Directed univalence in simplicial homotopy type theory. arXiv:2407.09146, 2024 (v2 2026)

    arXiv 2024

  21. [21]

    Groenendijk, M

    J. Groenendijk, M. Stokhof. Dynamic predicate logic.Linguistics and Philoso- phy14(1):39–100, 1991

    1991

  22. [22]

    Heim.The Semantics of Definite and Indefinite Noun Phrases

    I. Heim.The Semantics of Definite and Indefinite Noun Phrases. PhD disser- tation, University of Massachusetts, Amherst, 1982

    1982

  23. [23]

    Heyting.Intuitionism: An Introduction

    A. Heyting.Intuitionism: An Introduction. North-Holland, 1956

    1956

  24. [24]

    Jiang, G

    Y. Jiang, G. Rajendran, P. Ravikumar, B. Aragam, V. Veitch. On the origins of linear representations in large language models.Proceedings of the 41st International Conference on Machine Learning (ICML), PMLR 235:21879– 21911, 2024

    2024

  25. [25]

    A. Joyal. Quasi-categories and Kan complexes.Journal of Pure and Applied Algebra175:207–222, 2002

    2002

  26. [26]

    H. Kamp. A theory of truth and semantic representation. InFormal Methods in the Study of Language, Mathematisch Centrum, Amsterdam, 1981

    1981

  27. [27]

    Kripke.Naming and Necessity

    S. Kripke.Naming and Necessity. Harvard University Press, 1980

    1980

  28. [28]

    Kudasov, E

    N. Kudasov, E. Riehl, J. Weinberger. Formalizing the∞-categorical Yoneda lemma.Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), 2024. DOI 10.1145/3636501.3636945. 56

    work page doi:10.1145/3636501.3636945 2024

  29. [29]

    Ladyman, S

    J. Ladyman, S. Presnell. Identity in homotopy type theory, part II: the concep- tual and philosophical status of identity in HoTT.Philosophia Mathematica 25(2):210–245, 2017

    2017

  30. [30]

    B. M. Lake, G. L. Murphy. Word meaning in minds and machines.Psychological Review130(2):401–431, 2023

    2023

  31. [31]

    X. Li, A. D. Sarwate. Unraveling the localized latents: learning stratified manifold structures in LLM embedding space. arXiv:2502.13577, 2025

    arXiv 2025

  32. [32]

    S. Lossin. Cocartesian fibrations in synthetic simplicial type theory. arXiv:2604.18668, 2026

    Pith/arXiv arXiv 2026

  33. [33]

    Mahadevan

    S. Mahadevan. GAIA: categorical foundations of generative AI. arXiv:2402.18732, 2024

    arXiv 2024

  34. [34]

    Y. N. Moschovakis. A logical calculus of meaning and synonymy.Linguistics and Philosophy29:27–89, 2006

    2006

  35. [35]

    R. Muskens. Sense and the computation of reference.Linguistics and Philosophy 28(4):473–504, 2005

    2005

  36. [36]

    Nakaishi, Y

    K. Nakaishi, Y. Nishikawa, K. Hukushima. Phase transition in large language models and the criticality of natural languages. arXiv:2406.05335, 2026

    Pith/arXiv arXiv 2026

  37. [37]

    Pustejovsky.The Generative Lexicon

    J. Pustejovsky.The Generative Lexicon. MIT Press, 1995

    1995

  38. [38]

    D. Quigley. A vector logic for extensional formal semantics.Journal of Logic, Language and Information34(5):557–599, 2025

    2025

  39. [39]

    N. Rasekh. Simplicial homotopy type theory is not just simplicial: what are ∞-categories? arXiv:2508.07737, 2025

    arXiv 2025

  40. [40]

    Recanati.Mental Files

    F. Recanati.Mental Files. Oxford University Press, 2012

    2012

  41. [41]

    Riehl, M

    E. Riehl, M. Shulman. A type theory for synthetic ∞-categories.Higher Structures1(1):147–224, 2017

    2017

  42. [42]

    Robinson, S

    M. Robinson, S. Dey, S. Sweet. The structure of the token space for large language models. arXiv:2410.08993, 2024

    arXiv 2024

  43. [43]

    Robinson, S

    M. Robinson, S. Dey, T. Chiang. Token embeddings violate the manifold hypothesis.Advances in Neural Information Processing Systems 38 (NeurIPS),

  44. [44]

    B. M. Ruppik et al. Less is more: local intrinsic dimensions of contextual language models.Advances in Neural Information Processing Systems 38 (NeurIPS), 2025. arXiv:2506.01034. 57

    arXiv 2025

  45. [45]

    M. Schüle. On the semantics of large language models.Intellectica81:15–36, 2024

    2024

  46. [46]

    Tranchini

    L. Tranchini. Proof-theoretic semantics, paradoxes and the distinction between sense and denotation.Journal of Logic and Computation26(2):495–512, 2016

    2016

  47. [47]

    A. S. Troelstra, D. van Dalen.Constructivism in Mathematics: An Introduction, vol. I. North-Holland, 1988

    1988

  48. [48]

    Institute for Advanced Study, 2013

    The Univalent Foundations Program.Homotopy Type Theory: Univalent Foun- dations of Mathematics. Institute for Advanced Study, 2013

    2013

  49. [49]

    F. Veltman. Defaults in update semantics.Journal of Philosophical Logic 25(3):221–261, 1996

    1996

  50. [50]

    von Plato

    J. von Plato. The axioms of constructive geometry.Annals of Pure and Applied Logic76(2):169–200, 1995

    1995

  51. [51]

    Zhang, et al

    Y. Zhang, et al. Latent trajectory dynamics in large language models: a manifold evolution framework (DMET). arXiv:2505.20340, 2025. 58

    Pith/arXiv arXiv 2025