Partial functions - where can I learn more about this (heuristic, informal) system of conventions? Is there a name for the following (heuristic, informal) system of conventions for dealing with partial functions and undefined expressions? I'd like to know whether it has any undesirable quirks that I haven't picked up on.


There is an designated entity $U$ (intuitively, $U$ represents "undefinedness").
Functions can be partial, and every function $f$ corresponds to a set $\mathrm{dod}(f)$ called its domain of definition. Whenever $f$ is evaluated at some $x \notin \mathrm{dod}(f)$, it returns $U$. For example, if we're working in the real numbers, the expression $0^{-1}$ would return $U$. Furthermore, if $U$ is an input to a function, then $U$ is output. For example, in the real numbers, an expression like $U+4$ would equal $U$.
All relations are total and the logic is two-valued; and if a relation is given $U$ as an input, then $\mathbf{false}$ is output. For example, in the real numbers, an expression like $3 &lt; U$ would be false. This has the slightly odd result that $U = U$ is false (less surprisingly, $U \neq U$).
The entity $U$ is taken as being outside the domain over which quantifiers range. For example, from $\forall x(x = x)$ we cannot deduce $U = U$.


So just to reiterate, I'm looking for


more information / a reference.


In particular, I'd like to know:


Does this system of conventions have a name?
Does it have any weird quirks that make it a bad system of conventions?
This topic has been the subject of much debate by people who worry about formal specification languages. There is a paper by Stoddart, Dunne and Galloway, Undefined Expressions and Logic in Z and B, that compares various approaches and gives some references that may be useful (See http://dx.doi.org/10.1023/A:1008797018928 - or search for it via google if you don't have access to SpringerLink). 

"Free logic" as mentioned in a comment by Peter Smith may be of interest (see http://plato.stanford.edu/entries/logic-free/), but I don't think you are interested in having syntax for saying things like "such-and-such an expression is undefined".

Your proposal isn't very clear about this, but if you intend $U$ to be a semantic object that is not part of the syntax, then what you describe is very like the approach originally taken in Z (see Stoddart et al.). The main quirk is that it can be counter-intuitive: e.g., in Z, $1/0 = 1/0$ and $1/0 \not= 1/0$ are both false (because $\not=$ is defined in terms of set membership: $x \not= y$ means $(x, y) \in \{a, b : X \mathrel{|} \lnot a = b\}$).
Two claims are made here, among others:

(1) There is an undefined symbol U.
(2) If you evaluate a function outside its domain of definition, it returns U.

How are we to understand the second, given the first?
(a) It can't be that the function, for some argument $a$ &quot;outside the domain of definition&quot;, returns the symbol 'U' - for that object would be a perfectly good value, so $a$ is in the domain of definition after all (i.e. is an object which, given to the function $f$ as argument, yields a value).
(b) It can't be either that the the function, for some argument  $a$ outside the domain of definition, returns what 'U' denotes, since by hypothesis there is no such thing since 'U' is undefined.
So we seem to be heading for straight nonsense based on use/mention confusion.
(c) But perhaps, more charitably, the idea in (2) is that 'U' functions like the word 'zilch'. So when a function is applied to an object outside the domain of definition it returns zilch. But note 'zilch' isn't undefined (any more than 'nothing' is undefined) -- it's in the dictionary! And if 'U' works like 'zilch' it won't be undefined. So we still won't have (1).