In the literature on semantic presupposition, the behavior of presupposition triggers is often explained through a proposal that their meanings are somehow partial. They may, for example, denote partial functions, as in Heim and Kratzer 1998, or they may have meanings making use of “undefined” values, as in trivalent logic accounts. While the latter has devices for representing conditions on the definedness of terms denoting truth values, no account at present (as far as I know) allows for representing the presuppositions of terms of arbitrary type. In this talk, I give a sequent-like notation for reasoning with presuppositions during a semantic derivation. It has three important rules:

(1) Lift: lift a term without presuppositions into a term that presupposes True.

(2) Lower: lower a term with presuppositions whose value itself depends on presuppositions into a simpler term, joining the presuppositions.

(3) Application: apply a function with presuppositions to an argument with presuppositions, carrying along the presuppositions of both.

These rules let one simulate the partial meanings one wants to associate with presupposition triggers, while keeping track of the relevant definedness conditions all along the way. At the same time, because of Application, presupposition projection is automatic. Moreover, presuppositions may be associated with terms of arbitrary type (e.g., e), and meanings can be specified for lexical items that allow them to control how presuppositions are cancelled, are filtered, project, or affect the content of the assertion. Finally, the notation is shown to have a simple model-theoretic interpretation.