How does one generally use partial function in logical statements?

Question

How does one generally use partial function in logical statements? How it's done in practice?

Specifically, let $M$ by a Turing machine, $f_M:\{0,1\}^*\to\{0,1\}$ the characteristic function which corresponds to $M$, $U$ a universal Turing machine and $f_U$ the corresponding function which for given input takes values in $\{0,1\}$. Let the variables $x,\alpha$ be bit strings

Can I write $\forall x.\ \exists\alpha.\ f_U(\alpha,x)=f_M(x)$?

The problem is that for $x$ where the Turing machine loops, $f_M(x)$ doesn't even take a value and the sentence "$f_U(\alpha,x)=f_M(x)$" amounts to "$\%!?=!?\$?$".

And I don't even know how to prevent things from going wrong, because if I cautiously write

$\forall x.\ (f_M(x)\in\{0,1\}\implies \exists\alpha.\ f_U(\alpha,x)=f_M(x))$

puts the problem just on $f_M(x)\in\{0,1\}$, which can similarly just not make any sense as $f(x)$ might not have a value.

---

Edit: My initial motivation for the question comes from 'Computational Complexity: A Modern Approach - Sanjeev Arora and Boaz Barak'

http://www.math.sc.edu/~cooper/math778C/abct.pdf

In particular

How would one formally write the statement "forall $x$ ... such that $U(x,\alpha)=M_\alpha(x)$"? In the book, $M$ is previously define as a tupple $\langle \Gamma,\Sigma, Q,\delta,\dots$, so $M(x)$ here is just "suggestive notation" for the output of $M$ running on $x$. That's also why I went over to the characteristic (partial?) functions to formulate the question.

And I don't necessarily need to use the characteristic function - I've tried (and I think succeeded) in recursively defining a partial function (which I call $\mathrm{run}_M$) out of the transition function $\delta$ of a Turing machine $M$. But it's still a partial function and I can't just write $\forall x.\ \mathrm{run}_M(x)=$ because I'd first have to introduce a bounded quantifier to function notation $\mathrm{run}_M(x)$ to make sense.

Answer 1

First of all, you probably reversed your quantifiers, you probably mean: $\exists\alpha, \forall x, f_U(\alpha,x)=f_M(x)$.

About the "undefined" issue, it is not really a big deal to write an equality in case both are undefined. We can consider that "undefined" is a special value often written $\bot$, and a partial function is in fact a total function with values in $\{0,1,\bot\}$. It is just important to keep in mind that you cannot define a computable function $g$ by using "if $f(x)=\bot$ then return $1$", because if the machine $f$ you simulate does not terminate, then $g$ also does not terminate. That is why some people prefer to write "$f$ loops on $x$ " instead of $f(x)=\bot$, to keep in mind this restriction.

Answer 2

(1) On the question of how "in practice" to handle equations involving partial functions, here's a quote from Cutland's classic text Computability (CUP), at p.3, explaining a common device:

Often in computability we shall encounter functions, or expressions involving functions, that are not always defined. In such situations the following notation is very useful. Suppose that $\alpha(\mathbf{x})$ and $\beta(\mathbf{x})$ are expressions involving the variables $\mathbf{x} = (x_1 ... x_n)$. Then we write $$\alpha(\mathbf{x}) \simeq \beta(\mathbf{x}) $$

to mean that for any $\mathbf{x}$, the expressions $\alpha(\mathbf{x})$ and $\beta(\mathbf{x})$ are either both defined, or both undefined, and if defined they are equal.

(2) Suppose you want now more formally to logically regiment arguing with function expressions which may take no value, so e.g. $\alpha(\mathbf{x})$ is undefined. [NB Importantly, this doesn't mean that in such a case $\alpha(\mathbf{x})$ is nonsense like ?&%!. We may perfectly well understand the sense of the functional expression, understand what it is instructing us to do, and it is exactly because we understand it that we can work out that it fails to output a value]. Classical logic -- where, by stipulation, all terms denote -- obviously won't do. So we need a so-called free logic (i.e. a logic free from existence assumptions). See http://plato.stanford.edu/entries/logic-free/‎ for a helpful introduction and review of some of the options here.

Answer 3

Another way, following Peter Smith's remark, is to avoid terms (in this case : function symbols) and use instead a predicate (in computability theory we have it: Kleene's $T$ predicate).

We have a similar example in (formal) arithmetic. We define :

$a|b$ iff $\exists c \ (ac=b)$

so we may call $c$ the "quotient" of $b$ and $a$.

We may not (in classical logic) add to the language a function $\text {quot}(x,y)$ such that $\text{quot}(a,b)=c$ exactly because in $\mathbb{N}$ the operation of division is not always defined, i.e.

$\text{quot}(0,1)$ is undefined.

We may solve the problem with a predicate $\text{Quot}(a,b,c)$ that holds exactly when $c=a|b$.

In this case :

for all $n \in \mathbb{N}$, $\text{Quot}(0,1,n)$ does not hold.