Notation for Partial Functions

Question

Suppose we have sets $f$, $A$ and $B$ such that

$f\subset A\times B$ and $\forall x\in A\space \forall y,z\in B: [(x,y)\in f \land (x,z)\in f \implies y=z]$

i.e. $f$ is a partial function mapping $A$ to $B$.

Question: Can we then justify defining $\forall x\in A:\forall y \in B:[ f(x)=y\iff (x,y)\in f]$ allowing us to make all the substitutions entailed by equality?

Edit 1:

Or, alternatively, without equality...

$\forall x\in A: [f(x)\in B \iff \exists y:[y\in B \land (x,y)\in f]]$?

Edit 2:

The latter definition can be derived from the former. Not sure the other way, so they may not be equivalent.

---

Follow-up (One year later)

I have found that the following construct works well for a partial function $f$ of one variable mapping part of set $A$ to set $B$ where the subset $D\subset X$ is the domain of definition:

$\forall x:[x\in D \implies f(x)\in B]$

For a partial function $f$ of two variables mapping part of set $A\times B$ to set $C$ where the subset $D\subset A\times B$ is the domain of definition:

$\forall x,y: [(x,y)\in D\implies f(x,y)\in C]$

Example

Suppose, for some reason, you want to define exponentiation on $\mathbb{N}$, leaving $0^0$ undefined.

Let $D=\mathbb{N}^2 - (0,0)$. Then we can define exponentiation as follows

1. $\forall x,y:[(x,y)\in D \implies x^y \in \mathbb{N}]$

2. $\forall x,y:[(x,y) \in D\implies x^0=1]$

3. $0^1=0$

4. $\forall x,y:[(x,y)\in D\implies x^{y+1}=x^y\cdot x]$

Or equivalently...

1. $\forall x,y:[x\in \mathbb{N} \land y\in \mathbb{N} \land \neg [x=0 \land y=0] \implies x^y\in \mathbb{N}]$

2. $\forall x:[x\in \mathbb{N} \land x\ne 0] \implies x^0=1]$

3. $0^1=0$

4. $\forall x,y:[x\in \mathbb{N} \land y\in \mathbb{N} \land \neg [x=0 \land y=0] \implies x^{y+1}=x^y\cdot x]$

Answer 1

The mentioned property of $f$ being a partial function enables us to write $f(x)$ for the unique value $y$ such that $(x,y)\in f$, whenever it exists.

An alternative way to define partial function from $A$ to $B$ is to define it as a function $D\to B$ with some $D\subseteq A$ (called the domain of $f$), and then $f(x)$ exists [and is unique] iff $x\in D$.

Answer 2

Partial functions are a special case of relations. There is a notion of composition of relations, given in the case of binary relations by

$$ a RS b \Longleftrightarrow \exists c : a R c \wedge c S b $$

(or maybe $SR$ rather than $RS$ depending on your ordering convention)

There is also a corresponding notion of a partial element of a set, which can be identified with a partial function from the one point set to your set.

In particular, there is exactly one partial element of any set that is not an ordinary total element. It is not terribly unreasonable to call this the "undefined" element.

Along these lines, if $x$ is not in the domain of $f$, one would have $f(x)$ being the undefined element.

You can even go so far as to insist that the truth of an equation like $x = y$ has a partial truth value rather than a (total) truth value.

I've never seen anyone attempt to specify a formal syntax and semantics based on partial functions like this, and I've not tried too hard to work it out myself, so I can't really offer "a lot can be reasonably done, but I don't know exactly the right way to set up the details".

Looking at the internal logic of the category of sets and partial functions is probably a good approach to get something that is at least reasonable.

Answer 3

When you write $f(x)∈B$, you involve more definitions than you have here. The rest of the statements depends on those definitions, and so the answer to your question, I think, can be given only after we clarify what you mean.