First Order Logic with Domain Conditions

Abstract

This paper addresses the crucial issue in the design of a proof development system of how to deal with partial functions and the related question of how to treat undefined terms. Often the problem is avoided by artificially making all functions total. However, that does not correspond to the practice of everyday mathematics.

In type theory partial functions are modeled by giving functions extra arguments which are proof objects. In that case it will not be possible to apply functions outside their domain. However, having proofs as first class objects has the disadvantage that it will be unfamiliar to most mathematicians. Also many proof tools (like the theorem prover Otter) will not be usable for such a logic. Finally expressions get difficult to read because of these proof objects.

The PVS system solves the problem of partial functions differently. PVS generates type-correctness conditions (TCCs) for statements in its language. These are proof obligations that have to be satisfied ‘on the side’ to show that statements are well-formed.

We propose a TCC-like approach for the treatment of partial functions in type theory. We add domain conditions (DCs) to classical first-order logic and show the equivalence with a first order system that treats partial functions in the style of type theory.