I just encountered the concept of "undefined" values for any type from this blog article that " every Isabelle function is total". In addition
… This design has an important consequence: It allows the existence
of a polymorphic expression that inhabits any type, namelyundefined :: 'a
The naming of this term alone has caused a great deal of confusion for Isabelle beginners, or in communication with users of different systems, so I implore you to not read too much into the name.In fact, you will have a better time if you think of it as arbitrary or, even better, unknown.
we can observe an important fact: undefined is not an extra value
besides the “usual ones”. It is simply some value of that type …
So for example, if you define a function (e.g. division of natural numbers) without a specified value at certain input values (e.g. 0):
fun division :: "nat ⇒ nat ⇒ nat" where
"division n (Suc m) = n div (Suc m)"
then in Isabelle/HOL, at this input (0), the value of the function does exist, but is undefined/arbitrary/unknown.
⋀a. division a 0 = undefined
If I understand it right, in ordinary math, division at zero does not have a value. But in Isabelle/HOL logic, the notion is replaced by one that the value is undefined/unknown.
My question is:
Is there any rigorous formalization of the undefined/unknown value in mathematics elsewhere, and are there axioms to govern how "undefined" values behave?
For example, from this Math.SE question, we have $0 \cdot \infty = 0$ etc. Are there similar formal rules about the "undefined" value in Isabelle/HOL?
In Isabelle/HOL, there is:
lemma "undefined = undefined" by auto
By comparison, I am not so sure that $\infty = \infty$.
Best Answer
Disclaimer: there are several proof assistants for HOL and Isabelle/HOL is the one that I am least familiar with. The different proof assistants all take slightly different lines on the design of their mathematical libraries, but have the same basic mechanisms for defining the objects in those libraries. The principle here is common to all of them.
As discussed in the blog article that you reference, a feature of HOL is that the mechanism for introducing a new constant is not restricted to simple equational definitions, but allows you to give implicit and possibly loose specifications of the constant. So, for example, you could introduce $\pi$ with the defining property:
$$ 0 < \pi \land \forall x\cdot \sin x = 0 \Leftrightarrow \exists m:\Bbb{Z}\cdot x = m \times \pi$$
(There is a small price to pay: a proof obligation is imposed that ensures that the the defining property is consistent.)
The above is an implicit specification, but can be shown not to be loose: i.e., you can prove that there is exactly one real number $\pi$ that satisfies the above property. As a conceivable example of a loose specification, after defining the complex numbers as pairs of reals with the usual definition of the arithmetic operators, you could define $\mathbf{i}$ by:
$$ \mathbf{i}^2 = -1 $$
(The above example is not very likely in practice as it is more convenient to be less abstract and to require $\mathbf{i} = (0, 1)$. The blog article contains other relevant examples, e.g., see its discussion of $\mathtt{fromSome}$.)
$\mathtt{undefined}$ in Isabelle/HOL is an extreme example of loose specification: its defining property is just $\mathbf{true}$. It has a polymorphic type such that it can be instantiated to any type. Its instance in any type has all the properties that are common to all elements of the type. So you have properties like::
$$ (\mathtt{undefined} : \tau) = (\mathtt{undefined} : \tau) \\ \lnot (\mathtt{undefined} : \Bbb{N}) < 0 \\ (\mathtt{undefined} : \Bbb{R}) < 0.0 \lor (\mathtt{undefined} : \Bbb{R}) = 0.0 \lor (\mathtt{undefined} : \Bbb{R}) > 0.0 $$
where $\tau$ can be any type. $\mathtt{undefined}$ has no other special properties: In particular, $f(x) = \mathtt{undefined}$ does not imply that $x$ is not in the domain of $f$. The definition of $\mathtt{division}$ is just saying that $\mathtt{division} \, a \, 0$ is equal to $\mathtt{undefined}$, some unspecified, but perfectly ordinary natural number. As the blog article suggests, it would perhaps have been more appropriate to call it $\mathtt{unspecified}$, rather than $\mathtt{undefined}$.
There are logics that do explicitly model undefined terms. Tennant's natural logic is one example. See also this article on free logics. HOL is not one of these logics.
As regards the conventions for the use of $\infty$ in ordinary mathematics, good texts will make it quite clear what conventions are being used. I don't think equations like $\infty = \infty$ involving $\infty$ are considered as problematic. E.g., Rudin's Principles of Mathematical Analysis states a convention that $x + \infty = \infty$ when $x$ is finite.