A Simple Type Theory with Partial Functions and Subtypes
William M. Farmer
1993
Abstract
Simple type theory is a higher-order predicate logic for reasoning
about truth values, individuals, and simply typed total functions. We
present in this paper a version of simple type theory, called PF*, in
which functions may be partial and types may have subtypes. We define
both a Henkin-style general models semantics and an axiomatic system
for PF*, and we prove that the axiomatic system is complete with
respect to the general models semantics. We also define a notion of an
interpretation of one PF* theory in another. PF* is intended as a
foundation for mechanized mathematics. It is the basis for the logic
of IMPS, an Interactive Mathematical Proof System developed at The
MITRE Corporation.