# Defining a partial function in a formal theory

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?

• One could imagine using "function symbols" whose interpretation is a partial function. But standard first-order languages do not. One gets around it with predicate symbols. Commented Jun 24, 2014 at 5:49
• What do you mean by "gets around it with predicate symbols"?
– Jack
Commented Jun 24, 2014 at 5:53
• If we want to "emulate" a "partial function" symbol of arity $n$, one uses an $(n+1)$-ary predicate symbol $P$, adding the axiom that for all $x_1$ to $x_n$ there exists at most one $y$ such that $P(y,x_1,\dots,x_n)$. Commented Jun 24, 2014 at 5:57
• I see. So to my question above: how are functions over rational numbers defined in arithmetic?
– Jack
Commented Jun 24, 2014 at 6:00
• "Arithmetic" is usually not concerned with rationals. formal field theory has a standard axiomatization you are familiar with, it works perfectly well without a function symbol for division. Commented Jun 24, 2014 at 6:04

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!

• So... why does nobody bother to use a free logic to formalize? Obviously we have a very good model in denotational semantics, but is a free logic formalization not interesting? Commented Oct 23, 2022 at 13:07

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

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 )$