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 projects 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 $\iota
x_\psi(\varphi)$ which represents the unique $x$ satisfying
$\varphi$ whenever the condition $\psi$ 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.