Why do we have to prove the totallity of functions?

Question

While studying first-order theories (or logic in general) I often encountered the phrase that "it was not possible to show that a function $f$ is total" (i.e. defined everywhere) and hence I deduced that there is a need to show this everytime when I deal with a function.

But what does this even mean? Why should a function not be total? Wikipedia states that total function is just a synonym for function.

So when the language $L$ of my first-order theory $T$ contains a function symbol $f$, does "showing totallity" mean that I have to prove $(\forall x)[(\exists y)[f(x)=y]]$? Answers to my other question suggested that this is indeed not necessary as this can be proven from the usual axioms and deduction rules:

Let $f$ be a function symbol. Then $f(u)$ is a term. Using the reflexivity of $=$, we can deduce $f(u)=f(u)$. This allows to deduce $(\exists y)[f(u)=y]$ and finally by introduction of universal quantification also $(\forall x)[(\exists y)[f(x)=y]]$.

So my question is: what does it exactly mean to prove that a function is total and why is there a need to do so? I ask this question because the totallity of a function was mentioned several times while discussing this other question of mine.

Answer 1

Let $L=\{+,\cdot, 1, 0\}$ be the language of arithmetic, i.e. $+,\cdot$ are binary function symbols and $0,1$ are constant symbols. Consider the Gödelization $\overline\bullet:\mathbb{N}\to T^L$ which assigns to a natural number $n$ the $L$-Term $\underbrace{1+\dots+1}_{n\text{ times}}$

Let $\Phi$ be a set of $L$-sentences and $f:\mathbb{N}\to\mathbb{N}$ be a function. We say that $\Phi$ represents $f$ if there is a $L$-formula $\varphi_f(x,y)$ s.t. $$f(n)=m \qquad\text{iff}\qquad\Phi\models\varphi_f(\overline n, \overline m)$$

In particular, if $\Phi$ represents $f$, then for all $n$ there is $m$ s.t. $\Phi\models\varphi_f(\overline n, \overline m)$. This does however not imply that $\Phi\models\forall x \exists y \varphi_f(x,y)$. If the later holds, we say that $\Phi$ proves that $f$ is total.

For illustration let us look at the following results:

Theorem: Let $\Phi=PA$ be the theory of Peano Arithmetic, then $\Phi$ represents every computable function $f:\mathbb{N}\to\mathbb{N}$.

So in particular it represents the Goodstein Fuction $G$ by a formula $\varphi_G$, however we have

Kirby Paris Theorem: $PA$ does not prove that $G$ is total, i.e $$PA\not\models\forall x \exists y \varphi_G(x,y)$$

Answer 2

Often when we do mathematics it is assumed that whenever we talk about a function, it is assumed to be a total function, which means that $f(x)$ is defined for any $x \in X$. But functions can in fact not be total (if they are not total, they are called partial functions).

Now, in logic we require that any interpretation of a function symbol is a total function ... which is for various reasons we need not get into. So: when you suggest an interpretation for a function symbol, you really need to check that it is indeed defined for every object in the domain.

Thus, for example, if I suggest that some function symbol $f$ be interpreted as the predecessor function, and I declare the domain to be the natural numbers, then I am in trouble, since the predecessor function would not be defined for $0$. And note that being able to prove $\forall x \exists y f(x) = y$ does not help: that is a syntactical sentence that you are able to prove ... the predecessor of 0 in the domain of the natural numbers still does not exist!

Answer 3

This is my try to summarize my understanding of the topic that I got from the answers to my question.

The need for showing the totallity of a function does only arise when the function is implicitely defined. This excludes functions given by function symbols because these induce an explicit definition by the semantic interpretation.

For example, in first-order PA, one can ask if for any $x$ there is a $y$ with $Sy=x$. If so, then one could define a function $f(x)=y$ with the property $Sf(x)=x$. This is of course not the case. More generally, for some formula $\varphi$ one can ask if for any $x$ there is a $y$ so that $\varphi(x,y)$. It could be possible that we can be proven from a meta point of view that

$$\text{for all $n\in\Bbb N$ there is some $m\in \Bbb N$ so that $\varphi(\underbrace{1+\cdots+1}_n,\underbrace{1+\cdots +1}_m)$}.$$

It seems that this proves the statement for all natural numbers. But still, there could be a model of PA with some non-standard integer $x$ for which there is no $y$ so that $\varphi(x,y)$. So, even tho we could define a function $f:\Bbb N\to\Bbb N$ with $\varphi(x,f(x))$, we cannot prove its existence in PA, because PA does not describe the standard integers $\Bbb N$ but all models that satisfy its axioms. And we know there are many.