Vrftjkry

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 $tsimeq 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?

Yes, the context is about Partial functions :

In mathematics, a partial function from $X$ to $Y$ is a function $f: X′ → Y$, for some proper subset $X′$ of $X$.

For example, we can consider the square root function restricted to the integers :

$g colon mathbb {Z} to mathbb {Z}$ where $g(n) = sqrt {n}$.

Thus $g(n)$ is only defined for $n$ that are perfect squares. So, $g(25) = 5$, but $g(26)$ is undefined.

See Def.1.2.15 :

An n-ary predicate $P$ is recursively enumerable iff the partial function:

$$F(a_1, ldots, a_n) = begin{cases} 0, text{ if } P(a_1, ldots, a_n) \ text{ undefined otherwise} end{cases}$$

is partial recursive.

In this case we have defined a partial function $F$ : when $P(a_1, ldots, a_n)$ does not hold the valued of $F(a_1, ldots, a_n)$ is undefined.

In Def.1.2.13 the functions of rule (R1) are total. This fact is reflected in Th.1.2.19, where they are expressed by way of formulas with $=$.

We have partial functions in (R3) :

$F(a_1, ldots, a_n)$ is the smallest $x$ such that $G (a_1, ldots, a_n, 0), ldots, G (a_1, ldots, a_n, x)$ are defined and $G(a_1, ldots, a_n, x) simeq 0$, if there is such an $x$, and is undefined otherwise.

In the expression $G(a_1, ldots, a_n, x) simeq 0$ we have that $G(a_1, ldots, a_n, x)$ is defined because $0$ obviously is.

But I agree with you that in the treatment of case (R3) in Th.1.2.19 there is some sloppiness.

In $G(x_1, ldots, x_n, x_{n+1}) simeq y$, we have that $y$ is a variable: thus, it makes no sense to say that it is "undefined".

IMO, we have to read it as follows : if $G(x_1, ldots, x_n, x_{n+1})$ is undefined, then skip the input $(x_1, ldots, x_n, x_{n+1})$.

If $G(x_1, ldots, x_n, x_{n+1})$ is defined, then we can test each $n$ to verify if $G(x_1, ldots, x_n, x_{n+1})=n$.