3
$\begingroup$

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?

$\endgroup$
6
$\begingroup$

The usual set-up of first-order logic does not allow partial functions as such - all function symbols have to be interpreted as total (= always-defined) functions. To get around this, we just "relationalize" partial functions exactly as you suggest, treating them as subsets of an appropriate Cartesian product. In fact, relationalization even of total functions can be quite useful throughout model theory.

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.