Church's simple theory of types is a system of higher-order logic in which functions are assumed to be total. We present in this paper a version of Church's system called
PFin which functions may be partial. The semantics of PF, which is based on Henkin's general-models semantics, allows terms to be nondenoting but requires formulas to always denote a standard truth value. We prove that PFis complete with respect to its semantics. The reasoning mechanism in PFfor partial functions corresponds closely to mathematical practice, and the formulation of PFadheres tightly to the framework of Church's system.