# With respect to functions, how do I express definedness in first order logic?

My understanding is that a function $$F \colon X \to Y$$ is considered a partial function if $$F \colon X' \to Y$$ where $$X' \subset X$$. For example, the predecessor function for natural numbers with signature $$p \colon \mathbb{N} \to \mathbb{N}$$ could be defined as $$\forall x \exists! y \colon p(x) = y$$. Then $$p$$ is not defined for $$p(0)$$. I believe $$p(0)$$ is well formed with respect to its signature, but is undefined with respect to its definition.

My attempt to represent definedness for $$p$$ in FOL is to express the function as a binary relation, $$p\colon \mathbb{N} \times \mathbb{N}$$. where $$\forall x \colon \mathbb{N} , \exists! y \colon \mathbb{N} \colon p(x, y)$$ holds. Is this correct?

Alternatively, we can whip up an analogue of first-order logic which does permit partial functions, and prove a "metatheorem" letting us translate between the two. This basically hides the relationalization process under the hood, and is in my opinion more natural. However, it also requires more work, since we have to check that the version of $$\mathsf{FOL}$$ we produce does actually behave as desired.