English is not my native language, so please forgive if I do not express myself properly.
I am working with the book named above on proof theory, and I have a little problem with the authors use of the $\simeq$ symbol.
He does not introduce it within the frame of a proper definition.
Instead, in remark 1.2.12., he states: " $ t \simeq u $ means that, whenever $t$ or $u$ is defined, then both are defined, and in that case, $t=u$, where $t$ and $u$ are expressions involving partial functions."
I have a number of confusing thoughts in my mind that I'd like to share, some of them somehow not necessarily purely mathematical.
First a bunch of minor issues:
1) Thinking about it, I really wonder if there are any partial/total functions, or, in other words, if being partial/total is really a property $\textit{of the function}$, rather than a property of two sets, namely the functions domain and some superset of it.
Similarly, one may regard any function, as they are usually presented with their domain explicitly named, as total, but equally regard any function as partial, just by thinking about some superset of its domain.
2) If somebody gives a "definition" of a function by writing something like $$ f(x) = \begin{cases} 0, \ \text{some condition holds} \\ \ \text{not defined, that condition holds not} \end{cases}$$ then why not say that this function is indeed defined for any input, and if the condition doesn't hold, then the name of the value of the function is "not defined"?
3) What does $ t \simeq u $ mean, if $t$ and $u$ are both NOT defined? If it then means nothing, what do I do with it when it occurs in the theorems and their proofs (more on that later)? Or, if the symbol only has meaning if $t$ or $u$ is defined, then why not just always write $t=u$, because that is what it means then? (This would be in line with common mathematical practice, where of course I have to assume that expressions in use are defined.)
Often the author writes something like $F(x_1, … , x_n) \simeq y $, where the right hand side is apperently a variable for an $\textit{integer}$. Integers, being always defined, he could have straight away used the usual $=$ symbol, couldn't he? In a similar way, the use of the $\simeq$ in the construction schemes (R'1) of definition 1.2.13. is unnecessary, since they will always be defined, right?
Now, to come to the more crucial point in my difficulties with those expressions working through the book:
4) What does $t\simeq u$ really mean? How do I work with it? What proper definition can I use?
For example, in theorem 1.2.19., there is (under some premises) to show that the truth of the interpretation of some formal expression (from some formal system/language) $A[x_1,…,x_n,y]$ is equivalent to $F(x_1,…,x_n) \simeq y$. Well…if I take the author literally and just 'plug in' the "definition", that would be to show that (under the premises) $A[x_1,…,x_n,y]$ is equivalent to "if $F(x_1,…,x_n)$ or $y$ is defined, then both are defined, and in that case $F(x_1,…,x_n) = y$".
That is not what the author wanted to say.
The problem is the same in other theorems and their proofs, for example 1.3.5.
Fortunately the whole thing isn't too relevant/present in the book (in this subchapter) so that I could still go on and work quite ok with it.
I will be very thankful for explanations, hints, discussions…
Yours,
Ettore
PS (after Mauros answer):
Hey Mauro, thanks for helping me out, really appreciate, I think I get what you mean, by and large.
I'd like once more to focus the attention on theorem 1.2.19.
There is to show that for all those tuples, for which $F$ is defined, and for all $y$, that $F(..)=y$ if and only if the interpretation of $A[..]$ is true.
But what is there to show for all $y$ and for all those tuples, for which $F$ is NOT defined? If in that case there is nothing to show, I mean if for this case there is just no statement intended in the theorem, it would mean that we have always to suppose that we only think about tuples, for which $F$ is defined, when thinking through the proof.
But in that case, he might as well from the beginning have written $F(..)=y$ instead of $F(..)\simeq y$.
And not only in this particular case: If we always have to suppose that the expression $\simeq$ is defined to understand it, make use of it, and make sense of the proofs, then what was the point of introducing the symbol in the first place: He might in every case just have stuck to the usual equal sign $=$.
Or am I wrong, and indeed there is also something to show for the case when the expressions in the statements of the theorems are not defined?
But then, what?
If we consider a tuple for which $F$ is not defined, then what about $A$? Is its interpretation supposed to be true, false, or don't we know?
Best Answer
Partial functions are not encountered in many areas of mathematics. As you wrote, we can often just change the domain (to make a total function with the same graph and a smaller domain) or we can use a new "flag" value to indicate when the original function was not defined.
Computability theory is one of a few areas (unbounded linear operators are another) where partial functions are taken more seriously.
I think one reason computability theorists like the $\simeq$ notation is that it reminds us that $F(x)\simeq y$ is really two claims: first, that the computation of $F(x)$ eventually terminates; second, that the resulting value is y.
Another notation that is sometimes used: "$F(x)\mathord{\downarrow}$" means that the computation of $F(x)$ eventually terminates - which we describe in words either as "$F(x)$ is defined" or "$F(x)$ converges" (or even "$F(x)$ halts"). The accompanying notation "$F(x)\mathbin{\mathord{\downarrow}\mathord{=}}y$ " means that $F(x)$ is defined and equal to $y$ - the same as $F(x) \simeq y$. Having both claims visible helps remind us what the proof of $F(x) \simeq y$ needs to establish.
The notation also helps us keep in agreement with a common idiom in free logic, a logic that includes undefined terms. In many free logics, only things that are defined can be equal to anything - in that context, $F(x) = G(x)$ would imply that $F(x)$ and $G(x)$ are both defined and are equal, while the computability notation $F(x) \simeq G(x)$ says that either $F(x)$ and $G(x)$ are both undefined, or are (both defined and) equal.
There is also a pragmatic reason we don't come up with another symbol that means "not defined" so that we can redefine partial functions to be total, but taking this new value when they are not defined. Even if the original partial function was computable, the new "total" function may not be.
For a standard example, let $\phi_x$ be the computable function with program $x$, and let $f(x)$ be the partial computable function that, if $\phi_x(0)$ halts, returns the number of steps that were required for it to halt. So $f(x)$ is a partial computable function which is defined on the undecidable "halting set" $K = \{ x : \phi_x(0)\downarrow \}$. We can easily show there is no total computable function $g(x)$ that agrees with $f(x)$ - if there was, we could use $g$ to solve the decision problem for $K$. This is true if $g$ says "not defined" on inputs where $f$ was not defined, or if $g$ returns any other number it wants. Either way, we can use the output of $g(x)$ to tell whether $\phi_x(0)$ halts, by just running $\phi_x(0)$ for $g(x) +1 $ steps. (This means there is no algorithm at all - even a completely nonobvious one that ignores the definition of $f$ - that computes a total function extending $f$.)
Of course, we could artificially limit the domain of $f$ to $K$, so the restriction is a total function. But, because $K$ is not computable, this means we have no way to tell which numbers are in the domain, which leads us back to the same problems. It turns out to be easier to think of the domain as always $\mathbb{N}$, and handle the fact that a function may be partial with the $\simeq$ notation.