A Type Theory of Sense: Witnessed Choice in Stratified Semantic Spaces
This work offers a novel formal framework for semantic composition and hyperintensionality, potentially relevant to theoretical computer science and linguistics, but it is highly theoretical with no empirical validation.
The paper introduces TTS, a dependent type theory where semantic composition is modeled by horn filling and distinctions between completions are witnessed relative to measurement regimes. It provides a geometric account of Fregean sense and reference, with results on persistence of forks and coexistence of identifications and separations across regimes.
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.