Andrews' Type Theory with Undefinedness

William M. Farmer

${\mathcal{Q}}_0$ is an elegant version of Church's type theory formulated and extensively studied by Peter B. Andrews. Like other traditional logics, ${\mathcal{Q}}_0$ does not admit undefi…