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.

1. There is an designated entity $U$ (intuitively, $U$ represents "undefinedness").

2. 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$.

3. 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 < U$ would be false. This has the slightly odd result that $U = U$ is false (less surprisingly, $U \neq U$).

4. 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

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?
• Where all this happens? The reals, the integers, some other set...? Oct 8 '13 at 11:31
• Some people define functions as a particular type of relation. In which case 2. and 3. would be contradictory. Can you specify what you mean by a "relation"? Oct 8 '13 at 11:36
• Um, it almost sounds like your $U$ is functionally the same as the NaN in most programming languages. One question: what is the output of the sentence $\neg (x = x)$ evaluated at $U$? In many programming languages this would be true, but I am not sure if you count not equals to as a relation. Oct 8 '13 at 11:45
• The problem with defining $\neq$ to behave differently from $\neg(\cdot = \cdot)$ is that essentially you still have to parse sentences carefully involving $U$ to decide whether it is true or not. In which case, I don't see why you even bother with point (3): there can be two statements which evaluate the same for all $x$, but have opposite results when evaluated on $U$. Then for all intents and purposes I don't see how the requirement that relations are false for $U$ help simplify things at all. (Maybe I am missing something.) Oct 8 '13 at 12:44
• Like I said, the closest thing I can personally think of is that the type of partial function construction is quite necessary when doing computer science. Unfortunately there are disagreements even within that community about what happens when a function is evaluated on an argument of NaN and what happens to logical relations between NaN values. (Wikipedia link) There are, moreover, philosophical differences (I think) between your motivation and that of computer science, so I am not sure how helpful this would be. Oct 8 '13 at 13:12

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\}$).

• Thanks for the reference. Yeah the approach originally taken in $\mathrm{Z}$ was the one that I was trying to describe. Oct 10 '13 at 4:44
• Yes, your corrections make that clear now. Oct 10 '13 at 14:04
• Hey is there accepted terminology for functions/relations that return $U$ whenever $U$ is input? Like "regular" function or some such? Edit. I'm glad the question is better now !! Oct 10 '13 at 15:00
• Okay, I just learned they're called "strict". So, no worries. Oct 10 '13 at 18:39

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$$ "outside the domain of definition", 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).

• You seem to be reading the OP's proposal incorrectly rather than uncharitably. Specifically, you are reading (1) as a claim rather than a proposed definition. I think the intention of (1) is that $U$ is the semantic value to be used when a function symbol is applied to an argument outside its domain. The semantics of predicate symbols and of quantifiers work as if $U$ did not exist. There is nothing fundamentally wrong with this. The OP's semantics should exclude $U$ from what you call the "dictionary" - i.e., free variables should denote "defined" values. What's wrong with that? Oct 8 '13 at 23:11
• That suggests another confusion in the OP's proposal, between a partial function "returning" $U$ for some input $a$ outside the domain of definition, and the proposition $f(a)$ having the semantic value $U$. If the latter is really meant, fine: we can sensibly ask what the best form of free logic is when dealing with non-referring expressions like "f(a)", e.g. with $U$ as a third value. Fine. But that just does not tally with the consideration of expressions like "$U + 4$" or talking about instantiating universal quantifiers "at the point $U$." Oct 9 '13 at 6:24
• I suspect the OP has caused confusion by describing $U$ as a symbol. I suspect it is not intended to be part of the object language syntax but is just being used to describe how undefinedness propagates in the semantics. If my suspicion is incorrect, then I join you in finding the proposal incoherent. Oct 9 '13 at 9:27