Domains of Functions

Several approaches to logical specification of functions are compared. Main attention is paid to LPT, the logic of partial terms and functions, since it allows to model basic features of other approaches. A reduction of LPT to the standard first order logic is given, a cut-free Gentzen-type system GLPT is proved complete, a Herbrand-type theorem is established and a complete resolution calculus presented. 1 General Theory 1.1 Functions with special domains Recall the standard treatment (cf. Section 3 of [1]). Consider for simplicity the language of (one-sorted) predicate logic LPT, the Logic of Partial Terms with (possibly partial) monadic function symbols. The language has additional monadic predicate symbol # written in a postfix way: t #. The possible interpretations are structures M =! M;R M ; : : : f M : : : ? (1) where the domain M is nonempty, R M is a relation on M for every relational symbol R in the language, f M is a partial function on M for every function symbol..