How to Handle Undefined $F(x)$ in Logical Statements?

Question

Suppose we have a function $F$, meaning that for any $x\in\mathrm{dom}(F)$, there exists a unique $y$ such that $\langle{x,y}\rangle\in F$, and this $y$ is denoted as $F(x)$. Then, perhaps we can construct statement $$ \forall x\in\mathrm{dom}(F)\,\varphi(F(x))\tag{1} $$ Here, $\varphi(F(x))$ is a logical statement about $F(x)$. Everything seems fine at the moment, but when I rewrite (1) as $$ \forall x\,\forall y\,(\lnot\langle x,y\rangle \in F)\lor \varphi(F(x))\tag{1'} $$ it becomes quite strange. Because the $x$ in front of this statement is bound by a universal quantifier, but we have not defined $F(x)$ for all $x$—not all $x$ are within $\mathrm{dom}(F)$—how should I understand this statement? In the above paragraph, the definition of $\mathrm{dom}(F)$ is $$ x\in\mathrm{dom}(F)\Leftrightarrow \exists y\,\langle x,y\rangle \in F $$

Answer 1

I take $\varphi \left( F \left( x \right) \right)$ into $$ \left( \exists y \right) \left( \left\{ y \right\} = \left\{ \mathrm{snd} \left( t \right) | t \in F , \mathrm{fst} \left( t \right) = x \right\} \land \varphi \left( y \right) \right), $$ where $ \mathrm{fst} \left( \left\langle x , y \right\rangle \right) = x $, $ \mathrm{snd} \left( \left\langle x , y \right\rangle \right) = y $ and $\varphi$ is an atomic formula.

If $F \left( x \right)$ is undefined then $\left\{ \mathrm{snd} \left( t \right) | t \in F , \mathrm{fst} \left( t \right) = x \right\} = \emptyset$ so the atomic formula $\varphi \left( F \left( x \right) \right)$ is false.

---

Update: Add Motivation

In Coq, for a given set $B$, $\mathtt{option} \, B$ is also a set such that:

1. If $y \in B$ then $\mathtt{Some} \, y \in \mathtt{option} \, B$.
2. $\mathtt{None} \in \mathtt{option} \, B$.
3. For any $y \in B$, $\mathtt{Some} \, y \ne \mathtt{None}$.
4. For any $y_1 , y_2 \in B$, $\mathtt{Some} \, y_1 = \mathtt{Some} \, y_2$ implies $y_1 = y_2$.

The $\mathtt{option} \, B$ can be encoded in set theory by setting:

1. $\mathtt{Some} \, y := \left\{ y \right\} $ for $y \in B$.
2. $\mathtt{None} := \emptyset$.

One can consider $\emptyset$ as the default value.

We define another function $f : A \to \mathtt{option} \, B$ by $$ f \left( x \right) := \begin{cases} \mathtt{Some} \, F \left( x \right) & F \left( x \right) \, \mathrm{is} \, \mathrm{defined} \\ \mathtt{None} & F \left( x \right) \, \mathrm{is} \, \mathrm{undefined} \end{cases} $$ and change $y = F \left( x \right)$ into $\mathtt{Some} \, y = f \left( x \right)$.

Answer 2

It's important to realize that the way you handle these situations is ultimately a matter of definition. As far as I know, there isn't a universally accepted convention for how to interpret statements about undefined function evaluations, with the notable exception of "don't write statements using undefined function evaluations". Presuming that this convention is dissatisfying, I'll offer two alternatives which I personally use in my studies. I personally think these are both pretty intuitive, and nicely reduce the amount of conceptual overhead. I'll also consider a third alternative, which seems natural at first, but actually just make the ambiguities worse.

First approach: Use a default

Just say that $F(x)=0$ whenever it holds that $x\notin \operatorname{dom}(F)$. You don't necessarily need to use $0$ as your default, you could use $\{\}$ instead, or something else if you want. Regardless of which default value you use, having a default comes with many advantages. The most obvious advantage is that the interpretation of logical statements is straightforward, and otherwise-valid rewritings of logical statements will still be valid. This does come with the disadvantage of introducing some trash theorems, however, such as the absurd statement $\sqrt{\mathbb{R}}=0$ becoming true by definition. Regardless, this is still my preferred approach.

Second approach: Use 3-valued logic

Specifically, use Kleene's 3-valued logic. Three-valued logic introduces a third truth value, which I'll label $U$ for "unknown". In classical logic, the connectives $\lor$ and $\land$ behave as join and meet respectively, using the ordering $\bot < \top$. In Kleene's logic, this behavior is respected, and we simply extend the logical order so that we have $\bot<U<\top$. Kleene's logic also maintains that negation is an involution.

Whenever you have a function with undefined value, just say that $f(x)$ evaluates to $U$. We can extend all functions and relation symbols, so that when applied to $U$ they evaluate again to $U$. For the logical connectives however, there are many cases in which $U$ does not obliterate all meaning. For example, if you managed to prove that $\forall(x\in\operatorname{dom}(F)), \varphi(F(x))$, then it is still true that $\forall x, (\neg x\in \operatorname{dom}(F))\lor \varphi(F(x))$. This works because whenever $x\notin\operatorname{dom}(F)$ then the left operand is true, and otherwise the right operand is true, and Kleene's logic guarantees that $U\lor \top$ is logically true. The obvious disadvantage is that this breaks classical logic, so you'd need to familiarize yourself with how 3VL works. That said, among all versions of 3VL, Kleene's logic seems to respect classical intuition the most.

This approach is also robust in the face of extending definitions. In particular, any theorem which is proven to be true under this approach will still be proven true when using the Default approach. The only difference between this approach and the previous is that statements which ought to be nonsense are correctly marked as nonsense. In that way, the departure from classical logic is tightly controlled, and arguably desirable.

Third approach: undefined statements are false.

Ordinarily, we would say that an expression such as $\varphi(F(x))$ is really just shorthand for $\exists y, \left<x,y\right>\in F \land \varphi(y)$. This seems to be an obvious way to implement new function symbols using functional relations, but it's actually incoherent unless we make further clarifications. Essentially what this approach is saying is that, in the event where $x\notin\operatorname{dom}(F)$, then necessarily $\neg\varphi(F(x))$. Indeed, in such a case, there would not exist any such $y$ obeying $\left<x,y\right>\in F$. The incoherency of this definition occurs when we allow $\varphi$ to be a compound formula. For example, what about the formula $\neg\varphi(F(x))$? If this were to be interpreted as $\exists y, (\left<x,y\right>\in F)\land \neg\varphi(y)$, then that's false, but we already established that $\varphi(F(x))$ was false, i.e. $\neg\varphi(F(x))$ is true.

The above naive implementation can be recovered by restricting the definition scheme to atomic formulae. Unfortunately, this introduces the new problem of making the truth of defined relations ambiguous. For example, in Peano Arithmetic it's conventional to define the $<$ relation such that $n\leq k \iff \exists j, n+j=k$. Under this definition, we would say that $n\leq F(x)$ is false whenever $x\notin\operatorname{dom}(F)$, namely since $n+j=F(x)$ is false for all $j$. However, there is also an equivalent definition $n\leq k \iff \neg(k<n) \iff \forall j, \neg(k+j+1=n)$, and under that definition we would instead prove $n\leq F(x)$ true, precisely because $F(x)+j+1=n$ is always false.

This third approach seems untenable, since it demands that you keep careful track of how certain formulae are intensionally defined. In particular, even if we have proven $\phi(y)\iff \varphi(y)$ for all $y$, it may still be the case that $\phi(F(x)) \land \neg \varphi(F(x))$, which seems like an absurd oversight.

Answer 3

You are using the symbol $F$ in two different ways. On the one hand, when you write something like $\langle x, y \rangle \in F$, you are treating $F$ as if it were a constant symbol, denoting a particular set of ordered pairs. On the other hand, when you write something like $\varphi(F(x))$, you are treating $F$ as if it were an operation symbol.

Your question, then, is directly tied to the following issue. How do we take a given constant symbol and turn it into an operation symbol? Or more precisely, we are given a constant symbol denoting a particular set of ordered pairs, and we have an intuitive sense of what it would mean for an operation symbol to be equivalent to it. How do we define a new operation symbol that matches this intuition?

In general, new extralogical symbols are defined through what is called a definitorial extension. You can read about these in many places. One possibility is Section 2.6 of A Concise Introduction to Mathematical Logic by Wolfgang Rautenberg. But there is a problem. Any operation symbol—defined or not—must be compatible with all possible inputs. In other words, if $F$ is an operation symbol, then $F(t)$ is a term for all terms $t$. So if $F$ is meant to have a restricted domain, then $F$ cannot be an operation symbol, which means $\varphi(F(x))$ is not even a formula.

But if $\varphi(F(x))$ is not a formula, then what is it? Surely, it is meaningful and it is very common to see it in use. The answer is that it is shorthand. It is a concise way to refer to a more complicated formula. Not only is it concise, it is also well-suited to human readers that rely on intuition (as opposed to machines that have no problem with complicated strings of symbols). However, since it is shorthand, it is not formally defined. There is no rigorous set of rules that tell you which formula it refers to. There are conventions, but they have limited applicability. The author who uses such shorthand is responsible for removing any ambiguity that might occur.

For example, most readers would probably understand $\varphi(F(x))$ to be shorthand for $$ \exists y \, (\langle x, y \rangle \in F \wedge \varphi(y)) $$ But then how do we understand $\neg\varphi(F(x))$? Is it $$ \neg \exists y \, (\langle x, y \rangle \in F \wedge \varphi(y)) $$ Or is it $$ \exists y \, (\langle x, y \rangle \in F \wedge \neg \varphi(y)) $$ If you are using shorthand expressions like $\varphi(F(x))$ or $\neg\varphi(F(x))$, then both you and your readers must know exactly which of the above, rigorously-defined formulas you mean to be using. (By the way, the above example is exactly the issue in Bertrand Russell's example, "The King of France is bald.")

To connect all of this to your example, (1) ought to be translated as $$ \forall x \, (x \in {\rm dom}(F) \to \varphi(F(x))) $$ Substituting the definition of ${\rm dom}(F)$, we get $$ \forall x \, (\exists y \, \langle x, y \rangle \in F \to \varphi(F(x))) $$ At this point, the expression is still shorthand. Presumably, you mean for it to denote the formula $$ \forall x \, (\exists y \, \langle x, y \rangle \in F \to \exists y \, (\langle x, y \rangle \in F \wedge \varphi(y))) $$ You can now rewrite it, as you did in (1$'$), to get $$ \forall x \, (\forall y \, \neg \langle x, y \rangle \in F \vee \exists y \, (\langle x, y \rangle \in F \wedge \varphi(y))) $$ The final result is a formula (not shorthand), and it does not suffer from the counterintuitive issue you faced in your question.

Answer 4

This question is indeed a variation of the questions on restricted quantification (a.k.a. bounded quantification; see also a previous answer of mine).

We use two ways to specify the domain of quantification: Either we enunciate as the universe (domain) of discourse as an initial statement, or inscribe its definition into the formulas in consideration. The latter one is used also when we restrict the domain of quantification.

Since the mentioned formula is an instance of universal quantification, we shall apply the form

$$(\forall x)_{R(x)}\psi(x)\leftrightarrow\forall x(R(x)\rightarrow\psi(x))$$

We obtain

$$\forall x\forall y\Big(\exists y(\langle x,y\rangle\in F)\rightarrow\big(\lnot\langle x,y\rangle \in F)\lor \varphi(F(x)\big)\Big)$$

Let us schematically verbalise what this formula says:

For all $x$ and $y$, if there is at least one nice pair $(x, y)$, then there is no nice pair $(x, y)$ or $Q(x)$.

In case that there is no nice pair $(x, y)$, the implication vacuously holds. Otherwise, it depends on the value Q(x) is assigned to. Hence, the formula is satisfiable, but invalid.

Answer 5

Maybe try a different approach to mathematical functions as follows:

We can say that $f$ is a function mapping set $X$ to the set $Y$ if we have:

$\forall x: \forall y: [x\in X ~\land ~y\in Y \implies [y~=f(x) \iff P(x,~y)]] $

where $P$ is a binary predicate such that:

$\forall x: [x\in X \implies \exists y:[y\in Y ~\land [P(x,y) \land \forall z:[ z\in Y\implies [P(x,z) \implies z=y]]]]]$

--Based on Terance Tao, "Analysis I," p.49

Note that we cannot use this definition of $f$ to determine the truth value of $~y~=f(x)~$ if $~x\notin X$. We can only do so if $x\in X$ and $y\in Y.$ Therefore, to handle undefined $f(x)$ in logical statements, we need only add that $x\notin X$.