Extending a first order predicate calculus with partially defined iota terms

Partial functions and “undefinedness” have been around in mathematics for a long time, without causing any trouble. It was only when mathematics and computer science met in pro jects on “automatization” of formal reasoning that some problems came up [Hoogewijs 1987]. Where humans are able to avoid the application of a partial function on an argument outside “the domain” of the function, formalizing the rules for this activity seems to be less trivial. In [Farmer 1996] Farmer states that there does not exist a consensus on how partial functions should be mechanized and the developer of a mechanized mathematics system must choose among many different possible ways of representing and reasoning about partial functions. We want to add one more possibility by introducing “partially defined iota terms” of the form ιxψ (ϕ) which represents the unique x satisfying ϕ whenever the condition ψ is fulfilled. We present an extension of a two-valued first order sequent calculus for predicate logic with identity [Hermes 1973], where we are able to reason correctly about partially defined iota terms