A Type Theory of Sense

Wherever meaning is studied empirically, semantic verdicts come from instruments: an embedding model at a resolution decides whether two completions “say the same thing,” a finer resolution revokes the verdict, a different encoder disagrees licitly with both. Logics of meaning have had no place for any of this — no judgment form for the record of a measurement, no laws for how verdicts propagate when the instrument is refined or replaced, no guarantee that the analysis adds nothing to its data. We present TTS, a constructive extension of Martin-Löf type theory built for exactly that practice: a logic of consequence from measurement data. Judgments take the form Γ ⊢Δ J, where Δ is a measurement context — an instrument's verdict record, entering as constants. Two regime-indexed relation formers carry the logic: indiscernibility and apartness in the constructive tradition of Brouwer, Heyting and Bishop, graded by regimes — instruments at declared resolutions, ordered by refinement. Apartness has no premise-free introduction rule, and the metatheory makes the architecture enforceable rather than rhetorical: soundness over regime-indexed simplicial apartness spaces, conservativity over the base theory, no-fork-ex-nihilo, no-refutation-ex-nihilo, provenance (every derivable fork is forced by the record in every realizing model), and consistency of honest records. Two grades of compositional demand are derived, not primitive — canonicity (the instrument cannot distinguish any two fillers: composition is forced) and the fork (two warranted fillers, recorded apart: composition demands a genuine choice) — with a third, locked, constructed from them. Exclusion is a theorem; forks persist under refinement while canonicity does not, also theorems; and the consistency of an identity discovered by one instrument with a separation held by another is characterized exactly by the order relation between the instruments. The principal application is a formal reconstruction of Fregean sense: a sense is a choice of filler of a compositional demand, reference its boundary, hyperintensional distinctness apartness at a regime, the informativeness of identity its record-dependence — one cross-regime law, instantiated by lexical ambiguity at filler spaces and by the name-state configuration of Frege's celestial case. The motivating subject matter is the geometry of meaning in large language models, whose token spaces are measurably not manifolds: semantic space is stratified, and trajectories of generation encounter loci of genuine choice that the Kan condition of homotopy type theory renders invisible. The empirical sections instantiate the calculus's central judgments in generation behaviour — resampling and fill-in-the-middle protocols, fully logged — as a demonstration of non-vacuity and one replicated qualitative prediction, with an explicit honesty clause; the logic itself is not specific to machine systems. Full HTML text: https://icra.tanazur.org/papers/type-theory-of-sense/ — ICRA pre-print series: https://icra.tanazur.org/