Against successive cyclicity:

This paper proposes a novel analysis of extraction pathway marking in Type-Logical Grammar, taking advantage of proof-theoretic properties of logical proofs whose empirical application has so far been underexplored. The key idea is to allow certain linguistic expressions to be sensitive to the intermediate status of a syntactic proof. The relevant conditions can be stated concisely as constraints at the level of the proof term language, formally a special type of λ-calculus. The proposed analysis does not have any direct analog to either of the two familiar techniques for analyzing extraction pathway marking, namely, successive cyclic movement in derivational syntax and the SLASH feature percolation in HPSG. Moreover, the ‘meaning-centered’ perspective that naturally emerges from this new analysis is conceptually revealing: on this approach, extraction pathway marking essentially boils down to a strategy that certain languages employ to overtly flag the existence of a semantic variable inside a partially derived linguistic expression whose interpretation is dependent on a higher-order operator that is located in a larger structure.