Consider the famous Collatz sequence
$$ x_{n+1} = c(x_n) = \left\{ \matrix{x_n/2 & {\rm if \; x_n \; even} \hfil \cr 3x_n+1 & {\rm if \; x_n \; odd} \hfil \cr } \right. $$
and define $f: ℕ-\{0\}→\{0, 1\}$
$$ f(x) = \left\{ \matrix{ 0 & {\rm if} \; \exists n : c^n(x) = 1 \hfil\cr 1 & {\rm otherwise}\hfil\cr }\right. $$
Is that a valid definition for a function? Is it a constant function? What if we replace Collatz conjecture with a true proposition that however cannot be proved with current set of axioms (Gödel incompleteness)? What if it's replaced by something that can only be decided with a new axiom?
For any given $x\in ℕ$, I would say that $f(x)$ is a well defined number, but if that's true does it mean that for example well defined functions from naturals to $\{0, 1\}$ are either:
- non-constant functions
- provably constant functions
- functions that are constant but that cannot be proved constant
- functions for which cannot be decided if they're constant or not
(this to me sounds pretty crazy)
Yes, it is a valid definition of a function, and it is constant if and only if the Collatz conjecture is true. Yes, we can do this with things that are provably undecidable in some sense. For instance I can even say "let $x$ be the identity function on $\mathbb R^2$ if the continuum hypothesis is true and $x$ is the set of even numbers if it's false", and that's a perfectly well-defined object since I've covered all my bases. It's no issue that we cannot actually decide in ZFC what kind of object $x$ is... it's just like not being able to decide anything else.
When you define something, you just need to show that you have specified some unique object, you don't need to "compute" which object it is. That which object you end up with may be contingent on things you don't know, or even know you can't determine due to weakness of your assumptions, is not a problem. Think of well-definedness as a promise that we will never find ourselves in a situation where we don't have a value for $x$ or that we have more than one value... nothing more.