Classical Logic with Partial Functions
We introduce a semantics for classical logic with partial functions, in which ill-typed formulas are guaranteed to have no truth value, so that they cannot be used in any form of reasoning. The semantics makes it possible to mix reasoning about types and preconditions with reasoning about other properties. This makes it possible to deal with partial functions with preconditions of unlimited complexity. We show that, in spite of its increased complexity, the semantics is still a natural generalization of first-order logic with simple types. If one does not use the increased expressivity, the type system is not stronger than classical logic with simple types. We will define two sequent calculi for our semantics, and prove that they are sound and complete. The first calculus follows the semantics closely, and hence its completeness proof is fairly straightforward. The second calculus is further away from the semantics, but more suitable for practical use because it has better proof theoretic properties. Its completeness can be shown by proving that proofs from the first calculus can be translated.
type systems logic for partial functions multivalued semantics