A type reduction from proof-conditional to dynamic semantics

Dynamic and proof-conditional approaches to discourse (exemplified by Disco urse Representation Theory and Type-Theoretical Grammar, respectively) are related through translations and transitions labeled by first-order formula s with anaphoric twists. Type-theoretic contexts are defined relative to a signature and instantiated model-theoretically, subject to change.