Defining a partial function in a formal theory

Question

Assume we have a first-order theory $T$ of arithmetic (i.e., number theory). Suppose I wish to introduce a new function symbol $f$ in the theory, so that $f$ is a partial number function (namely, it is undefined for some values), and where the extension will be a conservative extension of $T$.

For example: the fraction function $x/y$ is undefined for $y=0$.

Is this possible? The problem is that to extend the language with a new function symbol we need the function to be total, no?

Answer 1

The problem is that to extend the language with a new function symbol we need the function to be total, no?

Well, yes, that's true if we are dealing with a standard interpreted first-order language where every term must denote. Why is that required? Well, if a term $\tau$ doesn't denote, a well formed formula $\varphi(\tau)$ won't take a truth value. But in our standard two-valued logic we require every well formed formula to have a determinate truth-value, true or false. Trouble!

But if we are prepared to allow truth-value gaps, we can then allow terms not to denote. We can treat partial functions directly (without trading them in for relations, for example), allowing expressions like '$f(a)$' to fail to denote. We can still be in the realm of first-order logic (the quantifiers will still range over objects in the domain), but this will be a first-order logic free of certain existence assumptions. We will be using a free logic, for short.

And, lo and behold, there are various brands of free logic on the market: see http://plato.stanford.edu/entries/logic-free/

But would it actually be worth the effort to use a formalized free logic when regimenting e.g. recursion theory (where partial functions are the default)? It is an interesting question why nobody bothers ... but that's a longer story!

Answer 2

Another solution (I think better) is to use relations (two variable predicates) instead of functions:

something like :

$ R(a,b) \equiv( f(a) = b \land a \not = p \land a \not = q ) $

Answer 3

Assuming I understand it correctly, computer science (denotational semantics?) deals with this by using total functions to represent partial functions. We define a distinguished element $\bot$ meaning undefined (usually pronounced "bottom"). Given a partial function $f:A \nrightarrow B$ we can represent it with a total function $f^{\prime}:A \rightarrow B_{\bot}$ where $B_{\bot}:=B \cup \{ \bot \}$. Any values of $A$ for which $f$ is undefined are mapped to $\bot$ under $f^{\prime}$.