We propose a novel architecture for categorial grammar that clarifies the relationship between semantically relevant combinatoric reasoning and semantically inert reasoning that only affects surface-oriented phonological form. To this end, we employ a level of
that mediates between syntax (abstract combinatorics) and phonology proper (strings). To notate structured phonologies, we employ a lambda calculus analogous to the
-terms of . However, unlike Oehrle’s purely equational
-calculus, our phonological calculus is
, in a way that is strongly analogous to the functional programming language LCF . Like LCF, our phonological terms are interpreted into a Henkin frame of posets, with degree of definedness (’height’ in the preorder that interprets the base type) corresponding to degree of pronounceability; only maximal elements are actual strings and therefore fully pronounceable. We illustrate with an analysis (also new) of some complex constituent-order phenomena in Japanese.