Abstract: We give a natural semantics for classical logic with partial functions. The semantics is based on multi-valued logic, so that formulas involving undefined values can have undefined truth values. An unusual aspect of our semantics is that it relies on the order of formulas. In this way, the semantics is able to capture the fact that functions must be declared before they are used.

We will introduce the notion of sequent. We argue that infinite sequents are more natural than finite sequents for our semantics. We introduce a sequent calculus for the infinite sequents, and prove the calculus sound and complete with respect to the semantics given before.

We think that our approach to partial functions is more natural than existing approaches, because in our approach, formulas involving undefined values are guaranteed to be undefined. This captures the natural behaviour of programs containing undefined values. The outcome of such programs should be undefined, even if an outcome could be deduced in principle.