Oracles and Choice Sequences for Type-theoretic Pragmatics
Abstract:
An adequate type-theoretic semantics for natural language
expressions must account for the presuppositions that are expressed by
determiners and pronouns. To this end, we extend Type Theory with a
choice operator called "require", which functions as a
non-deterministic oracle to retrieve the synthesis of a
previously-effected verification of a proposition. Then, we give an
intuitionistic semantics to this operator by appealing to Brouwer's
theory of the Creating Subject, and eliminate non-determinism via
spreads and choice sequences. This is based on joint work with Darryl
McAdams, to be published in O. Pombo, A. Nepomuceno, J. Redmond (Ed.) "Epistemology, Knowledge and the Impact of Interaction" (Springer).
Bio: Jon
Sterling completed his undergraduate at UC Berkeley in 2013, where he
focused on philology, historical linguistics and cuneiform languages.
He is currently developing a proof assistant for computational type
theory in the Nuprl tradition, and is interested in Brouwerian
mathematics and higher-dimensional type theory.